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