from_lrat's input CNF and its output theorem

Stream: mathlib4

[Juneyoung Lee]

Hi all, I have a quick question about from_lrat.
What is the relation between its input CNF and its constructed theorem?
I wonder whether they must be syntactically equivalent, or they are equivalent modulo some permutations or a limited set of rewriting rules.

[Mario Carneiro]

@Juneyoung Lee The theorem statement is generated from the input CNF, so there is no permutation or rewriting going on

[Mario Carneiro]

the CNF is straightforwardly translated into conjunctions and disjunctions