HTab-1.5.4: examples/sat/trclos1.frm
signature {
propositions { P1, P2, P3, P4 }
nominals { N1, N2 }
relations { R1 , RX : {trclosureof R1} }
}
theory {
!P4 v [R1](!P2 v ))));
!N1 v [RX](!P4 v ))));
P2 v N2:(!P1 v [R1](N1 v [RX](!N1 v !N1:(N2 v ))));
N1 v [R1](P3 v !N2:(!P4 v N2:(N1 v ))));
!N1 v [RX](!P3 v !N2:(N1 v !N1:(!N2 v ))));
!N1 v ))))
}