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