% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 20 -vars 8 -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 : (v2 | v26 | v40 | ~v16)) ). inputformula(mod2,hypothesis, (box r1 : (v12 | v40 | ~v21 | ~v28)) ). inputformula(mod3,hypothesis, (box r1 : (v16 | v29 | v40 | ~v5)) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (v13 | v16 | v39 | ~v19))) ). inputformula(mod5,hypothesis, (box r1 : (box r1 : (v39 | ~v16 | ~v21 | ~v28))) ). inputformula(mod6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v37 | ~v27 | ~v32))))) ). inputformula(mod7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v25 | v32 | v34 | ~v5)))))))) ). inputformula(mod8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v8 | v13 | ~v26 | ~v33))))))))) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v18 | v33 | ~v10))))))))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v20 | v31 | ~v33))))))))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v1 | v37 | ~v27 | ~v32)))))))))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v20 | v32 | ~v16)))))))))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v25 | v32 | v34 | ~v5)))))))))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v14 | v20 | v31 | ~v33))))))))))) ). inputformula(mod15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v28 | v30 | ~v17)))))))))))) ). inputformula(mod16,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 : (v2 | v5 | v9 | v29))))))))))))) ). inputformula(mod17,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 | v22 | v29 | ~v14))))))))))))) ). inputformula(mod18,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 : (v16 | v29 | v40 | ~v5))))))))))))) ). inputformula(mod19,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 | ~v4 | ~v15 | ~v29))))))))))))) ). inputformula(mod20,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 | v28 | v30 | ~v17)))))))))))))) ). inputformula(mod21,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 : (v12 | v40 | ~v21 | ~v28)))))))))))))) ). inputformula(mod22,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 : (v21 | v23 | v26 | v28)))))))))))))) ). inputformula(mod23,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 : (v39 | ~v16 | ~v21 | ~v28)))))))))))))) ). inputformula(mod24,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 : (v1 | v37 | ~v27 | ~v32))))))))))))))) ). inputformula(mod25,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 : (v2 | v26 | v40 | ~v16)))))))))))))))) ). inputformula(mod26,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 | v13 | ~v26 | ~v33)))))))))))))))) ). inputformula(mod27,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 : (v21 | v23 | v26 | v28)))))))))))))))) ). inputformula(mod28,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 | v32 | v34 | ~v5))))))))))))))))) ). inputformula(mod29,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 | ~v15 | ~v17 | ~v23))))))))))))))))))) ). inputformula(mod30,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 : (v14 | v18 | v23 | ~v11))))))))))))))))))) ). inputformula(mod31,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 : (v21 | v23 | v26 | v28))))))))))))))))))) ). inputformula(mod32,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 | v22 | v29 | ~v14)))))))))))))))))))) ). inputformula(mod33,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 | ~v10 | ~v12 | ~v21))))))))))))))))))))) ). inputformula(mod34,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 : (v12 | v40 | ~v21 | ~v28))))))))))))))))))))) ). inputformula(mod35,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 : (v21 | v23 | v26 | v28))))))))))))))))))))) ). inputformula(mod36,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 : (v39 | ~v16 | ~v21 | ~v28))))))))))))))))))))) ). inputformula(mod37,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 | v20 | v32 | ~v16)))))))))))))))))))))) ). inputformula(mod38,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 : (v14 | v20 | v31 | ~v33)))))))))))))))))))))) ). inputformula(mod39,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 : (v13 | v16 | v39 | ~v19))))))))))))))))))))))) ). inputformula(mod40,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 : (v12 | v18 | v33 | ~v10)))))))))))))))))))))))) ). inputformula(mod41,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 : (v14 | v18 | v23 | ~v11)))))))))))))))))))))))) ). inputformula(mod42,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 | v28 | v30 | ~v17))))))))))))))))))))))))) ). inputformula(mod43,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 : (v11 | ~v15 | ~v17 | ~v23))))))))))))))))))))))))) ). inputformula(mod44,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 : (v2 | v26 | v40 | ~v16)))))))))))))))))))))))))) ). inputformula(mod45,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 : (v7 | v20 | v32 | ~v16)))))))))))))))))))))))))) ). inputformula(mod46,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 : (v13 | v16 | v39 | ~v19)))))))))))))))))))))))))) ). inputformula(mod47,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 : (v16 | v29 | v40 | ~v5)))))))))))))))))))))))))) ). inputformula(mod48,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 : (v39 | ~v16 | ~v21 | ~v28)))))))))))))))))))))))))) ). inputformula(mod49,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 : (v11 | ~v15 | ~v17 | ~v23))))))))))))))))))))))))))) ). inputformula(mod50,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 : (~v1 | ~v4 | ~v15 | ~v29))))))))))))))))))))))))))) ). inputformula(mod51,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 : (v4 | v22 | v29 | ~v14)))))))))))))))))))))))))))) ). inputformula(mod52,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 : (v14 | v18 | v23 | ~v11)))))))))))))))))))))))))))) ). inputformula(mod53,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 : (v14 | v20 | v31 | ~v33)))))))))))))))))))))))))))) ). inputformula(mod54,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 : (v8 | v13 | ~v26 | ~v33))))))))))))))))))))))))))))) ). inputformula(mod55,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 : (v12 | v13 | ~v3 | ~v8))))))))))))))))))))))))))))) ). inputformula(mod56,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 | v16 | v39 | ~v19))))))))))))))))))))))))))))) ). inputformula(mod57,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 : (box r1 : (v6 | ~v10 | ~v12 | ~v21)))))))))))))))))))))))))))))) ). inputformula(mod58,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 : (box r1 : (v12 | v13 | ~v3 | ~v8)))))))))))))))))))))))))))))) ). inputformula(mod59,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 : (box r1 : (v12 | v18 | v33 | ~v10)))))))))))))))))))))))))))))) ). inputformula(mod60,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 : (box r1 : (v12 | v40 | ~v21 | ~v28)))))))))))))))))))))))))))))) ). inputformula(mod61,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 : (box r1 : (box r1 : (v11 | ~v15 | ~v17 | ~v23))))))))))))))))))))))))))))))) ). inputformula(mod62,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 : (box r1 : (box r1 : (v14 | v18 | v23 | ~v11))))))))))))))))))))))))))))))) ). inputformula(mod63,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 : (box r1 : (box r1 : (box r1 : (v6 | ~v10 | ~v12 | ~v21)))))))))))))))))))))))))))))))) ). inputformula(mod64,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 : (box r1 : (box r1 : (box r1 : (v12 | v18 | v33 | ~v10)))))))))))))))))))))))))))))))) ). inputformula(mod65,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 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v5 | v9 | v29))))))))))))))))))))))))))))))))) ). inputformula(mod66,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v8 | v13 | ~v26 | ~v33)))))))))))))))))))))))))))))))))) ). inputformula(mod67,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v13 | ~v3 | ~v8)))))))))))))))))))))))))))))))))) ). inputformula(mod68,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v7 | v20 | v32 | ~v16))))))))))))))))))))))))))))))))))) ). inputformula(mod69,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 | ~v10 | ~v12 | ~v21)))))))))))))))))))))))))))))))))))) ). inputformula(mod70,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v5 | v9 | v29))))))))))))))))))))))))))))))))))))) ). inputformula(mod71,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v16 | v29 | v40 | ~v5))))))))))))))))))))))))))))))))))))) ). inputformula(mod72,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v25 | v32 | v34 | ~v5))))))))))))))))))))))))))))))))))))) ). inputformula(mod73,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v4 | v22 | v29 | ~v14)))))))))))))))))))))))))))))))))))))) ). inputformula(mod74,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v1 | ~v4 | ~v15 | ~v29)))))))))))))))))))))))))))))))))))))) ). inputformula(mod75,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 | v28 | v30 | ~v17))))))))))))))))))))))))))))))))))))))) ). inputformula(mod76,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v13 | ~v3 | ~v8))))))))))))))))))))))))))))))))))))))) ). inputformula(mod77,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v5 | v9 | v29)))))))))))))))))))))))))))))))))))))))) ). inputformula(mod78,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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v2 | v26 | v40 | ~v16)))))))))))))))))))))))))))))))))))))))) ). inputformula(mod79,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 : (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 | v37 | ~v27 | ~v32))))))))))))))))))))))))))))))))))))))))) ). inputformula(mod80,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 : (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 | ~v4 | ~v15 | ~v29))))))))))))))))))))))))))))))))))))))))) ). 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 : ((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 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v9) & (pos r1 : ~v9))) & (pos r1 : v10) & (pos r1 : ~v10))) & (pos r1 : v11) & (pos r1 : ~v11))) & (pos r1 : v12) & (pos r1 : ~v12))) & (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 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v25) & (pos r1 : ~v25))) & (pos r1 : v26) & (pos r1 : ~v26))) & (pos r1 : v27) & (pos r1 : ~v27))) & (pos r1 : v28) & (pos r1 : ~v28))) & (pos r1 : v29) & (pos r1 : ~v29))) & (pos r1 : v30) & (pos r1 : ~v30))) & (pos r1 : v31) & (pos r1 : ~v31))) & (pos r1 : v32) & (pos r1 : ~v32))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true)) ). inputformula(alt2,hypothesis, (box r1 : (v40 => (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : v40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt3,hypothesis, (box r1 : (~v40 => (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : ~v40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt4,hypothesis, (box r1 : (box r1 : (v39 => (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : (v39 & (box r1 : v39)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt5,hypothesis, (box r1 : (box r1 : (~v39 => (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : (~v39 & (box r1 : ~v39)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (v37 => (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : v37)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (~v37 => (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : ~v37)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v34 => (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : (v34 & (box r1 : v34))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v34 => (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : (~v34 & (box r1 : ~v34))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v33 => (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : v33)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v33 => (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : ~v33)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v32 => (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : (v32 & (box r1 : v32))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v32 => (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : (~v32 & (box r1 : ~v32))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v31 => (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : v31)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v31 => (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : ~v31)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt16,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v30 => (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : (v30 & (box r1 : v30))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt17,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v30 => (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : (~v30 & (box r1 : ~v30))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt18,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 : (v29 => (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : v29)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt19,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 : (~v29 => (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : ~v29)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt20,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 => (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(alt21,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 => (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(alt22,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 : (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(alt23,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 : (~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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(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 : (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(alt56,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 : (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(alt57,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 : (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(alt58,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 : (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(alt59,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 : (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(alt60,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 : (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(alt61,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 : (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(alt62,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 : (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(alt63,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 : (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(alt64,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 : (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(alt65,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 : (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(alt66,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 : (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(alt67,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 : (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(alt68,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 : (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(alt69,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 : (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(alt70,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 : (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(alt71,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 : (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 ).