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