% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 40 -vars 4 -depth 4 -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 : (v1 | v13 | v15 | ~v20)) ). inputformula(mod2,hypothesis, (box r1 : (v4 | v7 | v16 | v20)) ). inputformula(mod3,hypothesis, (box r1 : (v6 | v11 | v13 | ~v20)) ). inputformula(mod4,hypothesis, (box r1 : (v11 | v15 | ~v5 | ~v20)) ). inputformula(mod5,hypothesis, (box r1 : (v13 | v15 | v20 | ~v12)) ). inputformula(mod6,hypothesis, (box r1 : (v16 | v20 | ~v8 | ~v11)) ). inputformula(mod7,hypothesis, (box r1 : (~v2 | ~v13 | ~v16 | ~v20)) ). inputformula(mod8,hypothesis, (box r1 : (~v9 | ~v14 | ~v15 | ~v20)) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (v2 | ~v8 | ~v15 | ~v19))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (v3 | v5 | v13 | ~v19))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (v4 | ~v5 | ~v6 | ~v19))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (v5 | v6 | v12 | ~v19))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (v9 | v16 | ~v5 | ~v19))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (v13 | v14 | v19 | ~v1))) ). inputformula(mod15,hypothesis, (box r1 : (box r1 : (v14 | v16 | v19 | ~v2))) ). inputformula(mod16,hypothesis, (box r1 : (box r1 : (v18 | ~v7 | ~v14 | ~v19))) ). inputformula(mod17,hypothesis, (box r1 : (box r1 : (v19 | ~v1 | ~v7 | ~v14))) ). inputformula(mod18,hypothesis, (box r1 : (box r1 : (v19 | ~v2 | ~v6 | ~v7))) ). inputformula(mod19,hypothesis, (box r1 : (box r1 : (box r1 : (v7 | v18 | ~v11 | ~v13)))) ). inputformula(mod20,hypothesis, (box r1 : (box r1 : (box r1 : (v17 | ~v6 | ~v7 | ~v18)))) ). inputformula(mod21,hypothesis, (box r1 : (box r1 : (box r1 : (v18 | ~v7 | ~v14 | ~v19)))) ). inputformula(mod22,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v8 | v14 | v17 | ~v3))))) ). inputformula(mod23,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 | ~v6 | ~v7 | ~v18))))) ). inputformula(mod24,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | ~v8 | ~v14 | ~v17))))) ). inputformula(mod25,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v7 | v16 | v20)))))) ). inputformula(mod26,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | ~v11 | ~v12 | ~v16)))))) ). inputformula(mod27,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v12 | v16 | ~v2)))))) ). inputformula(mod28,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v16 | ~v5 | ~v19)))))) ). inputformula(mod29,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v16 | v19 | ~v2)))))) ). inputformula(mod30,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v16 | ~v9 | ~v12)))))) ). inputformula(mod31,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v20 | ~v8 | ~v11)))))) ). inputformula(mod32,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | ~v1 | ~v8 | ~v11)))))) ). inputformula(mod33,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | ~v13 | ~v16 | ~v20)))))) ). inputformula(mod34,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v5 | v15 | ~v9))))))) ). inputformula(mod35,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v13 | v15 | ~v20))))))) ). inputformula(mod36,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | ~v8 | ~v15 | ~v19))))))) ). inputformula(mod37,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | v9 | ~v11 | ~v15))))))) ). inputformula(mod38,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v11 | v15 | ~v13))))))) ). inputformula(mod39,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v14 | ~v1 | ~v15))))))) ). inputformula(mod40,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v11 | v14 | ~v15))))))) ). inputformula(mod41,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v15 | ~v5 | ~v12))))))) ). inputformula(mod42,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v11 | v15 | ~v5 | ~v20))))))) ). inputformula(mod43,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v15 | v20 | ~v12))))))) ). inputformula(mod44,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v9 | ~v14 | ~v15 | ~v20))))))) ). inputformula(mod45,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v6 | ~v3 | ~v14)))))))) ). inputformula(mod46,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v14 | ~v2 | ~v5)))))))) ). inputformula(mod47,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v14 | ~v11 | ~v13)))))))) ). inputformula(mod48,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v8 | v14 | v17 | ~v3)))))))) ). inputformula(mod49,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v14 | ~v1 | ~v15)))))))) ). inputformula(mod50,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v11 | v14 | ~v15)))))))) ). inputformula(mod51,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v14 | v19 | ~v1)))))))) ). inputformula(mod52,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v16 | v19 | ~v2)))))))) ). inputformula(mod53,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v16 | ~v9 | ~v12)))))))) ). inputformula(mod54,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | ~v5 | ~v9 | ~v11)))))))) ). inputformula(mod55,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v18 | ~v7 | ~v14 | ~v19)))))))) ). inputformula(mod56,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v1 | ~v7 | ~v14)))))))) ). inputformula(mod57,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | ~v8 | ~v14 | ~v17)))))))) ). inputformula(mod58,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v9 | ~v14 | ~v15 | ~v20)))))))) ). inputformula(mod59,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v13 | v15 | ~v20))))))))) ). inputformula(mod60,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v5 | v13 | ~v19))))))))) ). inputformula(mod61,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v14 | ~v11 | ~v13))))))))) ). inputformula(mod62,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | v11 | v13 | ~v20))))))))) ). inputformula(mod63,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v18 | ~v11 | ~v13))))))))) ). inputformula(mod64,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v11 | v15 | ~v13))))))))) ). inputformula(mod65,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v14 | v19 | ~v1))))))))) ). inputformula(mod66,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v15 | v20 | ~v12))))))))) ). inputformula(mod67,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v2 | ~v13 | ~v16 | ~v20))))))))) ). inputformula(mod68,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v8 | v12 | ~v5)))))))))) ). inputformula(mod69,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | v6 | v12 | ~v19)))))))))) ). inputformula(mod70,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | ~v11 | ~v12 | ~v16)))))))))) ). inputformula(mod71,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v12 | v16 | ~v2)))))))))) ). inputformula(mod72,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v15 | ~v5 | ~v12)))))))))) ). inputformula(mod73,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v15 | v20 | ~v12)))))))))) ). inputformula(mod74,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v16 | ~v9 | ~v12)))))))))) ). inputformula(mod75,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v11 | ~v5 | ~v8))))))))))) ). inputformula(mod76,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v14 | ~v11 | ~v13))))))))))) ). inputformula(mod77,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | v9 | ~v11 | ~v15))))))))))) ). inputformula(mod78,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | v11 | v13 | ~v20))))))))))) ). inputformula(mod79,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | ~v11 | ~v12 | ~v16))))))))))) ). inputformula(mod80,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v18 | ~v11 | ~v13))))))))))) ). inputformula(mod81,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v11 | v15 | ~v13))))))))))) ). inputformula(mod82,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v11 | v14 | ~v15))))))))))) ). inputformula(mod83,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v11 | v15 | ~v5 | ~v20))))))))))) ). inputformula(mod84,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | ~v5 | ~v9 | ~v11))))))))))) ). inputformula(mod85,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v20 | ~v8 | ~v11))))))))))) ). inputformula(mod86,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | ~v1 | ~v8 | ~v11))))))))))) ). inputformula(mod87,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v8 | ~v1 | ~v6 | ~v10)))))))))))) ). inputformula(mod88,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v11 | v14 | ~v15)))))))))))) ). inputformula(mod89,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v10 | v15 | ~v5 | ~v12)))))))))))) ). inputformula(mod90,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 : (v1 | v5 | v15 | ~v9))))))))))))) ). inputformula(mod91,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 : (v4 | v6 | v7 | v9))))))))))))) ). inputformula(mod92,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 : (v6 | v9 | ~v11 | ~v15))))))))))))) ). inputformula(mod93,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 : (v9 | v11 | v15 | ~v13))))))))))))) ). inputformula(mod94,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 : (v9 | v14 | ~v1 | ~v15))))))))))))) ). inputformula(mod95,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 : (v9 | v16 | ~v5 | ~v19))))))))))))) ). inputformula(mod96,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 : (v14 | v16 | ~v9 | ~v12))))))))))))) ). inputformula(mod97,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 : (v14 | ~v5 | ~v9 | ~v11))))))))))))) ). inputformula(mod98,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 : (~v9 | ~v14 | ~v15 | ~v20))))))))))))) ). inputformula(mod99,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 : (v2 | v8 | v12 | ~v5)))))))))))))) ). inputformula(mod100,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 : (v2 | ~v8 | ~v15 | ~v19)))))))))))))) ). inputformula(mod101,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 : (v4 | v11 | ~v5 | ~v8)))))))))))))) ). inputformula(mod102,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 : (v8 | v14 | v17 | ~v3)))))))))))))) ). inputformula(mod103,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 : (v8 | ~v1 | ~v6 | ~v10)))))))))))))) ). inputformula(mod104,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 | v20 | ~v8 | ~v11)))))))))))))) ). inputformula(mod105,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 | ~v1 | ~v8 | ~v11)))))))))))))) ). inputformula(mod106,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 : (~v3 | ~v8 | ~v14 | ~v17)))))))))))))) ). inputformula(mod107,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 : (v4 | v6 | v7 | v9))))))))))))))) ). inputformula(mod108,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 : (v4 | v7 | v16 | v20))))))))))))))) ). inputformula(mod109,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 : (v7 | v12 | v16 | ~v2))))))))))))))) ). inputformula(mod110,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 : (v7 | v18 | ~v11 | ~v13))))))))))))))) ). inputformula(mod111,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 : (v17 | ~v6 | ~v7 | ~v18))))))))))))))) ). inputformula(mod112,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 : (v18 | ~v7 | ~v14 | ~v19))))))))))))))) ). inputformula(mod113,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 : (v19 | ~v1 | ~v7 | ~v14))))))))))))))) ). inputformula(mod114,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 : (v19 | ~v2 | ~v6 | ~v7))))))))))))))) ). inputformula(mod115,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 : (v4 | v6 | v7 | v9)))))))))))))))) ). inputformula(mod116,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 : (v4 | v6 | ~v3 | ~v14)))))))))))))))) ). inputformula(mod117,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 : (v4 | ~v5 | ~v6 | ~v19)))))))))))))))) ). inputformula(mod118,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 : (v5 | v6 | v12 | ~v19)))))))))))))))) ). inputformula(mod119,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 : (v6 | v9 | ~v11 | ~v15)))))))))))))))) ). inputformula(mod120,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 : (v6 | v11 | v13 | ~v20)))))))))))))))) ). inputformula(mod121,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 : (v6 | ~v11 | ~v12 | ~v16)))))))))))))))) ). inputformula(mod122,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 : (v8 | ~v1 | ~v6 | ~v10)))))))))))))))) ). inputformula(mod123,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 : (v17 | ~v6 | ~v7 | ~v18)))))))))))))))) ). inputformula(mod124,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 : (v19 | ~v2 | ~v6 | ~v7)))))))))))))))) ). inputformula(mod125,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 : (v1 | v5 | v15 | ~v9))))))))))))))))) ). inputformula(mod126,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 : (v2 | v8 | v12 | ~v5))))))))))))))))) ). inputformula(mod127,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 : (v3 | v5 | v13 | ~v19))))))))))))))))) ). inputformula(mod128,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 : (v4 | v11 | ~v5 | ~v8))))))))))))))))) ). inputformula(mod129,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 : (v4 | v14 | ~v2 | ~v5))))))))))))))))) ). inputformula(mod130,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 : (v4 | ~v5 | ~v6 | ~v19))))))))))))))))) ). inputformula(mod131,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 : (v5 | v6 | v12 | ~v19))))))))))))))))) ). inputformula(mod132,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 | v16 | ~v5 | ~v19))))))))))))))))) ). inputformula(mod133,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 : (v10 | v15 | ~v5 | ~v12))))))))))))))))) ). inputformula(mod134,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 : (v11 | v15 | ~v5 | ~v20))))))))))))))))) ). inputformula(mod135,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 : (v14 | ~v5 | ~v9 | ~v11))))))))))))))))) ). inputformula(mod136,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 : (v4 | v6 | v7 | v9)))))))))))))))))) ). inputformula(mod137,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 : (v4 | v6 | ~v3 | ~v14)))))))))))))))))) ). inputformula(mod138,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 : (v4 | v7 | v16 | v20)))))))))))))))))) ). inputformula(mod139,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 : (v4 | v11 | ~v5 | ~v8)))))))))))))))))) ). inputformula(mod140,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 : (v4 | v14 | ~v2 | ~v5)))))))))))))))))) ). inputformula(mod141,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 : (v4 | v14 | ~v11 | ~v13)))))))))))))))))) ). inputformula(mod142,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 : (v4 | ~v5 | ~v6 | ~v19)))))))))))))))))) ). inputformula(mod143,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 : (v3 | v5 | v13 | ~v19))))))))))))))))))) ). inputformula(mod144,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 : (v4 | v6 | ~v3 | ~v14))))))))))))))))))) ). inputformula(mod145,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 : (v8 | v14 | v17 | ~v3))))))))))))))))))) ). inputformula(mod146,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 : (~v3 | ~v8 | ~v14 | ~v17))))))))))))))))))) ). inputformula(mod147,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 : (v2 | v8 | v12 | ~v5)))))))))))))))))))) ). inputformula(mod148,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 : (v2 | ~v8 | ~v15 | ~v19)))))))))))))))))))) ). inputformula(mod149,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 : (v4 | v14 | ~v2 | ~v5)))))))))))))))))))) ). inputformula(mod150,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 : (v7 | v12 | v16 | ~v2)))))))))))))))))))) ). inputformula(mod151,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 : (v14 | v16 | v19 | ~v2)))))))))))))))))))) ). inputformula(mod152,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 : (v19 | ~v2 | ~v6 | ~v7)))))))))))))))))))) ). inputformula(mod153,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 : (~v2 | ~v13 | ~v16 | ~v20)))))))))))))))))))) ). inputformula(mod154,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 : (v1 | v5 | v15 | ~v9))))))))))))))))))))) ). inputformula(mod155,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 : (v1 | v13 | v15 | ~v20))))))))))))))))))))) ). inputformula(mod156,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 : (v8 | ~v1 | ~v6 | ~v10))))))))))))))))))))) ). inputformula(mod157,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 | v14 | ~v1 | ~v15))))))))))))))))))))) ). inputformula(mod158,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 : (v13 | v14 | v19 | ~v1))))))))))))))))))))) ). inputformula(mod159,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 : (v16 | ~v1 | ~v8 | ~v11))))))))))))))))))))) ). inputformula(mod160,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 : (v19 | ~v1 | ~v7 | ~v14))))))))))))))))))))) ). 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(alt2,hypothesis, (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 & (box r1 : (v20 & (box r1 : v20))))))))))))))))))))))))))))))))))))))) ). inputformula(alt3,hypothesis, (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 & (box r1 : (~v20 & (box r1 : ~v20))))))))))))))))))))))))))))))))))))))) ). inputformula(alt4,hypothesis, (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 & (box r1 : (v19 & (box r1 : v19)))))))))))))))))))))))))))))))))))))) ). inputformula(alt5,hypothesis, (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 & (box r1 : (~v19 & (box r1 : ~v19)))))))))))))))))))))))))))))))))))))) ). inputformula(alt6,hypothesis, (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 & (box r1 : (v18 & (box r1 : v18))))))))))))))))))))))))))))))))))))) ). inputformula(alt7,hypothesis, (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 & (box r1 : (~v18 & (box r1 : ~v18))))))))))))))))))))))))))))))))))))) ). inputformula(alt8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v17 => (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : (v17 & (box r1 : v17)))))))))))))))))))))))))))))))))))) ). inputformula(alt9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v17 => (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : (~v17 & (box r1 : ~v17)))))))))))))))))))))))))))))))))))) ). inputformula(alt10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 => (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : (v16 & (box r1 : v16))))))))))))))))))))))))))))))))))) ). inputformula(alt11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v16 => (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : (~v16 & (box r1 : ~v16))))))))))))))))))))))))))))))))))) ). inputformula(alt12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v15 => (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : (v15 & (box r1 : v15)))))))))))))))))))))))))))))))))) ). inputformula(alt13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v15 => (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : (~v15 & (box r1 : ~v15)))))))))))))))))))))))))))))))))) ). inputformula(alt14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 => (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : (v14 & (box r1 : v14))))))))))))))))))))))))))))))))) ). inputformula(alt15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v14 => (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : (~v14 & (box r1 : ~v14))))))))))))))))))))))))))))))))) ). inputformula(alt16,hypothesis, (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 & (box r1 : (v13 & (box r1 : v13)))))))))))))))))))))))))))))))) ). inputformula(alt17,hypothesis, (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 & (box r1 : (~v13 & (box r1 : ~v13)))))))))))))))))))))))))))))))) ). inputformula(alt18,hypothesis, (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 & (box r1 : (v12 & (box r1 : v12))))))))))))))))))))))))))))))) ). inputformula(alt19,hypothesis, (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 & (box r1 : (~v12 & (box r1 : ~v12))))))))))))))))))))))))))))))) ). inputformula(alt20,hypothesis, (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 & (box r1 : (v11 & (box r1 : v11)))))))))))))))))))))))))))))) ). inputformula(alt21,hypothesis, (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 & (box r1 : (~v11 & (box r1 : ~v11)))))))))))))))))))))))))))))) ). 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 : (v10 => (box r1 : (v10 & (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(alt23,hypothesis, (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 & (box r1 : (~v10 & (box r1 : ~v10))))))))))))))))))))))))))))) ). 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 : (v9 => (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : (v9 & (box r1 : v9)))))))))))))))))))))))))))) ). 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 : (~v9 => (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : (~v9 & (box r1 : ~v9)))))))))))))))))))))))))))) ). 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 : (v8 => (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : v8))))))))))))))))))))))))))) ). 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 : (~v8 => (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : ~v8))))))))))))))))))))))))))) ). 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 : (v7 => (box r1 : (v7 & (box r1 : (v7 & (box r1 : (v7 & (box r1 : (v7 & (box r1 : (v7 & (box r1 : v7)))))))))))))))))))))))))) ). 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 : (~v7 => (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : (~v7 & (box r1 : ~v7)))))))))))))))))))))))))) ). 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 : (v6 => (box r1 : (v6 & (box r1 : (v6 & (box r1 : (v6 & (box r1 : (v6 & (box r1 : v6))))))))))))))))))))))))) ). 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 : (~v6 => (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : ~v6))))))))))))))))))))))))) ). 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 : (v5 => (box r1 : (v5 & (box r1 : (v5 & (box r1 : (v5 & (box r1 : v5)))))))))))))))))))))))) ). 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 : (~v5 => (box r1 : (~v5 & (box r1 : (~v5 & (box r1 : (~v5 & (box r1 : ~v5)))))))))))))))))))))))) ). 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 : (v4 => (box r1 : (v4 & (box r1 : (v4 & (box r1 : v4))))))))))))))))))))))) ). 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 : (~v4 => (box r1 : (~v4 & (box r1 : (~v4 & (box r1 : ~v4))))))))))))))))))))))) ). 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 : (v3 => (box r1 : (v3 & (box r1 : v3)))))))))))))))))))))) ). 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 : (~v3 => (box r1 : (~v3 & (box r1 : ~v3)))))))))))))))))))))) ). 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 : (v2 => (box r1 : v2))))))))))))))))))))) ). 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 : (~v2 => (box r1 : ~v2))))))))))))))))))))) ). inputformula(result1,conjecture, false ).