% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 10 -vars 4 -depth 6 -lits 4 % -prneg 0.500000 -prmod 0.500000 % -ladner % 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 : (v20 | v28 | ~v6 | ~v7)) ). inputformula(mod2,hypothesis, (box r1 : (v24 | v28 | ~v7 | ~v25)) ). inputformula(mod3,hypothesis, (box r1 : (v28 | ~v5 | ~v7 | ~v20)) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (v5 | v8 | v10 | ~v27))) ). inputformula(mod5,hypothesis, (box r1 : (box r1 : (v13 | v27 | ~v6 | ~v12))) ). inputformula(mod6,hypothesis, (box r1 : (box r1 : (box r1 : (v19 | ~v5 | ~v23 | ~v26)))) ). inputformula(mod7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v5 | v25 | ~v20 | ~v21))))) ). inputformula(mod8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v24 | v28 | ~v7 | ~v25))))) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v13 | v20 | v24)))))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 | v28 | ~v7 | ~v25)))))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 | ~v10 | ~v11 | ~v13)))))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v18 | v23 | ~v8))))))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v5 | ~v23 | ~v26))))))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | v25 | ~v20 | ~v21))))))))) ). inputformula(mod15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | v25 | ~v20 | ~v21)))))))))) ). inputformula(mod16,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v13 | v20 | v24)))))))))) ). inputformula(mod17,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v20 | v28 | ~v6 | ~v7)))))))))) ). inputformula(mod18,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v28 | ~v5 | ~v7 | ~v20)))))))))) ). inputformula(mod19,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v5 | ~v23 | ~v26))))))))))) ). 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 : (v3 | v18 | v23 | ~v8)))))))))))) ). inputformula(mod21,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 : (v9 | v13 | v20 | v24))))))))))))))))) ). inputformula(mod22,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 : (v13 | v27 | ~v6 | ~v12))))))))))))))))) ). inputformula(mod23,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 : (v24 | ~v10 | ~v11 | ~v13))))))))))))))))) ). inputformula(mod24,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 : (v13 | v27 | ~v6 | ~v12)))))))))))))))))) ). inputformula(mod25,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 : (v24 | ~v10 | ~v11 | ~v13))))))))))))))))))) ). inputformula(mod26,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 : (v5 | v8 | v10 | ~v27)))))))))))))))))))) ). inputformula(mod27,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 : (v24 | ~v10 | ~v11 | ~v13)))))))))))))))))))) ). inputformula(mod28,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 : (v9 | v13 | v20 | v24))))))))))))))))))))) ). inputformula(mod29,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 : (v3 | v18 | v23 | ~v8)))))))))))))))))))))) ). inputformula(mod30,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 : (v5 | v8 | v10 | ~v27)))))))))))))))))))))) ). inputformula(mod31,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 : (v20 | v28 | ~v6 | ~v7))))))))))))))))))))))) ). inputformula(mod32,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 : (v24 | v28 | ~v7 | ~v25))))))))))))))))))))))) ). inputformula(mod33,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 : (v28 | ~v5 | ~v7 | ~v20))))))))))))))))))))))) ). inputformula(mod34,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 : (v13 | v27 | ~v6 | ~v12)))))))))))))))))))))))) ). inputformula(mod35,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 : (v20 | v28 | ~v6 | ~v7)))))))))))))))))))))))) ). inputformula(mod36,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 : (v5 | v8 | v10 | ~v27))))))))))))))))))))))))) ). inputformula(mod37,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 : (v5 | v25 | ~v20 | ~v21))))))))))))))))))))))))) ). inputformula(mod38,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 : (v19 | ~v5 | ~v23 | ~v26))))))))))))))))))))))))) ). inputformula(mod39,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 : (v28 | ~v5 | ~v7 | ~v20))))))))))))))))))))))))) ). inputformula(mod40,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 : (v3 | v18 | v23 | ~v8))))))))))))))))))))))))))) ). 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 : (pos r1 : true)) & (pos r1 : true))) & (pos r1 : v5) & (pos r1 : ~v5))) & (pos r1 : v6) & (pos r1 : ~v6))) & (pos r1 : v7) & (pos r1 : ~v7))) & (pos r1 : v8) & (pos r1 : ~v8))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v13) & (pos r1 : ~v13))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (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 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true)) ). inputformula(alt2,hypothesis, (box r1 : (v28 => (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : v28))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt3,hypothesis, (box r1 : (~v28 => (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : ~v28))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt4,hypothesis, (box r1 : (box r1 : (v27 => (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : v27)))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt5,hypothesis, (box r1 : (box r1 : (~v27 => (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : ~v27)))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt6,hypothesis, (box r1 : (box r1 : (box r1 : (v26 => (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : (v26 & (box r1 : v26))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt7,hypothesis, (box r1 : (box r1 : (box r1 : (~v26 => (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : (~v26 & (box r1 : ~v26))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v25 => (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : v25)))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v25 => (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : ~v25)))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 => (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : (v24 & (box r1 : v24))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v24 => (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : (~v24 & (box r1 : ~v24))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v23 => (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : v23)))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v23 => (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : ~v23)))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v21 => (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : (v21 & (box r1 : v21)))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v21 => (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : (~v21 & (box r1 : ~v21)))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt16,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v20 => (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : (v20 & (box r1 : v20))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt17,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v20 => (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : (~v20 & (box r1 : ~v20))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt18,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 => (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : (v19 & (box r1 : v19)))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt19,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v19 => (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : (~v19 & (box r1 : ~v19)))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt20,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v18 => (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : (v18 & (box r1 : v18))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt21,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v18 => (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : (~v18 & (box r1 : ~v18))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt22,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 : (v13 => (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : (v13 & (box r1 : v13)))))))))))))))))))))))))))))))))))) ). inputformula(alt23,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 : (~v13 => (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : (~v13 & (box r1 : ~v13)))))))))))))))))))))))))))))))))))) ). inputformula(alt24,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 : (v12 => (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : v12))))))))))))))))))))))))))))))))))) ). inputformula(alt25,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 : (~v12 => (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : ~v12))))))))))))))))))))))))))))))))))) ). inputformula(alt26,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 : (v11 => (box r1 : (v11 & (box r1 : (v11 & (box r1 : (v11 & (box r1 : (v11 & (box r1 : (v11 & (box r1 : (v11 & (box r1 : (v11 & (box r1 : v11)))))))))))))))))))))))))))))))))) ). inputformula(alt27,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 : (~v11 => (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : (~v11 & (box r1 : ~v11)))))))))))))))))))))))))))))))))) ). inputformula(alt28,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 : (v10 => (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : v10))))))))))))))))))))))))))))))))) ). inputformula(alt29,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 : (~v10 => (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : ~v10))))))))))))))))))))))))))))))))) ). inputformula(alt30,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 : (v9 => (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : v9)))))))))))))))))))))))))))))))) ). inputformula(alt31,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 : (~v9 => (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : ~v9)))))))))))))))))))))))))))))))) ). inputformula(alt32,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 : (v8 => (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : v8))))))))))))))))))))))))))))))) ). inputformula(alt33,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 : (~v8 => (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : ~v8))))))))))))))))))))))))))))))) ). inputformula(alt34,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 : (v7 => (box r1 : (v7 & (box r1 : (v7 & (box r1 : (v7 & (box r1 : v7)))))))))))))))))))))))))))))) ). inputformula(alt35,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 : (~v7 => (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : ~v7)))))))))))))))))))))))))))))) ). inputformula(alt36,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 : (v6 => (box r1 : (v6 & (box r1 : (v6 & (box r1 : v6))))))))))))))))))))))))))))) ). inputformula(alt37,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 : (~v6 => (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : ~v6))))))))))))))))))))))))))))) ). inputformula(alt38,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 : (v5 => (box r1 : (v5 & (box r1 : v5)))))))))))))))))))))))))))) ). inputformula(alt39,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 : (~v5 => (box r1 : (~v5 & (box r1 : ~v5)))))))))))))))))))))))))))) ). inputformula(result1,conjecture, false ).