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