% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 50 -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 : (v5 | v21 | v28 | ~v17)) ). inputformula(mod2,hypothesis, (box r1 : (v5 | v28 | ~v1 | ~v13)) ). inputformula(mod3,hypothesis, (box r1 : (v5 | ~v14 | ~v25 | ~v28)) ). inputformula(mod4,hypothesis, (box r1 : (v6 | v23 | ~v9 | ~v28)) ). inputformula(mod5,hypothesis, (box r1 : (v16 | v19 | v24 | v28)) ). inputformula(mod6,hypothesis, (box r1 : (v16 | v19 | v24 | ~v28)) ). inputformula(mod7,hypothesis, (box r1 : (v23 | ~v16 | ~v19 | ~v28)) ). inputformula(mod8,hypothesis, (box r1 : (v28 | ~v7 | ~v16 | ~v26)) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (v1 | v21 | v22 | v27))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (v3 | v8 | v22 | ~v27))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (v7 | v27 | ~v19 | ~v21))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (v19 | ~v21 | ~v24 | ~v27))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (v22 | ~v3 | ~v24 | ~v27))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (v23 | v27 | ~v4 | ~v6))) ). inputformula(mod15,hypothesis, (box r1 : (box r1 : (v24 | ~v7 | ~v25 | ~v27))) ). inputformula(mod16,hypothesis, (box r1 : (box r1 : (v27 | ~v7 | ~v12 | ~v14))) ). inputformula(mod17,hypothesis, (box r1 : (box r1 : (v27 | ~v10 | ~v21 | ~v23))) ). inputformula(mod18,hypothesis, (box r1 : (box r1 : (box r1 : (v6 | v18 | ~v16 | ~v26)))) ). inputformula(mod19,hypothesis, (box r1 : (box r1 : (box r1 : (v7 | v26 | ~v2 | ~v8)))) ). inputformula(mod20,hypothesis, (box r1 : (box r1 : (box r1 : (v11 | v13 | v24 | ~v26)))) ). inputformula(mod21,hypothesis, (box r1 : (box r1 : (box r1 : (v12 | v13 | v22 | ~v26)))) ). inputformula(mod22,hypothesis, (box r1 : (box r1 : (box r1 : (v15 | v22 | ~v3 | ~v26)))) ). inputformula(mod23,hypothesis, (box r1 : (box r1 : (box r1 : (v20 | v21 | v22 | ~v26)))) ). inputformula(mod24,hypothesis, (box r1 : (box r1 : (box r1 : (v25 | ~v13 | ~v16 | ~v26)))) ). inputformula(mod25,hypothesis, (box r1 : (box r1 : (box r1 : (v28 | ~v7 | ~v16 | ~v26)))) ). inputformula(mod26,hypothesis, (box r1 : (box r1 : (box r1 : (~v3 | ~v21 | ~v23 | ~v26)))) ). inputformula(mod27,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v8 | v13 | v25))))) ). inputformula(mod28,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v3 | ~v15 | ~v23 | ~v25))))) ). inputformula(mod29,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v8 | v25 | ~v24))))) ). inputformula(mod30,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v5 | ~v14 | ~v25 | ~v28))))) ). inputformula(mod31,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v24 | ~v22 | ~v25))))) ). inputformula(mod32,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v15 | v24 | ~v4 | ~v25))))) ). inputformula(mod33,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v24 | ~v7 | ~v25 | ~v27))))) ). inputformula(mod34,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v25 | ~v13 | ~v16 | ~v26))))) ). inputformula(mod35,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v5 | ~v14 | ~v25))))) ). inputformula(mod36,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v21 | ~v4 | ~v24)))))) ). inputformula(mod37,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v5 | v24 | ~v18)))))) ). inputformula(mod38,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v8 | v25 | ~v24)))))) ). inputformula(mod39,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v10 | v20 | ~v24)))))) ). inputformula(mod40,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v11 | v13 | v24 | ~v26)))))) ). inputformula(mod41,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v14 | v17 | ~v24)))))) ). inputformula(mod42,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v24 | ~v22 | ~v25)))))) ). inputformula(mod43,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v15 | v24 | ~v4 | ~v25)))))) ). inputformula(mod44,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | v24 | v28)))))) ). inputformula(mod45,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | v24 | ~v28)))))) ). inputformula(mod46,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v21 | ~v24 | ~v27)))))) ). inputformula(mod47,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v22 | ~v3 | ~v24 | ~v27)))))) ). inputformula(mod48,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 | ~v7 | ~v25 | ~v27)))))) ). inputformula(mod49,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 | ~v10 | ~v14 | ~v19)))))) ). inputformula(mod50,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | ~v17 | ~v22 | ~v23))))))) ). inputformula(mod51,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | ~v15 | ~v23 | ~v25))))))) ). inputformula(mod52,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | v23 | ~v9 | ~v28))))))) ). inputformula(mod53,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v23 | v27 | ~v4 | ~v6))))))) ). inputformula(mod54,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v23 | ~v1 | ~v2 | ~v5))))))) ). inputformula(mod55,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v23 | ~v16 | ~v19 | ~v28))))))) ). inputformula(mod56,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v27 | ~v10 | ~v21 | ~v23))))))) ). inputformula(mod57,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v7 | ~v12 | ~v23))))))) ). inputformula(mod58,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | ~v21 | ~v23 | ~v26))))))) ). inputformula(mod59,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v21 | v22 | v27)))))))) ). inputformula(mod60,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | ~v17 | ~v22 | ~v23)))))))) ). inputformula(mod61,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v21 | ~v22)))))))) ). inputformula(mod62,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v8 | v22 | ~v27)))))))) ). inputformula(mod63,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | ~v3 | ~v5 | ~v22)))))))) ). inputformula(mod64,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v13 | v22 | ~v26)))))))) ). inputformula(mod65,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v24 | ~v22 | ~v25)))))))) ). inputformula(mod66,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v13 | v18 | ~v1 | ~v22)))))))) ). inputformula(mod67,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v15 | v22 | ~v3 | ~v26)))))))) ). inputformula(mod68,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v20 | v21 | v22 | ~v26)))))))) ). inputformula(mod69,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v22 | ~v3 | ~v24 | ~v27)))))))) ). inputformula(mod70,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v21 | v22 | v27))))))))) ). inputformula(mod71,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v21 | ~v4 | ~v24))))))))) ). inputformula(mod72,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v3 | v21 | ~v22))))))))) ). inputformula(mod73,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v5 | v21 | v28 | ~v17))))))))) ). inputformula(mod74,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v27 | ~v19 | ~v21))))))))) ). inputformula(mod75,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v20 | ~v16 | ~v21))))))))) ). inputformula(mod76,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v21 | ~v1 | ~v12))))))))) ). inputformula(mod77,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v17 | v18 | ~v16 | ~v21))))))))) ). inputformula(mod78,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v21 | ~v24 | ~v27))))))))) ). inputformula(mod79,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v20 | v21 | v22 | ~v26))))))))) ). inputformula(mod80,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v27 | ~v10 | ~v21 | ~v23))))))))) ). inputformula(mod81,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 | ~v21 | ~v23 | ~v26))))))))) ). inputformula(mod82,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v10 | v20 | ~v24)))))))))) ). inputformula(mod83,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v9 | v20 | ~v16 | ~v21)))))))))) ). inputformula(mod84,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | ~v14 | ~v20)))))))))) ). inputformula(mod85,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v20 | v21 | v22 | ~v26)))))))))) ). inputformula(mod86,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v27 | ~v19 | ~v21))))))))))) ). inputformula(mod87,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | v24 | v28))))))))))) ). inputformula(mod88,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | v24 | ~v28))))))))))) ). inputformula(mod89,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v19 | ~v14 | ~v20))))))))))) ). inputformula(mod90,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v19 | ~v21 | ~v24 | ~v27))))))))))) ). inputformula(mod91,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v23 | ~v16 | ~v19 | ~v28))))))))))) ). inputformula(mod92,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v24 | ~v10 | ~v14 | ~v19))))))))))) ). 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 : (v2 | v7 | v18 | ~v8)))))))))))) ). 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 : (v4 | v5 | v24 | ~v18)))))))))))) ). 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 : (v6 | v18 | ~v16 | ~v26)))))))))))) ). 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 : (v13 | v18 | ~v1 | ~v22)))))))))))) ). 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 : (v17 | v18 | ~v16 | ~v21)))))))))))) ). 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 : (v1 | ~v17 | ~v22 | ~v23))))))))))))) ). 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 : (v5 | v21 | v28 | ~v17))))))))))))) ). 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 : (v12 | v14 | v17 | ~v24))))))))))))) ). 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 : (v17 | v18 | ~v16 | ~v21))))))))))))) ). 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 : (v6 | v18 | ~v16 | ~v26)))))))))))))) ). 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 : (v9 | v20 | ~v16 | ~v21)))))))))))))) ). 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 | v19 | v24 | v28)))))))))))))) ). 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 | v19 | v24 | ~v28)))))))))))))) ). 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 : (v16 | v19 | ~v14 | ~v20)))))))))))))) ). 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 : (v16 | v21 | ~v1 | ~v12)))))))))))))) ). 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 : (v17 | v18 | ~v16 | ~v21)))))))))))))) ). 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 : (v23 | ~v16 | ~v19 | ~v28)))))))))))))) ). 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 : (v25 | ~v13 | ~v16 | ~v26)))))))))))))) ). 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 : (v28 | ~v7 | ~v16 | ~v26)))))))))))))) ). 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 : (v3 | ~v15 | ~v23 | ~v25))))))))))))))) ). 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 : (v15 | v22 | ~v3 | ~v26))))))))))))))) ). 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 : (v15 | v24 | ~v4 | ~v25))))))))))))))) ). 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 : (v5 | ~v14 | ~v25 | ~v28)))))))))))))))) ). 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 : (v7 | ~v10 | ~v12 | ~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 : (v12 | v14 | v17 | ~v24)))))))))))))))) ). 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 : (v16 | v19 | ~v14 | ~v20)))))))))))))))) ). 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 : (v24 | ~v10 | ~v14 | ~v19)))))))))))))))) ). 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 : (v27 | ~v7 | ~v12 | ~v14)))))))))))))))) ). 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 : (~v1 | ~v5 | ~v14 | ~v25)))))))))))))))) ). 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 : (box r1 : (v2 | v8 | v13 | v25))))))))))))))))) ). 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 : (box r1 : (v2 | ~v8 | ~v10 | ~v13))))))))))))))))) ). 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 : (box r1 : (v5 | v28 | ~v1 | ~v13))))))))))))))))) ). 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 : (v11 | v13 | v24 | ~v26))))))))))))))))) ). 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 : (v12 | v13 | v22 | ~v26))))))))))))))))) ). 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 : (v13 | v18 | ~v1 | ~v22))))))))))))))))) ). 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 : (v25 | ~v13 | ~v16 | ~v26))))))))))))))))) ). 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 : (box r1 : (v7 | ~v10 | ~v12 | ~v14)))))))))))))))))) ). 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 : (box r1 : (v12 | v13 | v22 | ~v26)))))))))))))))))) ). 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 : (box r1 : (v12 | v14 | v17 | ~v24)))))))))))))))))) ). 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 : (box r1 : (v12 | v24 | ~v22 | ~v25)))))))))))))))))) ). 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 : (box r1 : (v16 | v21 | ~v1 | ~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 : (box r1 : (v27 | ~v7 | ~v12 | ~v14)))))))))))))))))) ). 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 : (box r1 : (~v1 | ~v7 | ~v12 | ~v23)))))))))))))))))) ). 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 : (box r1 : (v11 | v13 | v24 | ~v26))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v2 | ~v8 | ~v10 | ~v13)))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | v10 | v20 | ~v24)))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | ~v10 | ~v12 | ~v14)))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v24 | ~v10 | ~v14 | ~v19)))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v27 | ~v10 | ~v21 | ~v23)))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v6 | v23 | ~v9 | ~v28))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v9 | v20 | ~v16 | ~v21))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v9 | ~v3 | ~v5 | ~v22))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v2 | v7 | v18 | ~v8)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v2 | v8 | v13 | v25)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v2 | ~v8 | ~v10 | ~v13)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v3 | v8 | v22 | ~v27)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v4 | v8 | v25 | ~v24)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | v26 | ~v2 | ~v8)))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v2 | v7 | v18 | ~v8))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v3 | v7 | ~v1 | ~v5))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v7 | v10 | v20 | ~v24))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | v26 | ~v2 | ~v8))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | v27 | ~v19 | ~v21))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v7 | ~v10 | ~v12 | ~v14))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v24 | ~v7 | ~v25 | ~v27))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v27 | ~v7 | ~v12 | ~v14))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v28 | ~v7 | ~v16 | ~v26))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (~v1 | ~v7 | ~v12 | ~v23))))))))))))))))))))))) ). inputformula(mod161,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 | v18 | ~v16 | ~v26)))))))))))))))))))))))) ). inputformula(mod162,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 | v23 | ~v9 | ~v28)))))))))))))))))))))))) ). inputformula(mod163,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 : (v23 | v27 | ~v4 | ~v6)))))))))))))))))))))))) ). inputformula(mod164,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 : (v3 | v7 | ~v1 | ~v5))))))))))))))))))))))))) ). inputformula(mod165,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 : (v4 | v5 | v24 | ~v18))))))))))))))))))))))))) ). inputformula(mod166,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 | v21 | v28 | ~v17))))))))))))))))))))))))) ). inputformula(mod167,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 | v28 | ~v1 | ~v13))))))))))))))))))))))))) ). inputformula(mod168,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 | ~v14 | ~v25 | ~v28))))))))))))))))))))))))) ). inputformula(mod169,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 : (v9 | ~v3 | ~v5 | ~v22))))))))))))))))))))))))) ). inputformula(mod170,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 : (v23 | ~v1 | ~v2 | ~v5))))))))))))))))))))))))) ). inputformula(mod171,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 : (~v1 | ~v5 | ~v14 | ~v25))))))))))))))))))))))))) ). inputformula(mod172,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 : (v1 | v21 | ~v4 | ~v24)))))))))))))))))))))))))) ). inputformula(mod173,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 : (v4 | v5 | v24 | ~v18)))))))))))))))))))))))))) ). inputformula(mod174,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 : (v4 | v8 | v25 | ~v24)))))))))))))))))))))))))) ). inputformula(mod175,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 : (v15 | v24 | ~v4 | ~v25)))))))))))))))))))))))))) ). inputformula(mod176,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 : (v23 | v27 | ~v4 | ~v6)))))))))))))))))))))))))) ). inputformula(mod177,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 : (v2 | v3 | v21 | ~v22))))))))))))))))))))))))))) ). inputformula(mod178,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 | v7 | ~v1 | ~v5))))))))))))))))))))))))))) ). inputformula(mod179,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 | v8 | v22 | ~v27))))))))))))))))))))))))))) ). inputformula(mod180,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 | ~v15 | ~v23 | ~v25))))))))))))))))))))))))))) ). inputformula(mod181,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 : (v9 | ~v3 | ~v5 | ~v22))))))))))))))))))))))))))) ). inputformula(mod182,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 : (v15 | v22 | ~v3 | ~v26))))))))))))))))))))))))))) ). inputformula(mod183,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 : (v22 | ~v3 | ~v24 | ~v27))))))))))))))))))))))))))) ). inputformula(mod184,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 | ~v21 | ~v23 | ~v26))))))))))))))))))))))))))) ). inputformula(mod185,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 : (box r1 : (v2 | v3 | v21 | ~v22)))))))))))))))))))))))))))) ). inputformula(mod186,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 : (box r1 : (v2 | v7 | v18 | ~v8)))))))))))))))))))))))))))) ). inputformula(mod187,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 : (box r1 : (v2 | v8 | v13 | v25)))))))))))))))))))))))))))) ). inputformula(mod188,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 : (box r1 : (v2 | ~v8 | ~v10 | ~v13)))))))))))))))))))))))))))) ). inputformula(mod189,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 : (box r1 : (v7 | v26 | ~v2 | ~v8)))))))))))))))))))))))))))) ). inputformula(mod190,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 : (box r1 : (v23 | ~v1 | ~v2 | ~v5)))))))))))))))))))))))))))) ). inputformula(mod191,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 : (box r1 : (box r1 : (v1 | v21 | v22 | v27))))))))))))))))))))))))))))) ). inputformula(mod192,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 : (box r1 : (box r1 : (v1 | v21 | ~v4 | ~v24))))))))))))))))))))))))))))) ). inputformula(mod193,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 : (box r1 : (box r1 : (v1 | ~v17 | ~v22 | ~v23))))))))))))))))))))))))))))) ). inputformula(mod194,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 : (box r1 : (box r1 : (v3 | v7 | ~v1 | ~v5))))))))))))))))))))))))))))) ). inputformula(mod195,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 : (box r1 : (box r1 : (v5 | v28 | ~v1 | ~v13))))))))))))))))))))))))))))) ). inputformula(mod196,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 : (box r1 : (box r1 : (v13 | v18 | ~v1 | ~v22))))))))))))))))))))))))))))) ). inputformula(mod197,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 : (box r1 : (box r1 : (v16 | v21 | ~v1 | ~v12))))))))))))))))))))))))))))) ). inputformula(mod198,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 : (box r1 : (box r1 : (v23 | ~v1 | ~v2 | ~v5))))))))))))))))))))))))))))) ). inputformula(mod199,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 : (box r1 : (box r1 : (~v1 | ~v5 | ~v14 | ~v25))))))))))))))))))))))))))))) ). inputformula(mod200,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 : (box r1 : (box r1 : (~v1 | ~v7 | ~v12 | ~v23))))))))))))))))))))))))))))) ). 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 : ((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))) & (pos r1 : v21) & (pos r1 : ~v21))) & (pos r1 : v22) & (pos r1 : ~v22))) & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (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 & (box r1 : (~v23 & (box r1 : ~v23)))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v22 => (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : (v22 & (box r1 : v22))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v22 => (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : (~v22 & (box r1 : ~v22))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt16,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 & (box r1 : (v21 & (box r1 : v21)))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt17,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 & (box r1 : (~v21 & (box r1 : ~v21)))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt18,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 & (box r1 : (v20 & (box r1 : v20))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt19,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 & (box r1 : (~v20 & (box r1 : ~v20))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt20,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 & (box r1 : (v19 & (box r1 : v19)))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt21,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 & (box r1 : (~v19 & (box r1 : ~v19)))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (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(alt23,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 & (box r1 : (~v18 & (box r1 : ~v18))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(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 : (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(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 : (~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(alt40,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 & (box r1 : (v9 & (box r1 : v9)))))))))))))))))))))))))))))))))))) ). inputformula(alt41,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 & (box r1 : (~v9 & (box r1 : ~v9)))))))))))))))))))))))))))))))))))) ). inputformula(alt42,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 & (box r1 : (v8 & (box r1 : v8))))))))))))))))))))))))))))))))))) ). inputformula(alt43,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 & (box r1 : (~v8 & (box r1 : ~v8))))))))))))))))))))))))))))))))))) ). inputformula(alt44,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 & (box r1 : (v7 & (box r1 : v7)))))))))))))))))))))))))))))))))) ). inputformula(alt45,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 & (box r1 : (~v7 & (box r1 : ~v7)))))))))))))))))))))))))))))))))) ). inputformula(alt46,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 & (box r1 : (v6 & (box r1 : v6))))))))))))))))))))))))))))))))) ). inputformula(alt47,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 & (box r1 : (~v6 & (box r1 : ~v6))))))))))))))))))))))))))))))))) ). inputformula(alt48,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 & (box r1 : (v5 & (box r1 : v5)))))))))))))))))))))))))))))))) ). inputformula(alt49,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 & (box r1 : (~v5 & (box r1 : ~v5)))))))))))))))))))))))))))))))) ). inputformula(alt50,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 : (v4 => (box r1 : (v4 & (box r1 : (v4 & (box r1 : v4))))))))))))))))))))))))))))))) ). inputformula(alt51,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 : (~v4 => (box r1 : (~v4 & (box r1 : (~v4 & (box r1 : ~v4))))))))))))))))))))))))))))))) ). inputformula(alt52,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 => (box r1 : (v3 & (box r1 : v3)))))))))))))))))))))))))))))) ). inputformula(alt53,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 => (box r1 : (~v3 & (box r1 : ~v3)))))))))))))))))))))))))))))) ). inputformula(alt54,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 : (box r1 : (v2 => (box r1 : v2))))))))))))))))))))))))))))) ). inputformula(alt55,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 : (box r1 : (~v2 => (box r1 : ~v2))))))))))))))))))))))))))))) ). inputformula(result1,conjecture, false ).