benchmark formulas k_grz_n.txt
begin
1: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & true) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
2: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1)))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
3: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
4: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
5: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
6: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
7: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
8: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
9: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
10: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
11: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
12: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
13: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
14: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
15: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
16: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
17: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
18: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
19: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
20: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & ((((((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
21: (((box((box((box(p2 -> (box p2))) -> p2)) -> (box p2))) & (((((((((((((((((((((box((box(((box false) v p1) -> (box((box false) v p1)))) -> ((box false) v p1))) -> (box((box false) v p1))) & ((box((box((((box false) v p1) v p2) -> (box(((box false) v p1) v p2)))) -> (((box false) v p1) v p2))) -> (box(((box false) v p1) v p2)))) & ((box((box(((((box false) v p1) v p2) v p3) -> (box((((box false) v p1) v p2) v p3)))) -> ((((box false) v p1) v p2) v p3))) -> (box((((box false) v p1) v p2) v p3)))) & ((box((box((((((box false) v p1) v p2) v p3) v p4) -> (box(((((box false) v p1) v p2) v p3) v p4)))) -> (((((box false) v p1) v p2) v p3) v p4))) -> (box(((((box false) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box false) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box false) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) & ((box((box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) -> ((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1))) -> (box((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1)))) & ((box((box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) -> (((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2))) -> (box(((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2)))) & ((box((box(((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) -> (box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) -> ((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3))) -> (box((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3)))) & ((box((box((((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4) -> (box(((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)))) -> (((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))) -> (box(((((box(((((box(((((box(((((box(((((box false) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4)) v p1) v p2) v p3) v p4))))) & ((box((box((((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> (((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2))))))) -> (box(((box(p2 -> (box p2))) -> p2) & ((box((box(p2 -> (box p2))) -> p2)) -> (box(box((box(p2 -> (box p2))) -> p2)))))))) -> ((((box((box(p1 -> (box p1))) -> p1)) -> p1) v ((box((box(p2 -> (box p2))) -> p2)) -> p2)) v ((box((box(p3 -> (box p3))) -> p3)) -> p3))
end