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