% Unbounded Modal Sat from QBF - Randomly Generated
% -clauses 20 -vars 2 -depth 2 -lits 4 
% -prneg 0.500000 -prmod 0.500000
% Original reference Ladner, SIAM J. of Comp., SIAM Press
% Smart coding avoid the auxiliary variables of the original paper
% Parameter depth=-1 generate a random number of alternations
% With K,S4 flag prop variables hidden by modal proposition for K and S4
% Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)
% Copyright Fabio Massacci, November 1998

l:-[testref].

:-op(802,fy,box).
:-op(802,fy,pos).
:-op(801,yfy,':').
:-op(800,yfy,'|').
:-op(800,yfy,'&').
:-op(800,yfy,'=>'). % ?
:-op(799,fx,'~').

% Unbounded Modal Sat from QBF - Randomly Generated
% -clauses 20 -vars 2 -depth 2 -lits 4 
% -prneg 0.500000 -prmod 0.500000
% Original reference Ladner, SIAM J. of Comp., SIAM Press
% Smart coding avoid the auxiliary variables of the original paper
% Parameter depth=-1 generate a random number of alternations
% With K,S4 flag prop variables hidden by modal proposition for K and S4
% Benchmark generator by Fabio Massacci (massacci@dis.uniroma1.it)
% Copyright Fabio Massacci, November 1998


inputformula(mod1,hypothesis,
    (box r1 : (v1 | v4 | ~v3 => ~v6))
    ).


inputformula(mod2,hypothesis,
    (box r1 : (v2 | v3 | v6 | ~v4))
    ).

inputformula(mod3,hypothesis,
    (box r1 : (v3 | v4 | v5 | v6))
    ).

inputformula(mod4,hypothesis,
    (box r1 : (v3 | v4 | v6 | ~v2))
    ).

inputformula(mod5,hypothesis,
    (box r1 : (v3 | v5 | v6 | ~v4))
    ).

inputformula(mod6,hypothesis,
    (box r1 : (v3 | ~v1 | ~v4 | ~v6))
    ).

inputformula(mod7,hypothesis,
    (box r1 : (v3 | ~v4 | ~v5 | ~v6))
    ).

inputformula(mod8,hypothesis,
    (box r1 : (v4 | ~v1 | ~v3 | ~v6))
    ).

inputformula(mod9,hypothesis,
    (box r1 : (v4 | ~v3 | ~v5 | ~v6))
    ).

inputformula(mod10,hypothesis,
    (box r1 : (v6 | ~v3 | ~v4 | ~v5))
    ).

inputformula(mod11,hypothesis,
    (box r1 : (box r1 : (v1 | v3 | ~v4 | ~v5)))
    ).

inputformula(mod12,hypothesis,
    (box r1 : (box r1 : (v1 | v5 | ~v3 | ~v4)))
    ).

inputformula(mod13,hypothesis,
    (box r1 : (box r1 : (v2 | v3 | v4 | v5)))
    ).

inputformula(mod14,hypothesis,
    (box r1 : (box r1 : (v2 | v5 | ~v3 | ~v4)))
    ).

inputformula(mod15,hypothesis,
    (box r1 : (box r1 : (v2 | ~v3 | ~v4 | ~v5)))
    ).

inputformula(mod16,hypothesis,
    (box r1 : (box r1 : (v3 | v4 | v5 | v6)))
    ).

inputformula(mod17,hypothesis,
    (box r1 : (box r1 : (v3 | v4 | ~v2 | ~v5)))
    ).

inputformula(mod18,hypothesis,
    (box r1 : (box r1 : (v3 | v5 | v6 | ~v4)))
    ).

inputformula(mod19,hypothesis,
    (box r1 : (box r1 : (v3 | ~v4 | ~v5 | ~v6)))
    ).

inputformula(mod20,hypothesis,
    (box r1 : (box r1 : (v4 | ~v3 | ~v5 | ~v6)))
    ).

inputformula(mod21,hypothesis,
    (box r1 : (box r1 : (v5 | ~v2 | ~v3 | ~v4)))
    ).

inputformula(mod22,hypothesis,
    (box r1 : (box r1 : (v6 | ~v3 | ~v4 | ~v5)))
    ).

inputformula(mod23,hypothesis,
    (box r1 : (box r1 : (~v1 | ~v3 | ~v4 | ~v5)))
    ).

inputformula(mod24,hypothesis,
    (box r1 : (box r1 : (box r1 : (v1 | v3 | ~v4 | ~v5))))
    ).

inputformula(mod25,hypothesis,
    (box r1 : (box r1 : (box r1 : (v1 | v4 | ~v3 | ~v6))))
    ).

inputformula(mod26,hypothesis,
    (box r1 : (box r1 : (box r1 : (v1 | v5 | ~v3 | ~v4))))
    ).

inputformula(mod27,hypothesis,
    (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | v5))))
    ).

inputformula(mod28,hypothesis,
    (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | ~v1))))
    ).

inputformula(mod29,hypothesis,
    (box r1 : (box r1 : (box r1 : (v2 | v3 | v6 | ~v4))))
    ).

inputformula(mod30,hypothesis,
    (box r1 : (box r1 : (box r1 : (v2 | v5 | ~v3 | ~v4))))
    ).

inputformula(mod31,hypothesis,
    (box r1 : (box r1 : (box r1 : (v2 | ~v3 | ~v4 | ~v5))))
    ).

inputformula(mod32,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | v4 | v5 | v6))))
    ).

inputformula(mod33,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | v4 | v6 | ~v2))))
    ).

inputformula(mod34,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | v4 | ~v2 | ~v5))))
    ).

inputformula(mod35,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | v5 | v6 | ~v4))))
    ).

inputformula(mod36,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | ~v1 | ~v4 | ~v6))))
    ).

inputformula(mod37,hypothesis,
    (box r1 : (box r1 : (box r1 : (v3 | ~v4 | ~v5 | ~v6))))
    ).

inputformula(mod38,hypothesis,
    (box r1 : (box r1 : (box r1 : (v4 | ~v1 | ~v3 | ~v6))))
    ).

inputformula(mod39,hypothesis,
    (box r1 : (box r1 : (box r1 : (v4 | ~v3 | ~v5 | ~v6))))
    ).

inputformula(mod40,hypothesis,
    (box r1 : (box r1 : (box r1 : (v5 | ~v2 | ~v3 | ~v4))))
    ).

inputformula(mod41,hypothesis,
    (box r1 : (box r1 : (box r1 : (v6 | ~v3 | ~v4 | ~v5))))
    ).

inputformula(mod42,hypothesis,
    (box r1 : (box r1 : (box r1 : (~v1 | ~v2 | ~v3 | ~v4))))
    ).

inputformula(mod43,hypothesis,
    (box r1 : (box r1 : (box r1 : (~v1 | ~v3 | ~v4 | ~v5))))
    ).

inputformula(mod44,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v3 | ~v4 | ~v5)))))
    ).

inputformula(mod45,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v4 | ~v3 | ~v6)))))
    ).

inputformula(mod46,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v5 | ~v3 | ~v4)))))
    ).

inputformula(mod47,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | v5)))))
    ).

inputformula(mod48,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | ~v1)))))
    ).

inputformula(mod49,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v6 | ~v4)))))
    ).

inputformula(mod50,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v5 | ~v3 | ~v4)))))
    ).

inputformula(mod51,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v2 | ~v3 | ~v4 | ~v5)))))
    ).

inputformula(mod52,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v4 | v5 | v6)))))
    ).

inputformula(mod53,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v4 | v6 | ~v2)))))
    ).

inputformula(mod54,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v4 | ~v2 | ~v5)))))
    ).

inputformula(mod55,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v5 | v6 | ~v4)))))
    ).

inputformula(mod56,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | ~v1 | ~v4 | ~v6)))))
    ).

inputformula(mod57,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | ~v4 | ~v5 | ~v6)))))
    ).

inputformula(mod58,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v4 | ~v1 | ~v3 | ~v6)))))
    ).

inputformula(mod59,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v4 | ~v3 | ~v5 | ~v6)))))
    ).

inputformula(mod60,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v5 | ~v2 | ~v3 | ~v4)))))
    ).

inputformula(mod61,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v6 | ~v3 | ~v4 | ~v5)))))
    ).

inputformula(mod62,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v2 | ~v3 | ~v4)))))
    ).

inputformula(mod63,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v3 | ~v4 | ~v5)))))
    ).

inputformula(mod64,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | v5))))))
    ).

inputformula(mod65,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | ~v1))))))
    ).

inputformula(mod66,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v6 | ~v4))))))
    ).

inputformula(mod67,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v5 | ~v3 | ~v4))))))
    ).

inputformula(mod68,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | ~v3 | ~v4 | ~v5))))))
    ).

inputformula(mod69,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v4 | v6 | ~v2))))))
    ).

inputformula(mod70,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v4 | ~v2 | ~v5))))))
    ).

inputformula(mod71,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | ~v2 | ~v3 | ~v4))))))
    ).

inputformula(mod72,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v2 | ~v3 | ~v4))))))
    ).

inputformula(mod73,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v3 | ~v4 | ~v5)))))))
    ).

inputformula(mod74,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v4 | ~v3 | ~v6)))))))
    ).

inputformula(mod75,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v5 | ~v3 | ~v4)))))))
    ).

inputformula(mod76,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v4 | ~v1)))))))
    ).

inputformula(mod77,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | ~v1 | ~v4 | ~v6)))))))
    ).

inputformula(mod78,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | ~v1 | ~v3 | ~v6)))))))
    ).

inputformula(mod79,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v2 | ~v3 | ~v4)))))))
    ).

inputformula(mod80,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v3 | ~v4 | ~v5)))))))
    ).

inputformula(alt1,hypothesis,
    (box r1 : (v6 | (box r1 : ~v6)))
    ).

inputformula(alt2,hypothesis,
    (box r1 : (~v6 | (box r1 : v6)))
    ).

inputformula(alt3,hypothesis,
    (box r1 : (box r1 : (v5 | (box r1 : ~v5))))
    ).

inputformula(alt4,hypothesis,
    (box r1 : (box r1 : (v6 | (box r1 : ~v6))))
    ).

inputformula(alt5,hypothesis,
    (box r1 : (box r1 : (~v5 | (box r1 : v5))))
    ).

inputformula(alt6,hypothesis,
    (box r1 : (box r1 : (~v6 | (box r1 : v6))))
    ).

inputformula(alt7,hypothesis,
    (box r1 : (box r1 : (box r1 : (v4 | (box r1 : ~v4)))))
    ).

inputformula(alt8,hypothesis,
    (box r1 : (box r1 : (box r1 : (v5 | (box r1 : ~v5)))))
    ).

inputformula(alt9,hypothesis,
    (box r1 : (box r1 : (box r1 : (v6 | (box r1 : ~v6)))))
    ).

inputformula(alt10,hypothesis,
    (box r1 : (box r1 : (box r1 : (~v4 | (box r1 : v4)))))
    ).

inputformula(alt11,hypothesis,
    (box r1 : (box r1 : (box r1 : (~v5 | (box r1 : v5)))))
    ).

inputformula(alt12,hypothesis,
    (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : v6)))))
    ).

inputformula(alt13,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v3 | (box r1 : ~v3))))))
    ).

inputformula(alt14,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v4 | (box r1 : ~v4))))))
    ).

inputformula(alt15,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v5 | (box r1 : ~v5))))))
    ).

inputformula(alt16,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (v6 | (box r1 : ~v6))))))
    ).

inputformula(alt17,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | (box r1 : v3))))))
    ).

inputformula(alt18,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v4 | (box r1 : v4))))))
    ).

inputformula(alt19,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v5 | (box r1 : v5))))))
    ).

inputformula(alt20,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : v6))))))
    ).

inputformula(alt21,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | (box r1 : ~v2)))))))
    ).

inputformula(alt22,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | (box r1 : ~v3)))))))
    ).

inputformula(alt23,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | (box r1 : ~v4)))))))
    ).

inputformula(alt24,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | (box r1 : ~v5)))))))
    ).

inputformula(alt25,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | (box r1 : ~v6)))))))
    ).

inputformula(alt26,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | (box r1 : v2)))))))
    ).

inputformula(alt27,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | (box r1 : v3)))))))
    ).

inputformula(alt28,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v4 | (box r1 : v4)))))))
    ).

inputformula(alt29,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v5 | (box r1 : v5)))))))
    ).

inputformula(alt30,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v6 | (box r1 : v6)))))))
    ).

inputformula(alt31,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (pos r1 : true))))))
    ).

inputformula(alt32,hypothesis,
    (box r1 : (box r1 : (box r1 : (box r1 : (pos r1 : true)))))
    ).

inputformula(alt33,hypothesis,
    (box r1 : (box r1 : (box r1 : (pos r1 : v3))))
    ).

inputformula(alt34,hypothesis,
    (box r1 : (box r1 : (box r1 : (pos r1 : ~v3))))
    ).

inputformula(alt35,hypothesis,
    (box r1 : (box r1 : (pos r1 : v4)))
    ).

inputformula(alt36,hypothesis,
    (box r1 : (box r1 : (pos r1 : ~v4)))
    ).

inputformula(alt37,hypothesis,
    (box r1 : (pos r1 : true))
    ).

inputformula(alt38,hypothesis,
    (pos r1 : true)
    ).

inputformula(result1,conjecture,
    false
    ).

