%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP196^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n001.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:25:20 AM UTC 2026 % Result : Theorem 0.48s 0.90s % Output : Proof 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP196^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n001.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 04:19:05 EDT 2026 % 0.17/0.35 % CPUTime : % 0.40/0.62 %----Proving TH0 % 0.48/0.90 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.48/0.90 % SZS status Theorem % 0.48/0.90 % SZS output start Proof % 0.48/0.90 ( % 0.48/0.90 (declare-sort tptp.poly_real 0) % 0.48/0.90 (declare-sort tptp.list_poly_real 0) % 0.48/0.90 (declare-sort tptp.nat 0) % 0.48/0.90 (declare-sort tptp.produc1456530199y_real 0) % 0.48/0.90 (declare-sort tptp.produc1426596841y_real 0) % 0.48/0.90 (declare-sort tptp.set_list_poly_real 0) % 0.48/0.90 (declare-sort tptp.set_poly_real 0) % 0.48/0.90 (declare-sort tptp.produc796638169y_real 0) % 0.48/0.90 (declare-sort tptp.produc1060019729y_real 0) % 0.48/0.90 (declare-sort tptp.list_P693436111y_real 0) % 0.48/0.90 (declare-sort tptp.produc461822025y_real 0) % 0.48/0.90 (declare-sort tptp.set_Pr483210409y_real 0) % 0.48/0.90 (declare-sort tptp.set_Pr1405268809y_real 0) % 0.48/0.90 (declare-sort tptp.list_list_poly_real 0) % 0.48/0.90 (declare-sort tptp.list_l343759061y_real 0) % 0.48/0.90 (declare-sort tptp.list_P736648811y_real 0) % 0.48/0.90 (declare-sort tptp.list_l6097393y_real 0) % 0.48/0.90 (declare-sort tptp.list_l1245274212y_real 0) % 0.48/0.90 (declare-sort tptp.produc321349221y_real 0) % 0.48/0.90 (declare-sort tptp.option_poly_real 0) % 0.48/0.90 (declare-sort tptp.option1330723604y_real 0) % 0.48/0.90 (declare-sort tptp.option988260395y_real 0) % 0.48/0.90 (declare-sort tptp.list_P657095678y_real 0) % 0.48/0.90 (declare-sort tptp.list_nat 0) % 0.48/0.90 (declare-sort tptp.option293660815y_real 0) % 0.48/0.90 (declare-sort tptp.list_P991700890y_real 0) % 0.48/0.90 (declare-sort tptp.list_P1001591419y_real 0) % 0.48/0.90 (declare-const tptp.sturm_1683633594axioms (-> tptp.list_poly_real tptp.poly_real Bool)) % 0.48/0.90 (declare-const tptp.sturm_891428828rm_seq (-> tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.nil_poly_real tptp.list_poly_real) % 0.48/0.90 (declare-const tptp.append_poly_real (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.foldr_2117681201y_real (-> (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real) tptp.list_list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.map_po2132607150y_real (-> (-> tptp.poly_real tptp.poly_real) tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.ord_less_nat (-> tptp.nat tptp.nat Bool)) % 0.48/0.90 (declare-const tptp.lenlex_poly_real (-> tptp.set_Pr483210409y_real tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.map_ta954657966y_real (-> tptp.produc1456530199y_real tptp.produc1456530199y_real Bool)) % 0.48/0.90 (declare-const tptp.produc2087464649y_real (-> (-> tptp.poly_real tptp.poly_real) tptp.produc1426596841y_real tptp.produc1456530199y_real)) % 0.48/0.90 (declare-const tptp.listre572247515y_real (-> tptp.set_Pr483210409y_real tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.lexord_poly_real (-> tptp.set_Pr483210409y_real tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.times_times_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.48/0.90 (declare-const tptp.bNF_Gr851617109y_real (-> tptp.set_list_poly_real tptp.poly_real tptp.set_list_poly_real)) % 0.48/0.90 (declare-const tptp.lex_poly_real (-> tptp.set_Pr483210409y_real tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.produc490255505y_real (-> tptp.poly_real tptp.list_poly_real tptp.produc796638169y_real)) % 0.48/0.90 (declare-const tptp.produc1345584779y_real (-> (-> tptp.poly_real tptp.poly_real Bool) tptp.list_poly_real tptp.produc1060019729y_real)) % 0.48/0.90 (declare-const tptp.rotate_poly_real (-> tptp.nat tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.last_P21901160y_real (-> tptp.list_P693436111y_real tptp.produc461822025y_real)) % 0.48/0.90 (declare-const tptp.listrel1_poly_real (-> tptp.set_Pr483210409y_real tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.rotate1_poly_real (-> tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.rotate717473073y_real (-> tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.rotate623875384y_real (-> tptp.list_P736648811y_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.list_e2093379497y_real (-> (-> tptp.produc321349221y_real Bool) tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.null_poly_real (-> tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.null_P1782853975y_real (-> tptp.list_P693436111y_real Bool)) % 0.48/0.90 (declare-const tptp.list_e1507538962y_real (-> (-> tptp.produc461822025y_real Bool) tptp.list_P693436111y_real Bool)) % 0.48/0.90 (declare-const tptp.null_P89569907y_real (-> tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.map_fi249381555y_real (-> (-> tptp.produc461822025y_real tptp.option_poly_real) tptp.list_P693436111y_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.list_e809719936y_real (-> (-> tptp.list_poly_real Bool) tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.lexord1324236152y_real (-> (-> tptp.list_poly_real tptp.list_poly_real Bool) tptp.list_list_poly_real tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.map_fi1389003359y_real (-> (-> tptp.produc321349221y_real tptp.option1330723604y_real) tptp.list_P736648811y_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.map_fi1183202740y_real (-> (-> tptp.poly_real tptp.option_poly_real) tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.bind_P1861132770y_real (-> tptp.list_P736648811y_real (-> tptp.produc321349221y_real tptp.list_list_poly_real) tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.map_fi740944613y_real (-> (-> tptp.poly_real tptp.option988260395y_real) tptp.list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.bind_P755425362y_real (-> tptp.list_P736648811y_real (-> tptp.produc321349221y_real tptp.list_poly_real) tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.maps_P1366845948y_real (-> (-> tptp.produc461822025y_real tptp.list_poly_real) tptp.list_P693436111y_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.maps_l770007326y_real (-> (-> tptp.list_poly_real tptp.list_P736648811y_real) tptp.list_list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.cons_P1027346459y_real (-> tptp.produc321349221y_real tptp.list_P736648811y_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.maps_P116184344y_real (-> (-> tptp.produc321349221y_real tptp.list_poly_real) tptp.list_P736648811y_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.nil_Pr2056488424y_real tptp.list_P657095678y_real) % 0.48/0.90 (declare-const tptp.maps_p2108677294y_real (-> (-> tptp.poly_real tptp.list_P736648811y_real) tptp.list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.nil_li1299462869y_real tptp.list_l343759061y_real) % 0.48/0.90 (declare-const tptp.map_fi2104453077y_real (-> (-> tptp.list_poly_real tptp.option988260395y_real) tptp.list_list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.bind_p600434664y_real (-> tptp.list_poly_real (-> tptp.poly_real tptp.list_P736648811y_real) tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.splice1383748542y_real (-> tptp.list_P736648811y_real tptp.list_P736648811y_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.listre471999892y_real (-> (-> tptp.poly_real tptp.produc461822025y_real Bool) tptp.list_poly_real tptp.list_P693436111y_real Bool)) % 0.48/0.90 (declare-const tptp.maps_l502643659y_real (-> (-> tptp.list_poly_real tptp.list_list_poly_real) tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.nil_list_poly_real tptp.list_list_poly_real) % 0.48/0.90 (declare-const tptp.maps_p961674027y_real (-> (-> tptp.poly_real tptp.list_poly_real) tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.gen_length_poly_real (-> tptp.nat tptp.list_poly_real tptp.nat)) % 0.48/0.90 (declare-const tptp.rotate867081116y_real (-> tptp.list_P693436111y_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.listre1609905961y_real (-> (-> tptp.poly_real tptp.poly_real Bool) tptp.list_poly_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.bind_p1226679937y_real (-> tptp.list_poly_real (-> tptp.poly_real tptp.list_list_poly_real) tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.map_fi357666132y_real (-> (-> tptp.list_poly_real tptp.option1330723604y_real) tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.produc1000427809y_real (-> tptp.list_poly_real tptp.list_poly_real tptp.produc1426596841y_real)) % 0.48/0.90 (declare-const tptp.bind_p420216945y_real (-> tptp.list_poly_real (-> tptp.poly_real tptp.list_poly_real) tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.map_fi1988340932y_real (-> (-> tptp.list_poly_real tptp.option_poly_real) tptp.list_list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.member1782690048y_real (-> tptp.list_P736648811y_real tptp.produc321349221y_real Bool)) % 0.48/0.90 (declare-const tptp.list_e367462459y_real (-> (-> tptp.list_poly_real Bool) tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.map_fi1117002953y_real (-> (-> tptp.poly_real tptp.option293660815y_real) tptp.list_poly_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.collec329281332y_real (-> (-> tptp.produc461822025y_real Bool) tptp.set_Pr483210409y_real)) % 0.48/0.90 (declare-const tptp.bind_P120560694y_real (-> tptp.list_P693436111y_real (-> tptp.produc461822025y_real tptp.list_poly_real) tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.member_poly_real (-> tptp.list_poly_real tptp.poly_real Bool)) % 0.48/0.90 (declare-const tptp.maps_P54557608y_real (-> (-> tptp.produc321349221y_real tptp.list_list_poly_real) tptp.list_P736648811y_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.nil_Pr1492526187y_real tptp.list_P736648811y_real) % 0.48/0.90 (declare-const tptp.size_s259235672y_real (-> tptp.list_poly_real tptp.nat)) % 0.48/0.90 (declare-const tptp.bind_l146959617y_real (-> tptp.list_list_poly_real (-> tptp.list_poly_real tptp.list_poly_real) tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.listre1044472730y_real (-> (-> tptp.produc321349221y_real tptp.poly_real Bool) tptp.list_P736648811y_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.member1829603177y_real (-> tptp.list_list_poly_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.list_e1892536494y_real (-> (-> tptp.produc321349221y_real Bool) tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.maps_p1417280571y_real (-> (-> tptp.poly_real tptp.list_list_poly_real) tptp.list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.cons_P1129399039y_real (-> tptp.produc461822025y_real tptp.list_P693436111y_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.list_ex1_poly_real (-> (-> tptp.poly_real Bool) tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.accp_P948088014y_real (-> (-> tptp.produc1456530199y_real tptp.produc1456530199y_real Bool) tptp.produc1456530199y_real Bool)) % 0.48/0.90 (declare-const tptp.enumer1433313439y_real (-> tptp.nat tptp.list_list_poly_real tptp.list_P1001591419y_real)) % 0.48/0.90 (declare-const tptp.bind_l1810664209y_real (-> tptp.list_list_poly_real (-> tptp.list_poly_real tptp.list_list_poly_real) tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.listre321577258y_real (-> (-> tptp.produc321349221y_real tptp.list_poly_real Bool) tptp.list_P736648811y_real tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.subseqs_poly_real (-> tptp.list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.produc1867601537y_real (-> tptp.poly_real tptp.poly_real tptp.produc461822025y_real)) % 0.48/0.90 (declare-const tptp.bind_p988182092y_real (-> tptp.list_poly_real (-> tptp.poly_real tptp.list_P693436111y_real) tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.map_fi920577604y_real (-> (-> tptp.poly_real tptp.option1330723604y_real) tptp.list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.plus_c288199817y_real (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.bind_l429098840y_real (-> tptp.list_list_poly_real (-> tptp.list_poly_real tptp.list_P736648811y_real) tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.listre1751862142y_real (-> (-> tptp.produc461822025y_real tptp.poly_real Bool) tptp.list_P693436111y_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.maps_p86983698y_real (-> (-> tptp.poly_real tptp.list_P693436111y_real) tptp.list_poly_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.list_ex_poly_real (-> (-> tptp.poly_real Bool) tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.lexordp_eq_poly_real (-> (-> tptp.poly_real tptp.poly_real Bool) tptp.list_poly_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.member202023780y_real (-> tptp.list_P693436111y_real tptp.produc461822025y_real Bool)) % 0.48/0.90 (declare-const tptp.gen_le904455032y_real (-> tptp.nat tptp.list_P736648811y_real tptp.nat)) % 0.48/0.90 (declare-const tptp.list_e1312221069y_real (-> (-> tptp.produc461822025y_real Bool) tptp.list_P693436111y_real Bool)) % 0.48/0.90 (declare-const tptp.null_list_poly_real (-> tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.map_fi895935311y_real (-> (-> tptp.produc321349221y_real tptp.option_poly_real) tptp.list_P736648811y_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.gen_le1160603377y_real (-> tptp.nat tptp.list_list_poly_real tptp.nat)) % 0.48/0.90 (declare-const tptp.gen_le1524582876y_real (-> tptp.nat tptp.list_P693436111y_real tptp.nat)) % 0.48/0.90 (declare-const tptp.nil_Pr1207979855y_real tptp.list_P693436111y_real) % 0.48/0.90 (declare-const tptp.maps_l337560251y_real (-> (-> tptp.list_poly_real tptp.list_poly_real) tptp.list_list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.cons_poly_real (-> tptp.poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.bNF_Gr1644259033y_real (-> tptp.set_list_poly_real tptp.list_poly_real tptp.set_poly_real)) % 0.48/0.90 (declare-const tptp.splice2080530731y_real (-> tptp.list_list_poly_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.listre889482032y_real (-> (-> tptp.poly_real tptp.produc321349221y_real Bool) tptp.list_poly_real tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.splice1321784098y_real (-> tptp.list_P693436111y_real tptp.list_P693436111y_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.splice_poly_real (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.append527544425y_real (-> tptp.list_list_poly_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.nil_Pr570652676y_real tptp.list_P991700890y_real) % 0.48/0.90 (declare-const tptp.nil_Pr1161137915y_real tptp.list_P1001591419y_real) % 0.48/0.90 (declare-const tptp.map_ta316995199y_real (-> (-> tptp.list_poly_real tptp.list_poly_real) tptp.list_list_poly_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.nil_nat tptp.list_nat) % 0.48/0.90 (declare-const tptp.produc1360353227y_real (-> tptp.list_nat tptp.list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.produc1733309743y_real (-> tptp.list_poly_real tptp.list_poly_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.map_ta1919289823y_real (-> (-> tptp.poly_real tptp.poly_real) tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.lexord834705585y_real (-> (-> tptp.produc321349221y_real tptp.produc321349221y_real Bool) tptp.list_P736648811y_real tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.lexord1053351061y_real (-> (-> tptp.produc461822025y_real tptp.produc461822025y_real Bool) tptp.list_P693436111y_real tptp.list_P693436111y_real Bool)) % 0.48/0.90 (declare-const tptp.listre1793073465y_real (-> (-> tptp.poly_real tptp.list_poly_real Bool) tptp.list_poly_real tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.listre713353145y_real (-> (-> tptp.list_poly_real tptp.poly_real Bool) tptp.list_list_poly_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.listre1763068361y_real (-> (-> tptp.list_poly_real tptp.list_poly_real Bool) tptp.list_list_poly_real tptp.list_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.ord_le1233681790y_real (-> tptp.list_poly_real tptp.list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.listre1037026976y_real (-> (-> tptp.list_poly_real tptp.produc321349221y_real Bool) tptp.list_list_poly_real tptp.list_P736648811y_real Bool)) % 0.48/0.90 (declare-const tptp.produc523415045y_real (-> tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.cons_list_poly_real (-> tptp.list_poly_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.zip_nat_poly_real (-> tptp.list_nat tptp.list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.zip_po657915297y_real (-> tptp.list_poly_real tptp.list_poly_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.map_ta1513955567y_real (-> (-> tptp.poly_real tptp.list_poly_real) tptp.list_poly_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.map_ta434235247y_real (-> (-> tptp.list_poly_real tptp.poly_real) tptp.list_list_poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.map_ta632757498y_real (-> (-> tptp.poly_real tptp.produc321349221y_real) tptp.list_poly_real tptp.list_P736648811y_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.insert_poly_real (-> tptp.poly_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.map_ta787748196y_real (-> (-> tptp.produc321349221y_real tptp.poly_real) tptp.list_P736648811y_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.map_ta920933982y_real (-> (-> tptp.poly_real tptp.produc461822025y_real) tptp.list_poly_real tptp.list_P693436111y_real tptp.list_P693436111y_real)) % 0.48/0.90 (declare-const tptp.map_ta1674185578y_real (-> (-> tptp.list_poly_real tptp.produc321349221y_real) tptp.list_list_poly_real tptp.list_P736648811y_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.member1784523250y_real (-> tptp.produc461822025y_real tptp.set_Pr483210409y_real Bool)) % 0.48/0.90 (declare-const tptp.map_ta958735860y_real (-> (-> tptp.produc321349221y_real tptp.list_poly_real) tptp.list_P736648811y_real tptp.list_list_poly_real tptp.list_list_poly_real)) % 0.48/0.90 (declare-const tptp.map_ta53312584y_real (-> (-> tptp.produc461822025y_real tptp.poly_real) tptp.list_P693436111y_real tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.cons_l2022919326y_real (-> tptp.list_list_poly_real tptp.list_l1245274212y_real tptp.list_l1245274212y_real)) % 0.48/0.90 (declare-const tptp.nil_li2088348750y_real tptp.list_l1245274212y_real) % 0.48/0.90 (declare-const tptp.cons_l730969377y_real (-> tptp.list_P736648811y_real tptp.list_l6097393y_real tptp.list_l6097393y_real)) % 0.48/0.90 (declare-const tptp.nil_li579690865y_real tptp.list_l6097393y_real) % 0.48/0.90 (declare-const tptp.cons_l677353093y_real (-> tptp.list_P693436111y_real tptp.list_l343759061y_real tptp.list_l343759061y_real)) % 0.48/0.90 (declare-const tptp.collec1459394516y_real (-> (-> tptp.produc1426596841y_real Bool) tptp.set_Pr1405268809y_real)) % 0.48/0.90 (declare-const tptp.butlast_poly_real (-> tptp.list_poly_real tptp.list_poly_real)) % 0.48/0.90 (declare-const tptp.enumer1015405230y_real (-> tptp.nat tptp.list_P693436111y_real tptp.list_P657095678y_real)) % 0.48/0.90 (declare-const tptp.member403334290y_real (-> tptp.produc1426596841y_real tptp.set_Pr1405268809y_real Bool)) % 0.48/0.90 (declare-const tptp.collect_poly_real (-> (-> tptp.poly_real Bool) tptp.set_poly_real)) % 0.48/0.90 (declare-const tptp.enumer1123002698y_real (-> tptp.nat tptp.list_P736648811y_real tptp.list_P991700890y_real)) % 0.48/0.90 (declare-const tptp.member_poly_real2 (-> tptp.poly_real tptp.set_poly_real Bool)) % 0.48/0.90 (declare-const tptp.collec1537941401y_real (-> (-> tptp.list_poly_real Bool) tptp.set_list_poly_real)) % 0.48/0.90 (declare-const tptp.enumerate_poly_real (-> tptp.nat tptp.list_poly_real tptp.list_P736648811y_real)) % 0.48/0.90 (declare-const tptp.member708095579y_real (-> tptp.list_poly_real tptp.set_list_poly_real Bool)) % 0.48/0.90 (declare-const tptp.suc (-> tptp.nat tptp.nat)) % 0.48/0.90 (declare-const tptp.produc404352541y_real (-> tptp.nat tptp.poly_real tptp.produc321349221y_real)) % 0.48/0.90 (declare-const tptp.last_poly_real (-> tptp.list_poly_real tptp.poly_real)) % 0.48/0.90 (define tptp.sturm_1664866327rm_seq () (let ((_let_1 (@var "P2" tptp.poly_real))) (let ((_let_2 (@var "Ps2" tptp.list_poly_real))) (lambda (@list _let_2 _let_1) (and (_ tptp.sturm_891428828rm_seq _let_2) (_ (_ tptp.sturm_1683633594axioms _let_2) _let_1)))))) % 0.48/0.90 (define tptp.concat_poly_real () (let ((_let_1 (@var "Xss3" tptp.list_list_poly_real))) (lambda (@list _let_1) (_ (_ (_ tptp.foldr_2117681201y_real tptp.append_poly_real) _let_1) tptp.nil_poly_real)))) % 0.48/0.90 (define @t1 () (@var "Ps" tptp.list_poly_real)) % 0.48/0.90 (define @t2 () (not (= @t1 tptp.nil_poly_real))) % 0.48/0.90 (define @t3 () (_ tptp.sturm_891428828rm_seq @t1)) % 0.48/0.90 (define @t4 () (=> @t3 @t2)) % 0.48/0.90 (define @t5 () (@list @t1)) % 0.48/0.90 (define @t6 () (forall @t5 @t4)) % 0.48/0.90 (define @t7 () (@var "P" tptp.poly_real)) % 0.48/0.90 (define @t8 () (_ (_ tptp.sturm_1664866327rm_seq @t1) @t7)) % 0.48/0.90 (define @t9 () (@list @t1 @t7)) % 0.48/0.90 (define @t10 () (_ (_ tptp.sturm_1683633594axioms @t1) @t7)) % 0.48/0.90 (define @t11 () (@var "P3" (-> tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t12 () (@list @t11)) % 0.48/0.90 (define @t13 () (@var "P3" (-> tptp.list_poly_real Bool))) % 0.48/0.90 (define @t14 () (@list @t13)) % 0.48/0.90 (define @t15 () (@var "P3" (-> tptp.produc461822025y_real Bool))) % 0.48/0.90 (define @t16 () (@list @t15)) % 0.48/0.90 (define @t17 () (@var "P3" (-> tptp.poly_real Bool))) % 0.48/0.90 (define @t18 () (@list @t17)) % 0.48/0.90 (define @t19 () (@var "F" (-> tptp.poly_real tptp.list_poly_real))) % 0.48/0.90 (define @t20 () (@list @t19)) % 0.48/0.90 (define @t21 () (@var "F" (-> tptp.poly_real tptp.list_list_poly_real))) % 0.48/0.90 (define @t22 () (@list @t21)) % 0.48/0.90 (define @t23 () (@var "F" (-> tptp.list_poly_real tptp.list_poly_real))) % 0.48/0.90 (define @t24 () (@list @t23)) % 0.48/0.90 (define @t25 () (@var "F" (-> tptp.poly_real tptp.list_P736648811y_real))) % 0.48/0.90 (define @t26 () (@list @t25)) % 0.48/0.90 (define @t27 () (@var "F" (-> tptp.produc321349221y_real tptp.list_poly_real))) % 0.48/0.90 (define @t28 () (@list @t27)) % 0.48/0.90 (define @t29 () (@var "F" (-> tptp.list_poly_real tptp.list_list_poly_real))) % 0.48/0.90 (define @t30 () (@list @t29)) % 0.48/0.90 (define @t31 () (@var "F" (-> tptp.poly_real tptp.list_P693436111y_real))) % 0.48/0.90 (define @t32 () (@list @t31)) % 0.48/0.90 (define @t33 () (@var "F" (-> tptp.produc321349221y_real tptp.list_list_poly_real))) % 0.48/0.90 (define @t34 () (@list @t33)) % 0.48/0.90 (define @t35 () (@var "F" (-> tptp.list_poly_real tptp.list_P736648811y_real))) % 0.48/0.90 (define @t36 () (@list @t35)) % 0.48/0.90 (define @t37 () (@var "F" (-> tptp.produc461822025y_real tptp.list_poly_real))) % 0.48/0.90 (define @t38 () (@list @t37)) % 0.48/0.90 (define @t39 () (@var "Y" tptp.produc321349221y_real)) % 0.48/0.90 (define @t40 () (@var "Y" tptp.list_poly_real)) % 0.48/0.90 (define @t41 () (@list @t40)) % 0.48/0.90 (define @t42 () (@var "Y" tptp.produc461822025y_real)) % 0.48/0.90 (define @t43 () (@var "Y" tptp.poly_real)) % 0.48/0.90 (define @t44 () (@var "N" tptp.nat)) % 0.48/0.90 (define @t45 () (@list @t44)) % 0.48/0.90 (define @t46 () (_ tptp.gen_length_poly_real @t44)) % 0.48/0.90 (define @t47 () (_ tptp.maps_p961674027y_real @t19)) % 0.48/0.90 (define @t48 () (@var "F" (-> tptp.poly_real tptp.option_poly_real))) % 0.48/0.90 (define @t49 () (@var "F" (-> tptp.poly_real tptp.option1330723604y_real))) % 0.48/0.90 (define @t50 () (@var "F" (-> tptp.list_poly_real tptp.option_poly_real))) % 0.48/0.90 (define @t51 () (@var "F" (-> tptp.poly_real tptp.option988260395y_real))) % 0.48/0.90 (define @t52 () (@var "F" (-> tptp.produc321349221y_real tptp.option_poly_real))) % 0.48/0.90 (define @t53 () (@var "F" (-> tptp.list_poly_real tptp.option1330723604y_real))) % 0.48/0.90 (define @t54 () (@var "F" (-> tptp.poly_real tptp.option293660815y_real))) % 0.48/0.90 (define @t55 () (@var "F" (-> tptp.produc321349221y_real tptp.option1330723604y_real))) % 0.48/0.90 (define @t56 () (@var "F" (-> tptp.list_poly_real tptp.option988260395y_real))) % 0.48/0.90 (define @t57 () (@var "F" (-> tptp.produc461822025y_real tptp.option_poly_real))) % 0.48/0.90 (define @t58 () (@var "Xs" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t59 () (= @t58 tptp.nil_Pr1492526187y_real)) % 0.48/0.90 (define @t60 () (@list @t58)) % 0.48/0.90 (define @t61 () (@var "Xs" tptp.list_list_poly_real)) % 0.48/0.90 (define @t62 () (= @t61 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t63 () (@list @t61)) % 0.48/0.90 (define @t64 () (@var "Xs" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t65 () (= @t64 tptp.nil_Pr1207979855y_real)) % 0.48/0.90 (define @t66 () (@list @t64)) % 0.48/0.90 (define @t67 () (@var "Xs" tptp.list_poly_real)) % 0.48/0.90 (define @t68 () (= @t67 tptp.nil_poly_real)) % 0.48/0.90 (define @t69 () (@list @t67)) % 0.48/0.90 (define @t70 () (_ tptp.list_e2093379497y_real @t11)) % 0.48/0.90 (define @t71 () (_ tptp.list_e809719936y_real @t13)) % 0.48/0.90 (define @t72 () (_ tptp.list_e1312221069y_real @t15)) % 0.48/0.90 (define @t73 () (_ tptp.list_ex_poly_real @t17)) % 0.48/0.90 (define @t74 () (@var "Ys" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t75 () (_ tptp.splice1383748542y_real @t58)) % 0.48/0.90 (define @t76 () (@var "Ys" tptp.list_list_poly_real)) % 0.48/0.90 (define @t77 () (_ tptp.splice2080530731y_real @t61)) % 0.48/0.90 (define @t78 () (@var "Ys" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t79 () (_ tptp.splice1321784098y_real @t64)) % 0.48/0.90 (define @t80 () (@var "Ys" tptp.list_poly_real)) % 0.48/0.90 (define @t81 () (= @t80 tptp.nil_poly_real)) % 0.48/0.90 (define @t82 () (and @t68 @t81)) % 0.48/0.90 (define @t83 () (_ tptp.splice_poly_real @t67)) % 0.48/0.90 (define @t84 () (@list @t67 @t80)) % 0.48/0.90 (define @t85 () (_ tptp.enumerate_poly_real @t44)) % 0.48/0.90 (define @t86 () (@var "Uu" tptp.list_poly_real)) % 0.48/0.90 (define @t87 () (@list @t86)) % 0.48/0.90 (define @t88 () (@var "Bs" tptp.list_poly_real)) % 0.48/0.90 (define @t89 () (@var "F" (-> tptp.poly_real tptp.poly_real))) % 0.48/0.90 (define @t90 () (_ tptp.map_ta1919289823y_real @t89)) % 0.48/0.90 (define @t91 () (@var "Less" (-> tptp.produc321349221y_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t92 () (_ tptp.lexord834705585y_real @t91)) % 0.48/0.90 (define @t93 () (@var "Less" (-> tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t94 () (_ tptp.lexord1324236152y_real @t93)) % 0.48/0.90 (define @t95 () (@var "Less" (-> tptp.produc461822025y_real tptp.produc461822025y_real Bool))) % 0.48/0.90 (define @t96 () (_ tptp.lexord1053351061y_real @t95)) % 0.48/0.90 (define @t97 () (@var "Less" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t98 () (_ tptp.lexordp_eq_poly_real @t97)) % 0.48/0.90 (define @t99 () (_ @t92 @t58)) % 0.48/0.90 (define @t100 () (_ @t94 @t61)) % 0.48/0.90 (define @t101 () (_ @t96 @t64)) % 0.48/0.90 (define @t102 () (_ @t98 @t67)) % 0.48/0.90 (define @t103 () (@list @t97 @t67)) % 0.48/0.90 (define @t104 () (@var "R" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t105 () (_ tptp.listre1609905961y_real @t104)) % 0.48/0.90 (define @t106 () (@var "R" (-> tptp.poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t107 () (_ tptp.listre1793073465y_real @t106)) % 0.48/0.90 (define @t108 () (@var "R" (-> tptp.list_poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t109 () (_ tptp.listre713353145y_real @t108)) % 0.48/0.90 (define @t110 () (@var "R" (-> tptp.poly_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t111 () (_ tptp.listre889482032y_real @t110)) % 0.48/0.90 (define @t112 () (@var "R" (-> tptp.produc321349221y_real tptp.poly_real Bool))) % 0.48/0.90 (define @t113 () (_ tptp.listre1044472730y_real @t112)) % 0.48/0.90 (define @t114 () (@var "R" (-> tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t115 () (_ tptp.listre1763068361y_real @t114)) % 0.48/0.90 (define @t116 () (@var "R" (-> tptp.poly_real tptp.produc461822025y_real Bool))) % 0.48/0.90 (define @t117 () (_ tptp.listre471999892y_real @t116)) % 0.48/0.90 (define @t118 () (@var "R" (-> tptp.produc321349221y_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t119 () (_ tptp.listre321577258y_real @t118)) % 0.48/0.90 (define @t120 () (@var "R" (-> tptp.list_poly_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t121 () (_ tptp.listre1037026976y_real @t120)) % 0.48/0.90 (define @t122 () (@var "R" (-> tptp.produc461822025y_real tptp.poly_real Bool))) % 0.48/0.90 (define @t123 () (_ tptp.listre1751862142y_real @t122)) % 0.48/0.90 (define @t124 () (@list @t80)) % 0.48/0.90 (define @t125 () (@var "X" tptp.list_poly_real)) % 0.48/0.90 (define @t126 () (_ (_ tptp.cons_list_poly_real @t125) @t61)) % 0.48/0.90 (define @t127 () (_ @t94 @t126)) % 0.48/0.90 (define @t128 () (@var "X" tptp.produc321349221y_real)) % 0.48/0.90 (define @t129 () (_ (_ tptp.cons_P1027346459y_real @t128) @t58)) % 0.48/0.90 (define @t130 () (_ @t92 @t129)) % 0.48/0.90 (define @t131 () (@var "X" tptp.produc461822025y_real)) % 0.48/0.90 (define @t132 () (_ (_ tptp.cons_P1129399039y_real @t131) @t64)) % 0.48/0.90 (define @t133 () (_ @t96 @t132)) % 0.48/0.90 (define @t134 () (@var "X" tptp.poly_real)) % 0.48/0.90 (define @t135 () (_ tptp.cons_poly_real @t134)) % 0.48/0.90 (define @t136 () (_ @t135 @t67)) % 0.48/0.90 (define @t137 () (_ @t98 @t136)) % 0.48/0.90 (define @t138 () (@var "Xb" tptp.list_poly_real)) % 0.48/0.90 (define @t139 () (@var "A" tptp.poly_real)) % 0.48/0.90 (define @t140 () (@var "X" (-> tptp.poly_real tptp.poly_real))) % 0.48/0.90 (define @t141 () (@var "As" tptp.list_poly_real)) % 0.48/0.90 (define @t142 () (_ tptp.map_ta1919289823y_real @t140)) % 0.48/0.90 (define @t143 () (= @t40 (_ (_ @t142 @t141) (_ (_ tptp.cons_poly_real (_ @t140 @t139)) @t138)))) % 0.48/0.90 (define @t144 () (_ (_ tptp.cons_poly_real @t139) @t141)) % 0.48/0.90 (define @t145 () (@var "Xa" tptp.list_poly_real)) % 0.48/0.90 (define @t146 () (= @t145 @t144)) % 0.48/0.90 (define @t147 () (@list @t139 @t141)) % 0.48/0.90 (define @t148 () (= @t40 @t138)) % 0.48/0.90 (define @t149 () (not @t148)) % 0.48/0.90 (define @t150 () (= @t145 tptp.nil_poly_real)) % 0.48/0.90 (define @t151 () (= (_ (_ @t142 @t145) @t138) @t40)) % 0.48/0.90 (define @t152 () (@list @t140 @t145 @t138 @t40)) % 0.48/0.90 (define @t153 () (@var "Xb" tptp.list_list_poly_real)) % 0.48/0.90 (define @t154 () (@var "X" (-> tptp.poly_real tptp.list_poly_real))) % 0.48/0.90 (define @t155 () (_ tptp.map_ta1513955567y_real @t154)) % 0.48/0.90 (define @t156 () (@var "Y" tptp.list_list_poly_real)) % 0.48/0.90 (define @t157 () (not (= @t156 @t153))) % 0.48/0.90 (define @t158 () (@var "A" tptp.list_poly_real)) % 0.48/0.90 (define @t159 () (@var "X" (-> tptp.list_poly_real tptp.poly_real))) % 0.48/0.90 (define @t160 () (@var "As" tptp.list_list_poly_real)) % 0.48/0.90 (define @t161 () (_ tptp.map_ta434235247y_real @t159)) % 0.48/0.90 (define @t162 () (_ (_ tptp.cons_list_poly_real @t158) @t160)) % 0.48/0.90 (define @t163 () (@var "Xa" tptp.list_list_poly_real)) % 0.48/0.90 (define @t164 () (= @t163 @t162)) % 0.48/0.90 (define @t165 () (@list @t158 @t160)) % 0.48/0.90 (define @t166 () (= @t163 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t167 () (@var "Xb" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t168 () (@var "X" (-> tptp.poly_real tptp.produc321349221y_real))) % 0.48/0.90 (define @t169 () (_ tptp.map_ta632757498y_real @t168)) % 0.48/0.90 (define @t170 () (@var "Y" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t171 () (not (= @t170 @t167))) % 0.48/0.90 (define @t172 () (@var "X" (-> tptp.list_poly_real tptp.list_poly_real))) % 0.48/0.90 (define @t173 () (_ tptp.map_ta316995199y_real @t172)) % 0.48/0.90 (define @t174 () (@var "A" tptp.produc321349221y_real)) % 0.48/0.90 (define @t175 () (@var "X" (-> tptp.produc321349221y_real tptp.poly_real))) % 0.48/0.90 (define @t176 () (@var "As" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t177 () (_ tptp.map_ta787748196y_real @t175)) % 0.48/0.90 (define @t178 () (_ (_ tptp.cons_P1027346459y_real @t174) @t176)) % 0.48/0.90 (define @t179 () (@var "Xa" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t180 () (= @t179 @t178)) % 0.48/0.90 (define @t181 () (@list @t174 @t176)) % 0.48/0.90 (define @t182 () (= @t179 tptp.nil_Pr1492526187y_real)) % 0.48/0.90 (define @t183 () (@var "Xb" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t184 () (@var "X" (-> tptp.poly_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t185 () (_ tptp.map_ta920933982y_real @t184)) % 0.48/0.90 (define @t186 () (@var "Y" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t187 () (@var "X" (-> tptp.list_poly_real tptp.produc321349221y_real))) % 0.48/0.90 (define @t188 () (_ tptp.map_ta1674185578y_real @t187)) % 0.48/0.90 (define @t189 () (@var "X" (-> tptp.produc321349221y_real tptp.list_poly_real))) % 0.48/0.90 (define @t190 () (_ tptp.map_ta958735860y_real @t189)) % 0.48/0.90 (define @t191 () (@var "A" tptp.produc461822025y_real)) % 0.48/0.90 (define @t192 () (@var "X" (-> tptp.produc461822025y_real tptp.poly_real))) % 0.48/0.90 (define @t193 () (@var "As" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t194 () (_ tptp.map_ta53312584y_real @t192)) % 0.48/0.90 (define @t195 () (_ (_ tptp.cons_P1129399039y_real @t191) @t193)) % 0.48/0.90 (define @t196 () (@var "Xa" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t197 () (@var "X2" tptp.list_poly_real)) % 0.48/0.90 (define @t198 () (@var "X1" tptp.list_poly_real)) % 0.48/0.90 (define @t199 () (@var "P3" (-> tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t200 () (_ (_ @t199 @t198) @t197)) % 0.48/0.90 (define @t201 () (@var "Ys2" tptp.list_poly_real)) % 0.48/0.90 (define @t202 () (@var "Y2" tptp.poly_real)) % 0.48/0.90 (define @t203 () (_ tptp.cons_poly_real @t202)) % 0.48/0.90 (define @t204 () (_ @t203 @t201)) % 0.48/0.90 (define @t205 () (@var "Xs2" tptp.list_poly_real)) % 0.48/0.90 (define @t206 () (@var "X3" tptp.poly_real)) % 0.48/0.90 (define @t207 () (_ tptp.cons_poly_real @t206)) % 0.48/0.90 (define @t208 () (_ @t207 @t205)) % 0.48/0.90 (define @t209 () (_ @t199 @t208)) % 0.48/0.90 (define @t210 () (_ @t209 @t204)) % 0.48/0.90 (define @t211 () (_ @t199 @t205)) % 0.48/0.90 (define @t212 () (=> (_ @t211 @t201) @t210)) % 0.48/0.90 (define @t213 () (_ (_ @t105 @t205) @t201)) % 0.48/0.90 (define @t214 () (_ (_ @t104 @t206) @t202)) % 0.48/0.90 (define @t215 () (@list @t206 @t202 @t205 @t201)) % 0.48/0.90 (define @t216 () (_ @t199 tptp.nil_poly_real)) % 0.48/0.90 (define @t217 () (_ @t216 tptp.nil_poly_real)) % 0.48/0.90 (define @t218 () (@var "X2" tptp.list_list_poly_real)) % 0.48/0.90 (define @t219 () (@var "P3" (-> tptp.list_poly_real tptp.list_list_poly_real Bool))) % 0.48/0.90 (define @t220 () (@var "Ys2" tptp.list_list_poly_real)) % 0.48/0.90 (define @t221 () (@var "Y2" tptp.list_poly_real)) % 0.48/0.90 (define @t222 () (_ (_ tptp.cons_list_poly_real @t221) @t220)) % 0.48/0.90 (define @t223 () (_ (_ @t107 @t205) @t220)) % 0.48/0.90 (define @t224 () (_ (_ @t106 @t206) @t221)) % 0.48/0.90 (define @t225 () (@var "X1" tptp.list_list_poly_real)) % 0.48/0.90 (define @t226 () (@var "P3" (-> tptp.list_list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t227 () (@var "Xs2" tptp.list_list_poly_real)) % 0.48/0.90 (define @t228 () (@var "X3" tptp.list_poly_real)) % 0.48/0.90 (define @t229 () (_ tptp.cons_list_poly_real @t228)) % 0.48/0.90 (define @t230 () (_ @t229 @t227)) % 0.48/0.90 (define @t231 () (_ (_ @t109 @t227) @t201)) % 0.48/0.90 (define @t232 () (_ (_ @t108 @t228) @t202)) % 0.48/0.90 (define @t233 () (@var "X2" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t234 () (@var "P3" (-> tptp.list_poly_real tptp.list_P736648811y_real Bool))) % 0.48/0.90 (define @t235 () (@var "Ys2" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t236 () (@var "Y2" tptp.produc321349221y_real)) % 0.48/0.90 (define @t237 () (_ (_ tptp.cons_P1027346459y_real @t236) @t235)) % 0.48/0.90 (define @t238 () (_ (_ @t111 @t205) @t235)) % 0.48/0.90 (define @t239 () (_ (_ @t110 @t206) @t236)) % 0.48/0.90 (define @t240 () (@var "P3" (-> tptp.list_list_poly_real tptp.list_list_poly_real Bool))) % 0.48/0.90 (define @t241 () (_ (_ @t240 @t225) @t218)) % 0.48/0.90 (define @t242 () (_ (_ @t240 @t230) @t222)) % 0.48/0.90 (define @t243 () (=> (_ (_ @t240 @t227) @t220) @t242)) % 0.48/0.90 (define @t244 () (_ (_ @t115 @t227) @t220)) % 0.48/0.90 (define @t245 () (_ (_ @t114 @t228) @t221)) % 0.48/0.90 (define @t246 () (@list @t228 @t221 @t227 @t220)) % 0.48/0.90 (define @t247 () (_ @t240 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t248 () (@var "X1" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t249 () (@var "P3" (-> tptp.list_P736648811y_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t250 () (@var "Xs2" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t251 () (@var "X3" tptp.produc321349221y_real)) % 0.48/0.90 (define @t252 () (_ tptp.cons_P1027346459y_real @t251)) % 0.48/0.90 (define @t253 () (_ @t252 @t250)) % 0.48/0.90 (define @t254 () (_ (_ @t113 @t250) @t201)) % 0.48/0.90 (define @t255 () (_ (_ @t112 @t251) @t202)) % 0.48/0.90 (define @t256 () (@var "X2" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t257 () (@var "P3" (-> tptp.list_poly_real tptp.list_P693436111y_real Bool))) % 0.48/0.90 (define @t258 () (@var "Ys2" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t259 () (@var "Y2" tptp.produc461822025y_real)) % 0.48/0.90 (define @t260 () (_ (_ tptp.cons_P1129399039y_real @t259) @t258)) % 0.48/0.90 (define @t261 () (_ (_ @t117 @t205) @t258)) % 0.48/0.90 (define @t262 () (_ (_ @t116 @t206) @t259)) % 0.48/0.90 (define @t263 () (@var "P3" (-> tptp.list_list_poly_real tptp.list_P736648811y_real Bool))) % 0.48/0.90 (define @t264 () (_ (_ @t121 @t227) @t235)) % 0.48/0.90 (define @t265 () (_ (_ @t120 @t228) @t236)) % 0.48/0.90 (define @t266 () (@var "P3" (-> tptp.list_P736648811y_real tptp.list_list_poly_real Bool))) % 0.48/0.90 (define @t267 () (_ (_ @t119 @t250) @t220)) % 0.48/0.90 (define @t268 () (_ (_ @t118 @t251) @t221)) % 0.48/0.90 (define @t269 () (@var "X1" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t270 () (@var "P3" (-> tptp.list_P693436111y_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t271 () (@var "Xs2" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t272 () (@var "X3" tptp.produc461822025y_real)) % 0.48/0.90 (define @t273 () (_ tptp.cons_P1129399039y_real @t272)) % 0.48/0.90 (define @t274 () (_ @t273 @t271)) % 0.48/0.90 (define @t275 () (_ (_ @t123 @t271) @t201)) % 0.48/0.90 (define @t276 () (_ (_ @t122 @t272) @t202)) % 0.48/0.90 (define @t277 () (@var "Ys3" tptp.list_poly_real)) % 0.48/0.90 (define @t278 () (@var "Xs3" tptp.list_poly_real)) % 0.48/0.90 (define @t279 () (@var "R2" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t280 () (@var "Y3" tptp.poly_real)) % 0.48/0.90 (define @t281 () (@var "X4" tptp.poly_real)) % 0.48/0.90 (define @t282 () (_ (_ tptp.cons_poly_real @t280) @t277)) % 0.48/0.90 (define @t283 () (@var "A2" tptp.list_poly_real)) % 0.48/0.90 (define @t284 () (= @t283 @t282)) % 0.48/0.90 (define @t285 () (_ (_ tptp.cons_poly_real @t281) @t278)) % 0.48/0.90 (define @t286 () (@var "A1" tptp.list_poly_real)) % 0.48/0.90 (define @t287 () (= @t286 @t285)) % 0.48/0.90 (define @t288 () (@list @t281 @t280 @t278 @t277)) % 0.48/0.90 (define @t289 () (= @t283 tptp.nil_poly_real)) % 0.48/0.90 (define @t290 () (= @t286 tptp.nil_poly_real)) % 0.48/0.90 (define @t291 () (@var "Ys3" tptp.list_list_poly_real)) % 0.48/0.90 (define @t292 () (@var "R2" (-> tptp.poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t293 () (@var "Y3" tptp.list_poly_real)) % 0.48/0.90 (define @t294 () (@var "A2" tptp.list_list_poly_real)) % 0.48/0.90 (define @t295 () (= @t294 (_ (_ tptp.cons_list_poly_real @t293) @t291))) % 0.48/0.90 (define @t296 () (= @t294 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t297 () (@var "Xs3" tptp.list_list_poly_real)) % 0.48/0.90 (define @t298 () (@var "R2" (-> tptp.list_poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t299 () (@var "X4" tptp.list_poly_real)) % 0.48/0.90 (define @t300 () (@var "A1" tptp.list_list_poly_real)) % 0.48/0.90 (define @t301 () (= @t300 (_ (_ tptp.cons_list_poly_real @t299) @t297))) % 0.48/0.90 (define @t302 () (= @t300 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t303 () (@var "Ys3" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t304 () (@var "R2" (-> tptp.poly_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t305 () (@var "Y3" tptp.produc321349221y_real)) % 0.48/0.90 (define @t306 () (@var "A2" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t307 () (= @t306 (_ (_ tptp.cons_P1027346459y_real @t305) @t303))) % 0.48/0.90 (define @t308 () (= @t306 tptp.nil_Pr1492526187y_real)) % 0.48/0.90 (define @t309 () (@var "R2" (-> tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t310 () (@list @t299 @t293 @t297 @t291)) % 0.48/0.90 (define @t311 () (@var "Xs3" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t312 () (@var "R2" (-> tptp.produc321349221y_real tptp.poly_real Bool))) % 0.48/0.90 (define @t313 () (@var "X4" tptp.produc321349221y_real)) % 0.48/0.90 (define @t314 () (@var "A1" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t315 () (= @t314 (_ (_ tptp.cons_P1027346459y_real @t313) @t311))) % 0.48/0.90 (define @t316 () (= @t314 tptp.nil_Pr1492526187y_real)) % 0.48/0.90 (define @t317 () (@var "Ys3" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t318 () (@var "R2" (-> tptp.poly_real tptp.produc461822025y_real Bool))) % 0.48/0.90 (define @t319 () (@var "Y3" tptp.produc461822025y_real)) % 0.48/0.90 (define @t320 () (@var "A2" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t321 () (= @t320 (_ (_ tptp.cons_P1129399039y_real @t319) @t317))) % 0.48/0.90 (define @t322 () (@var "R2" (-> tptp.list_poly_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t323 () (@var "R2" (-> tptp.produc321349221y_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t324 () (@var "Xs3" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t325 () (@var "R2" (-> tptp.produc461822025y_real tptp.poly_real Bool))) % 0.48/0.90 (define @t326 () (@var "X4" tptp.produc461822025y_real)) % 0.48/0.90 (define @t327 () (@var "A1" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t328 () (= @t327 (_ (_ tptp.cons_P1129399039y_real @t326) @t324))) % 0.48/0.90 (define @t329 () (= @t327 tptp.nil_Pr1207979855y_real)) % 0.48/0.90 (define @t330 () (@var "A22" tptp.list_poly_real)) % 0.48/0.90 (define @t331 () (= @t330 @t204)) % 0.48/0.90 (define @t332 () (@list @t201)) % 0.48/0.90 (define @t333 () (@var "A12" tptp.list_poly_real)) % 0.48/0.90 (define @t334 () (= @t333 @t208)) % 0.48/0.90 (define @t335 () (@list @t206 @t202 @t205)) % 0.48/0.90 (define @t336 () (= @t330 tptp.nil_poly_real)) % 0.48/0.90 (define @t337 () (not @t336)) % 0.48/0.90 (define @t338 () (= @t333 tptp.nil_poly_real)) % 0.48/0.90 (define @t339 () (=> @t338 @t337)) % 0.48/0.90 (define @t340 () (@var "A22" tptp.list_list_poly_real)) % 0.48/0.90 (define @t341 () (= @t340 @t222)) % 0.48/0.90 (define @t342 () (@list @t220)) % 0.48/0.90 (define @t343 () (not (= @t340 tptp.nil_list_poly_real))) % 0.48/0.90 (define @t344 () (@var "A12" tptp.list_list_poly_real)) % 0.48/0.90 (define @t345 () (= @t344 @t230)) % 0.48/0.90 (define @t346 () (= @t344 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t347 () (@var "A22" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t348 () (= @t347 @t237)) % 0.48/0.90 (define @t349 () (@list @t235)) % 0.48/0.90 (define @t350 () (not (= @t347 tptp.nil_Pr1492526187y_real))) % 0.48/0.90 (define @t351 () (@list @t228 @t221 @t227)) % 0.48/0.90 (define @t352 () (@var "A12" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t353 () (= @t352 @t253)) % 0.48/0.90 (define @t354 () (= @t352 tptp.nil_Pr1492526187y_real)) % 0.48/0.90 (define @t355 () (@var "A22" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t356 () (= @t355 @t260)) % 0.48/0.90 (define @t357 () (@list @t258)) % 0.48/0.90 (define @t358 () (@var "A12" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t359 () (= @t358 @t274)) % 0.48/0.90 (define @t360 () (= @t358 tptp.nil_Pr1207979855y_real)) % 0.48/0.90 (define @t361 () (@var "X" tptp.list_list_poly_real)) % 0.48/0.90 (define @t362 () (= @t361 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t363 () (@var "X" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t364 () (@var "X" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t365 () (= @t125 @t208)) % 0.48/0.90 (define @t366 () (@list @t206 @t205)) % 0.48/0.90 (define @t367 () (= @t125 tptp.nil_poly_real)) % 0.48/0.90 (define @t368 () (_ (_ @t94 @t227) @t220)) % 0.48/0.90 (define @t369 () (not (_ (_ @t93 @t221) @t228))) % 0.48/0.90 (define @t370 () (_ (_ @t93 @t228) @t221)) % 0.48/0.90 (define @t371 () (not @t370)) % 0.48/0.90 (define @t372 () (@var "X_1" tptp.list_list_poly_real)) % 0.48/0.90 (define @t373 () (@var "P3" (-> tptp.list_P736648811y_real tptp.list_P736648811y_real Bool))) % 0.48/0.90 (define @t374 () (_ (_ @t373 @t253) @t237)) % 0.48/0.90 (define @t375 () (_ (_ @t92 @t250) @t235)) % 0.48/0.90 (define @t376 () (not (_ (_ @t91 @t236) @t251))) % 0.48/0.90 (define @t377 () (_ (_ @t91 @t251) @t236)) % 0.48/0.90 (define @t378 () (not @t377)) % 0.48/0.90 (define @t379 () (@list @t251 @t236 @t250 @t235)) % 0.48/0.90 (define @t380 () (@var "X_1" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t381 () (@var "P3" (-> tptp.list_P693436111y_real tptp.list_P693436111y_real Bool))) % 0.48/0.90 (define @t382 () (_ (_ @t381 @t274) @t260)) % 0.48/0.90 (define @t383 () (_ (_ @t96 @t271) @t258)) % 0.48/0.90 (define @t384 () (not (_ (_ @t95 @t259) @t272))) % 0.48/0.90 (define @t385 () (_ (_ @t95 @t272) @t259)) % 0.48/0.90 (define @t386 () (not @t385)) % 0.48/0.90 (define @t387 () (@list @t272 @t259 @t271 @t258)) % 0.48/0.90 (define @t388 () (@var "X_1" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t389 () (_ (_ @t98 @t205) @t201)) % 0.48/0.90 (define @t390 () (not (_ (_ @t97 @t202) @t206))) % 0.48/0.90 (define @t391 () (_ (_ @t97 @t206) @t202)) % 0.48/0.90 (define @t392 () (not @t391)) % 0.48/0.90 (define @t393 () (@var "X_1" tptp.list_poly_real)) % 0.48/0.90 (define @t394 () (forall (@list @t393) (_ @t216 @t393))) % 0.48/0.90 (define @t395 () (@var "Less2" (-> tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t396 () (_ (_ @t395 @t299) @t293)) % 0.48/0.90 (define @t397 () (@var "Less2" (-> tptp.produc321349221y_real tptp.produc321349221y_real Bool))) % 0.48/0.90 (define @t398 () (_ (_ @t397 @t313) @t305)) % 0.48/0.90 (define @t399 () (@list @t313 @t305 @t311 @t303)) % 0.48/0.90 (define @t400 () (@var "Less2" (-> tptp.produc461822025y_real tptp.produc461822025y_real Bool))) % 0.48/0.90 (define @t401 () (_ (_ @t400 @t326) @t319)) % 0.48/0.90 (define @t402 () (@list @t326 @t319 @t324 @t317)) % 0.48/0.90 (define @t403 () (@var "Less2" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t404 () (_ (_ @t403 @t281) @t280)) % 0.48/0.90 (define @t405 () (@list @t202)) % 0.48/0.90 (define @t406 () (@list @t205)) % 0.48/0.90 (define @t407 () (@list @t206)) % 0.48/0.90 (define @t408 () (@var "Y22" tptp.list_list_poly_real)) % 0.48/0.90 (define @t409 () (@var "X22" tptp.list_list_poly_real)) % 0.48/0.90 (define @t410 () (@var "Y21" tptp.list_poly_real)) % 0.48/0.90 (define @t411 () (@var "X21" tptp.list_poly_real)) % 0.48/0.90 (define @t412 () (@var "Y22" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t413 () (@var "X22" tptp.list_P736648811y_real)) % 0.48/0.90 (define @t414 () (@var "Y21" tptp.produc321349221y_real)) % 0.48/0.90 (define @t415 () (@var "X21" tptp.produc321349221y_real)) % 0.48/0.90 (define @t416 () (@var "Y22" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t417 () (@var "X22" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t418 () (@var "Y21" tptp.produc461822025y_real)) % 0.48/0.90 (define @t419 () (@var "X21" tptp.produc461822025y_real)) % 0.48/0.90 (define @t420 () (@var "Y22" tptp.list_poly_real)) % 0.48/0.90 (define @t421 () (@var "X22" tptp.list_poly_real)) % 0.48/0.90 (define @t422 () (@var "Y21" tptp.poly_real)) % 0.48/0.90 (define @t423 () (@var "X21" tptp.poly_real)) % 0.48/0.90 (define @t424 () (_ (_ tptp.cons_poly_real @t423) @t421)) % 0.48/0.90 (define @t425 () (_ @t102 @t80)) % 0.48/0.90 (define @t426 () (not (_ (_ @t97 @t43) @t134))) % 0.48/0.90 (define @t427 () (_ (_ @t97 @t134) @t43)) % 0.48/0.90 (define @t428 () (_ tptp.cons_poly_real @t43)) % 0.48/0.90 (define @t429 () (_ @t428 @t80)) % 0.48/0.90 (define @t430 () (_ @t137 @t429)) % 0.48/0.90 (define @t431 () (@var "Xss" tptp.list_l1245274212y_real)) % 0.48/0.90 (define @t432 () (@var "X" tptp.list_l1245274212y_real)) % 0.48/0.90 (define @t433 () (@var "Xss" tptp.list_l6097393y_real)) % 0.48/0.90 (define @t434 () (@var "X" tptp.list_l6097393y_real)) % 0.48/0.90 (define @t435 () (@var "Xss" tptp.list_l343759061y_real)) % 0.48/0.90 (define @t436 () (@var "X" tptp.list_l343759061y_real)) % 0.48/0.90 (define @t437 () (@var "Xss" tptp.list_list_poly_real)) % 0.48/0.90 (define @t438 () (_ tptp.cons_list_poly_real tptp.nil_poly_real)) % 0.48/0.90 (define @t439 () (@list @t134 @t67)) % 0.48/0.90 (define @t440 () (@var "A3" tptp.produc1426596841y_real)) % 0.48/0.90 (define @t441 () (@var "P3" (-> tptp.produc1426596841y_real Bool))) % 0.48/0.90 (define @t442 () (@var "A3" tptp.produc461822025y_real)) % 0.48/0.90 (define @t443 () (@var "A3" tptp.poly_real)) % 0.48/0.90 (define @t444 () (@var "A3" tptp.list_poly_real)) % 0.48/0.90 (define @t445 () (@var "A4" tptp.set_Pr1405268809y_real)) % 0.48/0.90 (define @t446 () (@var "X4" tptp.produc1426596841y_real)) % 0.48/0.90 (define @t447 () (@var "A4" tptp.set_Pr483210409y_real)) % 0.48/0.90 (define @t448 () (@var "A4" tptp.set_poly_real)) % 0.48/0.90 (define @t449 () (@var "A4" tptp.set_list_poly_real)) % 0.48/0.90 (define @t450 () (@var "A0" tptp.list_poly_real)) % 0.48/0.90 (define @t451 () (_ @t13 @t450)) % 0.48/0.90 (define @t452 () (_ @t207 @t201)) % 0.48/0.90 (define @t453 () (@list @t206 @t201)) % 0.48/0.90 (define @t454 () (_ @t13 tptp.nil_poly_real)) % 0.48/0.90 (define @t455 () (@list @t13 @t450)) % 0.48/0.90 (define @t456 () (not @t367)) % 0.48/0.90 (define @t457 () (@list @t125)) % 0.48/0.90 (define @t458 () (@var "A0" (-> tptp.list_poly_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t459 () (@var "P3" (-> (-> tptp.list_poly_real tptp.produc461822025y_real) tptp.list_list_poly_real tptp.list_P693436111y_real Bool))) % 0.48/0.90 (define @t460 () (@var "Bs2" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t461 () (@var "F2" (-> tptp.list_poly_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t462 () (_ @t459 @t461)) % 0.48/0.90 (define @t463 () (@var "A0" (-> tptp.produc321349221y_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t464 () (@var "P3" (-> (-> tptp.produc321349221y_real tptp.produc461822025y_real) tptp.list_P736648811y_real tptp.list_P693436111y_real Bool))) % 0.48/0.90 (define @t465 () (@var "F2" (-> tptp.produc321349221y_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t466 () (_ @t464 @t465)) % 0.48/0.90 (define @t467 () (@var "A0" (-> tptp.produc461822025y_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t468 () (@var "P3" (-> (-> tptp.produc461822025y_real tptp.produc461822025y_real) tptp.list_P693436111y_real tptp.list_P693436111y_real Bool))) % 0.48/0.90 (define @t469 () (@var "F2" (-> tptp.produc461822025y_real tptp.produc461822025y_real))) % 0.48/0.90 (define @t470 () (_ @t468 @t469)) % 0.48/0.90 (define @t471 () (@var "A0" (-> tptp.poly_real tptp.poly_real))) % 0.48/0.90 (define @t472 () (@var "P3" (-> (-> tptp.poly_real tptp.poly_real) tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t473 () (@var "Bs2" tptp.list_poly_real)) % 0.48/0.90 (define @t474 () (@var "F2" (-> tptp.poly_real tptp.poly_real))) % 0.48/0.90 (define @t475 () (_ @t472 @t474)) % 0.48/0.90 (define @t476 () (_ @t13 @t67)) % 0.48/0.90 (define @t477 () (_ @t13 @t208)) % 0.48/0.90 (define @t478 () (_ @t13 @t205)) % 0.48/0.90 (define @t479 () (not (= @t205 tptp.nil_poly_real))) % 0.48/0.90 (define @t480 () (_ @t207 tptp.nil_poly_real)) % 0.48/0.90 (define @t481 () (forall @t407 (_ @t13 @t480))) % 0.48/0.90 (define @t482 () (not @t68)) % 0.48/0.90 (define @t483 () (@list @t67 @t13)) % 0.48/0.90 (define @t484 () (@var "A0" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t485 () (@var "P3" (-> (-> tptp.poly_real tptp.poly_real Bool) tptp.list_poly_real Bool))) % 0.48/0.90 (define @t486 () (_ (_ @t485 @t484) @t333)) % 0.48/0.90 (define @t487 () (_ @t203 @t205)) % 0.48/0.90 (define @t488 () (_ @t207 @t487)) % 0.48/0.90 (define @t489 () (@var "P4" (-> tptp.poly_real tptp.poly_real Bool))) % 0.48/0.90 (define @t490 () (_ @t485 @t489)) % 0.48/0.90 (define @t491 () (@list @t489 @t206 @t202 @t205)) % 0.48/0.90 (define @t492 () (@list @t489 @t206)) % 0.48/0.90 (define @t493 () (@list @t489)) % 0.48/0.90 (define @t494 () (forall @t493 (_ @t490 tptp.nil_poly_real))) % 0.48/0.90 (define @t495 () (@list @t485 @t484 @t333)) % 0.48/0.90 (define @t496 () (= @t206 @t202)) % 0.48/0.90 (define @t497 () (not @t496)) % 0.48/0.90 (define @t498 () (@list @t489 @t206 @t201)) % 0.48/0.90 (define @t499 () (_ (_ @t199 @t450) @t333)) % 0.48/0.90 (define @t500 () (_ @t209 @t201)) % 0.48/0.90 (define @t501 () (@list @t206 @t205 @t202 @t201)) % 0.48/0.90 (define @t502 () (forall @t406 (_ @t211 tptp.nil_poly_real))) % 0.48/0.90 (define @t503 () (@list @t199 @t450 @t333)) % 0.48/0.90 (define @t504 () (@var "X222" tptp.list_poly_real)) % 0.48/0.90 (define @t505 () (@var "X212" tptp.poly_real)) % 0.48/0.90 (define @t506 () (@var "Zs" tptp.list_poly_real)) % 0.48/0.90 (define @t507 () (_ @t203 @t506)) % 0.48/0.90 (define @t508 () (@list @t13 @t67)) % 0.48/0.90 (define @t509 () (@list @t206 @t205 @t201)) % 0.48/0.90 (define @t510 () (_ (_ @t199 @t67) @t80)) % 0.48/0.90 (define @t511 () (forall @t501 @t212)) % 0.48/0.90 (define @t512 () (@list @t202 @t201)) % 0.48/0.90 (define @t513 () (forall @t512 (_ @t216 @t204))) % 0.48/0.90 (define @t514 () (= @t67 @t282)) % 0.48/0.90 (define @t515 () (@list @t280 @t277)) % 0.48/0.90 (define @t516 () (@var "List" tptp.list_poly_real)) % 0.48/0.90 (define @t517 () (@var "X23" tptp.list_poly_real)) % 0.48/0.90 (define @t518 () (@var "X12" tptp.poly_real)) % 0.48/0.90 (define @t519 () (@var "X223" tptp.list_poly_real)) % 0.48/0.90 (define @t520 () (@var "X213" tptp.poly_real)) % 0.48/0.90 (define @t521 () (@list @t97 @t134 @t43 @t67 @t80)) % 0.48/0.90 (define @t522 () (@list @t134 @t67 @t80)) % 0.48/0.90 (define @t523 () (@var "Ps3" tptp.list_poly_real)) % 0.48/0.90 (define @t524 () (@var "Q" tptp.poly_real)) % 0.48/0.90 (define @t525 () (@var "As2" tptp.list_poly_real)) % 0.48/0.90 (define @t526 () (_ tptp.cons_poly_real @t443)) % 0.48/0.90 (define @t527 () (= @t134 @t43)) % 0.48/0.90 (define @t528 () (_ (_ tptp.zip_po657915297y_real @t67) @t80)) % 0.48/0.90 (define @t529 () (@var "Va" tptp.list_poly_real)) % 0.48/0.90 (define @t530 () (@var "V" tptp.poly_real)) % 0.48/0.90 (define @t531 () (_ (_ tptp.cons_poly_real @t530) @t529)) % 0.48/0.90 (define @t532 () (@list @t530 @t529)) % 0.48/0.90 (define @t533 () (_ @t135 tptp.nil_poly_real)) % 0.48/0.90 (define @t534 () (_ tptp.append_poly_real @t67)) % 0.48/0.90 (define @t535 () (_ @t534 @t533)) % 0.48/0.90 (define @t536 () (_ tptp.append_poly_real (_ @t19 @t134))) % 0.48/0.90 (define @t537 () (_ tptp.suc @t44)) % 0.48/0.90 (define @t538 () (@list @t44 @t134 @t67)) % 0.48/0.90 (define @t539 () (_ @t534 @t80)) % 0.48/0.90 (define @t540 () (@list @t80 @t67)) % 0.48/0.90 (define @t541 () (@list @t444)) % 0.48/0.90 (define @t542 () (= @t67 @t80)) % 0.48/0.90 (define @t543 () (_ tptp.append_poly_real @t80)) % 0.48/0.90 (define @t544 () (_ @t543 (_ @t428 tptp.nil_poly_real))) % 0.48/0.90 (define @t545 () (@var "Zs2" tptp.list_poly_real)) % 0.48/0.90 (define @t546 () (_ @t543 @t545)) % 0.48/0.90 (define @t547 () (= @t136 @t546)) % 0.48/0.90 (define @t548 () (@var "Xs1" tptp.list_poly_real)) % 0.48/0.90 (define @t549 () (_ tptp.append_poly_real tptp.nil_poly_real)) % 0.48/0.90 (define @t550 () (_ @t549 @t80)) % 0.48/0.90 (define @t551 () (=> @t478 (_ @t13 (_ (_ tptp.append_poly_real @t205) @t480)))) % 0.48/0.90 (define @t552 () (_ @t203 tptp.nil_poly_real)) % 0.48/0.90 (define @t553 () (@var "Ys4" tptp.list_poly_real)) % 0.48/0.90 (define @t554 () (_ (_ tptp.append_poly_real @t553) @t545)) % 0.48/0.90 (define @t555 () (_ @t135 @t553)) % 0.48/0.90 (define @t556 () (@list @t553)) % 0.48/0.90 (define @t557 () (@var "Nat2" tptp.nat)) % 0.48/0.90 (define @t558 () (@var "Nat" tptp.nat)) % 0.48/0.90 (define @t559 () (@var "Y23" tptp.nat)) % 0.48/0.90 (define @t560 () (@var "X2" tptp.nat)) % 0.48/0.90 (define @t561 () (_ @t438 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t562 () (@var "Xss22" tptp.list_list_poly_real)) % 0.48/0.90 (define @t563 () (@var "Xs4" tptp.list_poly_real)) % 0.48/0.90 (define @t564 () (@var "Xss1" tptp.list_list_poly_real)) % 0.48/0.90 (define @t565 () (@var "Xss2" tptp.list_list_poly_real)) % 0.48/0.90 (define @t566 () (= @t565 tptp.nil_list_poly_real)) % 0.48/0.90 (define @t567 () (@var "Y" tptp.nat)) % 0.48/0.90 (define @t568 () (@var "X" tptp.nat)) % 0.48/0.90 (define @t569 () (@list @t67 @t134)) % 0.48/0.90 (define @t570 () (@var "Va2" tptp.list_poly_real)) % 0.48/0.90 (define @t571 () (@var "V2" tptp.poly_real)) % 0.48/0.90 (define @t572 () (_ (_ tptp.cons_poly_real @t571) @t570)) % 0.48/0.90 (define @t573 () (_ tptp.last_poly_real @t67)) % 0.48/0.90 (define @t574 () (_ tptp.last_poly_real @t539)) % 0.48/0.90 (define @t575 () (=> @t81 (= @t574 @t573))) % 0.48/0.90 (define @t576 () (_ tptp.last_poly_real @t80)) % 0.48/0.90 (define @t577 () (not @t81)) % 0.48/0.90 (define @t578 () (=> @t577 (= @t574 @t576))) % 0.48/0.90 (define @t579 () (_ tptp.produc1867601537y_real @t134)) % 0.48/0.90 (define @t580 () (_ @t579 @t43)) % 0.48/0.90 (define @t581 () (_ tptp.butlast_poly_real @t67)) % 0.48/0.90 (define @t582 () (_ tptp.butlast_poly_real @t80)) % 0.48/0.90 (define @t583 () (_ tptp.last_poly_real @t136)) % 0.48/0.90 (define @t584 () (=> @t482 (= @t583 @t573))) % 0.48/0.90 (define @t585 () (=> @t68 (= @t583 @t134))) % 0.48/0.90 (define @t586 () (@var "Ys5" tptp.list_poly_real)) % 0.48/0.90 (define @t587 () (@var "Xs5" tptp.list_poly_real)) % 0.48/0.90 (define @t588 () (@var "Xys" tptp.list_P693436111y_real)) % 0.48/0.90 (define @t589 () (_ tptp.produc1867601537y_real @t206)) % 0.48/0.90 (define @t590 () (_ @t589 @t202)) % 0.48/0.90 (define @t591 () (@var "Xy" tptp.produc461822025y_real)) % 0.48/0.90 (define @t592 () (@var "Ss" tptp.list_poly_real)) % 0.48/0.90 (define @t593 () (_ tptp.butlast_poly_real @t136)) % 0.48/0.90 (define @t594 () (_ tptp.butlast_poly_real @t539)) % 0.48/0.90 (define @t595 () (@var "R" tptp.set_Pr483210409y_real)) % 0.48/0.90 (define @t596 () (_ (_ tptp.member1784523250y_real @t580) @t595)) % 0.48/0.90 (define @t597 () (_ tptp.listrel1_poly_real @t595)) % 0.48/0.90 (define @t598 () (_ tptp.produc1000427809y_real @t67)) % 0.48/0.90 (define @t599 () (_ tptp.member403334290y_real (_ @t598 @t80))) % 0.48/0.90 (define @t600 () (_ @t599 @t597)) % 0.48/0.90 (define @t601 () (_ tptp.size_s259235672y_real @t80)) % 0.48/0.90 (define @t602 () (_ tptp.size_s259235672y_real @t67)) % 0.48/0.90 (define @t603 () (= @t602 @t601)) % 0.48/0.90 (define @t604 () (@list @t44 @t67)) % 0.48/0.90 (define @t605 () (_ tptp.produc1000427809y_real @t136)) % 0.48/0.90 (define @t606 () (_ tptp.member403334290y_real (_ @t605 @t429))) % 0.48/0.90 (define @t607 () (@list @t134 @t67 @t43 @t80 @t595)) % 0.48/0.90 (define @t608 () (_ tptp.member403334290y_real (_ @t598 tptp.nil_poly_real))) % 0.48/0.90 (define @t609 () (@list @t67 @t595)) % 0.48/0.90 (define @t610 () (_ tptp.produc1000427809y_real tptp.nil_poly_real)) % 0.48/0.90 (define @t611 () (_ tptp.member403334290y_real (_ @t610 @t67))) % 0.48/0.90 (define @t612 () (_ tptp.produc1345584779y_real @t489)) % 0.48/0.90 (define @t613 () (@var "X" tptp.produc1060019729y_real)) % 0.48/0.90 (define @t614 () (forall @t493 (not (= @t613 (_ @t612 tptp.nil_poly_real))))) % 0.48/0.90 (define @t615 () (@list @t613)) % 0.48/0.90 (define @t616 () (exists @t515 (and @t514 (= (_ tptp.size_s259235672y_real @t277) @t44)))) % 0.48/0.90 (define @t617 () (@var "Ws" tptp.list_poly_real)) % 0.48/0.90 (define @t618 () (@var "P3" (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t619 () (@var "Ws2" tptp.list_poly_real)) % 0.48/0.90 (define @t620 () (@var "W" tptp.poly_real)) % 0.48/0.90 (define @t621 () (@var "Z" tptp.poly_real)) % 0.48/0.90 (define @t622 () (_ (_ tptp.cons_poly_real @t621) @t506)) % 0.48/0.90 (define @t623 () (_ tptp.size_s259235672y_real @t506)) % 0.48/0.90 (define @t624 () (_ tptp.size_s259235672y_real @t201)) % 0.48/0.90 (define @t625 () (= @t624 @t623)) % 0.48/0.90 (define @t626 () (= (_ tptp.size_s259235672y_real @t205) @t624)) % 0.48/0.90 (define @t627 () (_ tptp.size_s259235672y_real @t545)) % 0.48/0.90 (define @t628 () (= @t601 @t627)) % 0.48/0.90 (define @t629 () (@var "P3" (-> tptp.list_poly_real tptp.list_poly_real tptp.list_poly_real Bool))) % 0.48/0.90 (define @t630 () (@var "F2" tptp.poly_real)) % 0.48/0.90 (define @t631 () (_ tptp.produc490255505y_real @t630)) % 0.48/0.90 (define @t632 () (@var "X" tptp.produc796638169y_real)) % 0.48/0.90 (define @t633 () (_ tptp.produc1000427809y_real @t208)) % 0.48/0.90 (define @t634 () (@var "X" tptp.produc1426596841y_real)) % 0.48/0.90 (define @t635 () (forall @t501 (not (= @t634 (_ @t633 @t204))))) % 0.48/0.90 (define @t636 () (not @t635)) % 0.48/0.90 (define @t637 () (_ tptp.produc1000427809y_real @t205)) % 0.48/0.90 (define @t638 () (forall @t406 (not (= @t634 (_ @t637 tptp.nil_poly_real))))) % 0.48/0.91 (define @t639 () (forall @t332 (not (= @t634 (_ @t610 @t201))))) % 0.48/0.91 (define @t640 () (@list @t634)) % 0.48/0.91 (define @t641 () (@list @t506)) % 0.48/0.91 (define @t642 () (_ (_ tptp.member1784523250y_real (_ @t589 @t43)) @t595)) % 0.48/0.91 (define @t643 () (_ tptp.member403334290y_real (_ @t598 @t429))) % 0.48/0.91 (define @t644 () (@list @t67 @t43 @t80 @t595)) % 0.48/0.91 (define @t645 () (@var "Pre" tptp.list_poly_real)) % 0.48/0.91 (define @t646 () (_ tptp.append_poly_real @t645)) % 0.48/0.91 (define @t647 () (@var "Vs" tptp.list_poly_real)) % 0.48/0.91 (define @t648 () (@var "Us" tptp.list_poly_real)) % 0.48/0.91 (define @t649 () (_ tptp.append_poly_real @t648)) % 0.48/0.91 (define @t650 () (_ (_ tptp.member1784523250y_real @t590) @t595)) % 0.48/0.91 (define @t651 () (@var "Vs2" tptp.list_poly_real)) % 0.48/0.91 (define @t652 () (@var "Us2" tptp.list_poly_real)) % 0.48/0.91 (define @t653 () (_ tptp.append_poly_real @t652)) % 0.48/0.91 (define @t654 () (_ tptp.suc @t602)) % 0.48/0.91 (define @t655 () (_ tptp.lex_poly_real @t595)) % 0.48/0.91 (define @t656 () (@var "Kl" tptp.set_list_poly_real)) % 0.48/0.91 (define @t657 () (@var "K" tptp.poly_real)) % 0.48/0.91 (define @t658 () (_ tptp.cons_poly_real @t657)) % 0.48/0.91 (define @t659 () (@var "Kl2" tptp.list_poly_real)) % 0.48/0.91 (define @t660 () (_ (_ tptp.member708095579y_real (_ (_ tptp.append_poly_real @t659) (_ @t658 tptp.nil_poly_real))) @t656)) % 0.48/0.91 (define @t661 () (_ tptp.bNF_Gr1644259033y_real @t656)) % 0.48/0.91 (define @t662 () (_ tptp.member_poly_real2 @t657)) % 0.48/0.91 (define @t663 () (_ @t662 (_ @t661 @t659))) % 0.48/0.91 (define @t664 () (_ (_ tptp.bNF_Gr851617109y_real @t656) @t657)) % 0.48/0.91 (define @t665 () (_ tptp.member708095579y_real tptp.nil_poly_real)) % 0.48/0.91 (define @t666 () (_ @t658 @t659)) % 0.48/0.91 (define @t667 () (@var "M" tptp.nat)) % 0.48/0.91 (define @t668 () (@var "K" tptp.nat)) % 0.48/0.91 (define @t669 () (_ tptp.times_times_nat (_ tptp.suc @t668))) % 0.48/0.91 (define @t670 () (_ tptp.lexord_poly_real @t595)) % 0.48/0.91 (define @t671 () (@var "B" tptp.poly_real)) % 0.48/0.91 (define @t672 () (_ (_ tptp.cons_poly_real @t671) @t40)) % 0.48/0.91 (define @t673 () (@var "U" tptp.list_poly_real)) % 0.48/0.91 (define @t674 () (_ tptp.append_poly_real @t673)) % 0.48/0.91 (define @t675 () (_ @t526 @t125)) % 0.48/0.91 (define @t676 () (_ (_ tptp.member1784523250y_real (_ (_ tptp.produc1867601537y_real @t443) @t671)) @t595)) % 0.48/0.91 (define @t677 () (_ tptp.listre572247515y_real @t595)) % 0.48/0.91 (define @t678 () (_ (_ tptp.member403334290y_real (_ @t637 @t201)) @t677)) % 0.48/0.91 (define @t679 () (_ tptp.produc1000427809y_real @t125)) % 0.48/0.91 (define @t680 () (@var "A5" tptp.poly_real)) % 0.48/0.91 (define @t681 () (@var "Z2" tptp.list_poly_real)) % 0.48/0.91 (define @t682 () (@var "B2" tptp.poly_real)) % 0.48/0.91 (define @t683 () (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t333) @t330)) @t677)) % 0.48/0.91 (define @t684 () (@list @t333 @t330 @t595)) % 0.48/0.91 (define @t685 () (_ tptp.produc2087464649y_real @t140)) % 0.48/0.91 (define @t686 () (_ tptp.accp_P948088014y_real tptp.map_ta954657966y_real)) % 0.48/0.91 (define @t687 () (@var "Ns" tptp.list_poly_real)) % 0.48/0.91 (define @t688 () (_ tptp.lenlex_poly_real @t595)) % 0.48/0.91 (define @t689 () (@list @t687 @t595)) % 0.48/0.91 (define @t690 () (@var "Ms" tptp.list_poly_real)) % 0.48/0.91 (define @t691 () (@var "N" tptp.poly_real)) % 0.48/0.91 (define @t692 () (@var "M" tptp.poly_real)) % 0.48/0.91 (define @t693 () (_ tptp.size_s259235672y_real @t687)) % 0.48/0.91 (define @t694 () (_ tptp.size_s259235672y_real @t690)) % 0.48/0.91 (define @t695 () (_ (_ tptp.ord_less_nat @t667) @t44)) % 0.48/0.91 (define @t696 () (_ (_ tptp.ord_less_nat (_ tptp.suc @t667)) @t537)) % 0.48/0.91 (define @t697 () (@list @t667 @t44)) % 0.48/0.91 (define @t698 () (_ tptp.map_po2132607150y_real @t89)) % 0.48/0.91 (define @t699 () (_ @t698 @t67)) % 0.48/0.91 (define @t700 () (@list @t89 @t67)) % 0.48/0.91 (define @t701 () (_ tptp.sturm_891428828rm_seq tptp.nil_poly_real)) % 0.48/0.91 (define @t702 () (@var "P2" tptp.poly_real)) % 0.48/0.91 (define @t703 () (@var "Ps2" tptp.list_poly_real)) % 0.48/0.91 (define @t704 () (lambda (@list @t703 @t702) (and (_ tptp.sturm_891428828rm_seq @t703) (_ (_ tptp.sturm_1683633594axioms @t703) @t702)))) % 0.48/0.91 (define @t705 () (@var "Xss3" tptp.list_list_poly_real)) % 0.48/0.91 (define @t706 () (lambda (@list @t705) (_ (_ (_ tptp.foldr_2117681201y_real tptp.append_poly_real) @t705) tptp.nil_poly_real))) % 0.48/0.91 (define @t707 () (tptp.sturm_891428828rm_seq tptp.nil_poly_real)) % 0.48/0.91 (define @t708 () (not @t707)) % 0.48/0.91 (define @t709 () (not (= tptp.nil_poly_real tptp.nil_poly_real))) % 0.48/0.91 (define @t710 () (or @t708 @t709)) % 0.48/0.91 (define @t711 () (not (= tptp.nil_poly_real @t1))) % 0.48/0.91 (define @t712 () (tptp.sturm_891428828rm_seq @t1)) % 0.48/0.91 (define @t713 () (not @t712)) % 0.48/0.91 (define @t714 () (or @t711 @t713 @t711)) % 0.48/0.91 (define @t715 () (or @t713 @t711)) % 0.48/0.91 (define @t716 () (not @t3)) % 0.48/0.91 (define @t717 () (or @t716 @t711)) % 0.48/0.91 (assume @p1 @t6) % 0.48/0.91 (assume @p2 (forall @t9 (=> @t8 @t3))) % 0.48/0.91 (assume @p3 (forall @t9 (=> @t3 (=> @t10 @t8)))) % 0.48/0.91 (assume @p4 (forall @t12 (not (_ (_ tptp.list_e1892536494y_real @t11) tptp.nil_Pr1492526187y_real)))) % 0.48/0.91 (assume @p5 (forall @t14 (not (_ (_ tptp.list_e367462459y_real @t13) tptp.nil_list_poly_real)))) % 0.48/0.91 (assume @p6 (forall @t16 (not (_ (_ tptp.list_e1507538962y_real @t15) tptp.nil_Pr1207979855y_real)))) % 0.48/0.91 (assume @p7 (forall @t18 (not (_ (_ tptp.list_ex1_poly_real @t17) tptp.nil_poly_real)))) % 0.48/0.91 (assume @p8 (forall @t20 (= (_ (_ tptp.bind_p420216945y_real tptp.nil_poly_real) @t19) tptp.nil_poly_real))) % 0.48/0.91 (assume @p9 (forall @t22 (= (_ (_ tptp.bind_p1226679937y_real tptp.nil_poly_real) @t21) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p10 (forall @t24 (= (_ (_ tptp.bind_l146959617y_real tptp.nil_list_poly_real) @t23) tptp.nil_poly_real))) % 0.48/0.91 (assume @p11 (forall @t26 (= (_ (_ tptp.bind_p600434664y_real tptp.nil_poly_real) @t25) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p12 (forall @t28 (= (_ (_ tptp.bind_P755425362y_real tptp.nil_Pr1492526187y_real) @t27) tptp.nil_poly_real))) % 0.48/0.91 (assume @p13 (forall @t30 (= (_ (_ tptp.bind_l1810664209y_real tptp.nil_list_poly_real) @t29) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p14 (forall @t32 (= (_ (_ tptp.bind_p988182092y_real tptp.nil_poly_real) @t31) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p15 (forall @t34 (= (_ (_ tptp.bind_P1861132770y_real tptp.nil_Pr1492526187y_real) @t33) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p16 (forall @t36 (= (_ (_ tptp.bind_l429098840y_real tptp.nil_list_poly_real) @t35) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p17 (forall @t38 (= (_ (_ tptp.bind_P120560694y_real tptp.nil_Pr1207979855y_real) @t37) tptp.nil_poly_real))) % 0.48/0.91 (assume @p18 (forall (@list @t39) (not (_ (_ tptp.member1782690048y_real tptp.nil_Pr1492526187y_real) @t39)))) % 0.48/0.91 (assume @p19 (forall @t41 (not (_ (_ tptp.member1829603177y_real tptp.nil_list_poly_real) @t40)))) % 0.48/0.91 (assume @p20 (forall (@list @t42) (not (_ (_ tptp.member202023780y_real tptp.nil_Pr1207979855y_real) @t42)))) % 0.48/0.91 (assume @p21 (forall (@list @t43) (not (_ (_ tptp.member_poly_real tptp.nil_poly_real) @t43)))) % 0.48/0.91 (assume @p22 (forall @t45 (= (_ (_ tptp.gen_le904455032y_real @t44) tptp.nil_Pr1492526187y_real) @t44))) % 0.48/0.91 (assume @p23 (forall @t45 (= (_ (_ tptp.gen_le1160603377y_real @t44) tptp.nil_list_poly_real) @t44))) % 0.48/0.91 (assume @p24 (forall @t45 (= (_ (_ tptp.gen_le1524582876y_real @t44) tptp.nil_Pr1207979855y_real) @t44))) % 0.48/0.91 (assume @p25 (forall @t45 (= (_ @t46 tptp.nil_poly_real) @t44))) % 0.48/0.91 (assume @p26 (forall @t20 (= (_ @t47 tptp.nil_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p27 (forall @t22 (= (_ (_ tptp.maps_p1417280571y_real @t21) tptp.nil_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p28 (forall @t24 (= (_ (_ tptp.maps_l337560251y_real @t23) tptp.nil_list_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p29 (forall @t26 (= (_ (_ tptp.maps_p2108677294y_real @t25) tptp.nil_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p30 (forall @t28 (= (_ (_ tptp.maps_P116184344y_real @t27) tptp.nil_Pr1492526187y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p31 (forall @t30 (= (_ (_ tptp.maps_l502643659y_real @t29) tptp.nil_list_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p32 (forall @t32 (= (_ (_ tptp.maps_p86983698y_real @t31) tptp.nil_poly_real) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p33 (forall @t34 (= (_ (_ tptp.maps_P54557608y_real @t33) tptp.nil_Pr1492526187y_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p34 (forall @t36 (= (_ (_ tptp.maps_l770007326y_real @t35) tptp.nil_list_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p35 (forall @t38 (= (_ (_ tptp.maps_P1366845948y_real @t37) tptp.nil_Pr1207979855y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p36 (forall (@list @t48) (= (_ (_ tptp.map_fi1183202740y_real @t48) tptp.nil_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p37 (forall (@list @t49) (= (_ (_ tptp.map_fi920577604y_real @t49) tptp.nil_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p38 (forall (@list @t50) (= (_ (_ tptp.map_fi1988340932y_real @t50) tptp.nil_list_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p39 (forall (@list @t51) (= (_ (_ tptp.map_fi740944613y_real @t51) tptp.nil_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p40 (forall (@list @t52) (= (_ (_ tptp.map_fi895935311y_real @t52) tptp.nil_Pr1492526187y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p41 (forall (@list @t53) (= (_ (_ tptp.map_fi357666132y_real @t53) tptp.nil_list_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p42 (forall (@list @t54) (= (_ (_ tptp.map_fi1117002953y_real @t54) tptp.nil_poly_real) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p43 (forall (@list @t55) (= (_ (_ tptp.map_fi1389003359y_real @t55) tptp.nil_Pr1492526187y_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p44 (forall (@list @t56) (= (_ (_ tptp.map_fi2104453077y_real @t56) tptp.nil_list_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p45 (forall (@list @t57) (= (_ (_ tptp.map_fi249381555y_real @t57) tptp.nil_Pr1207979855y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p46 (_ tptp.null_P89569907y_real tptp.nil_Pr1492526187y_real)) % 0.48/0.91 (assume @p47 (_ tptp.null_list_poly_real tptp.nil_list_poly_real)) % 0.48/0.91 (assume @p48 (_ tptp.null_P1782853975y_real tptp.nil_Pr1207979855y_real)) % 0.48/0.91 (assume @p49 (_ tptp.null_poly_real tptp.nil_poly_real)) % 0.48/0.91 (assume @p50 (forall @t60 (= @t59 (_ tptp.null_P89569907y_real @t58)))) % 0.48/0.91 (assume @p51 (forall @t63 (= @t62 (_ tptp.null_list_poly_real @t61)))) % 0.48/0.91 (assume @p52 (forall @t66 (= @t65 (_ tptp.null_P1782853975y_real @t64)))) % 0.48/0.91 (assume @p53 (forall @t69 (= @t68 (_ tptp.null_poly_real @t67)))) % 0.48/0.91 (assume @p54 (forall @t9 (=> @t8 @t10))) % 0.48/0.91 (assume @p55 (forall @t12 (not (_ @t70 tptp.nil_Pr1492526187y_real)))) % 0.48/0.91 (assume @p56 (forall @t14 (not (_ @t71 tptp.nil_list_poly_real)))) % 0.48/0.91 (assume @p57 (forall @t16 (not (_ @t72 tptp.nil_Pr1207979855y_real)))) % 0.48/0.91 (assume @p58 (forall @t18 (not (_ @t73 tptp.nil_poly_real)))) % 0.48/0.91 (assume @p59 (forall @t60 (= (= (_ tptp.rotate623875384y_real @t58) tptp.nil_Pr1492526187y_real) @t59))) % 0.48/0.91 (assume @p60 (forall @t63 (= (= (_ tptp.rotate717473073y_real @t61) tptp.nil_list_poly_real) @t62))) % 0.48/0.91 (assume @p61 (forall @t66 (= (= (_ tptp.rotate867081116y_real @t64) tptp.nil_Pr1207979855y_real) @t65))) % 0.48/0.91 (assume @p62 (forall @t69 (= (= (_ tptp.rotate1_poly_real @t67) tptp.nil_poly_real) @t68))) % 0.48/0.91 (assume @p63 (forall (@list @t58 @t74) (= (= (_ @t75 @t74) tptp.nil_Pr1492526187y_real) (and @t59 (= @t74 tptp.nil_Pr1492526187y_real))))) % 0.48/0.91 (assume @p64 (forall (@list @t61 @t76) (= (= (_ @t77 @t76) tptp.nil_list_poly_real) (and @t62 (= @t76 tptp.nil_list_poly_real))))) % 0.48/0.91 (assume @p65 (forall (@list @t64 @t78) (= (= (_ @t79 @t78) tptp.nil_Pr1207979855y_real) (and @t65 (= @t78 tptp.nil_Pr1207979855y_real))))) % 0.48/0.91 (assume @p66 (forall @t84 (= (= (_ @t83 @t80) tptp.nil_poly_real) @t82))) % 0.48/0.91 (assume @p67 (forall @t60 (= (_ @t75 tptp.nil_Pr1492526187y_real) @t58))) % 0.48/0.91 (assume @p68 (forall @t63 (= (_ @t77 tptp.nil_list_poly_real) @t61))) % 0.48/0.91 (assume @p69 (forall @t66 (= (_ @t79 tptp.nil_Pr1207979855y_real) @t64))) % 0.48/0.91 (assume @p70 (forall @t69 (= (_ @t83 tptp.nil_poly_real) @t67))) % 0.48/0.91 (assume @p71 (forall @t45 (= (_ (_ tptp.enumer1123002698y_real @t44) tptp.nil_Pr1492526187y_real) tptp.nil_Pr570652676y_real))) % 0.48/0.91 (assume @p72 (forall @t45 (= (_ (_ tptp.enumer1433313439y_real @t44) tptp.nil_list_poly_real) tptp.nil_Pr1161137915y_real))) % 0.48/0.91 (assume @p73 (forall @t45 (= (_ (_ tptp.enumer1015405230y_real @t44) tptp.nil_Pr1207979855y_real) tptp.nil_Pr2056488424y_real))) % 0.48/0.91 (assume @p74 (forall @t45 (= (_ @t85 tptp.nil_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p75 (forall @t87 (= (_ (_ tptp.produc1360353227y_real tptp.nil_nat) @t86) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p76 (forall @t87 (= (_ (_ tptp.produc1733309743y_real tptp.nil_poly_real) @t86) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p77 (forall (@list @t89 @t88) (= (_ (_ @t90 tptp.nil_poly_real) @t88) @t88))) % 0.48/0.91 (assume @p78 (forall (@list @t91 @t74) (_ (_ @t92 tptp.nil_Pr1492526187y_real) @t74))) % 0.48/0.91 (assume @p79 (forall (@list @t93 @t76) (_ (_ @t94 tptp.nil_list_poly_real) @t76))) % 0.48/0.91 (assume @p80 (forall (@list @t95 @t78) (_ (_ @t96 tptp.nil_Pr1207979855y_real) @t78))) % 0.48/0.91 (assume @p81 (forall (@list @t97 @t80) (_ (_ @t98 tptp.nil_poly_real) @t80))) % 0.48/0.91 (assume @p82 (forall (@list @t91 @t58) (= (_ @t99 tptp.nil_Pr1492526187y_real) @t59))) % 0.48/0.91 (assume @p83 (forall (@list @t93 @t61) (= (_ @t100 tptp.nil_list_poly_real) @t62))) % 0.48/0.91 (assume @p84 (forall (@list @t95 @t64) (= (_ @t101 tptp.nil_Pr1207979855y_real) @t65))) % 0.48/0.91 (assume @p85 (forall @t103 (= (_ @t102 tptp.nil_poly_real) @t68))) % 0.48/0.91 (assume @p86 (forall (@list @t104) (_ (_ @t105 tptp.nil_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p87 (forall (@list @t106) (_ (_ @t107 tptp.nil_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p88 (forall (@list @t108) (_ (_ @t109 tptp.nil_list_poly_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p89 (forall (@list @t110) (_ (_ @t111 tptp.nil_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p90 (forall (@list @t112) (_ (_ @t113 tptp.nil_Pr1492526187y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p91 (forall (@list @t114) (_ (_ @t115 tptp.nil_list_poly_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p92 (forall (@list @t116) (_ (_ @t117 tptp.nil_poly_real) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p93 (forall (@list @t118) (_ (_ @t119 tptp.nil_Pr1492526187y_real) tptp.nil_list_poly_real))) % 0.48/0.91 (assume @p94 (forall (@list @t120) (_ (_ @t121 tptp.nil_list_poly_real) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p95 (forall (@list @t122) (_ (_ @t123 tptp.nil_Pr1207979855y_real) tptp.nil_poly_real))) % 0.48/0.91 (assume @p96 (= tptp.lexordp_eq_poly_real tptp.lexordp_eq_poly_real)) % 0.48/0.91 (assume @p97 (forall @t103 (_ @t102 @t67))) % 0.48/0.91 (assume @p98 (forall (@list @t74) (= (_ (_ tptp.splice1383748542y_real tptp.nil_Pr1492526187y_real) @t74) @t74))) % 0.48/0.91 (assume @p99 (forall (@list @t76) (= (_ (_ tptp.splice2080530731y_real tptp.nil_list_poly_real) @t76) @t76))) % 0.48/0.91 (assume @p100 (forall (@list @t78) (= (_ (_ tptp.splice1321784098y_real tptp.nil_Pr1207979855y_real) @t78) @t78))) % 0.48/0.91 (assume @p101 (forall @t124 (= (_ (_ tptp.splice_poly_real tptp.nil_poly_real) @t80) @t80))) % 0.48/0.91 (assume @p102 (= (_ tptp.rotate623875384y_real tptp.nil_Pr1492526187y_real) tptp.nil_Pr1492526187y_real)) % 0.48/0.91 (assume @p103 (= (_ tptp.rotate717473073y_real tptp.nil_list_poly_real) tptp.nil_list_poly_real)) % 0.48/0.91 (assume @p104 (= (_ tptp.rotate867081116y_real tptp.nil_Pr1207979855y_real) tptp.nil_Pr1207979855y_real)) % 0.48/0.91 (assume @p105 (= (_ tptp.rotate1_poly_real tptp.nil_poly_real) tptp.nil_poly_real)) % 0.48/0.91 (assume @p106 (forall (@list @t93 @t125 @t61) (not (_ @t127 tptp.nil_list_poly_real)))) % 0.48/0.91 (assume @p107 (forall (@list @t91 @t128 @t58) (not (_ @t130 tptp.nil_Pr1492526187y_real)))) % 0.48/0.91 (assume @p108 (forall (@list @t95 @t131 @t64) (not (_ @t133 tptp.nil_Pr1207979855y_real)))) % 0.48/0.91 (assume @p109 (forall (@list @t97 @t134 @t67) (not (_ @t137 tptp.nil_poly_real)))) % 0.48/0.91 (assume @p110 (forall @t124 (= (_ (_ tptp.zip_nat_poly_real tptp.nil_nat) @t80) tptp.nil_Pr1492526187y_real))) % 0.48/0.91 (assume @p111 (forall @t124 (= (_ (_ tptp.zip_po657915297y_real tptp.nil_poly_real) @t80) tptp.nil_Pr1207979855y_real))) % 0.48/0.91 (assume @p112 (forall @t152 (=> @t151 (=> (=> @t150 @t149) (not (forall @t147 (=> @t146 (not @t143)))))))) % 0.48/0.91 (assume @p113 (forall (@list @t154 @t145 @t153 @t156) (=> (= (_ (_ @t155 @t145) @t153) @t156) (=> (=> @t150 @t157) (not (forall @t147 (=> @t146 (not (= @t156 (_ (_ @t155 @t141) (_ (_ tptp.cons_list_poly_real (_ @t154 @t139)) @t153))))))))))) % 0.48/0.91 (assume @p114 (forall (@list @t159 @t163 @t138 @t40) (=> (= (_ (_ @t161 @t163) @t138) @t40) (=> (=> @t166 @t149) (not (forall @t165 (=> @t164 (not (= @t40 (_ (_ @t161 @t160) (_ (_ tptp.cons_poly_real (_ @t159 @t158)) @t138))))))))))) % 0.48/0.91 (assume @p115 (forall (@list @t168 @t145 @t167 @t170) (=> (= (_ (_ @t169 @t145) @t167) @t170) (=> (=> @t150 @t171) (not (forall @t147 (=> @t146 (not (= @t170 (_ (_ @t169 @t141) (_ (_ tptp.cons_P1027346459y_real (_ @t168 @t139)) @t167))))))))))) % 0.48/0.91 (assume @p116 (forall (@list @t172 @t163 @t153 @t156) (=> (= (_ (_ @t173 @t163) @t153) @t156) (=> (=> @t166 @t157) (not (forall @t165 (=> @t164 (not (= @t156 (_ (_ @t173 @t160) (_ (_ tptp.cons_list_poly_real (_ @t172 @t158)) @t153))))))))))) % 0.48/0.91 (assume @p117 (forall (@list @t175 @t179 @t138 @t40) (=> (= (_ (_ @t177 @t179) @t138) @t40) (=> (=> @t182 @t149) (not (forall @t181 (=> @t180 (not (= @t40 (_ (_ @t177 @t176) (_ (_ tptp.cons_poly_real (_ @t175 @t174)) @t138))))))))))) % 0.48/0.91 (assume @p118 (forall (@list @t184 @t145 @t183 @t186) (=> (= (_ (_ @t185 @t145) @t183) @t186) (=> (=> @t150 (not (= @t186 @t183))) (not (forall @t147 (=> @t146 (not (= @t186 (_ (_ @t185 @t141) (_ (_ tptp.cons_P1129399039y_real (_ @t184 @t139)) @t183))))))))))) % 0.48/0.91 (assume @p119 (forall (@list @t187 @t163 @t167 @t170) (=> (= (_ (_ @t188 @t163) @t167) @t170) (=> (=> @t166 @t171) (not (forall @t165 (=> @t164 (not (= @t170 (_ (_ @t188 @t160) (_ (_ tptp.cons_P1027346459y_real (_ @t187 @t158)) @t167))))))))))) % 0.48/0.91 (assume @p120 (forall (@list @t189 @t179 @t153 @t156) (=> (= (_ (_ @t190 @t179) @t153) @t156) (=> (=> @t182 @t157) (not (forall @t181 (=> @t180 (not (= @t156 (_ (_ @t190 @t176) (_ (_ tptp.cons_list_poly_real (_ @t189 @t174)) @t153))))))))))) % 0.48/0.91 (assume @p121 (forall (@list @t192 @t196 @t138 @t40) (=> (= (_ (_ @t194 @t196) @t138) @t40) (=> (=> (= @t196 tptp.nil_Pr1207979855y_real) @t149) (not (forall (@list @t191 @t193) (=> (= @t196 @t195) (not (= @t40 (_ (_ @t194 @t193) (_ (_ tptp.cons_poly_real (_ @t192 @t191)) @t138))))))))))) % 0.48/0.91 (assume @p122 (forall (@list @t104 @t198 @t197 @t199) (=> (_ (_ @t105 @t198) @t197) (=> @t217 (=> (forall @t215 (=> @t214 (=> @t213 @t212))) @t200))))) % 0.48/0.91 (assume @p123 (forall (@list @t106 @t198 @t218 @t219) (=> (_ (_ @t107 @t198) @t218) (=> (_ (_ @t219 tptp.nil_poly_real) tptp.nil_list_poly_real) (=> (forall (@list @t206 @t221 @t205 @t220) (=> @t224 (=> @t223 (=> (_ (_ @t219 @t205) @t220) (_ (_ @t219 @t208) @t222))))) (_ (_ @t219 @t198) @t218)))))) % 0.48/0.91 (assume @p124 (forall (@list @t108 @t225 @t197 @t226) (=> (_ (_ @t109 @t225) @t197) (=> (_ (_ @t226 tptp.nil_list_poly_real) tptp.nil_poly_real) (=> (forall (@list @t228 @t202 @t227 @t201) (=> @t232 (=> @t231 (=> (_ (_ @t226 @t227) @t201) (_ (_ @t226 @t230) @t204))))) (_ (_ @t226 @t225) @t197)))))) % 0.48/0.91 (assume @p125 (forall (@list @t110 @t198 @t233 @t234) (=> (_ (_ @t111 @t198) @t233) (=> (_ (_ @t234 tptp.nil_poly_real) tptp.nil_Pr1492526187y_real) (=> (forall (@list @t206 @t236 @t205 @t235) (=> @t239 (=> @t238 (=> (_ (_ @t234 @t205) @t235) (_ (_ @t234 @t208) @t237))))) (_ (_ @t234 @t198) @t233)))))) % 0.48/0.91 (assume @p126 (forall (@list @t114 @t225 @t218 @t240) (=> (_ (_ @t115 @t225) @t218) (=> (_ @t247 tptp.nil_list_poly_real) (=> (forall @t246 (=> @t245 (=> @t244 @t243))) @t241))))) % 0.48/0.91 (assume @p127 (forall (@list @t112 @t248 @t197 @t249) (=> (_ (_ @t113 @t248) @t197) (=> (_ (_ @t249 tptp.nil_Pr1492526187y_real) tptp.nil_poly_real) (=> (forall (@list @t251 @t202 @t250 @t201) (=> @t255 (=> @t254 (=> (_ (_ @t249 @t250) @t201) (_ (_ @t249 @t253) @t204))))) (_ (_ @t249 @t248) @t197)))))) % 0.48/0.91 (assume @p128 (forall (@list @t116 @t198 @t256 @t257) (=> (_ (_ @t117 @t198) @t256) (=> (_ (_ @t257 tptp.nil_poly_real) tptp.nil_Pr1207979855y_real) (=> (forall (@list @t206 @t259 @t205 @t258) (=> @t262 (=> @t261 (=> (_ (_ @t257 @t205) @t258) (_ (_ @t257 @t208) @t260))))) (_ (_ @t257 @t198) @t256)))))) % 0.48/0.91 (assume @p129 (forall (@list @t120 @t225 @t233 @t263) (=> (_ (_ @t121 @t225) @t233) (=> (_ (_ @t263 tptp.nil_list_poly_real) tptp.nil_Pr1492526187y_real) (=> (forall (@list @t228 @t236 @t227 @t235) (=> @t265 (=> @t264 (=> (_ (_ @t263 @t227) @t235) (_ (_ @t263 @t230) @t237))))) (_ (_ @t263 @t225) @t233)))))) % 0.48/0.91 (assume @p130 (forall (@list @t118 @t248 @t218 @t266) (=> (_ (_ @t119 @t248) @t218) (=> (_ (_ @t266 tptp.nil_Pr1492526187y_real) tptp.nil_list_poly_real) (=> (forall (@list @t251 @t221 @t250 @t220) (=> @t268 (=> @t267 (=> (_ (_ @t266 @t250) @t220) (_ (_ @t266 @t253) @t222))))) (_ (_ @t266 @t248) @t218)))))) % 0.48/0.91 (assume @p131 (forall (@list @t122 @t269 @t197 @t270) (=> (_ (_ @t123 @t269) @t197) (=> (_ (_ @t270 tptp.nil_Pr1207979855y_real) tptp.nil_poly_real) (=> (forall (@list @t272 @t202 @t271 @t201) (=> @t276 (=> @t275 (=> (_ (_ @t270 @t271) @t201) (_ (_ @t270 @t274) @t204))))) (_ (_ @t270 @t269) @t197)))))) % 0.48/0.91 (assume @p132 (= tptp.listre1609905961y_real (lambda (@list @t279 @t286 @t283) (or (and @t290 @t289) (exists @t288 (and @t287 @t284 (_ (_ @t279 @t281) @t280) (_ (_ (_ tptp.listre1609905961y_real @t279) @t278) @t277))))))) % 0.48/0.91 (assume @p133 (= tptp.listre1793073465y_real (lambda (@list @t292 @t286 @t294) (or (and @t290 @t296) (exists (@list @t281 @t293 @t278 @t291) (and @t287 @t295 (_ (_ @t292 @t281) @t293) (_ (_ (_ tptp.listre1793073465y_real @t292) @t278) @t291))))))) % 0.48/0.91 (assume @p134 (= tptp.listre713353145y_real (lambda (@list @t298 @t300 @t283) (or (and @t302 @t289) (exists (@list @t299 @t280 @t297 @t277) (and @t301 @t284 (_ (_ @t298 @t299) @t280) (_ (_ (_ tptp.listre713353145y_real @t298) @t297) @t277))))))) % 0.48/0.91 (assume @p135 (= tptp.listre889482032y_real (lambda (@list @t304 @t286 @t306) (or (and @t290 @t308) (exists (@list @t281 @t305 @t278 @t303) (and @t287 @t307 (_ (_ @t304 @t281) @t305) (_ (_ (_ tptp.listre889482032y_real @t304) @t278) @t303))))))) % 0.48/0.91 (assume @p136 (= tptp.listre1763068361y_real (lambda (@list @t309 @t300 @t294) (or (and @t302 @t296) (exists @t310 (and @t301 @t295 (_ (_ @t309 @t299) @t293) (_ (_ (_ tptp.listre1763068361y_real @t309) @t297) @t291))))))) % 0.48/0.91 (assume @p137 (= tptp.listre1044472730y_real (lambda (@list @t312 @t314 @t283) (or (and @t316 @t289) (exists (@list @t313 @t280 @t311 @t277) (and @t315 @t284 (_ (_ @t312 @t313) @t280) (_ (_ (_ tptp.listre1044472730y_real @t312) @t311) @t277))))))) % 0.48/0.91 (assume @p138 (= tptp.listre471999892y_real (lambda (@list @t318 @t286 @t320) (or (and @t290 (= @t320 tptp.nil_Pr1207979855y_real)) (exists (@list @t281 @t319 @t278 @t317) (and @t287 @t321 (_ (_ @t318 @t281) @t319) (_ (_ (_ tptp.listre471999892y_real @t318) @t278) @t317))))))) % 0.48/0.91 (assume @p139 (= tptp.listre1037026976y_real (lambda (@list @t322 @t300 @t306) (or (and @t302 @t308) (exists (@list @t299 @t305 @t297 @t303) (and @t301 @t307 (_ (_ @t322 @t299) @t305) (_ (_ (_ tptp.listre1037026976y_real @t322) @t297) @t303))))))) % 0.48/0.91 (assume @p140 (= tptp.listre321577258y_real (lambda (@list @t323 @t314 @t294) (or (and @t316 @t296) (exists (@list @t313 @t293 @t311 @t291) (and @t315 @t295 (_ (_ @t323 @t313) @t293) (_ (_ (_ tptp.listre321577258y_real @t323) @t311) @t291))))))) % 0.48/0.91 (assume @p141 (= tptp.listre1751862142y_real (lambda (@list @t325 @t327 @t283) (or (and @t329 @t289) (exists (@list @t326 @t280 @t324 @t277) (and @t328 @t284 (_ (_ @t325 @t326) @t280) (_ (_ (_ tptp.listre1751862142y_real @t325) @t324) @t277))))))) % 0.48/0.91 (assume @p142 (forall (@list @t104 @t333 @t330) (=> (_ (_ @t105 @t333) @t330) (=> @t339 (not (forall @t335 (=> @t334 (forall @t332 (=> @t331 (=> @t214 (not @t213))))))))))) % 0.48/0.91 (assume @p143 (forall (@list @t106 @t333 @t340) (=> (_ (_ @t107 @t333) @t340) (=> (=> @t338 @t343) (not (forall (@list @t206 @t221 @t205) (=> @t334 (forall @t342 (=> @t341 (=> @t224 (not @t223))))))))))) % 0.48/0.91 (assume @p144 (forall (@list @t108 @t344 @t330) (=> (_ (_ @t109 @t344) @t330) (=> (=> @t346 @t337) (not (forall (@list @t228 @t202 @t227) (=> @t345 (forall @t332 (=> @t331 (=> @t232 (not @t231))))))))))) % 0.48/0.91 (assume @p145 (forall (@list @t110 @t333 @t347) (=> (_ (_ @t111 @t333) @t347) (=> (=> @t338 @t350) (not (forall (@list @t206 @t236 @t205) (=> @t334 (forall @t349 (=> @t348 (=> @t239 (not @t238))))))))))) % 0.48/0.91 (assume @p146 (forall (@list @t114 @t344 @t340) (=> (_ (_ @t115 @t344) @t340) (=> (=> @t346 @t343) (not (forall @t351 (=> @t345 (forall @t342 (=> @t341 (=> @t245 (not @t244))))))))))) % 0.48/0.91 (assume @p147 (forall (@list @t112 @t352 @t330) (=> (_ (_ @t113 @t352) @t330) (=> (=> @t354 @t337) (not (forall (@list @t251 @t202 @t250) (=> @t353 (forall @t332 (=> @t331 (=> @t255 (not @t254))))))))))) % 0.48/0.91 (assume @p148 (forall (@list @t116 @t333 @t355) (=> (_ (_ @t117 @t333) @t355) (=> (=> @t338 (not (= @t355 tptp.nil_Pr1207979855y_real))) (not (forall (@list @t206 @t259 @t205) (=> @t334 (forall @t357 (=> @t356 (=> @t262 (not @t261))))))))))) % 0.48/0.91 (assume @p149 (forall (@list @t120 @t344 @t347) (=> (_ (_ @t121 @t344) @t347) (=> (=> @t346 @t350) (not (forall (@list @t228 @t236 @t227) (=> @t345 (forall @t349 (=> @t348 (=> @t265 (not @t264))))))))))) % 0.48/0.91 (assume @p150 (forall (@list @t118 @t352 @t340) (=> (_ (_ @t119 @t352) @t340) (=> (=> @t354 @t343) (not (forall (@list @t251 @t221 @t250) (=> @t353 (forall @t342 (=> @t341 (=> @t268 (not @t267))))))))))) % 0.48/0.91 (assume @p151 (forall (@list @t122 @t358 @t330) (=> (_ (_ @t123 @t358) @t330) (=> (=> @t360 @t337) (not (forall (@list @t272 @t202 @t271) (=> @t359 (forall @t332 (=> @t331 (=> @t276 (not @t275))))))))))) % 0.48/0.91 (assume @p152 (forall (@list @t361 @t163 @t156) (=> (= (_ (_ tptp.splice2080530731y_real @t361) @t163) @t156) (=> (=> @t362 (not (= @t156 @t163))) (not (forall (@list @t228 @t227) (=> (= @t361 @t230) (not (= @t156 (_ @t229 (_ (_ tptp.splice2080530731y_real @t163) @t227))))))))))) % 0.48/0.91 (assume @p153 (forall (@list @t363 @t179 @t170) (=> (= (_ (_ tptp.splice1383748542y_real @t363) @t179) @t170) (=> (=> (= @t363 tptp.nil_Pr1492526187y_real) (not (= @t170 @t179))) (not (forall (@list @t251 @t250) (=> (= @t363 @t253) (not (= @t170 (_ @t252 (_ (_ tptp.splice1383748542y_real @t179) @t250))))))))))) % 0.48/0.91 (assume @p154 (forall (@list @t364 @t196 @t186) (=> (= (_ (_ tptp.splice1321784098y_real @t364) @t196) @t186) (=> (=> (= @t364 tptp.nil_Pr1207979855y_real) (not (= @t186 @t196))) (not (forall (@list @t272 @t271) (=> (= @t364 @t274) (not (= @t186 (_ @t273 (_ (_ tptp.splice1321784098y_real @t196) @t271))))))))))) % 0.48/0.91 (assume @p155 (forall (@list @t125 @t145 @t40) (=> (= (_ (_ tptp.splice_poly_real @t125) @t145) @t40) (=> (=> @t367 (not (= @t40 @t145))) (not (forall @t366 (=> @t365 (not (= @t40 (_ @t207 (_ (_ tptp.splice_poly_real @t145) @t205))))))))))) % 0.48/0.91 (assume @p156 (forall (@list @t93 @t225 @t218 @t240) (=> (_ (_ @t94 @t225) @t218) (=> (forall (@list @t372) (_ @t247 @t372)) (=> (forall @t246 (=> @t370 @t242)) (=> (forall @t246 (=> @t371 (=> @t369 (=> @t368 @t243)))) @t241)))))) % 0.48/0.91 (assume @p157 (forall (@list @t91 @t248 @t233 @t373) (=> (_ (_ @t92 @t248) @t233) (=> (forall (@list @t380) (_ (_ @t373 tptp.nil_Pr1492526187y_real) @t380)) (=> (forall @t379 (=> @t377 @t374)) (=> (forall @t379 (=> @t378 (=> @t376 (=> @t375 (=> (_ (_ @t373 @t250) @t235) @t374))))) (_ (_ @t373 @t248) @t233))))))) % 0.48/0.91 (assume @p158 (forall (@list @t95 @t269 @t256 @t381) (=> (_ (_ @t96 @t269) @t256) (=> (forall (@list @t388) (_ (_ @t381 tptp.nil_Pr1207979855y_real) @t388)) (=> (forall @t387 (=> @t385 @t382)) (=> (forall @t387 (=> @t386 (=> @t384 (=> @t383 (=> (_ (_ @t381 @t271) @t258) @t382))))) (_ (_ @t381 @t269) @t256))))))) % 0.48/0.91 (assume @p159 (forall (@list @t97 @t198 @t197 @t199) (=> (_ (_ @t98 @t198) @t197) (=> @t394 (=> (forall @t215 (=> @t391 @t210)) (=> (forall @t215 (=> @t392 (=> @t390 (=> @t389 @t212)))) @t200)))))) % 0.48/0.91 (assume @p160 (= tptp.lexord1324236152y_real (lambda (@list @t395 @t300 @t294) (or (exists (@list @t291) (and @t302 (= @t294 @t291))) (exists @t310 (and @t301 @t295 @t396)) (exists @t310 (and @t301 @t295 (not @t396) (not (_ (_ @t395 @t293) @t299)) (_ (_ (_ tptp.lexord1324236152y_real @t395) @t297) @t291))))))) % 0.48/0.91 (assume @p161 (= tptp.lexord834705585y_real (lambda (@list @t397 @t314 @t306) (or (exists (@list @t303) (and @t316 (= @t306 @t303))) (exists @t399 (and @t315 @t307 @t398)) (exists @t399 (and @t315 @t307 (not @t398) (not (_ (_ @t397 @t305) @t313)) (_ (_ (_ tptp.lexord834705585y_real @t397) @t311) @t303))))))) % 0.48/0.91 (assume @p162 (= tptp.lexord1053351061y_real (lambda (@list @t400 @t327 @t320) (or (exists (@list @t317) (and @t329 (= @t320 @t317))) (exists @t402 (and @t328 @t321 @t401)) (exists @t402 (and @t328 @t321 (not @t401) (not (_ (_ @t400 @t319) @t326)) (_ (_ (_ tptp.lexord1053351061y_real @t400) @t324) @t317))))))) % 0.48/0.91 (assume @p163 (= tptp.lexordp_eq_poly_real (lambda (@list @t403 @t286 @t283) (or (exists (@list @t277) (and @t290 (= @t283 @t277))) (exists @t288 (and @t287 @t284 @t404)) (exists @t288 (and @t287 @t284 (not @t404) (not (_ (_ @t403 @t280) @t281)) (_ (_ (_ tptp.lexordp_eq_poly_real @t403) @t278) @t277))))))) % 0.48/0.91 (assume @p164 (forall (@list @t93 @t344 @t340) (=> (_ (_ @t94 @t344) @t340) (=> (not @t346) (=> (forall (@list @t228) (=> (exists (@list @t227) @t345) (forall (@list @t221) (=> (exists @t342 @t341) @t371)))) (not (forall @t351 (=> @t345 (forall @t342 (=> @t341 (=> @t371 (=> @t369 (not @t368))))))))))))) % 0.48/0.91 (assume @p165 (forall (@list @t91 @t352 @t347) (=> (_ (_ @t92 @t352) @t347) (=> (not @t354) (=> (forall (@list @t251) (=> (exists (@list @t250) @t353) (forall (@list @t236) (=> (exists @t349 @t348) @t378)))) (not (forall (@list @t251 @t236 @t250) (=> @t353 (forall @t349 (=> @t348 (=> @t378 (=> @t376 (not @t375))))))))))))) % 0.48/0.91 (assume @p166 (forall (@list @t95 @t358 @t355) (=> (_ (_ @t96 @t358) @t355) (=> (not @t360) (=> (forall (@list @t272) (=> (exists (@list @t271) @t359) (forall (@list @t259) (=> (exists @t357 @t356) @t386)))) (not (forall (@list @t272 @t259 @t271) (=> @t359 (forall @t357 (=> @t356 (=> @t386 (=> @t384 (not @t383))))))))))))) % 0.48/0.91 (assume @p167 (forall (@list @t97 @t333 @t330) (=> (_ (_ @t98 @t333) @t330) (=> (not @t338) (=> (forall @t407 (=> (exists @t406 @t334) (forall @t405 (=> (exists @t332 @t331) @t392)))) (not (forall @t335 (=> @t334 (forall @t332 (=> @t331 (=> @t392 (=> @t390 (not @t389))))))))))))) % 0.48/0.91 (assume @p168 (forall (@list @t411 @t409 @t410 @t408) (= (= (_ (_ tptp.cons_list_poly_real @t411) @t409) (_ (_ tptp.cons_list_poly_real @t410) @t408)) (and (= @t411 @t410) (= @t409 @t408))))) % 0.48/0.91 (assume @p169 (forall (@list @t415 @t413 @t414 @t412) (= (= (_ (_ tptp.cons_P1027346459y_real @t415) @t413) (_ (_ tptp.cons_P1027346459y_real @t414) @t412)) (and (= @t415 @t414) (= @t413 @t412))))) % 0.48/0.91 (assume @p170 (forall (@list @t419 @t417 @t418 @t416) (= (= (_ (_ tptp.cons_P1129399039y_real @t419) @t417) (_ (_ tptp.cons_P1129399039y_real @t418) @t416)) (and (= @t419 @t418) (= @t417 @t416))))) % 0.48/0.91 (assume @p171 (forall (@list @t423 @t421 @t422 @t420) (= (= @t424 (_ (_ tptp.cons_poly_real @t422) @t420)) (and (= @t423 @t422) (= @t421 @t420))))) % 0.48/0.91 (assume @p172 (forall (@list @t93 @t125 @t61 @t40 @t76) (= (_ @t127 (_ (_ tptp.cons_list_poly_real @t40) @t76)) (or (_ (_ @t93 @t125) @t40) (and (not (_ (_ @t93 @t40) @t125)) (_ @t100 @t76)))))) % 0.48/0.91 (assume @p173 (forall (@list @t91 @t128 @t58 @t39 @t74) (= (_ @t130 (_ (_ tptp.cons_P1027346459y_real @t39) @t74)) (or (_ (_ @t91 @t128) @t39) (and (not (_ (_ @t91 @t39) @t128)) (_ @t99 @t74)))))) % 0.48/0.91 (assume @p174 (forall (@list @t95 @t131 @t64 @t42 @t78) (= (_ @t133 (_ (_ tptp.cons_P1129399039y_real @t42) @t78)) (or (_ (_ @t95 @t131) @t42) (and (not (_ (_ @t95 @t42) @t131)) (_ @t101 @t78)))))) % 0.48/0.91 (assume @p175 (forall (@list @t97 @t134 @t67 @t43 @t80) (= @t430 (or @t427 (and @t426 @t425))))) % 0.48/0.91 (assume @p176 (forall (@list @t13 @t125 @t61) (= (_ @t71 @t126) (or (_ @t13 @t125) (_ @t71 @t61))))) % 0.48/0.91 (assume @p177 (forall (@list @t11 @t128 @t58) (= (_ @t70 @t129) (or (_ @t11 @t128) (_ @t70 @t58))))) % 0.48/0.91 (assume @p178 (forall (@list @t15 @t131 @t64) (= (_ @t72 @t132) (or (_ @t15 @t131) (_ @t72 @t64))))) % 0.48/0.91 (assume @p179 (forall (@list @t17 @t134 @t67) (= (_ @t73 @t136) (or (_ @t17 @t134) (_ @t73 @t67))))) % 0.48/0.91 (assume @p180 (forall (@list @t432) (=> (not (= @t432 tptp.nil_li2088348750y_real)) (=> (forall (@list @t431) (not (= @t432 (_ (_ tptp.cons_l2022919326y_real tptp.nil_list_poly_real) @t431)))) (not (forall (@list @t228 @t227 @t431) (not (= @t432 (_ (_ tptp.cons_l2022919326y_real @t230) @t431))))))))) % 0.48/0.91 (assume @p181 (forall (@list @t434) (=> (not (= @t434 tptp.nil_li579690865y_real)) (=> (forall (@list @t433) (not (= @t434 (_ (_ tptp.cons_l730969377y_real tptp.nil_Pr1492526187y_real) @t433)))) (not (forall (@list @t251 @t250 @t433) (not (= @t434 (_ (_ tptp.cons_l730969377y_real @t253) @t433))))))))) % 0.48/0.91 (assume @p182 (forall (@list @t436) (=> (not (= @t436 tptp.nil_li1299462869y_real)) (=> (forall (@list @t435) (not (= @t436 (_ (_ tptp.cons_l677353093y_real tptp.nil_Pr1207979855y_real) @t435)))) (not (forall (@list @t272 @t271 @t435) (not (= @t436 (_ (_ tptp.cons_l677353093y_real @t274) @t435))))))))) % 0.48/0.91 (assume @p183 (forall (@list @t361) (=> (not @t362) (=> (forall (@list @t437) (not (= @t361 (_ @t438 @t437)))) (not (forall (@list @t206 @t205 @t437) (not (= @t361 (_ (_ tptp.cons_list_poly_real @t208) @t437))))))))) % 0.48/0.91 (assume @p184 (forall (@list @t125 @t61) (not (= @t126 @t61)))) % 0.48/0.91 (assume @p185 (forall (@list @t128 @t58) (not (= @t129 @t58)))) % 0.48/0.91 (assume @p186 (forall (@list @t131 @t64) (not (= @t132 @t64)))) % 0.48/0.91 (assume @p187 (forall @t439 (not (= @t136 @t67)))) % 0.48/0.91 (assume @p188 (forall (@list @t440 @t441) (= (_ (_ tptp.member403334290y_real @t440) (_ tptp.collec1459394516y_real @t441)) (_ @t441 @t440)))) % 0.48/0.91 (assume @p189 (forall (@list @t442 @t15) (= (_ (_ tptp.member1784523250y_real @t442) (_ tptp.collec329281332y_real @t15)) (_ @t15 @t442)))) % 0.48/0.91 (assume @p190 (forall (@list @t443 @t17) (= (_ (_ tptp.member_poly_real2 @t443) (_ tptp.collect_poly_real @t17)) (_ @t17 @t443)))) % 0.48/0.91 (assume @p191 (forall (@list @t444 @t13) (= (_ (_ tptp.member708095579y_real @t444) (_ tptp.collec1537941401y_real @t13)) (_ @t13 @t444)))) % 0.48/0.91 (assume @p192 (forall (@list @t445) (= (_ tptp.collec1459394516y_real (lambda (@list @t446) (_ (_ tptp.member403334290y_real @t446) @t445))) @t445))) % 0.48/0.91 (assume @p193 (forall (@list @t447) (= (_ tptp.collec329281332y_real (lambda (@list @t326) (_ (_ tptp.member1784523250y_real @t326) @t447))) @t447))) % 0.48/0.91 (assume @p194 (forall (@list @t448) (= (_ tptp.collect_poly_real (lambda (@list @t281) (_ (_ tptp.member_poly_real2 @t281) @t448))) @t448))) % 0.48/0.91 (assume @p195 (forall (@list @t449) (= (_ tptp.collec1537941401y_real (lambda (@list @t299) (_ (_ tptp.member708095579y_real @t299) @t449))) @t449))) % 0.48/0.91 (assume @p196 (forall @t455 (=> @t454 (=> (forall @t453 (=> (_ @t13 @t201) (_ @t13 @t452))) @t451)))) % 0.48/0.91 (assume @p197 (forall @t457 (=> @t456 (not (forall @t453 (not (= @t125 @t452))))))) % 0.48/0.91 (assume @p198 (forall (@list @t459 @t458 @t344 @t355) (=> (forall (@list @t461 @t388) (_ (_ @t462 tptp.nil_list_poly_real) @t388)) (=> (forall (@list @t461 @t158 @t160 @t460) (=> (_ (_ @t462 @t160) (_ (_ tptp.cons_P1129399039y_real (_ @t461 @t158)) @t460)) (_ (_ @t462 @t162) @t460))) (_ (_ (_ @t459 @t458) @t344) @t355))))) % 0.48/0.91 (assume @p199 (forall (@list @t464 @t463 @t352 @t355) (=> (forall (@list @t465 @t388) (_ (_ @t466 tptp.nil_Pr1492526187y_real) @t388)) (=> (forall (@list @t465 @t174 @t176 @t460) (=> (_ (_ @t466 @t176) (_ (_ tptp.cons_P1129399039y_real (_ @t465 @t174)) @t460)) (_ (_ @t466 @t178) @t460))) (_ (_ (_ @t464 @t463) @t352) @t355))))) % 0.48/0.91 (assume @p200 (forall (@list @t468 @t467 @t358 @t355) (=> (forall (@list @t469 @t388) (_ (_ @t470 tptp.nil_Pr1207979855y_real) @t388)) (=> (forall (@list @t469 @t191 @t193 @t460) (=> (_ (_ @t470 @t193) (_ (_ tptp.cons_P1129399039y_real (_ @t469 @t191)) @t460)) (_ (_ @t470 @t195) @t460))) (_ (_ (_ @t468 @t467) @t358) @t355))))) % 0.48/0.91 (assume @p201 (forall (@list @t472 @t471 @t333 @t330) (=> (forall (@list @t474 @t393) (_ (_ @t475 tptp.nil_poly_real) @t393)) (=> (forall (@list @t474 @t139 @t141 @t473) (=> (_ (_ @t475 @t141) (_ (_ tptp.cons_poly_real (_ @t474 @t139)) @t473)) (_ (_ @t475 @t144) @t473))) (_ (_ (_ @t472 @t471) @t333) @t330))))) % 0.48/0.91 (assume @p202 (forall @t483 (=> @t482 (=> @t481 (=> (forall @t366 (=> @t479 (=> @t478 @t477))) @t476))))) % 0.48/0.91 (assume @p203 (forall @t495 (=> @t494 (=> (forall @t492 (_ @t490 @t480)) (=> (forall @t491 (=> (_ @t490 @t487) (_ @t490 @t488))) @t486))))) % 0.48/0.91 (assume @p204 (forall @t455 (=> @t454 (=> @t481 (=> (forall @t335 (=> (=> @t496 @t477) (=> (=> @t497 (_ @t13 @t487)) (_ @t13 @t488)))) @t451))))) % 0.48/0.91 (assume @p205 (forall @t495 (=> @t494 (=> (forall @t498 (=> (_ @t490 @t201) (_ @t490 @t452))) @t486)))) % 0.48/0.91 (assume @p206 (forall @t457 (=> @t456 (=> (forall @t407 (not (= @t125 @t480))) (not (forall @t335 (not (= @t125 @t488)))))))) % 0.48/0.91 (assume @p207 (forall @t503 (=> @t394 (=> @t502 (=> (forall @t501 (=> (_ @t211 @t204) (=> @t500 @t210))) @t499))))) % 0.48/0.91 (assume @p208 (forall @t455 (=> (forall @t366 (=> (forall (@list @t505 @t504) (=> (= @t205 (_ (_ tptp.cons_poly_real @t505) @t504)) @t478)) @t477)) (=> @t454 @t451)))) % 0.48/0.91 (assume @p209 (forall @t457 (=> (forall @t366 (not @t365)) @t367))) % 0.48/0.91 (assume @p210 (forall @t508 (=> @t454 (=> @t481 (=> (forall (@list @t206 @t202 @t506) (=> (_ @t13 @t506) (=> (_ @t13 @t507) (_ @t13 (_ @t207 @t507))))) @t476))))) % 0.48/0.91 (assume @p211 (forall @t503 (=> @t394 (=> (forall @t509 (=> (_ (_ @t199 @t201) @t205) @t500)) @t499)))) % 0.48/0.91 (assume @p212 (forall (@list @t199 @t67 @t80) (=> @t217 (=> (forall @t366 (_ @t209 tptp.nil_poly_real)) (=> @t513 (=> @t511 @t510)))))) % 0.48/0.91 (assume @p213 (forall @t69 (= @t482 (exists @t515 @t514)))) % 0.48/0.91 (assume @p214 (forall (@list @t13 @t516) (=> @t454 (=> (forall (@list @t518 @t517) (=> (_ @t13 @t517) (_ @t13 (_ (_ tptp.cons_poly_real @t518) @t517)))) (_ @t13 @t516))))) % 0.48/0.91 (assume @p215 (forall @t41 (=> (not (= @t40 tptp.nil_poly_real)) (not (forall (@list @t520 @t519) (not (= @t40 (_ (_ tptp.cons_poly_real @t520) @t519)))))))) % 0.48/0.91 (assume @p216 (forall (@list @t516 @t423 @t421) (=> (= @t516 @t424) (not (= @t516 tptp.nil_poly_real))))) % 0.48/0.91 (assume @p217 (forall (@list @t423 @t421) (not (= tptp.nil_poly_real @t424)))) % 0.48/0.91 (assume @p218 (forall @t521 (=> (not @t427) (=> @t426 (=> @t425 @t430))))) % 0.48/0.91 (assume @p219 (forall @t521 (=> @t427 @t430))) % 0.48/0.91 (assume @p220 (forall @t522 (= (_ (_ tptp.splice_poly_real @t136) @t80) (_ @t135 (_ (_ tptp.splice_poly_real @t80) @t67))))) % 0.48/0.91 (assume @p221 (forall (@list @t104 @t134 @t43 @t67 @t80) (=> (_ (_ @t104 @t134) @t43) (=> (_ (_ @t105 @t67) @t80) (_ (_ @t105 @t136) @t429))))) % 0.48/0.91 (assume @p222 (forall @t9 (=> @t8 (not (forall (@list @t524 @t523) (not (= @t1 (_ (_ tptp.cons_poly_real @t7) (_ (_ tptp.cons_poly_real @t524) @t523))))))))) % 0.48/0.91 (assume @p223 (forall (@list @t89 @t443 @t525 @t88) (= (_ (_ @t90 (_ @t526 @t525)) @t88) (_ (_ @t90 @t525) (_ (_ tptp.cons_poly_real (_ @t89 @t443)) @t88))))) % 0.48/0.91 (assume @p224 (forall @t439 (not (_ tptp.null_poly_real @t136)))) % 0.48/0.91 (assume @p225 (forall (@list @t134 @t67 @t43) (= (_ (_ tptp.member_poly_real @t136) @t43) (or @t527 (_ (_ tptp.member_poly_real @t67) @t43))))) % 0.48/0.91 (assume @p226 (forall @t84 (= (= @t528 tptp.nil_Pr1207979855y_real) (or @t68 @t81)))) % 0.48/0.91 (assume @p227 (forall @t503 (=> @t511 (=> @t502 (=> @t513 @t499))))) % 0.48/0.91 (assume @p228 (forall @t503 (=> @t502 (=> (forall @t532 (_ @t216 @t531)) (=> @t511 @t499))))) % 0.48/0.91 (assume @p229 (forall (@list @t134) (= (_ (_ tptp.insert_poly_real @t134) tptp.nil_poly_real) @t533))) % 0.48/0.91 (assume @p230 (forall @t439 (not (_ (_ tptp.ord_le1233681790y_real @t136) tptp.nil_poly_real)))) % 0.48/0.91 (assume @p231 (forall @t439 (= (_ tptp.rotate1_poly_real @t136) @t535))) % 0.48/0.91 (assume @p232 (forall (@list @t134 @t67 @t19) (= (_ (_ tptp.bind_p420216945y_real @t136) @t19) (_ @t536 (_ (_ tptp.bind_p420216945y_real @t67) @t19))))) % 0.48/0.91 (assume @p233 (forall @t538 (= (_ @t46 @t136) (_ (_ tptp.gen_length_poly_real @t537) @t67)))) % 0.48/0.91 (assume @p234 (forall @t69 (= (_ @t534 tptp.nil_poly_real) @t67))) % 0.48/0.91 (assume @p235 (forall @t84 (= (= @t539 @t67) @t81))) % 0.48/0.91 (assume @p236 (forall @t84 (= (= @t67 @t539) @t81))) % 0.48/0.91 (assume @p237 (forall @t84 (= (= @t539 @t80) @t68))) % 0.48/0.91 (assume @p238 (forall @t540 (= (= @t80 @t539) @t68))) % 0.48/0.91 (assume @p239 (forall @t84 (= (= tptp.nil_poly_real @t539) @t82))) % 0.48/0.91 (assume @p240 (forall @t84 (= (= @t539 tptp.nil_poly_real) @t82))) % 0.48/0.91 (assume @p241 (forall @t541 (= (_ (_ tptp.append_poly_real @t444) tptp.nil_poly_real) @t444))) % 0.48/0.91 (assume @p242 (forall @t69 (= (_ (_ tptp.ord_le1233681790y_real @t67) tptp.nil_poly_real) @t68))) % 0.48/0.91 (assume @p243 (forall @t124 (_ (_ tptp.ord_le1233681790y_real tptp.nil_poly_real) @t80))) % 0.48/0.91 (assume @p244 (forall (@list @t67 @t134 @t80 @t43) (= (= @t535 @t544) (and @t542 @t527)))) % 0.48/0.91 (assume @p245 (forall (@list @t134 @t548 @t80 @t67 @t545) (=> (= (_ @t135 @t548) @t80) (=> (= @t67 (_ (_ tptp.append_poly_real @t548) @t545)) @t547)))) % 0.48/0.91 (assume @p246 (forall @t522 (= (_ (_ tptp.append_poly_real @t136) @t80) (_ @t135 @t539)))) % 0.48/0.91 (assume @p247 (forall @t84 (=> @t542 (= @t67 @t550)))) % 0.48/0.91 (assume @p248 (forall @t124 (= @t550 @t80))) % 0.48/0.91 (assume @p249 (forall @t541 (= (_ @t549 @t444) @t444))) % 0.48/0.91 (assume @p250 (forall @t508 (=> @t454 (=> (forall @t366 @t551) @t476)))) % 0.48/0.91 (assume @p251 (forall @t69 (=> @t482 (not (forall (@list @t201 @t202) (not (= @t67 (_ (_ tptp.append_poly_real @t201) @t552)))))))) % 0.48/0.91 (assume @p252 (forall (@list @t134 @t67 @t80 @t545) (= @t547 (or (and @t81 (= @t136 @t545)) (exists @t556 (and (= @t555 @t80) (= @t67 @t554))))))) % 0.48/0.91 (assume @p253 (forall (@list @t80 @t545 @t134 @t67) (= (= @t546 @t136) (or (and @t81 (= @t545 @t136)) (exists @t556 (and (= @t80 @t555) (= @t554 @t67))))))) % 0.48/0.91 (assume @p254 (forall @t483 (=> @t482 (=> @t481 (=> (forall @t366 (=> @t479 @t551)) @t476))))) % 0.48/0.91 (assume @p255 (forall (@list @t19 @t134 @t67) (= (_ @t47 @t136) (_ @t536 (_ @t47 @t67))))) % 0.48/0.91 (assume @p256 (forall (@list @t558 @t557) (= (= (_ tptp.suc @t558) (_ tptp.suc @t557)) (= @t558 @t557)))) % 0.48/0.91 (assume @p257 (forall (@list @t560 @t559) (= (= (_ tptp.suc @t560) (_ tptp.suc @t559)) (= @t560 @t559)))) % 0.48/0.91 (assume @p258 (= (_ tptp.produc523415045y_real tptp.nil_list_poly_real) @t561)) % 0.48/0.91 (assume @p259 (= (_ tptp.subseqs_poly_real tptp.nil_poly_real) @t561)) % 0.48/0.91 (assume @p260 (forall (@list @t565 @t80 @t545) (= (= (_ tptp.concat_poly_real @t565) @t546) (and (=> @t566 (and @t81 (= @t545 tptp.nil_poly_real))) (=> (not @t566) (exists (@list @t564 @t278 @t563 @t562) (and (= @t565 (_ (_ tptp.append527544425y_real @t564) (_ (_ tptp.cons_list_poly_real (_ (_ tptp.append_poly_real @t278) @t563)) @t562))) (= @t80 (_ (_ tptp.append_poly_real (_ tptp.concat_poly_real @t564)) @t278)) (= @t545 (_ (_ tptp.append_poly_real @t563) (_ tptp.concat_poly_real @t562)))))))))) % 0.48/0.91 (assume @p261 (= (_ tptp.concat_poly_real tptp.nil_list_poly_real) tptp.nil_poly_real)) % 0.48/0.91 (assume @p262 (forall (@list @t568 @t567) (=> (= (_ tptp.suc @t568) (_ tptp.suc @t567)) (= @t568 @t567)))) % 0.48/0.91 (assume @p263 (forall @t45 (not (= @t44 @t537)))) % 0.48/0.91 (assume @p264 (forall @t569 (= (_ tptp.butlast_poly_real @t535) @t67))) % 0.48/0.91 (assume @p265 (forall @t538 (= (_ @t85 @t136) (_ (_ tptp.cons_P1027346459y_real (_ (_ tptp.produc404352541y_real @t44) @t134)) (_ (_ tptp.enumerate_poly_real @t537) @t67))))) % 0.48/0.91 (assume @p266 (forall @t569 (= (_ tptp.last_poly_real @t535) @t134))) % 0.48/0.91 (assume @p267 (forall (@list @t571 @t570) (= (_ (_ tptp.plus_c288199817y_real tptp.nil_poly_real) @t572) @t572))) % 0.48/0.91 (assume @p268 (forall @t540 @t575)) % 0.48/0.91 (assume @p269 (forall @t540 @t578)) % 0.48/0.91 (assume @p270 (forall (@list @t134 @t67 @t43 @t80) (= (_ (_ tptp.zip_po657915297y_real @t136) @t429) (_ (_ tptp.cons_P1129399039y_real @t580) @t528)))) % 0.48/0.91 (assume @p271 (forall @t69 (=> @t482 (= (_ (_ tptp.append_poly_real @t581) (_ (_ tptp.cons_poly_real @t573) tptp.nil_poly_real)) @t67)))) % 0.48/0.91 (assume @p272 (= (_ tptp.butlast_poly_real tptp.nil_poly_real) tptp.nil_poly_real)) % 0.48/0.91 (assume @p273 (forall (@list @t67 @t134 @t80) (= (= @t535 @t80) (and @t577 (= @t582 @t67) (= @t576 @t134))))) % 0.48/0.91 (assume @p274 (forall @t569 (and @t585 @t584))) % 0.48/0.91 (assume @p275 (forall @t569 @t585)) % 0.48/0.91 (assume @p276 (forall @t569 @t584)) % 0.48/0.91 (assume @p277 (forall (@list @t67 @t80 @t591 @t588) (=> (= @t528 (_ (_ tptp.cons_P1129399039y_real @t591) @t588)) (not (forall (@list @t206 @t587) (=> (= @t67 (_ @t207 @t587)) (forall (@list @t202 @t586) (=> (= @t80 (_ @t203 @t586)) (=> (= @t591 @t590) (not (= @t588 (_ (_ tptp.zip_po657915297y_real @t587) @t586)))))))))))) % 0.48/0.91 (assume @p278 (forall @t69 (= (_ (_ tptp.plus_c288199817y_real @t67) tptp.nil_poly_real) @t67))) % 0.48/0.91 (assume @p279 (forall @t540 (and @t575 @t578))) % 0.48/0.91 (assume @p280 (forall @t84 (exists (@list @t592 @t587 @t586) (and (= @t67 (_ (_ tptp.append_poly_real @t587) @t592)) (= @t80 (_ (_ tptp.append_poly_real @t586) @t592)) (or (= @t587 tptp.nil_poly_real) (= @t586 tptp.nil_poly_real) (not (= (_ tptp.last_poly_real @t587) (_ tptp.last_poly_real @t586)))))))) % 0.48/0.91 (assume @p281 (forall @t569 (and (=> @t68 (= @t593 tptp.nil_poly_real)) (=> @t482 (= @t593 (_ @t135 @t581)))))) % 0.48/0.91 (assume @p282 (forall @t540 (and (=> @t81 (= @t594 @t581)) (=> @t577 (= @t594 (_ @t534 @t582)))))) % 0.48/0.91 (assume @p283 (forall (@list @t67 @t134 @t80 @t43 @t595) (= (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t535) @t544)) @t597) (or (and @t600 @t527) (and @t542 @t596))))) % 0.48/0.91 (assume @p284 (forall @t84 (=> @t482 (=> @t577 (=> @t603 (= (_ tptp.last_P21901160y_real @t528) (_ (_ tptp.produc1867601537y_real @t573) @t576))))))) % 0.48/0.91 (assume @p285 (forall @t604 (= (= (_ (_ tptp.rotate_poly_real @t44) @t67) tptp.nil_poly_real) @t68))) % 0.48/0.91 (assume @p286 (forall @t607 (= (_ @t606 @t597) (or (and @t596 @t542) (and @t527 @t600))))) % 0.48/0.91 (assume @p287 (forall @t609 (not (_ @t608 @t597)))) % 0.48/0.91 (assume @p288 (forall @t609 (not (_ @t611 @t597)))) % 0.48/0.91 (assume @p289 (forall (@list @t67 @t80 @t595 @t134) (=> @t600 (_ (_ tptp.member403334290y_real (_ @t605 (_ @t135 @t80))) @t597)))) % 0.48/0.91 (assume @p290 (forall @t615 (=> @t614 (=> (forall @t492 (not (= @t613 (_ @t612 @t480)))) (not (forall @t491 (not (= @t613 (_ @t612 @t488))))))))) % 0.48/0.91 (assume @p291 (forall @t615 (=> @t614 (not (forall @t498 (not (= @t613 (_ @t612 @t452)))))))) % 0.48/0.91 (assume @p292 (forall @t604 (= (= @t537 @t602) @t616))) % 0.48/0.91 (assume @p293 (forall (@list @t67 @t44) (= (= @t602 @t537) @t616))) % 0.48/0.91 (assume @p294 (forall (@list @t67 @t80 @t545 @t617 @t618) (=> @t603 (=> @t628 (=> (= @t627 (_ tptp.size_s259235672y_real @t617)) (=> (_ (_ (_ (_ @t618 tptp.nil_poly_real) tptp.nil_poly_real) tptp.nil_poly_real) tptp.nil_poly_real) (=> (forall (@list @t206 @t205 @t202 @t201 @t621 @t506 @t620 @t619) (=> @t626 (=> @t625 (=> (= @t623 (_ tptp.size_s259235672y_real @t619)) (=> (_ (_ (_ (_ @t618 @t205) @t201) @t506) @t619) (_ (_ (_ (_ @t618 @t208) @t204) @t622) (_ (_ tptp.cons_poly_real @t620) @t619))))))) (_ (_ (_ (_ @t618 @t67) @t80) @t545) @t617)))))))) % 0.48/0.91 (assume @p295 (forall (@list @t67 @t80 @t545 @t629) (=> @t603 (=> @t628 (=> (_ (_ (_ @t629 tptp.nil_poly_real) tptp.nil_poly_real) tptp.nil_poly_real) (=> (forall (@list @t206 @t205 @t202 @t201 @t621 @t506) (=> @t626 (=> @t625 (=> (_ (_ (_ @t629 @t205) @t201) @t506) (_ (_ (_ @t629 @t208) @t204) @t622))))) (_ (_ (_ @t629 @t67) @t80) @t545))))))) % 0.48/0.91 (assume @p296 (forall (@list @t67 @t80 @t199) (=> @t603 (=> @t217 (=> (forall @t501 (=> @t626 @t212)) @t510))))) % 0.48/0.91 (assume @p297 (forall (@list @t632) (=> (forall (@list @t630 @t206 @t205) (not (= @t632 (_ @t631 @t208)))) (not (forall (@list @t630) (not (= @t632 (_ @t631 tptp.nil_poly_real)))))))) % 0.48/0.91 (assume @p298 (forall @t640 (=> @t639 (=> @t638 @t636)))) % 0.48/0.91 (assume @p299 (forall @t640 (=> @t638 (=> (forall @t532 (not (= @t634 (_ @t610 @t531)))) @t636)))) % 0.48/0.91 (assume @p300 (forall @t640 (=> @t635 (=> @t638 (not (forall @t512 (not (= @t634 (_ @t610 @t204))))))))) % 0.48/0.91 (assume @p301 (forall @t644 (=> (_ @t643 @t597) (=> (forall @t407 (=> (= @t67 (_ @t207 @t80)) (not @t642))) (not (forall @t641 (=> (= @t67 (_ @t428 @t506)) (not (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t506) @t80)) @t597))))))))) % 0.48/0.91 (assume @p302 (forall (@list @t134 @t67 @t80 @t595) (=> (_ (_ tptp.member403334290y_real (_ @t605 @t80)) @t597) (=> (forall @t405 (=> (= @t80 (_ @t203 @t67)) (not (_ (_ tptp.member1784523250y_real (_ @t579 @t202)) @t595)))) (not (forall @t641 (=> (= @t80 (_ @t135 @t506)) (not (_ (_ tptp.member403334290y_real (_ @t598 @t506)) @t597))))))))) % 0.48/0.91 (assume @p303 (forall (@list @t134 @t43 @t595 @t67) (=> @t596 (_ (_ tptp.member403334290y_real (_ @t605 (_ @t428 @t67))) @t597)))) % 0.48/0.91 (assume @p304 (forall @t84 (=> (not @t542) (=> @t603 (exists (@list @t645 @t206 @t587 @t202 @t586) (and @t497 (= @t67 (_ @t646 (_ (_ tptp.append_poly_real @t480) @t587))) (= @t80 (_ @t646 (_ (_ tptp.append_poly_real @t552) @t586))))))))) % 0.48/0.91 (assume @p305 (forall (@list @t67 @t80 @t595) (=> @t600 (not (forall (@list @t206 @t202) (=> @t650 (forall (@list @t648 @t647) (=> (= @t67 (_ @t649 (_ @t207 @t647))) (not (= @t80 (_ @t649 (_ @t203 @t647)))))))))))) % 0.48/0.91 (assume @p306 (forall (@list @t134 @t43 @t595 @t67 @t652 @t651 @t80) (=> @t596 (=> (= @t67 (_ @t653 (_ @t135 @t651))) (=> (= @t80 (_ @t653 (_ @t428 @t651))) @t600))))) % 0.48/0.91 (assume @p307 (forall @t569 (= (_ tptp.size_s259235672y_real @t535) @t654))) % 0.48/0.91 (assume @p308 (forall @t640 (=> @t639 (not (forall @t509 (not (= @t634 (_ @t633 @t201)))))))) % 0.48/0.91 (assume @p309 (forall @t439 (= (_ tptp.size_s259235672y_real @t136) @t654))) % 0.48/0.91 (assume @p310 (forall @t607 (= (_ @t606 @t655) (or (and @t596 @t603) (and @t527 (_ @t599 @t655)))))) % 0.48/0.91 (assume @p311 (forall @t609 (not (_ @t608 @t655)))) % 0.48/0.91 (assume @p312 (forall (@list @t80 @t595) (not (_ (_ tptp.member403334290y_real (_ @t610 @t80)) @t655)))) % 0.48/0.91 (assume @p313 (forall (@list @t657 @t656 @t659) (=> @t663 @t660))) % 0.48/0.91 (assume @p314 (forall (@list @t659 @t657 @t656) (=> @t660 @t663))) % 0.48/0.91 (assume @p315 (forall (@list @t656 @t657) (=> (_ @t665 @t656) (=> (_ @t662 (_ @t661 tptp.nil_poly_real)) (_ @t665 @t664))))) % 0.48/0.91 (assume @p316 (forall (@list @t656 @t657 @t659) (= (_ (_ tptp.bNF_Gr1644259033y_real @t664) @t659) (_ @t661 @t666)))) % 0.48/0.91 (assume @p317 (forall (@list @t659 @t656 @t657) (=> (_ (_ tptp.member708095579y_real @t659) @t664) (_ (_ tptp.member708095579y_real @t666) @t656)))) % 0.48/0.91 (assume @p318 (forall (@list @t668 @t667 @t44) (= (= (_ @t669 @t667) (_ @t669 @t44)) (= @t667 @t44)))) % 0.48/0.91 (assume @p319 (forall (@list @t443 @t671 @t595 @t673 @t125 @t40) (=> @t676 (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real (_ @t674 @t675)) (_ @t674 @t672))) @t670)))) % 0.48/0.91 (assume @p320 (forall (@list @t198 @t197 @t595 @t199) (=> (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t198) @t197)) @t677) (=> @t217 (=> (forall @t215 (=> @t650 (=> @t678 @t212))) @t200))))) % 0.48/0.91 (assume @p321 (forall (@list @t443 @t125 @t671 @t40 @t595) (= (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t675) @t672)) @t670) (or @t676 (and (= @t443 @t671) (_ (_ tptp.member403334290y_real (_ @t679 @t40)) @t670)))))) % 0.48/0.91 (assume @p322 (forall (@list @t40 @t595) (= (_ (_ tptp.member403334290y_real (_ @t610 @t40)) @t670) (exists (@list @t680 @t299) (= @t40 (_ (_ tptp.cons_poly_real @t680) @t299)))))) % 0.48/0.91 (assume @p323 (forall (@list @t125 @t595) (not (_ (_ tptp.member403334290y_real (_ @t679 tptp.nil_poly_real)) @t670)))) % 0.48/0.91 (assume @p324 (forall @t609 (=> (_ @t608 @t677) @t68))) % 0.48/0.91 (assume @p325 (forall @t609 (=> (_ @t611 @t677) @t68))) % 0.48/0.91 (assume @p326 (forall (@list @t595) (_ (_ tptp.member403334290y_real (_ @t610 tptp.nil_poly_real)) @t677))) % 0.48/0.91 (assume @p327 (forall @t644 (=> (_ @t643 @t677) (not (forall @t366 (=> (= @t67 @t208) (=> @t642 (not (_ (_ tptp.member403334290y_real (_ @t637 @t80)) @t677))))))))) % 0.48/0.91 (assume @p328 (forall (@list @t43 @t80 @t67 @t595) (=> (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t429) @t67)) @t677) (not (forall @t512 (=> (= @t67 @t204) (=> (_ (_ tptp.member1784523250y_real (_ (_ tptp.produc1867601537y_real @t43) @t202)) @t595) (not (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t80) @t201)) @t677))))))))) % 0.48/0.91 (assume @p329 (forall (@list @t134 @t43 @t595 @t67 @t80) (=> @t596 (=> (_ @t599 @t677) (_ @t606 @t677))))) % 0.48/0.91 (assume @p330 (forall (@list @t40 @t125 @t595) (=> (exists (@list @t682 @t681) (= @t40 (_ (_ tptp.cons_poly_real @t682) @t681))) (_ (_ tptp.member403334290y_real (_ @t679 (_ (_ tptp.append_poly_real @t125) @t40))) @t670)))) % 0.48/0.91 (assume @p331 (forall @t684 (=> @t683 (=> @t339 (not (forall @t335 (=> @t334 (forall @t332 (=> @t331 (=> @t650 (not @t678))))))))))) % 0.48/0.91 (assume @p332 (forall @t684 (= @t683 (or (and @t338 @t336) (exists @t288 (and (= @t333 @t285) (= @t330 @t282) (_ (_ tptp.member1784523250y_real (_ (_ tptp.produc1867601537y_real @t281) @t280)) @t595) (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t278) @t277)) @t677))))))) % 0.48/0.91 (assume @p333 (forall @t152 (=> @t151 (=> (_ @t686 (_ @t685 (_ (_ tptp.produc1000427809y_real @t145) @t138))) (=> (=> @t150 (=> @t148 (not (_ @t686 (_ @t685 (_ @t610 @t138)))))) (not (forall @t147 (=> @t146 (=> @t143 (not (_ @t686 (_ @t685 (_ (_ tptp.produc1000427809y_real @t144) @t138))))))))))))) % 0.48/0.91 (assume @p334 (forall @t689 (= (_ (_ tptp.member403334290y_real (_ @t610 @t687)) @t688) (not (= @t687 tptp.nil_poly_real))))) % 0.48/0.91 (assume @p335 (forall @t689 (not (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t687) tptp.nil_poly_real)) @t688)))) % 0.48/0.91 (assume @p336 (forall (@list @t692 @t690 @t691 @t687 @t595) (= (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real (_ (_ tptp.cons_poly_real @t692) @t690)) (_ (_ tptp.cons_poly_real @t691) @t687))) @t688) (or (_ (_ tptp.ord_less_nat @t694) @t693) (and (= @t694 @t693) (_ (_ tptp.member1784523250y_real (_ (_ tptp.produc1867601537y_real @t692) @t691)) @t595)) (and (= @t692 @t691) (_ (_ tptp.member403334290y_real (_ (_ tptp.produc1000427809y_real @t690) @t687)) @t688)))))) % 0.48/0.91 (assume @p337 (forall @t697 (= @t696 @t695))) % 0.48/0.91 (assume @p338 (forall @t697 (=> @t695 @t696))) % 0.48/0.91 (assume @p339 (forall @t45 (_ (_ tptp.ord_less_nat @t44) @t537))) % 0.48/0.91 (assume @p340 (forall (@list @t89 @t444) (= (= (_ @t698 @t444) tptp.nil_poly_real) (= @t444 tptp.nil_poly_real)))) % 0.48/0.91 (assume @p341 (forall @t700 (= (= @t699 tptp.nil_poly_real) @t68))) % 0.48/0.91 (assume @p342 (forall @t700 (= (= tptp.nil_poly_real @t699) @t68))) % 0.48/0.91 (assume @p343 (not (not @t701))) % 0.48/0.91 (assume @p344 true) % 0.48/0.91 (step @p345 (= tptp.sturm_1664866327rm_seq @t704) :rule refl :args (@t704)) % 0.48/0.91 (step @p346 (= tptp.concat_poly_real @t706) :rule refl :args (@t706)) % 0.48/0.91 (step @p347 :rule aci_norm :args ((= (or @t708 false) @t708))) % 0.48/0.91 (step @p348 :rule evaluate :args ((not true))) % 0.48/0.91 (step @p349 :rule eq-refl :args (tptp.nil_poly_real)) % 0.48/0.91 (step @p350 :rule cong :premises (@p349) :args (@t709)) % 0.48/0.91 (step @p351 :rule trans :premises (@p350 @p348)) % 0.48/0.91 (step @p352 :rule refl :args (@t708)) % 0.48/0.91 (step @p353 :rule nary_cong :premises (@p352 @p351) :args (@t710)) % 0.48/0.91 (step @p354 :rule trans :premises (@p353 @p347)) % 0.48/0.91 (step @p355 :rule quant-var-elim-eq :args ((= (forall @t5 (or @t2 @t713 @t711)) @t710))) % 0.48/0.91 (step @p356 :rule refl :args (@t711)) % 0.48/0.91 (step @p357 :rule refl :args (@t713)) % 0.48/0.91 (step @p358 :rule eq-symm :args (tptp.nil_poly_real @t1)) % 0.48/0.91 (step @p359 :rule cong :premises (@p358) :args (@t711)) % 0.48/0.91 (step @p360 :rule nary_cong :premises (@p359 @p357 @p356) :args (@t714)) % 0.48/0.91 (step @p361 :rule aci_norm :args ((= @t715 @t714))) % 0.48/0.91 (step @p362 :rule trans :premises (@p361 @p360)) % 0.48/0.91 (step @p363 :rule cong :premises (@p362) :args ((forall @t5 @t715))) % 0.48/0.91 (step @p364 :rule trans :premises (@p363 @p355)) % 0.48/0.91 (step @p365 :rule trans :premises (@p364 @p354)) % 0.48/0.91 (step @p366 :rule refl :args (@t712)) % 0.48/0.91 (step @p367 :rule refl :args (@t3)) % 0.48/0.91 (step @p368 :rule cong :premises (@p367 @p366) :args ((= @t3 @t712))) % 0.48/0.91 (step @p369 :rule symm :premises (@p368)) % 0.48/0.91 (step @p370 :rule eq_resolve :premises (@p367 @p369)) % 0.48/0.91 (step @p371 :rule cong :premises (@p370) :args (@t716)) % 0.48/0.91 (step @p372 :rule nary_cong :premises (@p371 @p356) :args (@t717)) % 0.48/0.91 (step @p373 :rule cong :premises (@p372) :args ((forall @t5 @t717))) % 0.48/0.91 (step @p374 :rule trans :premises (@p373 @p365)) % 0.48/0.91 (step @p375 :rule bool-impl-elim :args (@t3 @t711)) % 0.48/0.91 (step @p376 :rule cong :premises (@p375) :args ((forall @t5 (=> @t3 @t711)))) % 0.48/0.91 (step @p377 :rule trans :premises (@p376 @p374)) % 0.48/0.91 (step @p378 :rule eq-symm :args (@t1 tptp.nil_poly_real)) % 0.48/0.91 (step @p379 :rule cong :premises (@p378) :args (@t2)) % 0.48/0.91 (step @p380 :rule refl :args (@t3)) % 0.48/0.91 (step @p381 :rule cong :premises (@p380 @p379) :args (@t4)) % 0.48/0.91 (step @p382 :rule cong :premises (@p381) :args (@t6)) % 0.48/0.91 (step @p383 :rule trans :premises (@p382 @p377)) % 0.48/0.91 (step @p384 :rule eq_resolve :premises (@p1 @p383)) % 0.48/0.91 (step @p385 :rule refl :args (@t707)) % 0.48/0.91 (step @p386 :rule refl :args (@t701)) % 0.48/0.91 (step @p387 :rule cong :premises (@p386 @p385) :args ((= @t701 @t707))) % 0.48/0.91 (step @p388 :rule symm :premises (@p387)) % 0.48/0.91 (step @p389 :rule eq_resolve :premises (@p386 @p388)) % 0.48/0.91 (step @p390 :rule bool-double-not-elim :args (@t701)) % 0.48/0.91 (step @p391 :rule trans :premises (@p390 @p389)) % 0.48/0.91 (step @p392 :rule eq_resolve :premises (@p343 @p391)) % 0.48/0.91 (step @p393 false :rule chain_m_resolution :premises (@p392 @p384) :args (false (@list true) (@list @t707))) % 0.48/0.91 ) % 0.48/0.91 % SZS output end Proof % 0.48/0.91 % cvc5 exiting %------------------------------------------------------------------------------