inputformula(
6,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(box p0)))) & ((box((box(p0 -> (box p0))) -> p0)) -> ((dia(box p0)) -> p0))))))) & (~(box(box(box(box((box((box(p0 -> (box p0))) -> p0)) -> ((dia(box p0)) -> (box p0))))))))) -> ((dia(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 (dia(dia(dia(dia(dia(~((box((box p0) -> (box(box p0)))) & ((box((box(p0 -> (box p0))) -> p0)) -> ((dia(box p0)) -> p0))))))))))
).
inputformula(1,conjecture,true).