begin
(n1 v !([R1](n3 v (n3:(!n4 v !(n2:(p8 v ([R1](p6 v ([R1](!p3 v !(n4:(n2 v (n2:(n1 v (n4:(n3 v p1))))))))))))))))) &
(!n4 v !(n3:(!n1 v (n2:(!n3 v !([R1](n3 v (n4:(n2 v ([R1](p7 v !(n3:(p6 v !(n4:(n1 v !([R1](n1 v !p5))))))))))))))))) &
(p4 v !([R1](n4 v ([R1](!n4 v (n1:(n3 v !([R1](!n1 v ([R1](!n3 v (n4:(!p6 v !(n2:(!p3 v !(n4:(!n3 v n1))))))))))))))))) &
(n4 v !([R1](!p2 v (n3:(!n2 v (n4:(!n1 v !([R1](!p7 v !(n2:(!n4 v ([R1](!p2 v !(n3:(!p6 v (n2:(!n1 v p6))))))))))))))))) &
(n2 v ([R1](n3 v !(n2:(!n3 v (n3:(!n4 v (n3:(!p2 v ([R1](!p2 v (n3:(!p3 v !([R1](!p3 v ([R1](n2 v !n1))))))))))))))))) &
(!n2 v (n4:(!p4 v !([R1](n1 v (n4:(p4 v (n4:(p4 v !(n3:(p2 v ([R1](!p1 v ([R1](p1 v ([R1](n2 v !n1))))))))))))))))) &
(n4 v !(n1:(!n3 v (n1:(!p2 v ([R1](n1 v !(n4:(!p3 v !([R1](n2 v ([R1](!n2 v (n1:(!p4 v ([R1](n4 v !n3)))))))))))))))))
end