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