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