Tseitin Rule in Proof Log

[HarryBryant99]

Hi,

I was trying to understand the Tseitin Rule in the Proof Logs. It was my understanding that the Tseitin Rule would be used in order to create CNF formula when a Unit Clause is present. E.g. for Or(a,b):

For the formula Or(a,b) it creates the following clauses:
[Not(Or(a,b)), a, b]
[Not(a), Or(a,b)]
[Not(b), Or(a,b)]

This process makes sense to me, following the standard rules of the transformation but replacing the new variable X with Or(a,b).

However, I ran some further examples and they did not follow the convention?

tseitin(IL946_dot__op_EN_cp_SEL_0,
IL946_dot__op_EN_cp_JS_0,
Not(Or(IL946_dot__op_EN_cp_SEL_0,
IL946_dot__op_EN_cp_JS_0))) [] [Not(Or(IL946_dot__op_EN_cp_SEL_0, IL946_dot__op_EN_cp_JS_0))]

tseitin(Not(And(Not(IL946_dot_ENABLED_0),
Or(IL946_dot__op_EN_cp_SEL_0,
IL946_dot__op_EN_cp_JS_0))),
Or(IL946_dot__op_EN_cp_SEL_0,
IL946_dot__op_EN_cp_JS_0)) [] [Not(And(Not(IL946_dot_ENABLED_0),
Or(IL946_dot__op_EN_cp_SEL_0,
IL946_dot__op_EN_cp_JS_0)))]

Any advice on what the rule is doing would be greatly appreciated. It was my understand that the rule wanted to make a CNF so that RUP can derive further inferences that can be checked with unit-clause propagation.

Many thanks
Harry Bryant