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