% 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 : (box r1 : (box r1 : (v78 | ~v8 | ~v28 | ~v52)))) ). inputformula(mod2,hypothesis, (box r1 : (box r1 : (box r1 : (v78 | ~v50 | ~v52 | ~v66)))) ). inputformula(mod3,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v59 | v64 | v75 | ~v37))))))) ). inputformula(mod4,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v12 | v50 | v51 | v74)))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v78 | ~v50 | ~v52 | ~v66)))))))))))))))) ). 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 : (v1 | v27 | v65 | ~v25))))))))))))))))) ). 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 : (v59 | v64 | v75 | ~v37)))))))))))))))))) ). 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 : (~v6 | ~v44 | ~v57 | ~v61))))))))))))))))))))) ). 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 : (v59 | v64 | v75 | ~v37))))))))))))))))))))))) ). 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 : (box r1 : (~v6 | ~v44 | ~v57 | ~v61))))))))))))))))))))))))) ). 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 : (v31 | v37 | v54 | ~v35)))))))))))))))))))))))))))) ). 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 : (box r1 : (v78 | ~v8 | ~v28 | ~v52)))))))))))))))))))))))))))))) ). 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 : (v78 | ~v50 | ~v52 | ~v66)))))))))))))))))))))))))))))) ). 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 : (v12 | v50 | v51 | v74))))))))))))))))))))))))))))))) ). 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 : (v12 | v50 | v51 | v74)))))))))))))))))))))))))))))))) ). 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 : (v78 | ~v50 | ~v52 | ~v66)))))))))))))))))))))))))))))))) ). 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 : (v3 | ~v28 | ~v43 | ~v49))))))))))))))))))))))))))))))))) ). 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 : (v10 | v49 | ~v31 | ~v40))))))))))))))))))))))))))))))))) ). 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 : (~v6 | ~v44 | ~v57 | ~v61)))))))))))))))))))))))))))))))))))))) ). 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 : (v3 | ~v28 | ~v43 | ~v49))))))))))))))))))))))))))))))))))))))) ). 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 : (v10 | v49 | ~v31 | ~v40)))))))))))))))))))))))))))))))))))))))))) ). 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 : (v31 | v37 | v54 | ~v35))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v59 | v64 | v75 | ~v37))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v23 | v33 | ~v29 | ~v35))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v31 | v37 | v54 | ~v35))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v23 | v33 | ~v29 | ~v35))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v10 | v49 | ~v31 | ~v40))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v31 | v37 | v54 | ~v35))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v23 | v33 | ~v29 | ~v35))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v3 | ~v28 | ~v43 | ~v49)))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v78 | ~v8 | ~v28 | ~v52)))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v1 | v27 | v65 | ~v25))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v1 | v27 | v65 | ~v25))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v23 | v33 | ~v29 | ~v35))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (v12 | v50 | v51 | v74)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v10 | v49 | ~v31 | ~v40)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v78 | ~v8 | ~v28 | ~v52)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (~v6 | ~v44 | ~v57 | ~v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v3 | ~v28 | ~v43 | ~v49))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (v1 | v27 | v65 | ~v25))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : ((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 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v23) & (pos r1 : ~v23))) & (pos r1 : true))) & (pos r1 : v25) & (pos r1 : ~v25))) & (pos r1 : true))) & (pos r1 : v27) & (pos r1 : ~v27))) & (pos r1 : v28) & (pos r1 : ~v28))) & (pos r1 : v29) & (pos r1 : ~v29))) & (pos r1 : true))) & (pos r1 : v31) & (pos r1 : ~v31))) & (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 : v49) & (pos r1 : ~v49))) & (pos r1 : v50) & (pos r1 : ~v50))) & (pos r1 : v51) & (pos r1 : ~v51))) & (pos r1 : v52) & (pos r1 : ~v52))) & (pos r1 : true))) & (pos r1 : v54) & (pos r1 : ~v54))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v57) & (pos r1 : ~v57))) & (pos r1 : true))) & (pos r1 : v59) & (pos r1 : ~v59))) & (pos r1 : true))) & (pos r1 : v61) & (pos r1 : ~v61))) & (pos r1 : true))) & (pos r1 : true))) & (pos r1 : v64) & (pos r1 : ~v64))) & (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 : (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 & (box r1 : (v78 & (box r1 : v78))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt3,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 & (box r1 : (~v78 & (box r1 : ~v78))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt4,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 & (box r1 : (v75 & (box r1 : v75)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt5,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 & (box r1 : (~v75 & (box r1 : ~v75)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt6,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v74 => (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : (v74 & (box r1 : v74))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt7,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v74 => (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : (~v74 & (box r1 : ~v74))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (v66 => (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : (v66 & (box r1 : v66))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (box r1 : (box r1 : (box r1 : (~v66 => (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : (~v66 & (box r1 : ~v66))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v65 => (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : (v65 & (box r1 : v65)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v65 => (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : (~v65 & (box r1 : ~v65)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v64 => (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : (v64 & (box r1 : v64))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v64 => (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : (~v64 & (box r1 : ~v64))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (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 & (box r1 : (v61 & (box r1 : v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~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 & (box r1 : (~v61 & (box r1 : ~v61)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v59 => (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : (v59 & (box r1 : v59)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v59 => (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : (~v59 & (box r1 : ~v59)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v57 => (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : (v57 & (box r1 : v57)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v57 => (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : (~v57 & (box r1 : ~v57)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v54 => (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : (v54 & (box r1 : v54))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v54 => (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : (~v54 & (box r1 : ~v54))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v52 => (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : (v52 & (box r1 : v52))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v52 => (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : (~v52 & (box r1 : ~v52))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (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 & (box r1 : (v51 & (box r1 : v51)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~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 & (box r1 : (~v51 & (box r1 : ~v51)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (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 & (box r1 : (v50 & (box r1 : v50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~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 & (box r1 : (~v50 & (box r1 : ~v50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v49 => (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : (v49 & (box r1 : v49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v49 => (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : (~v49 & (box r1 : ~v49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v44 => (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : (v44 & (box r1 : v44))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v44 => (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : (~v44 & (box r1 : ~v44))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v43 => (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : (v43 & (box r1 : v43)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~v43 => (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : (~v43 & (box r1 : ~v43)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v40 => (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : (v40 & (box r1 : v40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v40 => (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : (~v40 & (box r1 : ~v40))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v37 => (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : (v37 & (box r1 : v37)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v37 => (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : (~v37 & (box r1 : ~v37)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (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 & (box r1 : (v35 & (box r1 : v35)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (~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 & (box r1 : (~v35 & (box r1 : ~v35)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). 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 : (v33 => (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : (v33 & (box r1 : v33)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v33 => (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : (~v33 & (box r1 : ~v33)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v31 => (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : (v31 & (box r1 : v31)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v31 => (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : (~v31 & (box r1 : ~v31)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v29 => (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : (v29 & (box r1 : v29)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v29 => (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : (~v29 & (box r1 : ~v29)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v28 => (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : (v28 & (box r1 : v28))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v28 => (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : (~v28 & (box r1 : ~v28))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v27 => (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : (v27 & (box r1 : v27)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v27 => (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : (~v27 & (box r1 : ~v27)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v25 => (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : (v25 & (box r1 : v25)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v25 => (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : (~v25 & (box r1 : ~v25)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v23 => (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : (v23 & (box r1 : v23)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v23 => (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : (~v23 & (box r1 : ~v23)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v12 => (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : (v12 & (box r1 : v12))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v12 => (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : (~v12 & (box r1 : ~v12))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (v10 => (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : (v10 & (box r1 : v10))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(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 : (~v10 => (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : (~v10 & (box r1 : ~v10))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt58,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v8 => (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : (v8 & (box r1 : v8))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt59,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v8 => (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : (~v8 & (box r1 : ~v8))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt60,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v6 => (box r1 : (v6 & (box r1 : (v6 & (box r1 : (v6 & (box r1 : (v6 & (box r1 : v6))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt61,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v6 => (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : (~v6 & (box r1 : ~v6))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt62,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (v3 => (box r1 : (v3 & (box r1 : v3)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(alt63,hypothesis, (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (box r1 : (~v3 => (box r1 : (~v3 & (box r1 : ~v3)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). inputformula(result1,conjecture, false ).