signature {

propositions { P1, P2, P3, P4 }
nominals { N1, N2 }
relations { R1 , RX : {trclosureof R1} }

}

theory {

!P4 v [R1](!P2 v ![R1](N2 v [RX](P2 v !N1:(!N2 v ![R1](!N2 v N1)))));
!N1 v [RX](!P4 v ![RX](!N2 v [RX](P4 v [RX](!P4 v !N1:(!P4 v P3)))));
P2 v N2:(!P1 v [R1](N1 v [RX](!N1 v !N1:(N2 v ![RX](!N1 v P1)))));
N1 v [R1](P3 v !N2:(!P4 v N2:(N1 v ![R1](N1 v [RX](N1 v !N2)))));
!N1 v [RX](!P3 v !N2:(N1 v !N1:(!N2 v ![R1](!P3 v [RX](N2 v !N1)))));
!N1 v ![R1](!P4 v ![RX](!N2 v N1:(N2 v [RX](P3 v [R1](!N1 v P2)))))

}