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