inputformula(
1,hypothesis, (true & (~(box(box((box((box(p0 -> (box p0))) -> p0)) -> ((dia(box p0)) -> p0)))))) -> ((dia(dia(~(((((box((box(p0 -> (box p0))) -> p0)) -> (box(box((box(p0 -> (box p0))) -> p0)))) & (box((box p0) -> (box(box p0))))) & ((box((box(p0 -> (box p0))) -> p0)) -> ((dia(box p0)) -> (p0 v (box p0))))) & ((box((box((p0 -> (box p0)) -> (box(p0 -> (box p0))))) -> (p0 -> (box p0)))) -> ((dia(box(p0 -> (box p0)))) -> ((p0 -> (box p0)) v (box(p0 -> (box p0)))))))))) v false)
).
inputformula(1,conjecture,false).