% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 20 -vars 16 -depth 6 -lits 4 % -prneg 0.500000 -prmod 0.500000 % -sss % Original reference Ladner, SIAM JOC, 1977, SIAM Press % Smart coding avoid the auxiliary variables of the original paper % With ladner flag encoding further optimized % With sss flag encoding by Schimdt-Schauss Smolka, AIJ 1991, Elsevier % With K,S4 flag prop variables hidden by modal proposition for K and S4 % (formulae are no longer in CNF) due to Halpern, AIJ 95, Elsevier % Parameter depth=-1 generate a random number of alternations % Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it) % Copyright Fabio Massacci, November 1998 inputformula(mod1,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v108 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v64 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v51 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v37))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod2,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v108 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v101 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v95 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v24)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod3,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v106 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v82 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v37 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v25))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v102 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v90 | (box r1 : (box r1 : (~v88 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v39))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod5,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v101 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v94 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v51 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v3))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v99 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v92 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v25 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v94 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v52 | (box r1 : (box r1 : (box r1 : (box r1 : (v48 | (box r1 : (box r1 : (box r1 : (box r1 : v44)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v89 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v73 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v61 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v16)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v87 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v69 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v58 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v45))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v86 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v53 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v47 | (box r1 : ~v46)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v85 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v44 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v34 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v27))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v85 | (box r1 : (~v84 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v74 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v14)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v84 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v23 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v16 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v82 | (box r1 : (~v81 | (box r1 : (box r1 : (box r1 : (box r1 : (v77 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v41))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v82 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v52 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v38 | (box r1 : v37))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod16,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v76 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v31 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v25 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v8)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod17,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v73 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v62 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v39))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod18,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v67 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v53 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v23 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod19,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v54 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v42 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v25 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v11))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod20,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v34 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v21 | (box r1 : (box r1 : (v19 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v13))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt1,hypothesis, ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : (pos r1 : true)) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v19) & (pos r1 : ~v19))) & (pos r1 : true))) & (pos r1 : v21) & (pos r1 : ~v21))) & (pos r1 : true))) & (pos r1 : v23) & (pos r1 : ~v23))) & (pos r1 : v24) & (pos r1 : ~v24))) & (pos r1 : v25) & (pos r1 : ~v25))) & (pos r1 : true))) & (pos r1 : v27) & (pos r1 : ~v27))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v31) & (pos r1 : ~v31))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v51) & (pos r1 : ~v51))) & (pos r1 : v52) & (pos r1 : ~v52))) & (pos r1 : v53) & (pos r1 : ~v53))) & (pos r1 : v54) & (pos r1 : ~v54))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v58) & (pos r1 : ~v58))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v61) & (pos r1 : ~v61))) & (pos r1 : v62) & (pos r1 : ~v62))) & (pos r1 : true))) & (pos r1 : v64) & (pos r1 : ~v64))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v81) & (pos r1 : ~v81))) & (pos r1 : v82) & (pos r1 : ~v82))) & (pos r1 : true))) & (pos r1 : v84) & (pos r1 : ~v84))) & (pos r1 : v85) & (pos r1 : ~v85))) & (pos r1 : v86) & (pos r1 : ~v86))) & (pos r1 : v87) & (pos r1 : ~v87))) & (pos r1 : v88) & (pos r1 : ~v88))) & (pos r1 : v89) & (pos r1 : ~v89))) & (pos r1 : v90) & (pos r1 : ~v90))) & (pos r1 : true))) & (pos r1 : v92) & (pos r1 : ~v92))) & (pos r1 : true))) & (pos r1 : v94) & (pos r1 : ~v94))) & (pos r1 : v95) & (pos r1 : ~v95))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true)) ). inputformula(result1,conjecture, false ).