% Unbounded Modal Sat from QBF - Randomly Generated % -clauses 10 -vars 16 -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 : (v16 | v60 | ~v58 | ~v80)) ). inputformula(mod2,hypothesis, (box r1 : (v80 | ~v15 | ~v28 | ~v53)) ). inputformula(mod3,hypothesis, (box r1 : (box r1 : (box r1 : (v28 | v40 | ~v50 | ~v78)))) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v15 | v17 | v53 | v75))))))) ). inputformula(mod5,hypothesis, (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 | v27 | ~v17 | ~v69))))))))))))) ). inputformula(mod6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v20 | ~v35 | ~v61))))))))))))))))))))) ). inputformula(mod7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v60 | ~v58 | ~v80)))))))))))))))))))))) ). inputformula(mod8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | ~v3 | ~v5 | ~v60)))))))))))))))))))))) ). inputformula(mod9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v16 | v32 | v58)))))))))))))))))))))))) ). inputformula(mod10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v60 | ~v58 | ~v80)))))))))))))))))))))))) ). inputformula(mod11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v17 | v53 | v75))))))))))))))))))))))))))))) ). inputformula(mod12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v80 | ~v15 | ~v28 | ~v53))))))))))))))))))))))))))))) ). inputformula(mod13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 | ~v7 | ~v13 | ~v19))))))))))))))))))))))))))))))) ). inputformula(mod14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v40 | ~v50 | ~v78)))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v40 | ~v50 | ~v78)))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v24 | ~v13 | ~v39))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v20 | ~v35 | ~v61))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v16 | v32 | v58)))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v40 | ~v50 | ~v78)))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v80 | ~v15 | ~v28 | ~v53)))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v27 | ~v17 | ~v69))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | ~v3 | ~v5 | ~v60)))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v24 | ~v13 | ~v39)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v24 | ~v13 | ~v39)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v20 | ~v35 | ~v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 | ~v7 | ~v13 | ~v19))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v27 | ~v17 | ~v69))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v17 | v53 | v75))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v16 | v32 | v58)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v60 | ~v58 | ~v80)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v16 | v32 | v58))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v17 | v53 | v75))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v80 | ~v15 | ~v28 | ~v53))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v20 | ~v35 | ~v61))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v24 | ~v13 | ~v39))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 | ~v7 | ~v13 | ~v19))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | v27 | ~v17 | ~v69))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 | ~v7 | ~v13 | ~v19))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | ~v3 | ~v5 | ~v60))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 | ~v3 | ~v5 | ~v60))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((box r1 : ((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 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v17) & (pos r1 : ~v17))) & (pos r1 : true))) & (pos r1 : v19) & (pos r1 : ~v19))) & (pos r1 : v20) & (pos r1 : ~v20))) & (pos r1 : true))) & (pos r1 : v22) & (pos r1 : ~v22))) & (pos r1 : true))) & (pos r1 : v24) & (pos r1 : ~v24))) & (pos r1 : true))) & (pos r1 : v26) & (pos r1 : ~v26))) & (pos r1 : v27) & (pos r1 : ~v27))) & (pos r1 : v28) & (pos r1 : ~v28))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (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))) & (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 : true))) & (pos r1 : v50) & (pos r1 : ~v50))) & (pos r1 : v51) & (pos r1 : ~v51))) & (pos r1 : true))) & (pos r1 : v53) & (pos r1 : ~v53))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v58) & (pos r1 : ~v58))) & (pos r1 : true))) & (pos r1 : v60) & (pos r1 : ~v60))) & (pos r1 : v61) & (pos r1 : ~v61))) & (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 : true))) & (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 : true))) & (pos r1 : true)) ). inputformula(alt2,hypothesis, (box r1 : (v80 => (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : (v80 & (box r1 : v80))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt3,hypothesis, (box r1 : (~v80 => (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : (~v80 & (box r1 : ~v80))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt4,hypothesis, (box r1 : (box r1 : (box r1 : (v78 => (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : (v78 & (box r1 : v78))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt5,hypothesis, (box r1 : (box r1 : (box r1 : (~v78 => (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : (~v78 & (box r1 : ~v78))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v75 => (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : (v75 & (box r1 : v75)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v75 => (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : (~v75 & (box r1 : ~v75)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt8,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v69 => (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : (v69 & (box r1 : v69)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt9,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v69 => (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : (~v69 & (box r1 : ~v69)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt10,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v61 => (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : (v61 & (box r1 : v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt11,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v61 => (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : (~v61 & (box r1 : ~v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt12,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v60 => (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : (v60 & (box r1 : v60))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt13,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v60 => (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : (~v60 & (box r1 : ~v60))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt14,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v58 => (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : (v58 & (box r1 : v58))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt15,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v58 => (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : (~v58 & (box r1 : ~v58))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v53 => (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : (v53 & (box r1 : v53)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v53 => (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : (~v53 & (box r1 : ~v53)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v51 => (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : (v51 & (box r1 : v51)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v51 => (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : (~v51 & (box r1 : ~v51)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v50 => (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : (v50 & (box r1 : v50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v50 => (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : (~v50 & (box r1 : ~v50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 => (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 => (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v35 => (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : (v35 & (box r1 : v35)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v35 => (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : (~v35 & (box r1 : ~v35)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 => (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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 => (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(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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (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)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(result1,conjecture, false ).