% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 40 -vars 4 -depth 4 -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 : (v20 | (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 : (~v6 | (box r1 : (box r1 : (box r1 : ~v3))))))))))))))))))))) ). inputformula(mod2,hypothesis, (box r1 : (v20 | (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 : (v5 | (box r1 : v4)))))))))))))))))))) ). inputformula(mod3,hypothesis, (box r1 : (v20 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | (box r1 : (box r1 : (box r1 : (box r1 : (~v8 | (box r1 : (box r1 : (box r1 : ~v5))))))))))))))))))) ). inputformula(mod4,hypothesis, (box r1 : (v20 | (box r1 : (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 : (v6 | (box r1 : (box r1 : v4)))))))))))))))))))) ). inputformula(mod5,hypothesis, (box r1 : (~v20 | (box r1 : (box r1 : (v18 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v13 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v6)))))))))))))))))) ). inputformula(mod6,hypothesis, (box r1 : (~v20 | (box r1 : (box r1 : (box r1 : (box r1 : (v16 | (box r1 : (box r1 : (box r1 : (~v13 | (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 : (~v20 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (box r1 : (box r1 : (v11 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v6)))))))))))))))))) ). inputformula(mod8,hypothesis, (box r1 : (~v20 | (box r1 : (box r1 : (box r1 : (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 : (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (v19 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : (box r1 : v4)))))))))))))))))))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (box r1 : (~v18 | (box r1 : (~v17 | (box r1 : (v16 | (box r1 : (box r1 : ~v14)))))))))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (box r1 : (~v18 | (box r1 : (box r1 : (box r1 : (box r1 : (~v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v8 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (box r1 : (~v18 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v11 | (box r1 : (box r1 : (box r1 : (v8 | (box r1 : (box r1 : (box r1 : ~v5))))))))))))))))))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (v16 | (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v10)))))))))))))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (~v16 | (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(mod15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (~v13 | (box r1 : (box r1 : (box r1 : (box r1 : v9))))))))))))))) ). inputformula(mod16,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (box r1 : (v12 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v6)))))))))))))))))) ). inputformula(mod17,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (box r1 : (box r1 : (box r1 : (~v13 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v1))))))))))))))))))))))) ). inputformula(mod18,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v8 | (box r1 : (box r1 : (~v6 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v1))))))))))))))))))))))) ). inputformula(mod19,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v17 | (box r1 : (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | (box r1 : (box r1 : v4)))))))))))))))))))) ). inputformula(mod20,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v17 | (box r1 : (box r1 : (~v15 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v9 | (box r1 : v8)))))))))))))))) ). inputformula(mod21,hypothesis, (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 : v4)))))))))))))))))))) ). inputformula(mod22,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v17 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v11 | (box r1 : (box r1 : (box r1 : (v8 | (box r1 : (box r1 : (box r1 : ~v5))))))))))))))))))) ). inputformula(mod23,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v17 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v9 | (box r1 : (~v8 | (box r1 : (box r1 : (box r1 : ~v5))))))))))))))))))) ). inputformula(mod24,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (v12 | (box r1 : (box r1 : v10)))))))))))))) ). inputformula(mod25,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (v12 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v4)))))))))))))))))))) ). inputformula(mod26,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (box r1 : (~v11 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v2)))))))))))))))))))))) ). inputformula(mod27,hypothesis, (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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v4 | (box r1 : ~v3))))))))))))))))))))) ). inputformula(mod28,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | (box r1 : (box r1 : (box r1 : (v13 | (box r1 : (box r1 : (v11 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod29,hypothesis, (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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod30,hypothesis, (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 : (v9 | (box r1 : (box r1 : (v7 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod31,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v15 | (box r1 : (box r1 : (box r1 : (box r1 : (v11 | (box r1 : (box r1 : (box r1 : (v8 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : ~v2)))))))))))))))))))))) ). inputformula(mod32,hypothesis, (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 : (v6 | (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | (box r1 : v1))))))))))))))))))))))) ). inputformula(mod33,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (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 : (v4 | (box r1 : (box r1 : (box r1 : ~v1))))))))))))))))))))))) ). inputformula(mod34,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | (box r1 : (box r1 : (~v12 | (box r1 : (~v11 | (box r1 : (box r1 : (box r1 : (box r1 : v7))))))))))))))))) ). inputformula(mod35,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | (box r1 : ~v1))))))))))))))))))))))) ). inputformula(mod36,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | (box r1 : v1))))))))))))))))))))))) ). inputformula(mod37,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v14 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | (box r1 : v1))))))))))))))))))))))) ). inputformula(mod38,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | (box r1 : (box r1 : (box r1 : (~v10 | (box r1 : (v9 | (box r1 : ~v8)))))))))))))))) ). inputformula(mod39,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v13 | (box r1 : (box r1 : (box r1 : (box r1 : (v9 | (box r1 : (~v8 | (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : v2)))))))))))))))))))))) ). inputformula(mod40,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | (box r1 : (box r1 : (~v10 | (box r1 : (box r1 : (v8 | (box r1 : (box r1 : v6)))))))))))))))))) ). 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 : (pos r1 : true)) & (pos r1 : true))) & (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 : 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)) ). inputformula(result1,conjecture, false ).