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