% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 10 -vars 4 -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 : (v28 | (box r1 : (box r1 : (box r1 : (box r1 : (v24 | (box r1 : (box r1 : (box r1 : (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 : (box r1 : ~v7))))))))))))))))))))))))) ). inputformula(mod2,hypothesis, (box r1 : (~v28 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v21 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v16 | (box r1 : (box r1 : (box r1 : (box r1 : v12)))))))))))))))))))) ). inputformula(mod3,hypothesis, (box r1 : (box r1 : (box r1 : (v26 | (box r1 : (box r1 : (box r1 : (box r1 : (~v22 | (box r1 : (v21 | (box r1 : (box r1 : (box r1 : ~v18)))))))))))))) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (box r1 : (~v26 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v19 | (box r1 : (box r1 : (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v7))))))))))))))))))))))))) ). inputformula(mod5,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v25 | (box r1 : (box r1 : (box r1 : (~v22 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v4)))))))))))))))))))))))))))) ). inputformula(mod6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v24 | (box r1 : (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 : (v10 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v3))))))))))))))))))))))))))))) ). inputformula(mod7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | (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 : (box r1 : (v5 | (box r1 : (box r1 : (box r1 : v2)))))))))))))))))))))))))))))) ). 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 : (v17 | (box r1 : (box r1 : (box r1 : (~v14 | (box r1 : (~v13 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v3))))))))))))))))))))))))))))) ). 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 : (~v17 | (box r1 : (box r1 : (box r1 : (v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v7 | (box r1 : (box r1 : (box r1 : (box r1 : v3))))))))))))))))))))))))))))) ). 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 : (v16 | (box r1 : (box r1 : (~v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v9 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v3))))))))))))))))))))))))))))) ). 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 : (pos r1 : true)) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v5) & (pos r1 : ~v5))) & (pos r1 : true))) & (pos r1 : v7) & (pos r1 : ~v7))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v13) & (pos r1 : ~v13))) & (pos r1 : v14) & (pos r1 : ~v14))) & (pos r1 : v15) & (pos r1 : ~v15))) & (pos r1 : v16) & (pos r1 : ~v16))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v21) & (pos r1 : ~v21))) & (pos r1 : v22) & (pos r1 : ~v22))) & (pos r1 : true))) & (pos r1 : v24) & (pos r1 : ~v24))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true)) ). inputformula(result1,conjecture, false ).