HTab-1.6.1: examples/sat/test43.frm

begin
-N2 v -N1 v [R1](N2 v -P2 v -N5:(-N4 v N3:(N4 v [R1](-N2 v -N1 v P1)) v [R1](-N3 v P2 v -P3)));
P5 v -N4 v -[R1](-N3 v N5:(-N2 v -N4 v -N2:(-P5 v -N4 v -[R1](N5 v -N3 v N4))) v -[R1](N1 v -N2:(-N3 v N1 v -N5)));
N3 v -N5 v [R1](P5 v -N4:(P3 v [R1](N4 v -N1:(P3 v P4 v -N3)) v -N5:(-N4 v -N1 v -P4)) v N5:(-N1 v [R1](P2 v -P5 v -P3)));
N1 v -P4 v -[R1](-N2 v N1 v -[R1](N3 v N1 v N4:(-P4 v N2:(-P5 v -N1 v N3))));
P5 v -P3 v N4:(N3 v -P4 v N1:(-P1 v [R1](P5 v [R1](-P4 v -N1 v N5)) v -[R1](-N5 v N1 v P3)));
P1 v [R1](P3 v -N4 v -[R1](-P5 v -N5 v -N5:(-N1 v -P4 v -N4:(N5 v -N2 v N3)))) v -[R1](N1 v N1:(-P1 v N4 v -N2:(N5 v N4 v P4)) v -N2:(N5 v -P3 v -P2));
P1 v N4 v N2:(P3 v N1:(-P4 v [R1](N1 v -N5 v -[R1](-N5 v -P3 v P2)) v -[R1](-P3 v -P5 v -P2)) v [R1](N2 v [R1](-N1 v N4 v N3)));
-P1 v -P4 v [R1](N5 v -N2:(-N5 v -P4 v -[R1](N2 v N1 v N4:(P1 v -N1 v P5))) v [R1](-P1 v -P5 v N1:(N5 v N4 v N3)));
-P1 v [R1](-P2 v -P5 v -N1:(N4 v N4:(P3 v -[R1](N1 v N5 v -N2)) v -[R1](-N1 v -N2 v -N5))) v -[R1](-N2 v -N3:(P1 v -N1:(-P2 v -P3 v P1)) v N2:(N1 v -P2 v -P1));
-P4 v -[R1](N1 v P2 v -N5:(P4 v -N1 v -[R1](N3 v P4 v -N5:(-N4 v -P3 v -N1)))) v -N2:(-N5 v N3 v [R1](-N4 v -P5 v -N2:(P4 v P5 v N1)));
-N4 v -N5:(P2 v [R1](-P4 v -[R1](N3 v -P1 v -N1:(P4 v N4 v -P3)) v -N3:(N2 v -N4 v N1)) v -N1:(-N2 v -N4 v [R1](-P2 v P3 v P4))) v -N5:(-N3 v -P5 v [R1](-N3 v -N1 v -[R1](-N2 v N5 v -P1)));
-P5 v -N5 v -N1:(-N5 v [R1](N5 v [R1](-N1 v P4 v -N5:(-N4 v N1 v -N2)) v N3:(-P2 v -N2 v N1)) v N2:(-N3 v -P4 v [R1](-N5 v -N3 v N4)));
-N2 v -P4 v [R1](N5 v -P1 v -[R1](-P2 v -N4:(-N5 v -N3:(-P2 v N1 v N2)) v -N1:(P5 v -P4 v N4)));
P1 v -P2 v N2:(P2 v P3 v N3:(P2 v [R1](N4 v -N1 v -[R1](-N5 v P5 v -P3)) v -[R1](-N5 v N4 v P5)));
N2 v N4 v N4:(-N5 v [R1](N1 v -[R1](-P5 v P1 v -N4:(N1 v N5 v -N2)) v -N4:(-P1 v P5 v P4)) v N4:(-P4 v -P1 v [R1](-P1 v -P2 v N3)));
P1 v [R1](-N3 v -N1:(N3 v -N2 v -N1:(-P3 v -[R1](P3 v P2 v P4))) v [R1](-N5 v -N1 v -N5:(-N1 v P4 v N4))) v -N3:(-P4 v -P1 v -[R1](-N3 v N2:(P1 v -N3 v -N1)));
-N3 v -[R1](N2 v [R1](P4 v N3:(-P1 v N2:(N3 v N5 v N1)) v -N3:(-N1 v P1 v -P3)) v -N1:(P2 v P1 v -N3:(P4 v -N2 v -N5))) v [R1](P4 v -N5:(P3 v N5:(N1 v N2 v N3)) v N1:(N2 v P3 v N3));
-P5 v -N2:(-P3 v N1:(N3 v -[R1](-N4 v [R1](N1 v P1 v P3)) v [R1](-P5 v P4 v P3)) v [R1](N2 v -[R1](N2 v P3 v -N4))) v -[R1](N3 v [R1](-P2 v -N2:(P5 v P1 v -N3)) v -N4:(P1 v P3 v N1));
N5 v N2 v N3:(P5 v -N5:(-P3 v [R1](-N1 v [R1](P1 v P5 v N2)) v [R1](-P2 v N2 v N3)) v -[R1](P2 v -[R1](-N4 v -P5 v -N5)));
N5 v P4 v -[R1](-P5 v [R1](-N3 v N1:(-P4 v -N4:(-P2 v N2 v -N5)) v -N2:(-N5 v -P5 v -N1)) v -N3:(N5 v N5:(-N2 v -P4 v -P3)));
-N3 v [R1](P5 v [R1](-N3 v -P3 v -N5:(-N1 v N3:(N4 v P3 v -N5))) v -N2:(-P2 v N1:(P2 v N5 v N4))) v -N5:(P5 v -N4 v -N1:(-P5 v [R1](-N2 v -N3 v N4)));
-N4 v -N2:(P4 v -[R1](-N4 v -N5 v N2:(-P3 v -[R1](-N5 v -N3 v P1))) v -N5:(-N1 v [R1](-N5 v -P5 v P2))) v -N3:(-P3 v N4 v -[R1](-P1 v -[R1](-N2 v P2 v P1)));
-P4 v P3 v -[R1](N5 v -N5:(-P3 v [R1](N5 v -N1:(-P1 v -P3 v -P4)) v -N5:(P4 v -P3 v P2)) v -[R1](-P2 v -P3 v N4:(-P1 v -P4 v N5)));
-N1 v -P1 v [R1](P4 v -P3 v -N3:(N2 v N5:(N2 v N1 v [R1](-N2 v P3 v -P5)) v [R1](P2 v -P5 v P3)));
P5 v -P3 v -N4:(-P3 v P2 v -N5:(-P2 v -N1 v -[R1](-P2 v -N1 v -[R1](-P3 v N1 v P5))));
-N4 v -N3:(-P1 v -N2 v -N3:(-P5 v -[R1](-P3 v [R1](N1 v P1 v N2)) v -[R1](N1 v N4 v -P3))) v [R1](-N2 v -N2:(-P4 v N3 v -[R1](P3 v -P5 v P4)) v -[R1](-N5 v -N3 v N4));
-N1 v -N2 v -N3:(-P2 v [R1](N2 v -N1 v -[R1](-P4 v -N1:(-P1 v -P4 v -P5))) v [R1](P2 v -P1 v N2:(N5 v -N4 v P2)));
-P3 v -[R1](P3 v N1:(N4 v -N2:(P3 v -[R1](N2 v P2 v -P5)) v [R1](-P4 v -N1 v N4)) v [R1](P1 v N3 v N5:(-P5 v P3 v N2))) v [R1](-P2 v -P1 v N5:(P4 v P1 v -N5:(N3 v P1 v -P3)));
P2 v P5 v [R1](P3 v -N5:(-P5 v -N2:(P5 v -P1 v -[R1](-N3 v N1 v -P3)) v [R1](-P5 v -N4 v N3)) v [R1](-N5 v N4:(P5 v -N1 v -P3)));
-N1 v -[R1](-P4 v N4:(N5 v [R1](P1 v N5:(P1 v N4 v -N2)) v -N5:(-P3 v -P5 v -N3)) v N5:(-P1 v P5 v -[R1](P5 v P2 v P4))) v -N3:(-N5 v -P2 v -N2:(-N5 v [R1](N1 v N3 v P3)));
-N4 v -[R1](P1 v -N4 v [R1](N5 v N3:(P3 v -P1 v N1:(N5 v -P4 v P2)) v -N4:(N1 v P3 v -P1))) v -[R1](-N5 v -N3 v -N1:(P5 v N4 v -N3:(P1 v N2 v -N4)));
N5 v -N1:(N5 v -N2 v -N5:(-N1 v -[R1](-N4 v P4 v -[R1](P4 v N3 v N4)) v [R1](N4 v P2 v N5))) v -[R1](P1 v N2 v N4:(N2 v -N3 v -[R1](P2 v -P3 v P5)));
N3 v P2 v N4:(-N3 v N2:(-P3 v [R1](P1 v -[R1](P4 v -N4 v -N5)) v [R1](P4 v -P3 v -P1)) v [R1](-P1 v -[R1](-P1 v -P3 v N4)));
-P2 v -[R1](P3 v -N2 v N2:(-N4 v N3 v [R1](N5 v -N1:(P5 v -N3 v -N5)))) v -[R1](N2 v -N5:(N2 v N4:(-N5 v P3 v -N3)) v -N3:(-N2 v -P3 v P4));
N1 v N2 v -N2:(N4 v [R1](P2 v N4:(P1 v -N3 v [R1](-N4 v -P3 v -P2)) v -[R1](-P4 v -N3 v -N5)) v -N4:(N1 v -P1 v -[R1](-P3 v N1 v P5)));
-N1 v N3:(-N2 v P3 v -[R1](-N3 v -P5 v -[R1](P2 v N5 v N2:(-P1 v -P5 v -N1)))) v [R1](P4 v N4 v -N3:(N1 v -N5 v -[R1](N4 v -P5 v -P3)));
-P4 v P2 v -N4:(N3 v -N4:(-P1 v -N2 v [R1](-P3 v -[R1](-N1 v P2 v P5))) v -[R1](P4 v [R1](N3 v P3 v P5)));
P1 v [R1](P4 v -[R1](P5 v N1:(P5 v N5:(P5 v P2 v -P3)) v N1:(-P4 v N3 v -N2)) v N5:(-P2 v -N3:(N1 v -N2 v -P1))) v -N1:(N3 v -P1 v -[R1](P2 v P3 v -N2:(P3 v P5 v -N1)));
N1 v -P2 v -[R1](N1 v -N1:(N5 v N4 v N5:(-P3 v N3 v [R1](-N3 v N2 v N4))) v [R1](-P2 v -N5:(N2 v -P4 v P5)));
P4 v P5 v -[R1](-N5 v N1 v N5:(-N2 v [R1](N2 v -N5 v N2:(P1 v N5 v P4)) v -N1:(-P2 v N5 v -P5)));
-P2 v -N5 v -N1:(N5 v -N2:(-P4 v N1 v -[R1](N3 v -[R1](-P5 v -N2 v P1))) v -[R1](-N4 v -N3 v [R1](-N2 v N3 v N4)));
P3 v P2 v -[R1](-P1 v -P5 v [R1](-N2 v -P2 v -N4:(N1 v -N4:(-P2 v P4 v N3))));
P1 v P4 v [R1](-P5 v -N1 v -N2:(N3 v -[R1](N4 v -P2 v -N5:(P3 v -N3 v P2)) v -N3:(-N1 v N2 v -N4)));
P1 v N5:(-P2 v -[R1](P1 v -[R1](-P3 v -P1 v N1:(-P2 v -P4 v P5)) v -N4:(P5 v -P4 v -N1)) v [R1](P2 v P5 v N4:(P3 v N1 v N5))) v -[R1](P5 v N5 v N3:(-N1 v -N2 v -[R1](P2 v -P5 v P1)));
N4 v -[R1](-N5 v N2 v -N1:(-P1 v N3 v N3:(P4 v -P1 v -[R1](-N5 v -P4 v P1)))) v N2:(N4 v -N3 v N1:(N4 v -N3 v -[R1](-N4 v -N2 v -N5)));
N3 v N2 v -N5:(N4 v -[R1](-P2 v -N2 v [R1](N4 v -N5:(-P1 v P3 v N3))) v [R1](-N5 v -N2:(P4 v -P2 v -N3)));
-P5 v -P3 v -N5:(-P3 v -P5 v -[R1](-N2 v -[R1](-N2 v N5 v N1:(-P1 v -N4 v P5)) v -N4:(P5 v P1 v P2)));
N5 v [R1](P1 v -P2 v -[R1](-P1 v -P5 v -N3:(-N1 v -P2 v N5:(-N4 v -P4 v P5)))) v -N2:(P3 v -N5 v N1:(P1 v -[R1](N4 v -P1 v -N1)));
N4 v P4 v -N5:(N1 v [R1](N3 v -P3 v [R1](N4 v -P5 v -N3:(P5 v -N5 v -P3))) v [R1](-N4 v N2:(N4 v N1 v -N3)));
-N1 v P2 v N5:(P3 v N1 v -[R1](N3 v N2:(-P1 v -P4 v -[R1](-N2 v N5 v -P3)) v -[R1](N5 v -P4 v -N3)));
-N1 v -[R1](-N1 v -P4 v -N3:(N2 v N4 v [R1](-N1 v P2 v -N5:(-N4 v -P2 v -P1)))) v [R1](N3 v -N4:(-P4 v -P5 v -N2:(-N5 v -N4 v -N1)) v N2:(N1 v N5 v -N3));
N4 v -[R1](-N5 v P3 v -N4:(-N2 v N1:(-N3 v N2 v -[R1](N4 v P5 v P2)) v [R1](N5 v N4 v -P3))) v -N1:(N4 v P2 v [R1](-N2 v -N5 v N2:(-P1 v -N4 v -P5)));
-P5 v -P4 v [R1](N3 v -[R1](-P2 v -N1 v N5:(-N1 v N3:(-P2 v -N1 v P4))) v -N3:(N1 v N1:(N4 v P4 v -P3)));
P3 v N3:(-N4 v N5 v N1:(P4 v [R1](P1 v [R1](-P5 v -P4 v N4)) v -[R1](-P2 v -P5 v P4))) v [R1](N1 v -N3:(-P5 v [R1](-N3 v -P1 v N1)) v [R1](P4 v -P3 v -P2));
-P4 v [R1](P2 v N2 v -N1:(N5 v -[R1](-N1 v -N5:(-P2 v N4 v P1)) v N3:(-N4 v -N5 v -P5))) v [R1](-P1 v -N1 v -N3:(-P1 v N4:(P3 v -P2 v -P5)));
-P4 v -N1:(P4 v -[R1](N3 v -[R1](-P1 v -N1:(-P3 v N3 v N5)) v -N1:(N5 v N3 v N4)) v -N3:(N1 v -P5 v [R1](P4 v -N4 v P2))) v N1:(N5 v -[R1](N1 v N3 v [R1](P5 v -P3 v P2)) v -[R1](P2 v -N4 v -N5));
-P4 v -N1:(-P1 v -N4 v -N3:(N1 v N2 v [R1](N2 v [R1](-P3 v N4 v N1)))) v -N3:(-N5 v P4 v -[R1](N4 v -[R1](N1 v P1 v P5)));
P5 v -[R1](N3 v -N2 v [R1](-P1 v N2 v N3:(N5 v N4 v -N5:(N1 v -N3 v -N2)))) v [R1](-P4 v -P3 v N3:(-N1 v N2 v -N5:(N1 v -P1 v -P2)));
-P1 v -P3 v [R1](N1 v -[R1](P1 v -N3 v -N4:(P4 v -N2 v N3:(-P1 v P4 v N2))) v -N1:(P4 v -N2 v -N3:(-P1 v N5 v -P2)));
-P2 v -N1:(P5 v -[R1](P5 v [R1](-N1 v -N5:(-P2 v -P3 v P1)) v N1:(-P1 v -P3 v N2)) v -N1:(P5 v N3 v [R1](N2 v N3 v P4))) v N3:(-P2 v -[R1](-N2 v P1 v [R1](N2 v -N3 v -N5)) v [R1](P2 v -N5 v N1))
end