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