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