benchmark formulas k_lin_p.txt
begin
1: (false v ((box((p1 & (box p1)) -> p1)) v (box((p1 & (box p1)) -> p1)))) v (~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2)))))))
2: (false v ((box((p2 & (box p2)) -> p2)) v (box((p2 & (box p2)) -> p2)))) v ((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3))))))))
3: ((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v ((box((p3 & (box p3)) -> p3)) v (box((p3 & (box p3)) -> p3)))) v ((~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4))))))))
4: ((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v ((box((p4 & (box p4)) -> p4)) v (box((p4 & (box p4)) -> p4)))) v (((~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5))))))))
5: ((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v ((box((p5 & (box p5)) -> p5)) v (box((p5 & (box p5)) -> p5)))) v ((((~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6))))))))
6: (((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v ((box((p6 & (box p6)) -> p6)) v (box((p6 & (box p6)) -> p6)))) v ((((~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7))))))))
7: (((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v ((box((p7 & (box p7)) -> p7)) v (box((p7 & (box p7)) -> p7)))) v (((((~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8))))))))
8: (((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v ((box((p8 & (box p8)) -> p8)) v (box((p8 & (box p8)) -> p8)))) v ((((((~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9))))))))
9: ((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v ((box((p9 & (box p9)) -> p9)) v (box((p9 & (box p9)) -> p9)))) v ((((((~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10))))))))
10: ((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v ((box((p10 & (box p10)) -> p10)) v (box((p10 & (box p10)) -> p10)))) v (((((((~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11))))))))
11: ((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v ((box((p11 & (box p11)) -> p11)) v (box((p11 & (box p11)) -> p11)))) v ((((((((~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12))))))))
12: (((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v ((box((p12 & (box p12)) -> p12)) v (box((p12 & (box p12)) -> p12)))) v ((((((((~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13))))))))
13: (((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v ((box((p13 & (box p13)) -> p13)) v (box((p13 & (box p13)) -> p13)))) v (((((((((~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14))))))))
14: (((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v ((box((p14 & (box p14)) -> p14)) v (box((p14 & (box p14)) -> p14)))) v ((((((((((~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15))))))))
15: ((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v ((box((p15 & (box p15)) -> p15)) v (box((p15 & (box p15)) -> p15)))) v ((((((((((~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16))))))))
16: ((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v ((box((p16 & (box p16)) -> p16)) v (box((p16 & (box p16)) -> p16)))) v (((((((((((~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17))))))))
17: ((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v ((box((p17 & (box p17)) -> p17)) v (box((p17 & (box p17)) -> p17)))) v ((((((((((((~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17)))))))) v (~((((box((((p17 & (box p17)) & p17) -> p18) v ((~p17) -> (~((box p18) & p18))))) & (box((box(((p17 & (box p17)) & p17) -> p18)) v ((~p17) -> (~((box p18) & p18)))))) & (box((((p17 & (box p17)) & p17) -> p18) v (box((~p17) -> (~((box p18) & p18))))))) -> ((box(((p17 & (box p17)) & p17) -> p18)) v (box((~p17) -> (~((box p18) & p18))))))))
18: (((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v ((box((p18 & (box p18)) -> p18)) v (box((p18 & (box p18)) -> p18)))) v ((((((((((((~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17)))))))) v (~((((box((((p17 & (box p17)) & p17) -> p18) v ((~p17) -> (~((box p18) & p18))))) & (box((box(((p17 & (box p17)) & p17) -> p18)) v ((~p17) -> (~((box p18) & p18)))))) & (box((((p17 & (box p17)) & p17) -> p18) v (box((~p17) -> (~((box p18) & p18))))))) -> ((box(((p17 & (box p17)) & p17) -> p18)) v (box((~p17) -> (~((box p18) & p18)))))))) v (~((((box((((p18 & (box p18)) & p18) -> p19) v ((~p18) -> (~((box p19) & p19))))) & (box((box(((p18 & (box p18)) & p18) -> p19)) v ((~p18) -> (~((box p19) & p19)))))) & (box((((p18 & (box p18)) & p18) -> p19) v (box((~p18) -> (~((box p19) & p19))))))) -> ((box(((p18 & (box p18)) & p18) -> p19)) v (box((~p18) -> (~((box p19) & p19))))))))
19: (((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v ((box((p19 & (box p19)) -> p19)) v (box((p19 & (box p19)) -> p19)))) v (((((((((((((~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17)))))))) v (~((((box((((p17 & (box p17)) & p17) -> p18) v ((~p17) -> (~((box p18) & p18))))) & (box((box(((p17 & (box p17)) & p17) -> p18)) v ((~p17) -> (~((box p18) & p18)))))) & (box((((p17 & (box p17)) & p17) -> p18) v (box((~p17) -> (~((box p18) & p18))))))) -> ((box(((p17 & (box p17)) & p17) -> p18)) v (box((~p17) -> (~((box p18) & p18)))))))) v (~((((box((((p18 & (box p18)) & p18) -> p19) v ((~p18) -> (~((box p19) & p19))))) & (box((box(((p18 & (box p18)) & p18) -> p19)) v ((~p18) -> (~((box p19) & p19)))))) & (box((((p18 & (box p18)) & p18) -> p19) v (box((~p18) -> (~((box p19) & p19))))))) -> ((box(((p18 & (box p18)) & p18) -> p19)) v (box((~p18) -> (~((box p19) & p19)))))))) v (~((((box((((p19 & (box p19)) & p19) -> p20) v ((~p19) -> (~((box p20) & p20))))) & (box((box(((p19 & (box p19)) & p19) -> p20)) v ((~p19) -> (~((box p20) & p20)))))) & (box((((p19 & (box p19)) & p19) -> p20) v (box((~p19) -> (~((box p20) & p20))))))) -> ((box(((p19 & (box p19)) & p19) -> p20)) v (box((~p19) -> (~((box p20) & p20))))))))
20: (((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v ((box((p20 & (box p20)) -> p20)) v (box((p20 & (box p20)) -> p20)))) v ((((((((((((((~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8))))))) v (~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9)))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17)))))))) v (~((((box((((p17 & (box p17)) & p17) -> p18) v ((~p17) -> (~((box p18) & p18))))) & (box((box(((p17 & (box p17)) & p17) -> p18)) v ((~p17) -> (~((box p18) & p18)))))) & (box((((p17 & (box p17)) & p17) -> p18) v (box((~p17) -> (~((box p18) & p18))))))) -> ((box(((p17 & (box p17)) & p17) -> p18)) v (box((~p17) -> (~((box p18) & p18)))))))) v (~((((box((((p18 & (box p18)) & p18) -> p19) v ((~p18) -> (~((box p19) & p19))))) & (box((box(((p18 & (box p18)) & p18) -> p19)) v ((~p18) -> (~((box p19) & p19)))))) & (box((((p18 & (box p18)) & p18) -> p19) v (box((~p18) -> (~((box p19) & p19))))))) -> ((box(((p18 & (box p18)) & p18) -> p19)) v (box((~p18) -> (~((box p19) & p19)))))))) v (~((((box((((p19 & (box p19)) & p19) -> p20) v ((~p19) -> (~((box p20) & p20))))) & (box((box(((p19 & (box p19)) & p19) -> p20)) v ((~p19) -> (~((box p20) & p20)))))) & (box((((p19 & (box p19)) & p19) -> p20) v (box((~p19) -> (~((box p20) & p20))))))) -> ((box(((p19 & (box p19)) & p19) -> p20)) v (box((~p19) -> (~((box p20) & p20)))))))) v (~((((box((((p20 & (box p20)) & p20) -> p21) v ((~p20) -> (~((box p21) & p21))))) & (box((box(((p20 & (box p20)) & p20) -> p21)) v ((~p20) -> (~((box p21) & p21)))))) & (box((((p20 & (box p20)) & p20) -> p21) v (box((~p20) -> (~((box p21) & p21))))))) -> ((box(((p20 & (box p20)) & p20) -> p21)) v (box((~p20) -> (~((box p21) & p21))))))))
21: ((((((((~((((box((((p1 & (box p1)) & p1) -> p2) v ((~p1) -> (~((box p2) & p2))))) & (box((box(((p1 & (box p1)) & p1) -> p2)) v ((~p1) -> (~((box p2) & p2)))))) & (box((((p1 & (box p1)) & p1) -> p2) v (box((~p1) -> (~((box p2) & p2))))))) -> ((box(((p1 & (box p1)) & p1) -> p2)) v (box((~p1) -> (~((box p2) & p2))))))) v (~((((box((((p2 & (box p2)) & p2) -> p3) v ((~p2) -> (~((box p3) & p3))))) & (box((box(((p2 & (box p2)) & p2) -> p3)) v ((~p2) -> (~((box p3) & p3)))))) & (box((((p2 & (box p2)) & p2) -> p3) v (box((~p2) -> (~((box p3) & p3))))))) -> ((box(((p2 & (box p2)) & p2) -> p3)) v (box((~p2) -> (~((box p3) & p3)))))))) v (~((((box((((p3 & (box p3)) & p3) -> p4) v ((~p3) -> (~((box p4) & p4))))) & (box((box(((p3 & (box p3)) & p3) -> p4)) v ((~p3) -> (~((box p4) & p4)))))) & (box((((p3 & (box p3)) & p3) -> p4) v (box((~p3) -> (~((box p4) & p4))))))) -> ((box(((p3 & (box p3)) & p3) -> p4)) v (box((~p3) -> (~((box p4) & p4)))))))) v (~((((box((((p4 & (box p4)) & p4) -> p5) v ((~p4) -> (~((box p5) & p5))))) & (box((box(((p4 & (box p4)) & p4) -> p5)) v ((~p4) -> (~((box p5) & p5)))))) & (box((((p4 & (box p4)) & p4) -> p5) v (box((~p4) -> (~((box p5) & p5))))))) -> ((box(((p4 & (box p4)) & p4) -> p5)) v (box((~p4) -> (~((box p5) & p5)))))))) v (~((((box((((p5 & (box p5)) & p5) -> p6) v ((~p5) -> (~((box p6) & p6))))) & (box((box(((p5 & (box p5)) & p5) -> p6)) v ((~p5) -> (~((box p6) & p6)))))) & (box((((p5 & (box p5)) & p5) -> p6) v (box((~p5) -> (~((box p6) & p6))))))) -> ((box(((p5 & (box p5)) & p5) -> p6)) v (box((~p5) -> (~((box p6) & p6)))))))) v (~((((box((((p6 & (box p6)) & p6) -> p7) v ((~p6) -> (~((box p7) & p7))))) & (box((box(((p6 & (box p6)) & p6) -> p7)) v ((~p6) -> (~((box p7) & p7)))))) & (box((((p6 & (box p6)) & p6) -> p7) v (box((~p6) -> (~((box p7) & p7))))))) -> ((box(((p6 & (box p6)) & p6) -> p7)) v (box((~p6) -> (~((box p7) & p7)))))))) v (~((((box((((p7 & (box p7)) & p7) -> p8) v ((~p7) -> (~((box p8) & p8))))) & (box((box(((p7 & (box p7)) & p7) -> p8)) v ((~p7) -> (~((box p8) & p8)))))) & (box((((p7 & (box p7)) & p7) -> p8) v (box((~p7) -> (~((box p8) & p8))))))) -> ((box(((p7 & (box p7)) & p7) -> p8)) v (box((~p7) -> (~((box p8) & p8)))))))) v ((box((p21 & (box p21)) -> p21)) v (box((p21 & (box p21)) -> p21)))) v ((((((((((((((~((((box((((p8 & (box p8)) & p8) -> p9) v ((~p8) -> (~((box p9) & p9))))) & (box((box(((p8 & (box p8)) & p8) -> p9)) v ((~p8) -> (~((box p9) & p9)))))) & (box((((p8 & (box p8)) & p8) -> p9) v (box((~p8) -> (~((box p9) & p9))))))) -> ((box(((p8 & (box p8)) & p8) -> p9)) v (box((~p8) -> (~((box p9) & p9))))))) v (~((((box((((p9 & (box p9)) & p9) -> p10) v ((~p9) -> (~((box p10) & p10))))) & (box((box(((p9 & (box p9)) & p9) -> p10)) v ((~p9) -> (~((box p10) & p10)))))) & (box((((p9 & (box p9)) & p9) -> p10) v (box((~p9) -> (~((box p10) & p10))))))) -> ((box(((p9 & (box p9)) & p9) -> p10)) v (box((~p9) -> (~((box p10) & p10)))))))) v (~((((box((((p10 & (box p10)) & p10) -> p11) v ((~p10) -> (~((box p11) & p11))))) & (box((box(((p10 & (box p10)) & p10) -> p11)) v ((~p10) -> (~((box p11) & p11)))))) & (box((((p10 & (box p10)) & p10) -> p11) v (box((~p10) -> (~((box p11) & p11))))))) -> ((box(((p10 & (box p10)) & p10) -> p11)) v (box((~p10) -> (~((box p11) & p11)))))))) v (~((((box((((p11 & (box p11)) & p11) -> p12) v ((~p11) -> (~((box p12) & p12))))) & (box((box(((p11 & (box p11)) & p11) -> p12)) v ((~p11) -> (~((box p12) & p12)))))) & (box((((p11 & (box p11)) & p11) -> p12) v (box((~p11) -> (~((box p12) & p12))))))) -> ((box(((p11 & (box p11)) & p11) -> p12)) v (box((~p11) -> (~((box p12) & p12)))))))) v (~((((box((((p12 & (box p12)) & p12) -> p13) v ((~p12) -> (~((box p13) & p13))))) & (box((box(((p12 & (box p12)) & p12) -> p13)) v ((~p12) -> (~((box p13) & p13)))))) & (box((((p12 & (box p12)) & p12) -> p13) v (box((~p12) -> (~((box p13) & p13))))))) -> ((box(((p12 & (box p12)) & p12) -> p13)) v (box((~p12) -> (~((box p13) & p13)))))))) v (~((((box((((p13 & (box p13)) & p13) -> p14) v ((~p13) -> (~((box p14) & p14))))) & (box((box(((p13 & (box p13)) & p13) -> p14)) v ((~p13) -> (~((box p14) & p14)))))) & (box((((p13 & (box p13)) & p13) -> p14) v (box((~p13) -> (~((box p14) & p14))))))) -> ((box(((p13 & (box p13)) & p13) -> p14)) v (box((~p13) -> (~((box p14) & p14)))))))) v (~((((box((((p14 & (box p14)) & p14) -> p15) v ((~p14) -> (~((box p15) & p15))))) & (box((box(((p14 & (box p14)) & p14) -> p15)) v ((~p14) -> (~((box p15) & p15)))))) & (box((((p14 & (box p14)) & p14) -> p15) v (box((~p14) -> (~((box p15) & p15))))))) -> ((box(((p14 & (box p14)) & p14) -> p15)) v (box((~p14) -> (~((box p15) & p15)))))))) v (~((((box((((p15 & (box p15)) & p15) -> p16) v ((~p15) -> (~((box p16) & p16))))) & (box((box(((p15 & (box p15)) & p15) -> p16)) v ((~p15) -> (~((box p16) & p16)))))) & (box((((p15 & (box p15)) & p15) -> p16) v (box((~p15) -> (~((box p16) & p16))))))) -> ((box(((p15 & (box p15)) & p15) -> p16)) v (box((~p15) -> (~((box p16) & p16)))))))) v (~((((box((((p16 & (box p16)) & p16) -> p17) v ((~p16) -> (~((box p17) & p17))))) & (box((box(((p16 & (box p16)) & p16) -> p17)) v ((~p16) -> (~((box p17) & p17)))))) & (box((((p16 & (box p16)) & p16) -> p17) v (box((~p16) -> (~((box p17) & p17))))))) -> ((box(((p16 & (box p16)) & p16) -> p17)) v (box((~p16) -> (~((box p17) & p17)))))))) v (~((((box((((p17 & (box p17)) & p17) -> p18) v ((~p17) -> (~((box p18) & p18))))) & (box((box(((p17 & (box p17)) & p17) -> p18)) v ((~p17) -> (~((box p18) & p18)))))) & (box((((p17 & (box p17)) & p17) -> p18) v (box((~p17) -> (~((box p18) & p18))))))) -> ((box(((p17 & (box p17)) & p17) -> p18)) v (box((~p17) -> (~((box p18) & p18)))))))) v (~((((box((((p18 & (box p18)) & p18) -> p19) v ((~p18) -> (~((box p19) & p19))))) & (box((box(((p18 & (box p18)) & p18) -> p19)) v ((~p18) -> (~((box p19) & p19)))))) & (box((((p18 & (box p18)) & p18) -> p19) v (box((~p18) -> (~((box p19) & p19))))))) -> ((box(((p18 & (box p18)) & p18) -> p19)) v (box((~p18) -> (~((box p19) & p19)))))))) v (~((((box((((p19 & (box p19)) & p19) -> p20) v ((~p19) -> (~((box p20) & p20))))) & (box((box(((p19 & (box p19)) & p19) -> p20)) v ((~p19) -> (~((box p20) & p20)))))) & (box((((p19 & (box p19)) & p19) -> p20) v (box((~p19) -> (~((box p20) & p20))))))) -> ((box(((p19 & (box p19)) & p19) -> p20)) v (box((~p19) -> (~((box p20) & p20)))))))) v (~((((box((((p20 & (box p20)) & p20) -> p21) v ((~p20) -> (~((box p21) & p21))))) & (box((box(((p20 & (box p20)) & p20) -> p21)) v ((~p20) -> (~((box p21) & p21)))))) & (box((((p20 & (box p20)) & p20) -> p21) v (box((~p20) -> (~((box p21) & p21))))))) -> ((box(((p20 & (box p20)) & p20) -> p21)) v (box((~p20) -> (~((box p21) & p21)))))))) v (~((((box((((p21 & (box p21)) & p21) -> p22) v ((~p21) -> (~((box p22) & p22))))) & (box((box(((p21 & (box p21)) & p21) -> p22)) v ((~p21) -> (~((box p22) & p22)))))) & (box((((p21 & (box p21)) & p21) -> p22) v (box((~p21) -> (~((box p22) & p22))))))) -> ((box(((p21 & (box p21)) & p21) -> p22)) v (box((~p21) -> (~((box p22) & p22))))))))
end