%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP035^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 : n015.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:24:51 AM UTC 2026 % Result : Theorem 0.42s 0.82s % Output : Proof 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP035^1 : TPTP v9.2.1. Released v7.5.0. % 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.15/0.34 % Computer : n015.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Jun 2 04:11:19 EDT 2026 % 0.15/0.34 % CPUTime : % 0.39/0.58 %----Proving TH0 % 0.42/0.82 --- 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.42/0.82 % SZS status Theorem % 0.42/0.82 % SZS output start Proof % 0.42/0.82 ( % 0.42/0.82 (declare-sort tptp.set_complex 0) % 0.42/0.82 (declare-sort tptp.complex 0) % 0.42/0.82 (declare-sort tptp.set_complex_complex 0) % 0.42/0.82 (declare-sort tptp.nat 0) % 0.42/0.82 (declare-sort tptp.real 0) % 0.42/0.82 (declare-sort tptp.set_real 0) % 0.42/0.82 (declare-sort tptp.set_nat 0) % 0.42/0.82 (declare-const tptp.member_complex (-> tptp.complex tptp.set_complex Bool)) % 0.42/0.82 (declare-const tptp.topolo2127351575omplex (-> tptp.set_complex Bool)) % 0.42/0.82 (declare-const tptp.ln_ln_complex (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.ln_ln_real (-> tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.arsinh_complex (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.arsinh_real (-> tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.artanh_complex (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.collect_complex (-> (-> tptp.complex Bool) tptp.set_complex)) % 0.42/0.82 (declare-const tptp.comp_c819638635l_real (-> (-> tptp.complex tptp.real) (-> tptp.real tptp.complex) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.if_complex (-> Bool tptp.complex tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.comp_real_real_real (-> (-> tptp.real tptp.real) (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.image_real_real (-> (-> tptp.real tptp.real) tptp.set_real tptp.set_real)) % 0.42/0.82 (declare-const tptp.comple372758642hic_on (-> (-> tptp.complex tptp.complex) tptp.set_complex Bool)) % 0.42/0.82 (declare-const tptp.times_times_real (-> tptp.real tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.s tptp.set_complex) % 0.42/0.82 (declare-const tptp.times_times_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.42/0.82 (declare-const tptp.times_times_complex (-> tptp.complex tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.g (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.f (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.times_1316095593omplex (-> tptp.set_complex tptp.set_complex tptp.set_complex)) % 0.42/0.82 (declare-const tptp.compow1667379464omplex (-> tptp.nat (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.zero_zero_complex tptp.complex) % 0.42/0.82 (declare-const tptp.zero_zero_real tptp.real) % 0.42/0.82 (declare-const tptp.one_one_real tptp.real) % 0.42/0.82 (declare-const tptp.zero_zero_nat tptp.nat) % 0.42/0.82 (declare-const tptp.arcosh_complex (-> tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.deriv_real (-> (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.compow1098280738omplex (-> tptp.nat (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex) (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.compow_real_real (-> tptp.nat (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.comp_c881053372omplex (-> (-> (-> tptp.complex tptp.complex) tptp.complex) (-> tptp.complex tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.one_one_nat tptp.nat) % 0.42/0.82 (declare-const tptp.id_real_real (-> (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.topolo935673511omplex (-> tptp.set_complex Bool)) % 0.42/0.82 (declare-const tptp.deriv_complex (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.compow1723822618l_real (-> tptp.nat (-> (-> tptp.real tptp.real) tptp.real tptp.real) (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.comp_c1610621014omplex (-> (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex) (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex) (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.one_one_complex tptp.complex) % 0.42/0.82 (declare-const tptp.w tptp.complex) % 0.42/0.82 (declare-const tptp.times_times_set_nat (-> tptp.set_nat tptp.set_nat tptp.set_nat)) % 0.42/0.82 (declare-const tptp.if_nat (-> Bool tptp.nat tptp.nat tptp.nat)) % 0.42/0.82 (declare-const tptp.if_real (-> Bool tptp.real tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 0.42/0.82 (declare-const tptp.times_times_set_real (-> tptp.set_real tptp.set_real tptp.set_real)) % 0.42/0.82 (declare-const tptp.member_real (-> tptp.real tptp.set_real Bool)) % 0.42/0.82 (declare-const tptp.funpow1854104714omplex (-> tptp.nat (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex) (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.funpow_real_real (-> tptp.nat (-> (-> tptp.real tptp.real) tptp.real tptp.real) (-> tptp.real tptp.real) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.funpow_complex (-> tptp.nat (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.t tptp.set_complex) % 0.42/0.82 (declare-const tptp.comp_r667767405omplex (-> (-> tptp.real tptp.complex) (-> tptp.complex tptp.real) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.image_58037603omplex (-> (-> tptp.complex tptp.complex) tptp.set_complex tptp.set_complex)) % 0.42/0.82 (declare-const tptp.comp_c606622857omplex (-> (-> tptp.complex tptp.complex tptp.complex) (-> (-> tptp.complex tptp.complex) tptp.complex) (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.comp_r2009261319omplex (-> (-> tptp.real tptp.complex tptp.complex) (-> (-> tptp.complex tptp.complex) tptp.real) (-> tptp.complex tptp.complex) tptp.complex tptp.complex)) % 0.42/0.82 (declare-const tptp.image_944012797omplex (-> (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex) tptp.set_complex_complex tptp.set_complex_complex)) % 0.42/0.82 (declare-const tptp.comp_c1884694328l_real (-> (-> (-> tptp.complex tptp.complex) tptp.real) (-> tptp.real tptp.complex tptp.complex) tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.arcosh_real (-> tptp.real tptp.real)) % 0.42/0.82 (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool)) % 0.42/0.82 (declare-const tptp.id_set_real (-> tptp.set_real tptp.set_real)) % 0.42/0.82 (declare-const tptp.id_set1618538368omplex (-> tptp.set_complex_complex tptp.set_complex_complex)) % 0.42/0.82 (declare-const tptp.id_set_complex (-> tptp.set_complex tptp.set_complex)) % 0.42/0.82 (declare-const tptp.ord_less_eq_real (-> tptp.real tptp.real Bool)) % 0.42/0.82 (declare-const tptp.artanh_real (-> tptp.real tptp.real)) % 0.42/0.82 (define tptp.id_real () (let ((_let_1 (@var "X" tptp.real))) (lambda (@list _let_1) _let_1))) % 0.42/0.82 (define tptp.id_complex_complex () (let ((_let_1 (@var "__flatten_var_0" tptp.complex))) (let ((_let_2 (@var "X" (-> tptp.complex tptp.complex)))) (lambda (@list _let_2 _let_1) (_ _let_2 _let_1))))) % 0.42/0.82 (define tptp.id_complex () (let ((_let_1 (@var "X" tptp.complex))) (lambda (@list _let_1) _let_1))) % 0.42/0.82 (define tptp.comp_c130555887omplex () (let ((_let_1 (@var "X" tptp.complex))) (let ((_let_2 (@var "G" (-> tptp.complex tptp.complex)))) (let ((_let_3 (@var "F2" (-> tptp.complex tptp.complex)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.42/0.82 (define tptp.ord_le701908932omplex () (let ((_let_1 (@var "B5" tptp.set_complex))) (let ((_let_2 (@var "X" tptp.complex))) (let ((_let_3 (_ tptp.member_complex _let_2))) (let ((_let_4 (@var "A5" tptp.set_complex))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.42/0.82 (define @t1 () (@var "Z" tptp.real)) % 0.42/0.82 (define @t2 () (_ (_ (_ (_ tptp.compow1723822618l_real tptp.one_one_nat) tptp.deriv_real) tptp.id_real) @t1)) % 0.42/0.82 (define @t3 () (= tptp.one_one_nat tptp.zero_zero_nat)) % 0.42/0.82 (define @t4 () (not @t3)) % 0.42/0.82 (define @t5 () (@var "Z" tptp.complex)) % 0.42/0.82 (define @t6 () (_ (_ (_ (_ tptp.compow1098280738omplex tptp.one_one_nat) tptp.deriv_complex) tptp.id_complex) @t5)) % 0.42/0.82 (define @t7 () (@list @t5)) % 0.42/0.82 (define @t8 () (lambda (@list (@var "Z2" tptp.complex)) tptp.one_one_complex)) % 0.42/0.82 (define @t9 () (_ tptp.deriv_complex tptp.id_complex)) % 0.42/0.82 (define @t10 () (= @t9 @t8)) % 0.42/0.82 (define @t11 () (@var "F" (-> tptp.real tptp.real))) % 0.42/0.82 (define @t12 () (@var "X" tptp.real)) % 0.42/0.82 (define @t13 () (_ @t11 @t12)) % 0.42/0.82 (define @t14 () (@list @t12)) % 0.42/0.82 (define @t15 () (@list @t11)) % 0.42/0.82 (define @t16 () (@var "F" (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex))) % 0.42/0.82 (define @t17 () (@var "X" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t18 () (_ @t16 @t17)) % 0.42/0.82 (define @t19 () (@list @t17)) % 0.42/0.82 (define @t20 () (@list @t16)) % 0.42/0.82 (define @t21 () (@var "F" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t22 () (@var "X" tptp.complex)) % 0.42/0.82 (define @t23 () (_ @t21 @t22)) % 0.42/0.82 (define @t24 () (@list @t22)) % 0.42/0.82 (define @t25 () (@list @t21)) % 0.42/0.82 (define @t26 () (@var "N" tptp.nat)) % 0.42/0.82 (define @t27 () (_ tptp.compow1723822618l_real @t26)) % 0.42/0.82 (define @t28 () (_ (_ (_ @t27 tptp.deriv_real) tptp.id_real) @t1)) % 0.42/0.82 (define @t29 () (= @t26 tptp.one_one_nat)) % 0.42/0.82 (define @t30 () (not @t29)) % 0.42/0.82 (define @t31 () (= @t26 tptp.zero_zero_nat)) % 0.42/0.82 (define @t32 () (not @t31)) % 0.42/0.82 (define @t33 () (_ tptp.compow1098280738omplex @t26)) % 0.42/0.82 (define @t34 () (_ @t33 tptp.deriv_complex)) % 0.42/0.82 (define @t35 () (_ (_ @t34 tptp.id_complex) @t5)) % 0.42/0.82 (define @t36 () (@var "X2" tptp.complex)) % 0.42/0.82 (define @t37 () (@list @t36)) % 0.42/0.82 (define @t38 () (@var "X2" tptp.nat)) % 0.42/0.82 (define @t39 () (@list @t38)) % 0.42/0.82 (define @t40 () (@var "X2" tptp.real)) % 0.42/0.82 (define @t41 () (@list @t40)) % 0.42/0.82 (define @t42 () (_ tptp.compow_real_real @t26)) % 0.42/0.82 (define @t43 () (@list @t26)) % 0.42/0.82 (define @t44 () (_ tptp.compow1667379464omplex @t26)) % 0.42/0.82 (define @t45 () (_ @t9 tptp.w)) % 0.42/0.82 (define @t46 () (_ (_ tptp.deriv_complex tptp.g) (_ tptp.f tptp.w))) % 0.42/0.82 (define @t47 () (_ (_ tptp.deriv_complex tptp.f) tptp.w)) % 0.42/0.82 (define @t48 () (_ (_ tptp.times_times_complex @t47) @t46)) % 0.42/0.82 (define @t49 () (_ (_ tptp.deriv_complex (_ (_ tptp.comp_c130555887omplex tptp.g) tptp.f)) tptp.w)) % 0.42/0.82 (define @t50 () (_ (_ tptp.times_times_complex @t46) @t47)) % 0.42/0.82 (define @t51 () (@var "A" tptp.complex)) % 0.42/0.82 (define @t52 () (_ tptp.times_times_complex tptp.zero_zero_complex)) % 0.42/0.82 (define @t53 () (@list @t51)) % 0.42/0.82 (define @t54 () (@var "A" tptp.nat)) % 0.42/0.82 (define @t55 () (_ tptp.times_times_nat tptp.zero_zero_nat)) % 0.42/0.82 (define @t56 () (@list @t54)) % 0.42/0.82 (define @t57 () (@var "A" tptp.real)) % 0.42/0.82 (define @t58 () (_ tptp.times_times_real tptp.zero_zero_real)) % 0.42/0.82 (define @t59 () (@list @t57)) % 0.42/0.82 (define @t60 () (_ tptp.times_times_complex @t51)) % 0.42/0.82 (define @t61 () (_ tptp.times_times_nat @t54)) % 0.42/0.82 (define @t62 () (_ tptp.times_times_real @t57)) % 0.42/0.82 (define @t63 () (@var "B" tptp.complex)) % 0.42/0.82 (define @t64 () (= @t63 tptp.zero_zero_complex)) % 0.42/0.82 (define @t65 () (= @t51 tptp.zero_zero_complex)) % 0.42/0.82 (define @t66 () (or @t65 @t64)) % 0.42/0.82 (define @t67 () (_ @t60 @t63)) % 0.42/0.82 (define @t68 () (= @t67 tptp.zero_zero_complex)) % 0.42/0.82 (define @t69 () (@list @t51 @t63)) % 0.42/0.82 (define @t70 () (@var "B" tptp.nat)) % 0.42/0.82 (define @t71 () (= @t70 tptp.zero_zero_nat)) % 0.42/0.82 (define @t72 () (= @t54 tptp.zero_zero_nat)) % 0.42/0.82 (define @t73 () (or @t72 @t71)) % 0.42/0.82 (define @t74 () (_ @t61 @t70)) % 0.42/0.82 (define @t75 () (= @t74 tptp.zero_zero_nat)) % 0.42/0.82 (define @t76 () (@list @t54 @t70)) % 0.42/0.82 (define @t77 () (@var "B" tptp.real)) % 0.42/0.82 (define @t78 () (= @t77 tptp.zero_zero_real)) % 0.42/0.82 (define @t79 () (= @t57 tptp.zero_zero_real)) % 0.42/0.82 (define @t80 () (or @t79 @t78)) % 0.42/0.82 (define @t81 () (_ @t62 @t77)) % 0.42/0.82 (define @t82 () (= @t81 tptp.zero_zero_real)) % 0.42/0.82 (define @t83 () (@list @t57 @t77)) % 0.42/0.82 (define @t84 () (= @t51 @t63)) % 0.42/0.82 (define @t85 () (@var "C" tptp.complex)) % 0.42/0.82 (define @t86 () (= @t85 tptp.zero_zero_complex)) % 0.42/0.82 (define @t87 () (or @t86 @t84)) % 0.42/0.82 (define @t88 () (_ tptp.times_times_complex @t85)) % 0.42/0.82 (define @t89 () (_ @t88 @t63)) % 0.42/0.82 (define @t90 () (_ @t88 @t51)) % 0.42/0.82 (define @t91 () (= @t90 @t89)) % 0.42/0.82 (define @t92 () (@list @t85 @t51 @t63)) % 0.42/0.82 (define @t93 () (= @t54 @t70)) % 0.42/0.82 (define @t94 () (@var "C" tptp.nat)) % 0.42/0.82 (define @t95 () (= @t94 tptp.zero_zero_nat)) % 0.42/0.82 (define @t96 () (or @t95 @t93)) % 0.42/0.82 (define @t97 () (_ tptp.times_times_nat @t94)) % 0.42/0.82 (define @t98 () (_ @t97 @t70)) % 0.42/0.82 (define @t99 () (_ @t97 @t54)) % 0.42/0.82 (define @t100 () (= @t99 @t98)) % 0.42/0.82 (define @t101 () (@list @t94 @t54 @t70)) % 0.42/0.82 (define @t102 () (= @t57 @t77)) % 0.42/0.82 (define @t103 () (@var "C" tptp.real)) % 0.42/0.82 (define @t104 () (= @t103 tptp.zero_zero_real)) % 0.42/0.82 (define @t105 () (or @t104 @t102)) % 0.42/0.82 (define @t106 () (_ tptp.times_times_real @t103)) % 0.42/0.82 (define @t107 () (_ @t106 @t77)) % 0.42/0.82 (define @t108 () (_ @t106 @t57)) % 0.42/0.82 (define @t109 () (= @t108 @t107)) % 0.42/0.82 (define @t110 () (@list @t103 @t57 @t77)) % 0.42/0.82 (define @t111 () (_ tptp.times_times_complex @t63)) % 0.42/0.82 (define @t112 () (_ @t111 @t85)) % 0.42/0.82 (define @t113 () (_ @t60 @t85)) % 0.42/0.82 (define @t114 () (= @t113 @t112)) % 0.42/0.82 (define @t115 () (_ tptp.times_times_nat @t70)) % 0.42/0.82 (define @t116 () (_ @t115 @t94)) % 0.42/0.82 (define @t117 () (_ @t61 @t94)) % 0.42/0.82 (define @t118 () (= @t117 @t116)) % 0.42/0.82 (define @t119 () (_ tptp.times_times_real @t77)) % 0.42/0.82 (define @t120 () (_ @t119 @t103)) % 0.42/0.82 (define @t121 () (_ @t62 @t103)) % 0.42/0.82 (define @t122 () (= @t121 @t120)) % 0.42/0.82 (define @t123 () (_ tptp.times_times_complex tptp.one_one_complex)) % 0.42/0.82 (define @t124 () (_ tptp.times_times_nat tptp.one_one_nat)) % 0.42/0.82 (define @t125 () (_ tptp.times_times_real tptp.one_one_real)) % 0.42/0.82 (define @t126 () (@var "G2" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t127 () (_ tptp.comp_c130555887omplex tptp.id_complex)) % 0.42/0.82 (define @t128 () (_ tptp.comp_c130555887omplex @t21)) % 0.42/0.82 (define @t129 () (@var "X2" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t130 () (_ (_ tptp.compow1098280738omplex tptp.zero_zero_nat) @t16)) % 0.42/0.82 (define @t131 () (@var "X2" (-> tptp.real tptp.real))) % 0.42/0.82 (define @t132 () (@var "F" (-> (-> tptp.real tptp.real) tptp.real tptp.real))) % 0.42/0.82 (define @t133 () (_ (_ tptp.compow1723822618l_real tptp.zero_zero_nat) @t132)) % 0.42/0.82 (define @t134 () (_ (_ tptp.compow1667379464omplex tptp.zero_zero_nat) @t21)) % 0.42/0.82 (define @t135 () (or @t86 (= @t51 tptp.one_one_complex))) % 0.42/0.82 (define @t136 () (= @t57 tptp.one_one_real)) % 0.42/0.82 (define @t137 () (or @t104 @t136)) % 0.42/0.82 (define @t138 () (or @t86 (= @t63 tptp.one_one_complex))) % 0.42/0.82 (define @t139 () (@list @t85 @t63)) % 0.42/0.82 (define @t140 () (= @t77 tptp.one_one_real)) % 0.42/0.82 (define @t141 () (or @t104 @t140)) % 0.42/0.82 (define @t142 () (@list @t103 @t77)) % 0.42/0.82 (define @t143 () (@list @t103 @t57)) % 0.42/0.82 (define @t144 () (_ tptp.member_complex @t5)) % 0.42/0.82 (define @t145 () (_ @t60 @t112)) % 0.42/0.82 (define @t146 () (_ tptp.times_times_complex @t67)) % 0.42/0.82 (define @t147 () (_ @t61 @t116)) % 0.42/0.82 (define @t148 () (@list @t54 @t70 @t94)) % 0.42/0.82 (define @t149 () (_ @t62 @t120)) % 0.42/0.82 (define @t150 () (_ tptp.times_times_real @t81)) % 0.42/0.82 (define @t151 () (@list @t57 @t77 @t103)) % 0.42/0.82 (define @t152 () (@var "H" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t153 () (_ tptp.comp_c130555887omplex @t126)) % 0.42/0.82 (define @t154 () (_ @t153 @t152)) % 0.42/0.82 (define @t155 () (_ @t128 @t154)) % 0.42/0.82 (define @t156 () (_ @t128 @t126)) % 0.42/0.82 (define @t157 () (_ (_ tptp.comp_c130555887omplex @t156) @t152)) % 0.42/0.82 (define @t158 () (@list @t21 @t126 @t152)) % 0.42/0.82 (define @t159 () (_ @t44 @t21)) % 0.42/0.82 (define @t160 () (_ tptp.comp_real_real_real @t11)) % 0.42/0.82 (define @t161 () (@var "V" tptp.complex)) % 0.42/0.82 (define @t162 () (@var "D" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t163 () (@var "C" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t164 () (@var "B" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t165 () (@var "A" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t166 () (_ @t165 (_ @t164 @t161))) % 0.42/0.82 (define @t167 () (_ (_ tptp.comp_c130555887omplex @t165) @t164)) % 0.42/0.82 (define @t168 () (= @t167 (_ (_ tptp.comp_c130555887omplex @t163) @t162))) % 0.42/0.82 (define @t169 () (@var "V2" tptp.complex)) % 0.42/0.82 (define @t170 () (_ @t33 @t16)) % 0.42/0.82 (define @t171 () (_ @t27 @t132)) % 0.42/0.82 (define @t172 () (_ @t21 @t36)) % 0.42/0.82 (define @t173 () (= @t166 (_ @t163 @t161))) % 0.42/0.82 (define @t174 () (@list @t165 @t164 @t163 @t161)) % 0.42/0.82 (define @t175 () (= @t40 tptp.zero_zero_real)) % 0.42/0.82 (define @t176 () (= @t36 tptp.zero_zero_complex)) % 0.42/0.82 (define @t177 () (not @t64)) % 0.42/0.82 (define @t178 () (not @t65)) % 0.42/0.82 (define @t179 () (not @t68)) % 0.42/0.82 (define @t180 () (not @t71)) % 0.42/0.82 (define @t181 () (not @t72)) % 0.42/0.82 (define @t182 () (not @t75)) % 0.42/0.82 (define @t183 () (not @t78)) % 0.42/0.82 (define @t184 () (not @t79)) % 0.42/0.82 (define @t185 () (not @t82)) % 0.42/0.82 (define @t186 () (@var "P" (-> tptp.complex Bool))) % 0.42/0.82 (define @t187 () (_ tptp.collect_complex @t186)) % 0.42/0.82 (define @t188 () (_ tptp.member_complex @t51)) % 0.42/0.82 (define @t189 () (@var "A2" tptp.set_complex)) % 0.42/0.82 (define @t190 () (_ tptp.member_complex @t22)) % 0.42/0.82 (define @t191 () (_ @t190 @t189)) % 0.42/0.82 (define @t192 () (@list @t189)) % 0.42/0.82 (define @t193 () (@var "A3" tptp.complex)) % 0.42/0.82 (define @t194 () (@var "B2" tptp.complex)) % 0.42/0.82 (define @t195 () (@var "A3" tptp.nat)) % 0.42/0.82 (define @t196 () (@var "B2" tptp.nat)) % 0.42/0.82 (define @t197 () (@list @t195 @t196)) % 0.42/0.82 (define @t198 () (@var "A3" tptp.real)) % 0.42/0.82 (define @t199 () (@var "B2" tptp.real)) % 0.42/0.82 (define @t200 () (@list @t198 @t199)) % 0.42/0.82 (define @t201 () (@list @t70 @t54 @t94)) % 0.42/0.82 (define @t202 () (@list @t77 @t57 @t103)) % 0.42/0.82 (define @t203 () (not @t86)) % 0.42/0.82 (define @t204 () (not @t95)) % 0.42/0.82 (define @t205 () (not @t104)) % 0.42/0.82 (define @t206 () (@var "T" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t207 () (_ @t60 @t36)) % 0.42/0.82 (define @t208 () (_ @t62 @t40)) % 0.42/0.82 (define @t209 () (@var "Y" tptp.complex)) % 0.42/0.82 (define @t210 () (= @t36 @t209)) % 0.42/0.82 (define @t211 () (= @t207 (_ @t60 @t209))) % 0.42/0.82 (define @t212 () (@list @t51 @t36 @t209)) % 0.42/0.82 (define @t213 () (@var "Y" tptp.real)) % 0.42/0.82 (define @t214 () (= @t40 @t213)) % 0.42/0.82 (define @t215 () (= @t208 (_ @t62 @t213))) % 0.42/0.82 (define @t216 () (@list @t57 @t40 @t213)) % 0.42/0.82 (define @t217 () (_ @t111 @t36)) % 0.42/0.82 (define @t218 () (= @t207 @t217)) % 0.42/0.82 (define @t219 () (_ @t119 @t40)) % 0.42/0.82 (define @t220 () (= @t208 @t219)) % 0.42/0.82 (define @t221 () (@var "Q" tptp.complex)) % 0.42/0.82 (define @t222 () (@var "P" Bool)) % 0.42/0.82 (define @t223 () (_ (_ tptp.times_times_complex (_ (_ (_ tptp.if_complex @t222) tptp.one_one_complex) tptp.zero_zero_complex)) @t221)) % 0.42/0.82 (define @t224 () (not @t222)) % 0.42/0.82 (define @t225 () (@var "Q" tptp.nat)) % 0.42/0.82 (define @t226 () (_ (_ tptp.times_times_nat (_ (_ (_ tptp.if_nat @t222) tptp.one_one_nat) tptp.zero_zero_nat)) @t225)) % 0.42/0.82 (define @t227 () (@var "Q" tptp.real)) % 0.42/0.82 (define @t228 () (_ (_ tptp.times_times_real (_ (_ (_ tptp.if_real @t222) tptp.one_one_real) tptp.zero_zero_real)) @t227)) % 0.42/0.82 (define @t229 () (@var "D2" tptp.set_complex)) % 0.42/0.82 (define @t230 () (@var "C2" tptp.set_complex)) % 0.42/0.82 (define @t231 () (_ tptp.times_1316095593omplex @t230)) % 0.42/0.82 (define @t232 () (_ tptp.member_complex @t63)) % 0.42/0.82 (define @t233 () (@var "D2" tptp.set_nat)) % 0.42/0.82 (define @t234 () (@var "C2" tptp.set_nat)) % 0.42/0.82 (define @t235 () (@var "D2" tptp.set_real)) % 0.42/0.82 (define @t236 () (@var "C2" tptp.set_real)) % 0.42/0.82 (define @t237 () (@var "K" tptp.nat)) % 0.42/0.82 (define @t238 () (= @t237 tptp.zero_zero_nat)) % 0.42/0.82 (define @t239 () (@var "M" tptp.nat)) % 0.42/0.82 (define @t240 () (= @t239 @t26)) % 0.42/0.82 (define @t241 () (or @t240 @t238)) % 0.42/0.82 (define @t242 () (_ tptp.times_times_nat @t26)) % 0.42/0.82 (define @t243 () (_ tptp.times_times_nat @t239)) % 0.42/0.82 (define @t244 () (_ tptp.times_times_nat @t237)) % 0.42/0.82 (define @t245 () (= (_ @t244 @t239) (_ @t244 @t26))) % 0.42/0.82 (define @t246 () (@list @t237 @t239 @t26)) % 0.42/0.82 (define @t247 () (@list @t239)) % 0.42/0.82 (define @t248 () (= @t239 tptp.zero_zero_nat)) % 0.42/0.82 (define @t249 () (_ @t243 @t26)) % 0.42/0.82 (define @t250 () (@list @t239 @t26)) % 0.42/0.82 (define @t251 () (and (= @t239 tptp.one_one_nat) @t29)) % 0.42/0.82 (define @t252 () (@var "I" tptp.nat)) % 0.42/0.82 (define @t253 () (_ (_ tptp.compow1098280738omplex @t252) tptp.deriv_complex)) % 0.42/0.82 (define @t254 () (@var "W" tptp.complex)) % 0.42/0.82 (define @t255 () (= (_ @t21 @t254) (_ @t126 @t254))) % 0.42/0.82 (define @t256 () (@var "S" tptp.set_complex)) % 0.42/0.82 (define @t257 () (_ tptp.member_complex @t254)) % 0.42/0.82 (define @t258 () (@list @t254)) % 0.42/0.82 (define @t259 () (_ @t144 @t256)) % 0.42/0.82 (define @t260 () (_ tptp.topolo935673511omplex @t256)) % 0.42/0.82 (define @t261 () (_ tptp.comple372758642hic_on @t126)) % 0.42/0.82 (define @t262 () (_ tptp.comple372758642hic_on @t21)) % 0.42/0.82 (define @t263 () (_ @t262 @t256)) % 0.42/0.82 (define @t264 () (_ tptp.deriv_complex @t21)) % 0.42/0.82 (define @t265 () (_ @t60 @t217)) % 0.42/0.82 (define @t266 () (@list @t51 @t63 @t36)) % 0.42/0.82 (define @t267 () (_ @t62 @t219)) % 0.42/0.82 (define @t268 () (@list @t57 @t77 @t40)) % 0.42/0.82 (define @t269 () (@var "B3" tptp.set_complex)) % 0.42/0.82 (define @t270 () (@var "B4" tptp.complex)) % 0.42/0.82 (define @t271 () (@var "A4" tptp.complex)) % 0.42/0.82 (define @t272 () (_ tptp.member_complex @t36)) % 0.42/0.82 (define @t273 () (@var "B3" tptp.set_nat)) % 0.42/0.82 (define @t274 () (@var "B4" tptp.nat)) % 0.42/0.82 (define @t275 () (@var "A2" tptp.set_nat)) % 0.42/0.82 (define @t276 () (@var "A4" tptp.nat)) % 0.42/0.82 (define @t277 () (@list @t276 @t274)) % 0.42/0.82 (define @t278 () (@var "B3" tptp.set_real)) % 0.42/0.82 (define @t279 () (@var "B4" tptp.real)) % 0.42/0.82 (define @t280 () (@var "A2" tptp.set_real)) % 0.42/0.82 (define @t281 () (@var "A4" tptp.real)) % 0.42/0.82 (define @t282 () (@list @t281 @t279)) % 0.42/0.82 (define @t283 () (@var "V" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t284 () (_ @t153 @t21)) % 0.42/0.82 (define @t285 () (_ tptp.deriv_complex @t126)) % 0.42/0.82 (define @t286 () (@var "S2" tptp.set_complex)) % 0.42/0.82 (define @t287 () (_ @t261 @t286)) % 0.42/0.82 (define @t288 () (_ @t262 @t286)) % 0.42/0.82 (define @t289 () (= @t156 tptp.id_complex)) % 0.42/0.82 (define @t290 () (@var "F" (-> tptp.real tptp.complex))) % 0.42/0.82 (define @t291 () (@var "G2" (-> tptp.complex tptp.real))) % 0.42/0.82 (define @t292 () (_ tptp.comp_c819638635l_real @t291)) % 0.42/0.82 (define @t293 () (= (_ (_ tptp.comp_r667767405omplex @t290) @t291) tptp.id_complex)) % 0.42/0.82 (define @t294 () (@var "F" (-> (-> tptp.complex tptp.complex) tptp.complex))) % 0.42/0.82 (define @t295 () (@var "G2" (-> tptp.complex tptp.complex tptp.complex))) % 0.42/0.82 (define @t296 () (_ tptp.comp_c606622857omplex @t295)) % 0.42/0.82 (define @t297 () (= (_ (_ tptp.comp_c881053372omplex @t294) @t295) tptp.id_complex)) % 0.42/0.82 (define @t298 () (@var "F" (-> tptp.complex tptp.real))) % 0.42/0.82 (define @t299 () (@var "G2" (-> tptp.real tptp.complex))) % 0.42/0.82 (define @t300 () (_ tptp.comp_r667767405omplex @t299)) % 0.42/0.82 (define @t301 () (= (_ (_ tptp.comp_c819638635l_real @t298) @t299) tptp.id_real)) % 0.42/0.82 (define @t302 () (@var "G2" (-> tptp.real tptp.real))) % 0.42/0.82 (define @t303 () (_ tptp.comp_real_real_real @t302)) % 0.42/0.82 (define @t304 () (= (_ @t160 @t302) tptp.id_real)) % 0.42/0.82 (define @t305 () (@var "F" (-> (-> tptp.complex tptp.complex) tptp.real))) % 0.42/0.82 (define @t306 () (@var "G2" (-> tptp.real tptp.complex tptp.complex))) % 0.42/0.82 (define @t307 () (_ tptp.comp_r2009261319omplex @t306)) % 0.42/0.82 (define @t308 () (= (_ (_ tptp.comp_c1884694328l_real @t305) @t306) tptp.id_real)) % 0.42/0.82 (define @t309 () (@var "F" (-> tptp.complex tptp.complex tptp.complex))) % 0.42/0.82 (define @t310 () (@var "G2" (-> (-> tptp.complex tptp.complex) tptp.complex))) % 0.42/0.82 (define @t311 () (_ tptp.comp_c881053372omplex @t310)) % 0.42/0.82 (define @t312 () (= (_ (_ tptp.comp_c606622857omplex @t309) @t310) tptp.id_complex_complex)) % 0.42/0.82 (define @t313 () (@var "F" (-> tptp.real tptp.complex tptp.complex))) % 0.42/0.82 (define @t314 () (@var "G2" (-> (-> tptp.complex tptp.complex) tptp.real))) % 0.42/0.82 (define @t315 () (_ tptp.comp_c1884694328l_real @t314)) % 0.42/0.82 (define @t316 () (= (_ (_ tptp.comp_r2009261319omplex @t313) @t314) tptp.id_complex_complex)) % 0.42/0.82 (define @t317 () (@var "G2" (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex))) % 0.42/0.82 (define @t318 () (_ tptp.comp_c1610621014omplex @t317)) % 0.42/0.82 (define @t319 () (= (_ (_ tptp.comp_c1610621014omplex @t16) @t317) tptp.id_complex_complex)) % 0.42/0.82 (define @t320 () (@var "H" (-> tptp.real tptp.complex))) % 0.42/0.82 (define @t321 () (@var "H" (-> (-> tptp.complex tptp.complex) tptp.complex))) % 0.42/0.82 (define @t322 () (@var "H" (-> tptp.complex tptp.real))) % 0.42/0.82 (define @t323 () (@var "H" (-> tptp.real tptp.real))) % 0.42/0.82 (define @t324 () (@var "H" (-> (-> tptp.complex tptp.complex) tptp.real))) % 0.42/0.82 (define @t325 () (@var "H" (-> tptp.complex tptp.complex tptp.complex))) % 0.42/0.82 (define @t326 () (@var "H" (-> tptp.real tptp.complex tptp.complex))) % 0.42/0.82 (define @t327 () (@var "H" (-> (-> tptp.complex tptp.complex) tptp.complex tptp.complex))) % 0.42/0.82 (define @t328 () (@var "L" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t329 () (_ tptp.comp_c130555887omplex @t328)) % 0.42/0.82 (define @t330 () (@var "R" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t331 () (@var "L1" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t332 () (_ tptp.comp_c130555887omplex @t331)) % 0.42/0.82 (define @t333 () (@var "L2" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t334 () (@var "R2" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t335 () (@var "R1" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t336 () (@var "T" tptp.set_complex)) % 0.42/0.82 (define @t337 () (_ @t261 @t336)) % 0.42/0.82 (define @t338 () (@var "X3" tptp.complex)) % 0.42/0.82 (define @t339 () (_ @t21 @t338)) % 0.42/0.82 (define @t340 () (= @t339 (_ @t126 @t338))) % 0.42/0.82 (define @t341 () (_ tptp.member_complex @t338)) % 0.42/0.82 (define @t342 () (@list @t338)) % 0.42/0.82 (define @t343 () (forall @t342 (=> (_ @t341 @t286) @t340))) % 0.42/0.82 (define @t344 () (@list @t21 @t286 @t126)) % 0.42/0.82 (define @t345 () (@var "B" Bool)) % 0.42/0.82 (define @t346 () (_ tptp.if_complex @t345)) % 0.42/0.82 (define @t347 () (_ (_ tptp.times_times_complex (_ (_ @t346 @t36) tptp.zero_zero_complex)) @t209)) % 0.42/0.82 (define @t348 () (not @t345)) % 0.42/0.82 (define @t349 () (_ tptp.times_times_complex @t36)) % 0.42/0.82 (define @t350 () (_ @t349 @t209)) % 0.42/0.82 (define @t351 () (@list @t345 @t36 @t209)) % 0.42/0.82 (define @t352 () (@var "Y" tptp.nat)) % 0.42/0.82 (define @t353 () (_ tptp.if_nat @t345)) % 0.42/0.82 (define @t354 () (_ (_ tptp.times_times_nat (_ (_ @t353 @t38) tptp.zero_zero_nat)) @t352)) % 0.42/0.82 (define @t355 () (_ tptp.times_times_nat @t38)) % 0.42/0.82 (define @t356 () (_ @t355 @t352)) % 0.42/0.82 (define @t357 () (@list @t345 @t38 @t352)) % 0.42/0.82 (define @t358 () (_ tptp.if_real @t345)) % 0.42/0.82 (define @t359 () (_ (_ tptp.times_times_real (_ (_ @t358 @t40) tptp.zero_zero_real)) @t213)) % 0.42/0.82 (define @t360 () (_ tptp.times_times_real @t40)) % 0.42/0.82 (define @t361 () (_ @t360 @t213)) % 0.42/0.82 (define @t362 () (@list @t345 @t40 @t213)) % 0.42/0.82 (define @t363 () (_ @t349 (_ (_ @t346 @t209) tptp.zero_zero_complex))) % 0.42/0.82 (define @t364 () (_ @t355 (_ (_ @t353 @t352) tptp.zero_zero_nat))) % 0.42/0.82 (define @t365 () (_ @t360 (_ (_ @t358 @t213) tptp.zero_zero_real))) % 0.42/0.82 (define @t366 () (_ tptp.ord_less_eq_nat @t26)) % 0.42/0.82 (define @t367 () (_ tptp.image_real_real tptp.id_real)) % 0.42/0.82 (define @t368 () (_ tptp.image_944012797omplex tptp.id_complex_complex)) % 0.42/0.82 (define @t369 () (_ tptp.image_58037603omplex tptp.id_complex)) % 0.42/0.82 (define @t370 () (@var "F3" tptp.set_complex)) % 0.42/0.82 (define @t371 () (_ (_ tptp.times_1316095593omplex @t229) @t370)) % 0.42/0.82 (define @t372 () (@var "E" tptp.set_complex)) % 0.42/0.82 (define @t373 () (_ @t231 @t372)) % 0.42/0.82 (define @t374 () (_ (_ tptp.ord_le701908932omplex @t372) @t370)) % 0.42/0.82 (define @t375 () (_ (_ tptp.ord_le701908932omplex @t230) @t229)) % 0.42/0.82 (define @t376 () (_ (_ tptp.comple372758642hic_on @t284) @t286)) % 0.42/0.82 (define @t377 () (_ tptp.image_58037603omplex @t21)) % 0.42/0.82 (define @t378 () (_ @t377 @t286)) % 0.42/0.82 (define @t379 () (@var "R" tptp.set_complex)) % 0.42/0.82 (define @t380 () (_ tptp.image_58037603omplex @t126)) % 0.42/0.82 (define @t381 () (_ tptp.comp_c130555887omplex @t152)) % 0.42/0.82 (define @t382 () (_ @t377 @t189)) % 0.42/0.82 (define @t383 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 0.42/0.82 (define @t384 () (_ @t383 @t94)) % 0.42/0.82 (define @t385 () (_ tptp.ord_less_eq_nat @t54)) % 0.42/0.82 (define @t386 () (_ @t385 @t70)) % 0.42/0.82 (define @t387 () (_ (_ tptp.ord_less_eq_real @t108) @t107)) % 0.42/0.82 (define @t388 () (_ tptp.ord_less_eq_real tptp.zero_zero_real)) % 0.42/0.82 (define @t389 () (_ @t388 @t103)) % 0.42/0.82 (define @t390 () (_ tptp.ord_less_eq_real @t57)) % 0.42/0.82 (define @t391 () (_ @t390 @t77)) % 0.42/0.82 (define @t392 () (_ tptp.ord_less_eq_real @t77)) % 0.42/0.82 (define @t393 () (_ @t392 tptp.zero_zero_real)) % 0.42/0.82 (define @t394 () (_ @t390 tptp.zero_zero_real)) % 0.42/0.82 (define @t395 () (_ @t388 @t77)) % 0.42/0.82 (define @t396 () (_ @t388 @t57)) % 0.42/0.82 (define @t397 () (or (and @t396 @t395) (and @t394 @t393))) % 0.42/0.82 (define @t398 () (_ @t388 @t81)) % 0.42/0.82 (define @t399 () (_ tptp.ord_less_eq_nat @t70)) % 0.42/0.82 (define @t400 () (_ @t399 tptp.zero_zero_nat)) % 0.42/0.82 (define @t401 () (_ @t383 @t54)) % 0.42/0.82 (define @t402 () (_ tptp.ord_less_eq_nat @t74)) % 0.42/0.82 (define @t403 () (_ @t402 tptp.zero_zero_nat)) % 0.42/0.82 (define @t404 () (_ @t383 @t70)) % 0.42/0.82 (define @t405 () (_ @t385 tptp.zero_zero_nat)) % 0.42/0.82 (define @t406 () (_ tptp.ord_less_eq_real @t81)) % 0.42/0.82 (define @t407 () (_ @t406 tptp.zero_zero_real)) % 0.42/0.82 (define @t408 () (or (and @t396 @t393) (and @t394 @t395))) % 0.42/0.82 (define @t409 () (_ tptp.ord_less_eq_nat @t117)) % 0.42/0.82 (define @t410 () (_ tptp.ord_less_eq_real @t121)) % 0.42/0.82 (define @t411 () (_ @t410 @t120)) % 0.42/0.82 (define @t412 () (_ tptp.ord_less_eq_real @t103)) % 0.42/0.82 (define @t413 () (_ @t412 tptp.zero_zero_real)) % 0.42/0.82 (define @t414 () (_ @t392 @t57)) % 0.42/0.82 (define @t415 () (@var "D" tptp.nat)) % 0.42/0.82 (define @t416 () (=> @t384 (_ @t409 (_ @t115 @t415)))) % 0.42/0.82 (define @t417 () (_ tptp.ord_less_eq_nat @t94)) % 0.42/0.82 (define @t418 () (_ @t417 @t415)) % 0.42/0.82 (define @t419 () (@list @t54 @t70 @t94 @t415)) % 0.42/0.82 (define @t420 () (@var "D" tptp.real)) % 0.42/0.82 (define @t421 () (=> @t389 (_ @t410 (_ @t119 @t420)))) % 0.42/0.82 (define @t422 () (_ @t412 @t420)) % 0.42/0.82 (define @t423 () (@list @t57 @t77 @t103 @t420)) % 0.42/0.82 (define @t424 () (_ tptp.ord_less_eq_real tptp.one_one_real)) % 0.42/0.82 (define @t425 () (@var "W2" tptp.complex)) % 0.42/0.82 (define @t426 () (_ @t21 @t425)) % 0.42/0.82 (define @t427 () (_ (_ tptp.member_complex @t425) @t256)) % 0.42/0.82 (define @t428 () (@var "Z3" tptp.complex)) % 0.42/0.82 (define @t429 () (@var "T2" tptp.set_complex)) % 0.42/0.82 (define @t430 () (_ @t399 tptp.one_one_nat)) % 0.42/0.82 (define @t431 () (_ @t385 tptp.one_one_nat)) % 0.42/0.82 (define @t432 () (_ @t392 tptp.one_one_real)) % 0.42/0.82 (define @t433 () (_ @t390 tptp.one_one_real)) % 0.42/0.82 (define @t434 () (_ tptp.ord_less_eq_real @t213)) % 0.42/0.82 (define @t435 () (_ @t434 tptp.one_one_real)) % 0.42/0.82 (define @t436 () (_ @t388 @t213)) % 0.42/0.82 (define @t437 () (_ @t388 @t40)) % 0.42/0.82 (define @t438 () (@list @t40 @t213)) % 0.42/0.82 (define @t439 () (= @t189 @t269)) % 0.42/0.82 (define @t440 () (_ tptp.ord_le701908932omplex @t269)) % 0.42/0.82 (define @t441 () (_ @t440 @t189)) % 0.42/0.82 (define @t442 () (_ tptp.ord_le701908932omplex @t189)) % 0.42/0.82 (define @t443 () (_ @t442 @t269)) % 0.42/0.82 (define @t444 () (@list @t189 @t269)) % 0.42/0.82 (define @t445 () (_ @t232 @t382)) % 0.42/0.82 (define @t446 () (_ @t272 @t189)) % 0.42/0.82 (define @t447 () (= @t63 @t172)) % 0.42/0.82 (define @t448 () (_ @t341 @t189)) % 0.42/0.82 (define @t449 () (@var "J" tptp.nat)) % 0.42/0.82 (define @t450 () (_ tptp.ord_less_eq_nat @t252)) % 0.42/0.82 (define @t451 () (_ @t450 @t449)) % 0.42/0.82 (define @t452 () (@list @t252 @t449 @t237)) % 0.42/0.82 (define @t453 () (_ tptp.times_times_nat @t449)) % 0.42/0.82 (define @t454 () (_ tptp.ord_less_eq_nat (_ (_ tptp.times_times_nat @t252) @t237))) % 0.42/0.82 (define @t455 () (@var "L" tptp.nat)) % 0.42/0.82 (define @t456 () (_ @t243 @t239)) % 0.42/0.82 (define @t457 () (_ tptp.ord_less_eq_nat @t239)) % 0.42/0.82 (define @t458 () (@var "X4" tptp.complex)) % 0.42/0.82 (define @t459 () (_ tptp.member_complex @t458)) % 0.42/0.82 (define @t460 () (@list @t458)) % 0.42/0.82 (define @t461 () (@list @t21 @t189 @t186)) % 0.42/0.82 (define @t462 () (@var "N2" tptp.set_complex)) % 0.42/0.82 (define @t463 () (@var "M2" tptp.set_complex)) % 0.42/0.82 (define @t464 () (_ @t186 @t338)) % 0.42/0.82 (define @t465 () (_ tptp.member_complex @t85)) % 0.42/0.82 (define @t466 () (@var "B5" tptp.set_complex)) % 0.42/0.82 (define @t467 () (@var "T3" tptp.complex)) % 0.42/0.82 (define @t468 () (_ tptp.member_complex @t467)) % 0.42/0.82 (define @t469 () (@var "A5" tptp.set_complex)) % 0.42/0.82 (define @t470 () (@list @t469 @t466)) % 0.42/0.82 (define @t471 () (@var "Q2" (-> tptp.complex Bool))) % 0.42/0.82 (define @t472 () (_ (_ tptp.ord_le701908932omplex @t187) (_ tptp.collect_complex @t471))) % 0.42/0.82 (define @t473 () (@list @t186 @t471)) % 0.42/0.82 (define @t474 () (@var "Z4" tptp.set_complex)) % 0.42/0.82 (define @t475 () (@var "Y2" tptp.set_complex)) % 0.42/0.82 (define @t476 () (lambda (@list @t475 @t474) (= @t475 @t474))) % 0.42/0.82 (define @t477 () (_ tptp.ord_le701908932omplex @t382)) % 0.42/0.82 (define @t478 () (_ @t477 @t269)) % 0.42/0.82 (define @t479 () (@var "C3" tptp.set_complex)) % 0.42/0.82 (define @t480 () (_ @t440 @t382)) % 0.42/0.82 (define @t481 () (@list @t269 @t21 @t189)) % 0.42/0.82 (define @t482 () (@var "AA" tptp.set_complex)) % 0.42/0.82 (define @t483 () (@var "X2" tptp.set_complex)) % 0.42/0.82 (define @t484 () (_ tptp.ord_le701908932omplex @t483)) % 0.42/0.82 (define @t485 () (_ tptp.ord_less_eq_nat @t38)) % 0.42/0.82 (define @t486 () (_ tptp.ord_less_eq_real @t40)) % 0.42/0.82 (define @t487 () (@var "I3" tptp.nat)) % 0.42/0.82 (define @t488 () (@var "X4" (-> tptp.nat tptp.real))) % 0.42/0.82 (define @t489 () (_ @t488 @t487)) % 0.42/0.82 (define @t490 () (@var "F" (-> (-> tptp.nat tptp.real) tptp.nat tptp.real))) % 0.42/0.82 (define @t491 () (_ (_ @t490 @t488) @t487)) % 0.42/0.82 (define @t492 () (@var "L3" (-> (-> tptp.nat tptp.real) tptp.nat tptp.nat))) % 0.42/0.82 (define @t493 () (_ (_ @t492 @t488) @t487)) % 0.42/0.82 (define @t494 () (= @t493 tptp.one_one_nat)) % 0.42/0.82 (define @t495 () (@var "Q2" (-> tptp.nat Bool))) % 0.42/0.82 (define @t496 () (_ @t495 @t487)) % 0.42/0.82 (define @t497 () (@var "P" (-> (-> tptp.nat tptp.real) Bool))) % 0.42/0.82 (define @t498 () (_ @t497 @t488)) % 0.42/0.82 (define @t499 () (@list @t488 @t487)) % 0.42/0.82 (define @t500 () (= @t493 tptp.zero_zero_nat)) % 0.42/0.82 (define @t501 () (@var "I2" tptp.nat)) % 0.42/0.82 (define @t502 () (@var "X3" (-> tptp.nat tptp.real))) % 0.42/0.82 (define @t503 () (_ @t502 @t501)) % 0.42/0.82 (define @t504 () (_ @t497 @t502)) % 0.42/0.82 (define @t505 () (@list @t502)) % 0.42/0.82 (define @t506 () (@var "Sup" (-> tptp.set_real tptp.real))) % 0.42/0.82 (define @t507 () (@var "A2" tptp.set_complex_complex)) % 0.42/0.82 (define @t508 () (@var "Sup" (-> tptp.set_complex_complex tptp.complex tptp.complex))) % 0.42/0.82 (define @t509 () (@var "Sup" (-> tptp.set_complex tptp.complex))) % 0.42/0.82 (define @t510 () (_ @t457 @t26)) % 0.42/0.82 (define @t511 () (_ @t366 @t239)) % 0.42/0.82 (define @t512 () (@var "X3" tptp.nat)) % 0.42/0.82 (define @t513 () (@var "Y4" tptp.nat)) % 0.42/0.82 (define @t514 () (@var "P" (-> tptp.nat Bool))) % 0.42/0.82 (define @t515 () (@var "Y3" tptp.nat)) % 0.42/0.82 (define @t516 () (@var "B" tptp.set_complex)) % 0.42/0.82 (define @t517 () (@var "A" tptp.set_complex)) % 0.42/0.82 (define @t518 () (= @t517 @t516)) % 0.42/0.82 (define @t519 () (_ tptp.ord_le701908932omplex @t517)) % 0.42/0.82 (define @t520 () (_ @t519 @t516)) % 0.42/0.82 (define @t521 () (_ (_ tptp.ord_le701908932omplex @t516) @t517)) % 0.42/0.82 (define @t522 () (_ @t399 @t54)) % 0.42/0.82 (define @t523 () (@var "B2" tptp.set_complex)) % 0.42/0.82 (define @t524 () (@var "A3" tptp.set_complex)) % 0.42/0.82 (define @t525 () (@var "Z4" tptp.nat)) % 0.42/0.82 (define @t526 () (@var "Y2" tptp.nat)) % 0.42/0.82 (define @t527 () (@var "Z4" tptp.real)) % 0.42/0.82 (define @t528 () (@var "Y2" tptp.real)) % 0.42/0.82 (define @t529 () (@var "C" tptp.set_complex)) % 0.42/0.82 (define @t530 () (_ tptp.ord_le701908932omplex @t529)) % 0.42/0.82 (define @t531 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 0.42/0.82 (define @t532 () (_ (_ @t531 @t276) @t274)) % 0.42/0.82 (define @t533 () (@var "P" (-> tptp.real tptp.real Bool))) % 0.42/0.82 (define @t534 () (_ (_ @t533 @t281) @t279)) % 0.42/0.82 (define @t535 () (@var "Z" tptp.set_complex)) % 0.42/0.82 (define @t536 () (@var "Y" tptp.set_complex)) % 0.42/0.82 (define @t537 () (@var "Z" tptp.nat)) % 0.42/0.82 (define @t538 () (_ @t486 @t213)) % 0.42/0.82 (define @t539 () (_ @t390 @t103)) % 0.42/0.82 (define @t540 () (_ @t434 @t40)) % 0.42/0.82 (define @t541 () (@var "N3" tptp.nat)) % 0.42/0.82 (define @t542 () (@list @t38 @t352)) % 0.42/0.82 (define @t543 () (@list @t36 @t209)) % 0.42/0.82 (define @t544 () (= @t45 tptp.one_one_complex)) % 0.42/0.82 (define @t545 () (not @t544)) % 0.42/0.82 (define @t546 () (lambda @t14 @t12)) % 0.42/0.82 (define @t547 () (@var "__flatten_var_0" tptp.complex)) % 0.42/0.82 (define @t548 () (lambda (@list @t17 @t547) (_ @t17 @t547))) % 0.42/0.82 (define @t549 () (lambda @t24 @t22)) % 0.42/0.82 (define @t550 () (@var "G" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t551 () (@var "F2" (-> tptp.complex tptp.complex))) % 0.42/0.82 (define @t552 () (lambda (@list @t551 @t550 @t22) (_ @t551 (_ @t550 @t22)))) % 0.42/0.82 (define @t553 () (lambda @t470 (forall @t24 (=> (_ @t190 @t469) (_ @t190 @t466))))) % 0.42/0.82 (define @t554 () (@purify @t8)) % 0.42/0.82 (define @t555 () (@purify @t549)) % 0.42/0.82 (define @t556 () (_ tptp.deriv_complex @t555)) % 0.42/0.82 (define @t557 () (_ tptp.deriv_complex @t549)) % 0.42/0.82 (define @t558 () (tptp.deriv_complex @t555 tptp.w)) % 0.42/0.82 (define @t559 () (_ @t556 tptp.w)) % 0.42/0.82 (define @t560 () (_ @t557 tptp.w)) % 0.42/0.82 (define @t561 () (= tptp.one_one_complex @t560)) % 0.42/0.82 (define @t562 () (= tptp.one_one_complex @t559)) % 0.42/0.82 (define @t563 () (= @t556 @t554)) % 0.42/0.82 (define @t564 () (=> @t563 (= @t559 tptp.one_one_complex))) % 0.42/0.82 (define @t565 () (= tptp.one_one_complex @t558)) % 0.42/0.82 (assume @p1 (forall (@list @t1) (and (=> @t3 (= @t2 @t1)) (=> @t4 (= @t2 tptp.one_one_real))))) % 0.42/0.82 (assume @p2 (forall @t7 (and (=> @t3 (= @t6 @t5)) (=> @t4 (= @t6 tptp.one_one_complex))))) % 0.42/0.82 (assume @p3 (_ (_ tptp.member_complex tptp.w) tptp.s)) % 0.42/0.82 (assume @p4 @t10) % 0.42/0.82 (assume @p5 (= (_ tptp.deriv_real tptp.id_real) (lambda (@list (@var "Z2" tptp.real)) tptp.one_one_real))) % 0.42/0.82 (assume @p6 (forall @t15 (= (forall @t14 (= @t13 @t12)) (= @t11 tptp.id_real)))) % 0.42/0.82 (assume @p7 (forall @t20 (= (forall @t19 (= @t18 @t17)) (= @t16 tptp.id_complex_complex)))) % 0.42/0.82 (assume @p8 (forall @t25 (= (forall @t24 (= @t23 @t22)) (= @t21 tptp.id_complex)))) % 0.42/0.82 (assume @p9 (forall (@list @t26 @t1) (and (=> @t31 (= @t28 @t1)) (=> @t32 (and (=> @t29 (= @t28 tptp.one_one_real)) (=> @t30 (= @t28 tptp.zero_zero_real))))))) % 0.42/0.82 (assume @p10 (forall (@list @t26 @t5) (and (=> @t31 (= @t35 @t5)) (=> @t32 (and (=> @t29 (= @t35 tptp.one_one_complex)) (=> @t30 (= @t35 tptp.zero_zero_complex))))))) % 0.42/0.82 (assume @p11 (forall @t37 (= (= tptp.one_one_complex @t36) (= @t36 tptp.one_one_complex)))) % 0.42/0.82 (assume @p12 (forall @t39 (= (= tptp.one_one_nat @t38) (= @t38 tptp.one_one_nat)))) % 0.42/0.82 (assume @p13 (forall @t41 (= (= tptp.one_one_real @t40) (= @t40 tptp.one_one_real)))) % 0.42/0.82 (assume @p14 (forall @t43 (= (_ @t42 tptp.id_real) tptp.id_real))) % 0.42/0.82 (assume @p15 (forall @t43 (= (_ @t27 tptp.id_real_real) tptp.id_real_real))) % 0.42/0.82 (assume @p16 (forall @t43 (= (_ @t44 tptp.id_complex) tptp.id_complex))) % 0.42/0.82 (assume @p17 (forall @t43 (= (_ @t33 tptp.id_complex_complex) tptp.id_complex_complex))) % 0.42/0.82 (assume @p18 (= @t48 @t45)) % 0.42/0.82 (assume @p19 (= @t49 @t45)) % 0.42/0.82 (assume @p20 (not (= tptp.zero_zero_nat tptp.one_one_nat))) % 0.42/0.82 (assume @p21 (not (= tptp.zero_zero_real tptp.one_one_real))) % 0.42/0.82 (assume @p22 (not (= tptp.zero_zero_complex tptp.one_one_complex))) % 0.42/0.82 (assume @p23 (= @t48 @t50)) % 0.42/0.82 (assume @p24 (forall @t53 (= (_ @t52 @t51) tptp.zero_zero_complex))) % 0.42/0.82 (assume @p25 (forall @t56 (= (_ @t55 @t54) tptp.zero_zero_nat))) % 0.42/0.82 (assume @p26 (forall @t59 (= (_ @t58 @t57) tptp.zero_zero_real))) % 0.42/0.82 (assume @p27 (forall @t53 (= (_ @t60 tptp.zero_zero_complex) tptp.zero_zero_complex))) % 0.42/0.82 (assume @p28 (forall @t56 (= (_ @t61 tptp.zero_zero_nat) tptp.zero_zero_nat))) % 0.42/0.82 (assume @p29 (forall @t59 (= (_ @t62 tptp.zero_zero_real) tptp.zero_zero_real))) % 0.42/0.82 (assume @p30 (forall @t69 (= @t68 @t66))) % 0.42/0.82 (assume @p31 (forall @t76 (= @t75 @t73))) % 0.42/0.82 (assume @p32 (forall @t83 (= @t82 @t80))) % 0.42/0.82 (assume @p33 (forall @t92 (= @t91 @t87))) % 0.42/0.82 (assume @p34 (forall @t101 (= @t100 @t96))) % 0.42/0.82 (assume @p35 (forall @t110 (= @t109 @t105))) % 0.42/0.82 (assume @p36 (forall (@list @t51 @t85 @t63) (= @t114 @t87))) % 0.42/0.82 (assume @p37 (forall (@list @t54 @t94 @t70) (= @t118 @t96))) % 0.42/0.82 (assume @p38 (forall (@list @t57 @t103 @t77) (= @t122 @t105))) % 0.42/0.82 (assume @p39 (forall @t53 (= (_ @t60 tptp.one_one_complex) @t51))) % 0.42/0.82 (assume @p40 (forall @t56 (= (_ @t61 tptp.one_one_nat) @t54))) % 0.42/0.82 (assume @p41 (forall @t59 (= (_ @t62 tptp.one_one_real) @t57))) % 0.42/0.82 (assume @p42 (forall @t53 (= (_ @t123 @t51) @t51))) % 0.42/0.82 (assume @p43 (forall @t56 (= (_ @t124 @t54) @t54))) % 0.42/0.82 (assume @p44 (forall @t59 (= (_ @t125 @t57) @t57))) % 0.42/0.82 (assume @p45 (forall (@list @t126) (= (_ @t127 @t126) @t126))) % 0.42/0.82 (assume @p46 (forall @t25 (= (_ @t128 tptp.id_complex) @t21))) % 0.42/0.82 (assume @p47 (forall (@list @t16 @t129) (= (_ @t130 @t129) @t129))) % 0.42/0.82 (assume @p48 (forall (@list @t132 @t131) (= (_ @t133 @t131) @t131))) % 0.42/0.82 (assume @p49 (forall (@list @t21 @t36) (= (_ @t134 @t36) @t36))) % 0.42/0.82 (assume @p50 (_ tptp.topolo935673511omplex tptp.s)) % 0.42/0.82 (assume @p51 (= @t50 @t49)) % 0.42/0.82 (assume @p52 (forall (@list @t51 @t85) (= (= @t113 @t85) @t135))) % 0.42/0.82 (assume @p53 (forall (@list @t57 @t103) (= (= @t121 @t103) @t137))) % 0.42/0.82 (assume @p54 (forall @t139 (= (= @t85 @t112) @t138))) % 0.42/0.82 (assume @p55 (forall @t142 (= (= @t103 @t120) @t141))) % 0.42/0.82 (assume @p56 (forall (@list @t85 @t51) (= (= @t90 @t85) @t135))) % 0.42/0.82 (assume @p57 (forall @t143 (= (= @t108 @t103) @t137))) % 0.42/0.82 (assume @p58 (forall @t139 (= (= @t85 @t89) @t138))) % 0.42/0.82 (assume @p59 (forall @t142 (= (= @t103 @t107) @t141))) % 0.42/0.82 (assume @p60 (forall @t7 (=> (_ @t144 tptp.s) (= (_ tptp.g (_ tptp.f @t5)) @t5)))) % 0.42/0.82 (assume @p61 (_ (_ tptp.comple372758642hic_on tptp.f) tptp.s)) % 0.42/0.82 (assume @p62 (forall (@list @t51 @t63 @t85) (= (_ @t146 @t85) @t145))) % 0.42/0.82 (assume @p63 (forall @t148 (= (_ (_ tptp.times_times_nat @t74) @t94) @t147))) % 0.42/0.82 (assume @p64 (forall @t151 (= (_ @t150 @t103) @t149))) % 0.42/0.82 (assume @p65 (forall @t158 (= @t157 @t155))) % 0.42/0.82 (assume @p66 (forall (@list @t26 @t21) (= (_ @t33 @t128) (_ tptp.comp_c130555887omplex @t159)))) % 0.42/0.82 (assume @p67 (forall (@list @t26 @t11) (= (_ @t27 @t160) (_ tptp.comp_real_real_real (_ @t42 @t11))))) % 0.42/0.82 (assume @p68 (forall (@list @t165 @t164 @t163 @t162 @t161) (=> @t168 (= @t166 (_ @t163 (_ @t162 @t161)))))) % 0.42/0.82 (assume @p69 (forall (@list @t165 @t164 @t163 @t162) (=> @t168 (forall (@list @t169) (= (_ @t165 (_ @t164 @t169)) (_ @t163 (_ @t162 @t169))))))) % 0.42/0.82 (assume @p70 (forall (@list @t16 @t26 @t129) (= (_ @t16 (_ @t170 @t129)) (_ @t170 (_ @t16 @t129))))) % 0.42/0.82 (assume @p71 (forall (@list @t132 @t26 @t131) (= (_ @t132 (_ @t171 @t131)) (_ @t171 (_ @t132 @t131))))) % 0.42/0.82 (assume @p72 (forall (@list @t21 @t26 @t36) (= (_ @t21 (_ @t159 @t36)) (_ @t159 @t172)))) % 0.42/0.82 (assume @p73 (forall @t174 (=> (= @t167 @t163) @t173))) % 0.42/0.82 (assume @p74 (forall @t39 (= (= tptp.zero_zero_nat @t38) (= @t38 tptp.zero_zero_nat)))) % 0.42/0.82 (assume @p75 (forall @t41 (= (= tptp.zero_zero_real @t40) @t175))) % 0.42/0.82 (assume @p76 (forall @t37 (= (= tptp.zero_zero_complex @t36) @t176))) % 0.42/0.82 (assume @p77 (forall @t69 (=> @t179 (and @t178 @t177)))) % 0.42/0.82 (assume @p78 (forall @t76 (=> @t182 (and @t181 @t180)))) % 0.42/0.82 (assume @p79 (forall @t83 (=> @t185 (and @t184 @t183)))) % 0.42/0.82 (assume @p80 (forall (@list @t51 @t186) (= (_ @t188 @t187) (_ @t186 @t51)))) % 0.42/0.82 (assume @p81 (forall @t192 (= (_ tptp.collect_complex (lambda @t24 @t191)) @t189))) % 0.42/0.82 (assume @p82 (= tptp.times_times_complex (lambda (@list @t193 @t194) (_ (_ tptp.times_times_complex @t194) @t193)))) % 0.42/0.82 (assume @p83 (= tptp.times_times_nat (lambda @t197 (_ (_ tptp.times_times_nat @t196) @t195)))) % 0.42/0.82 (assume @p84 (= tptp.times_times_real (lambda @t200 (_ (_ tptp.times_times_real @t199) @t198)))) % 0.42/0.82 (assume @p85 (forall (@list @t63 @t51 @t85) (= (_ @t111 @t113) @t145))) % 0.42/0.82 (assume @p86 (forall @t201 (= (_ @t115 @t117) @t147))) % 0.42/0.82 (assume @p87 (forall @t202 (= (_ @t119 @t121) @t149))) % 0.42/0.82 (assume @p88 (forall @t69 (=> @t68 @t66))) % 0.42/0.82 (assume @p89 (forall @t76 (=> @t75 @t73))) % 0.42/0.82 (assume @p90 (forall @t83 (=> @t82 @t80))) % 0.42/0.82 (assume @p91 (forall @t69 (=> @t178 (=> @t177 @t179)))) % 0.42/0.82 (assume @p92 (forall @t76 (=> @t181 (=> @t180 @t182)))) % 0.42/0.82 (assume @p93 (forall @t83 (=> @t184 (=> @t183 @t185)))) % 0.42/0.82 (assume @p94 (forall @t92 (=> @t203 (= @t91 @t84)))) % 0.42/0.82 (assume @p95 (forall @t101 (=> @t204 (= @t100 @t93)))) % 0.42/0.82 (assume @p96 (forall @t110 (=> @t205 (= @t109 @t102)))) % 0.42/0.82 (assume @p97 (forall @t92 (=> @t203 (= @t114 @t84)))) % 0.42/0.82 (assume @p98 (forall @t101 (=> @t204 (= @t118 @t93)))) % 0.42/0.82 (assume @p99 (forall @t110 (=> @t205 (= @t122 @t102)))) % 0.42/0.82 (assume @p100 (forall @t174 (=> (= @t167 (_ @t127 @t163)) @t173))) % 0.42/0.82 (assume @p101 (forall @t15 (= (_ (_ tptp.compow_real_real tptp.zero_zero_nat) @t11) tptp.id_real))) % 0.42/0.82 (assume @p102 (forall @t20 (= @t130 tptp.id_complex_complex))) % 0.42/0.82 (assume @p103 (forall (@list @t132) (= @t133 tptp.id_real_real))) % 0.42/0.82 (assume @p104 (forall @t25 (= @t134 tptp.id_complex))) % 0.42/0.82 (assume @p105 (forall (@list @t206) (= (_ @t127 @t206) @t206))) % 0.42/0.82 (assume @p106 (forall @t37 (= (_ @t123 @t36) @t36))) % 0.42/0.82 (assume @p107 (forall @t41 (= (_ @t125 @t40) @t40))) % 0.42/0.82 (assume @p108 (forall (@list @t51 @t36) (= (= @t207 tptp.zero_zero_complex) (or @t65 @t176)))) % 0.42/0.82 (assume @p109 (forall (@list @t57 @t40) (= (= @t208 tptp.zero_zero_real) (or @t79 @t175)))) % 0.42/0.82 (assume @p110 (forall @t37 (= (_ @t52 @t36) tptp.zero_zero_complex))) % 0.42/0.82 (assume @p111 (forall @t41 (= (_ @t58 @t40) tptp.zero_zero_real))) % 0.42/0.82 (assume @p112 (forall @t212 (= @t211 (or @t210 @t65)))) % 0.42/0.82 (assume @p113 (forall @t216 (= @t215 (or @t214 @t79)))) % 0.42/0.82 (assume @p114 (forall (@list @t51 @t36 @t63) (= @t218 (or @t84 @t176)))) % 0.42/0.82 (assume @p115 (forall (@list @t57 @t40 @t77) (= @t220 (or @t102 @t175)))) % 0.42/0.82 (assume @p116 (forall (@list @t222 @t221) (and (=> @t222 (= @t223 @t221)) (=> @t224 (= @t223 tptp.zero_zero_complex))))) % 0.42/0.82 (assume @p117 (forall (@list @t222 @t225) (and (=> @t222 (= @t226 @t225)) (=> @t224 (= @t226 tptp.zero_zero_nat))))) % 0.42/0.82 (assume @p118 (forall (@list @t222 @t227) (and (=> @t222 (= @t228 @t227)) (=> @t224 (= @t228 tptp.zero_zero_real))))) % 0.42/0.82 (assume @p119 (forall (@list @t51 @t230 @t63 @t229) (=> (_ @t188 @t230) (=> (_ @t232 @t229) (_ (_ tptp.member_complex @t67) (_ @t231 @t229)))))) % 0.42/0.82 (assume @p120 (forall (@list @t54 @t234 @t70 @t233) (=> (_ (_ tptp.member_nat @t54) @t234) (=> (_ (_ tptp.member_nat @t70) @t233) (_ (_ tptp.member_nat @t74) (_ (_ tptp.times_times_set_nat @t234) @t233)))))) % 0.42/0.82 (assume @p121 (forall (@list @t57 @t236 @t77 @t235) (=> (_ (_ tptp.member_real @t57) @t236) (=> (_ (_ tptp.member_real @t77) @t235) (_ (_ tptp.member_real @t81) (_ (_ tptp.times_times_set_real @t236) @t235)))))) % 0.42/0.82 (assume @p122 (= tptp.funpow1854104714omplex tptp.compow1098280738omplex)) % 0.42/0.82 (assume @p123 (= tptp.funpow_real_real tptp.compow1723822618l_real)) % 0.42/0.82 (assume @p124 (= tptp.funpow_complex tptp.compow1667379464omplex)) % 0.42/0.82 (assume @p125 (_ tptp.topolo935673511omplex tptp.t)) % 0.42/0.82 (assume @p126 (_ (_ tptp.comple372758642hic_on tptp.g) tptp.t)) % 0.42/0.82 (assume @p127 (forall (@list @t239 @t237 @t26) (= (= (_ @t243 @t237) (_ @t242 @t237)) @t241))) % 0.42/0.82 (assume @p128 (forall @t246 (= @t245 @t241))) % 0.42/0.82 (assume @p129 (forall @t247 (= (_ @t243 tptp.zero_zero_nat) tptp.zero_zero_nat))) % 0.42/0.82 (assume @p130 (forall @t250 (= (= @t249 tptp.zero_zero_nat) (or @t248 @t31)))) % 0.42/0.82 (assume @p131 (forall @t250 (= (= @t249 tptp.one_one_nat) @t251))) % 0.42/0.82 (assume @p132 (forall @t250 (= (= tptp.one_one_nat @t249) @t251))) % 0.42/0.82 (assume @p133 (forall (@list @t21 @t256 @t126 @t5 @t252) (=> @t263 (=> (_ @t261 @t256) (=> @t260 (=> @t259 (=> (forall @t258 (=> (_ @t257 @t256) @t255)) (= (_ (_ @t253 @t21) @t5) (_ (_ @t253 @t126) @t5))))))))) % 0.42/0.82 (assume @p134 (forall (@list @t21 @t256 @t26) (=> @t263 (=> @t260 (_ (_ tptp.comple372758642hic_on (_ @t34 @t21)) @t256))))) % 0.42/0.82 (assume @p135 (forall (@list @t21 @t256) (=> @t263 (=> @t260 (_ (_ tptp.comple372758642hic_on @t264) @t256))))) % 0.42/0.82 (assume @p136 (forall @t43 (= (_ @t55 @t26) tptp.zero_zero_nat))) % 0.42/0.82 (assume @p137 (forall @t43 (= (_ @t242 tptp.one_one_nat) @t26))) % 0.42/0.82 (assume @p138 (forall @t43 (= (_ @t124 @t26) @t26))) % 0.42/0.82 (assume @p139 (forall (@list @t26 @t239 @t16) (= (_ @t33 (_ (_ tptp.compow1098280738omplex @t239) @t16)) (_ (_ tptp.compow1098280738omplex @t249) @t16)))) % 0.42/0.82 (assume @p140 (forall (@list @t26 @t239 @t132) (= (_ @t27 (_ (_ tptp.compow1723822618l_real @t239) @t132)) (_ (_ tptp.compow1723822618l_real @t249) @t132)))) % 0.42/0.82 (assume @p141 (forall (@list @t26 @t239 @t21) (= (_ @t44 (_ (_ tptp.compow1667379464omplex @t239) @t21)) (_ (_ tptp.compow1667379464omplex @t249) @t21)))) % 0.42/0.82 (assume @p142 (forall @t250 (=> (= @t239 @t249) (or @t29 @t248)))) % 0.42/0.82 (assume @p143 (forall @t266 (= @t265 (_ @t111 @t207)))) % 0.42/0.82 (assume @p144 (forall @t268 (= @t267 (_ @t119 @t208)))) % 0.42/0.82 (assume @p145 (forall @t266 (= @t265 (_ @t146 @t36)))) % 0.42/0.82 (assume @p146 (forall @t268 (= @t267 (_ @t150 @t40)))) % 0.42/0.82 (assume @p147 (forall (@list @t36 @t189 @t269) (=> (_ @t272 (_ (_ tptp.times_1316095593omplex @t189) @t269)) (not (forall (@list @t271 @t270) (=> (= @t36 (_ (_ tptp.times_times_complex @t271) @t270)) (=> (_ (_ tptp.member_complex @t271) @t189) (not (_ (_ tptp.member_complex @t270) @t269))))))))) % 0.42/0.82 (assume @p148 (forall (@list @t38 @t275 @t273) (=> (_ (_ tptp.member_nat @t38) (_ (_ tptp.times_times_set_nat @t275) @t273)) (not (forall @t277 (=> (= @t38 (_ (_ tptp.times_times_nat @t276) @t274)) (=> (_ (_ tptp.member_nat @t276) @t275) (not (_ (_ tptp.member_nat @t274) @t273))))))))) % 0.42/0.82 (assume @p149 (forall (@list @t40 @t280 @t278) (=> (_ (_ tptp.member_real @t40) (_ (_ tptp.times_times_set_real @t280) @t278)) (not (forall @t282 (=> (= @t40 (_ (_ tptp.times_times_real @t281) @t279)) (=> (_ (_ tptp.member_real @t281) @t280) (not (_ (_ tptp.member_real @t279) @t278))))))))) % 0.42/0.82 (assume @p150 (forall (@list @t126 @t21 @t283) (= (_ @t153 (_ @t128 @t283)) (_ (_ tptp.comp_c130555887omplex @t284) @t283)))) % 0.42/0.82 (assume @p151 (forall (@list @t36 @t51 @t63) (=> (not @t176) (=> @t218 @t84)))) % 0.42/0.82 (assume @p152 (forall (@list @t40 @t57 @t77) (=> (not @t175) (=> @t220 @t102)))) % 0.42/0.82 (assume @p153 (forall @t212 (=> @t178 (=> @t211 @t210)))) % 0.42/0.82 (assume @p154 (forall @t216 (=> @t184 (=> @t215 @t214)))) % 0.42/0.82 (assume @p155 (= @t127 tptp.id_complex_complex)) % 0.42/0.82 (assume @p156 (forall (@list @t21 @t286 @t126 @t5) (=> @t288 (=> @t287 (=> (_ tptp.topolo935673511omplex @t286) (=> (_ @t144 @t286) (=> (forall @t258 (=> (_ @t257 @t286) @t255)) (= (_ @t264 @t5) (_ @t285 @t5))))))))) % 0.42/0.82 (assume @p157 (forall (@list @t286) (_ (_ tptp.comple372758642hic_on tptp.id_complex) @t286))) % 0.42/0.82 (assume @p158 (forall (@list @t85 @t286) (_ (_ tptp.comple372758642hic_on @t88) @t286))) % 0.42/0.82 (assume @p159 (forall (@list @t21 @t126 @t36) (=> @t289 (= (_ @t21 (_ @t126 @t36)) @t36)))) % 0.42/0.82 (assume @p160 (forall (@list @t290 @t291) (= (and @t293 (= (_ @t292 @t290) tptp.id_real)) (and (forall @t24 (= (_ @t290 (_ @t291 @t22)) @t22)) (forall @t14 (= (_ @t291 (_ @t290 @t12)) @t12)))))) % 0.42/0.82 (assume @p161 (forall (@list @t294 @t295) (= (and @t297 (= (_ @t296 @t294) tptp.id_complex_complex)) (and (forall @t24 (= (_ @t294 (_ @t295 @t22)) @t22)) (forall @t19 (= (_ @t295 (_ @t294 @t17)) @t17)))))) % 0.42/0.82 (assume @p162 (forall (@list @t298 @t299) (= (and @t301 (= (_ @t300 @t298) tptp.id_complex)) (and (forall @t14 (= (_ @t298 (_ @t299 @t12)) @t12)) (forall @t24 (= (_ @t299 (_ @t298 @t22)) @t22)))))) % 0.42/0.82 (assume @p163 (forall (@list @t11 @t302) (= (and @t304 (= (_ @t303 @t11) tptp.id_real)) (and (forall @t14 (= (_ @t11 (_ @t302 @t12)) @t12)) (forall @t14 (= (_ @t302 @t13) @t12)))))) % 0.42/0.82 (assume @p164 (forall (@list @t305 @t306) (= (and @t308 (= (_ @t307 @t305) tptp.id_complex_complex)) (and (forall @t14 (= (_ @t305 (_ @t306 @t12)) @t12)) (forall @t19 (= (_ @t306 (_ @t305 @t17)) @t17)))))) % 0.42/0.82 (assume @p165 (forall (@list @t309 @t310) (= (and @t312 (= (_ @t311 @t309) tptp.id_complex)) (and (forall @t19 (= (_ @t309 (_ @t310 @t17)) @t17)) (forall @t24 (= (_ @t310 (_ @t309 @t22)) @t22)))))) % 0.42/0.82 (assume @p166 (forall (@list @t313 @t314) (= (and @t316 (= (_ @t315 @t313) tptp.id_real)) (and (forall @t19 (= (_ @t313 (_ @t314 @t17)) @t17)) (forall @t14 (= (_ @t314 (_ @t313 @t12)) @t12)))))) % 0.42/0.82 (assume @p167 (forall (@list @t16 @t317) (= (and @t319 (= (_ @t318 @t16) tptp.id_complex_complex)) (and (forall @t19 (= (_ @t16 (_ @t317 @t17)) @t17)) (forall @t19 (= (_ @t317 @t18) @t17)))))) % 0.42/0.82 (assume @p168 (forall (@list @t21 @t126) (= (and @t289 (= @t284 tptp.id_complex)) (and (forall @t24 (= (_ @t21 (_ @t126 @t22)) @t22)) (forall @t24 (= (_ @t126 @t23) @t22)))))) % 0.42/0.82 (assume @p169 (forall (@list @t290 @t291 @t320) (=> @t293 (=> (= (_ @t292 @t320) tptp.id_real) (= @t290 @t320))))) % 0.42/0.82 (assume @p170 (forall (@list @t294 @t295 @t321) (=> @t297 (=> (= (_ @t296 @t321) tptp.id_complex_complex) (= @t294 @t321))))) % 0.42/0.82 (assume @p171 (forall (@list @t298 @t299 @t322) (=> @t301 (=> (= (_ @t300 @t322) tptp.id_complex) (= @t298 @t322))))) % 0.42/0.82 (assume @p172 (forall (@list @t11 @t302 @t323) (=> @t304 (=> (= (_ @t303 @t323) tptp.id_real) (= @t11 @t323))))) % 0.42/0.82 (assume @p173 (forall (@list @t305 @t306 @t324) (=> @t308 (=> (= (_ @t307 @t324) tptp.id_complex_complex) (= @t305 @t324))))) % 0.42/0.82 (assume @p174 (forall (@list @t309 @t310 @t325) (=> @t312 (=> (= (_ @t311 @t325) tptp.id_complex) (= @t309 @t325))))) % 0.42/0.82 (assume @p175 (forall (@list @t313 @t314 @t326) (=> @t316 (=> (= (_ @t315 @t326) tptp.id_real) (= @t313 @t326))))) % 0.42/0.82 (assume @p176 (forall (@list @t16 @t317 @t327) (=> @t319 (=> (= (_ @t318 @t327) tptp.id_complex_complex) (= @t16 @t327))))) % 0.42/0.82 (assume @p177 (forall @t158 (=> @t289 (=> (= @t154 tptp.id_complex) (= @t21 @t152))))) % 0.42/0.82 (assume @p178 (forall (@list @t21 @t126 @t328 @t152) (=> (= @t156 @t328) (= @t155 (_ @t329 @t152))))) % 0.42/0.82 (assume @p179 (forall (@list @t126 @t152 @t330 @t21) (=> (= @t154 @t330) (= @t157 (_ @t128 @t330))))) % 0.42/0.82 (assume @p180 (forall (@list @t21 @t126 @t331 @t333 @t152 @t330) (=> (= @t156 (_ @t332 @t333)) (=> (= (_ (_ tptp.comp_c130555887omplex @t333) @t152) @t330) (= @t155 (_ @t332 @t330)))))) % 0.42/0.82 (assume @p181 (forall (@list @t126 @t152 @t335 @t334 @t21 @t328) (=> (= @t154 (_ (_ tptp.comp_c130555887omplex @t335) @t334)) (=> (= (_ @t128 @t335) @t328) (= @t157 (_ @t329 @t334)))))) % 0.42/0.82 (assume @p182 (forall (@list @t286 @t336 @t21 @t126) (=> (= @t286 @t336) (=> @t343 (= @t288 @t337))))) % 0.42/0.82 (assume @p183 (forall @t344 (=> @t288 (=> @t343 @t287)))) % 0.42/0.82 (assume @p184 (_ (_ tptp.ord_le701908932omplex (_ (_ tptp.image_58037603omplex tptp.f) tptp.s)) tptp.t)) % 0.42/0.82 (assume @p185 (forall @t246 (= @t245 (or @t238 @t240)))) % 0.42/0.82 (assume @p186 (forall @t351 (and (=> @t345 (= @t347 @t350)) (=> @t348 (= @t347 tptp.zero_zero_complex))))) % 0.42/0.82 (assume @p187 (forall @t357 (and (=> @t345 (= @t354 @t356)) (=> @t348 (= @t354 tptp.zero_zero_nat))))) % 0.42/0.82 (assume @p188 (forall @t362 (and (=> @t345 (= @t359 @t361)) (=> @t348 (= @t359 tptp.zero_zero_real))))) % 0.42/0.82 (assume @p189 (forall @t351 (and (=> @t345 (= @t363 @t350)) (=> @t348 (= @t363 tptp.zero_zero_complex))))) % 0.42/0.82 (assume @p190 (forall @t357 (and (=> @t345 (= @t364 @t356)) (=> @t348 (= @t364 tptp.zero_zero_nat))))) % 0.42/0.82 (assume @p191 (forall @t362 (and (=> @t345 (= @t365 @t361)) (=> @t348 (= @t365 tptp.zero_zero_real))))) % 0.42/0.82 (assume @p192 (= (_ tptp.arcosh_real tptp.one_one_real) tptp.zero_zero_real)) % 0.42/0.82 (assume @p193 (= (_ tptp.arcosh_complex tptp.one_one_complex) tptp.zero_zero_complex)) % 0.42/0.82 (assume @p194 (forall @t43 (= (_ @t366 tptp.zero_zero_nat) @t31))) % 0.42/0.82 (assume @p195 (= @t367 tptp.id_set_real)) % 0.42/0.82 (assume @p196 (= @t368 tptp.id_set1618538368omplex)) % 0.42/0.82 (assume @p197 (= @t369 tptp.id_set_complex)) % 0.42/0.82 (assume @p198 (forall (@list @t230 @t229 @t372 @t370) (=> @t375 (=> @t374 (_ (_ tptp.ord_le701908932omplex @t373) @t371))))) % 0.42/0.82 (assume @p199 (forall (@list @t21 @t286 @t126 @t336) (=> @t288 (=> @t337 (=> (_ (_ tptp.ord_le701908932omplex @t378) @t336) @t376))))) % 0.42/0.82 (assume @p200 (forall (@list @t21 @t126 @t379) (= (_ @t377 (_ @t380 @t379)) (_ (_ tptp.image_58037603omplex @t156) @t379)))) % 0.42/0.82 (assume @p201 (forall (@list @t21 @t189 @t126 @t269 @t152) (=> (= @t382 (_ @t380 @t269)) (= (_ (_ tptp.image_58037603omplex (_ @t381 @t21)) @t189) (_ (_ tptp.image_58037603omplex (_ @t381 @t126)) @t269))))) % 0.42/0.82 (assume @p202 (forall @t39 (_ @t383 @t38))) % 0.42/0.82 (assume @p203 (forall (@list @t21 @t286 @t336) (=> @t288 (=> (_ (_ tptp.ord_le701908932omplex @t336) @t286) (_ @t262 @t336))))) % 0.42/0.82 (assume @p204 (forall (@list @t230 @t229 @t372 @t370 @t36) (=> @t375 (=> @t374 (=> (_ @t272 @t373) (_ @t272 @t371)))))) % 0.42/0.82 (assume @p205 (forall @t148 (=> @t386 (=> @t384 (_ (_ tptp.ord_less_eq_nat @t99) @t98))))) % 0.42/0.82 (assume @p206 (forall @t151 (=> @t391 (=> @t389 @t387)))) % 0.42/0.82 (assume @p207 (forall @t83 (= @t398 @t397))) % 0.42/0.82 (assume @p208 (forall @t76 (=> @t401 (=> @t400 (_ (_ tptp.ord_less_eq_nat (_ @t115 @t54)) tptp.zero_zero_nat))))) % 0.42/0.82 (assume @p209 (forall @t83 (=> @t396 (=> @t393 (_ (_ tptp.ord_less_eq_real (_ @t119 @t57)) tptp.zero_zero_real))))) % 0.42/0.82 (assume @p210 (forall @t76 (=> @t405 (=> @t404 @t403)))) % 0.42/0.82 (assume @p211 (forall @t83 (=> @t394 (=> @t395 @t407)))) % 0.42/0.82 (assume @p212 (forall @t76 (=> @t401 (=> @t400 @t403)))) % 0.42/0.82 (assume @p213 (forall @t83 (=> @t396 (=> @t393 @t407)))) % 0.42/0.82 (assume @p214 (forall @t76 (=> @t401 (=> @t404 (_ @t383 @t74))))) % 0.42/0.82 (assume @p215 (forall @t83 (=> @t396 (=> @t395 @t398)))) % 0.42/0.82 (assume @p216 (forall @t76 (=> (or (and @t401 @t400) (and @t405 @t404)) @t403))) % 0.42/0.82 (assume @p217 (forall @t83 (=> @t408 @t407))) % 0.42/0.82 (assume @p218 (forall @t83 (= @t407 @t408))) % 0.42/0.82 (assume @p219 (forall @t148 (=> @t386 (=> @t384 (_ @t409 @t116))))) % 0.42/0.82 (assume @p220 (forall @t151 (=> @t391 (=> @t389 @t411)))) % 0.42/0.82 (assume @p221 (forall @t202 (=> @t414 (=> @t413 @t411)))) % 0.42/0.82 (assume @p222 (forall @t83 (=> @t394 (=> @t393 @t398)))) % 0.42/0.82 (assume @p223 (forall @t202 (=> @t414 (=> @t413 @t387)))) % 0.42/0.82 (assume @p224 (forall @t83 (=> @t397 @t398))) % 0.42/0.82 (assume @p225 (forall @t59 (_ @t388 (_ @t62 @t57)))) % 0.42/0.82 (assume @p226 (forall @t419 (=> @t386 (=> @t418 (=> @t401 @t416))))) % 0.42/0.82 (assume @p227 (forall @t423 (=> @t391 (=> @t422 (=> @t396 @t421))))) % 0.42/0.82 (assume @p228 (forall @t419 (=> @t386 (=> @t418 (=> @t404 @t416))))) % 0.42/0.82 (assume @p229 (forall @t423 (=> @t391 (=> @t422 (=> @t395 @t421))))) % 0.42/0.82 (assume @p230 (_ @t383 tptp.one_one_nat)) % 0.42/0.82 (assume @p231 (_ @t388 tptp.one_one_real)) % 0.42/0.82 (assume @p232 (not (_ (_ tptp.ord_less_eq_nat tptp.one_one_nat) tptp.zero_zero_nat))) % 0.42/0.82 (assume @p233 (not (_ @t424 tptp.zero_zero_real))) % 0.42/0.82 (assume @p234 (forall @t344 (=> @t288 (=> (_ @t261 @t378) @t376)))) % 0.42/0.82 (assume @p235 (forall (@list @t21 @t256 @t126 @t429 @t425) (=> @t263 (=> (_ @t261 @t429) (=> @t260 (=> (_ tptp.topolo935673511omplex @t429) (=> (_ (_ tptp.ord_le701908932omplex (_ @t377 @t256)) @t429) (=> (forall (@list @t428) (=> (_ (_ tptp.member_complex @t428) @t256) (= (_ @t126 (_ @t21 @t428)) @t428))) (=> @t427 (= (_ (_ tptp.times_times_complex (_ @t264 @t425)) (_ @t285 @t426)) tptp.one_one_complex)))))))))) % 0.42/0.82 (assume @p236 (forall (@list @t94 @t54) (=> (_ @t417 tptp.one_one_nat) (=> @t401 (_ @t409 @t54))))) % 0.42/0.82 (assume @p237 (forall @t143 (=> (_ @t412 tptp.one_one_real) (=> @t396 (_ @t410 @t57))))) % 0.42/0.82 (assume @p238 (forall @t76 (=> @t431 (=> @t404 (=> @t430 (_ @t402 tptp.one_one_nat)))))) % 0.42/0.82 (assume @p239 (forall @t83 (=> @t433 (=> @t395 (=> @t432 (_ @t406 tptp.one_one_real)))))) % 0.42/0.82 (assume @p240 (forall @t438 (=> @t437 (=> @t436 (=> @t435 (_ (_ tptp.ord_less_eq_real @t361) @t40)))))) % 0.42/0.82 (assume @p241 (forall @t438 (=> @t437 (=> @t436 (=> @t435 (_ (_ tptp.ord_less_eq_real (_ (_ tptp.times_times_real @t213) @t40)) @t40)))))) % 0.42/0.82 (assume @p242 (forall @t76 (=> @t401 (=> @t431 (=> @t430 (= (= @t74 tptp.one_one_nat) (and (= @t54 tptp.one_one_nat) (= @t70 tptp.one_one_nat)))))))) % 0.42/0.82 (assume @p243 (forall @t83 (=> @t396 (=> @t433 (=> @t432 (= (= @t81 tptp.one_one_real) (and @t136 @t140))))))) % 0.42/0.82 (assume @p244 (= (_ tptp.artanh_real tptp.zero_zero_real) tptp.zero_zero_real)) % 0.42/0.82 (assume @p245 (= (_ tptp.artanh_complex tptp.zero_zero_complex) tptp.zero_zero_complex)) % 0.42/0.82 (assume @p246 (= (_ tptp.arsinh_real tptp.zero_zero_real) tptp.zero_zero_real)) % 0.42/0.82 (assume @p247 (= (_ tptp.arsinh_complex tptp.zero_zero_complex) tptp.zero_zero_complex)) % 0.42/0.82 (assume @p248 (forall @t444 (=> @t443 (=> @t441 @t439)))) % 0.42/0.82 (assume @p249 (forall (@list @t63 @t21 @t36 @t189) (=> @t447 (=> @t446 @t445)))) % 0.42/0.82 (assume @p250 (forall @t444 (=> (forall @t342 (=> @t448 (_ @t341 @t269))) @t443))) % 0.42/0.82 (assume @p251 (forall @t43 (_ @t383 @t26))) % 0.42/0.82 (assume @p252 (forall @t56 @t401)) % 0.42/0.82 (assume @p253 (forall @t56 (= @t405 @t72))) % 0.42/0.82 (assume @p254 (forall @t56 (=> @t405 @t72))) % 0.42/0.82 (assume @p255 (forall @t452 (=> @t451 (_ (_ tptp.ord_less_eq_nat (_ @t244 @t252)) (_ @t244 @t449))))) % 0.42/0.82 (assume @p256 (forall @t452 (=> @t451 (_ @t454 (_ @t453 @t237))))) % 0.42/0.82 (assume @p257 (forall (@list @t252 @t449 @t237 @t455) (=> @t451 (=> (_ (_ tptp.ord_less_eq_nat @t237) @t455) (_ @t454 (_ @t453 @t455)))))) % 0.42/0.82 (assume @p258 (forall @t247 (_ @t457 @t456))) % 0.42/0.82 (assume @p259 (forall @t247 (_ @t457 (_ @t243 @t456)))) % 0.42/0.82 (assume @p260 (forall (@list @t36 @t189 @t21) (=> @t446 (_ (_ tptp.member_complex @t172) @t382)))) % 0.42/0.82 (assume @p261 (forall (@list @t5 @t21 @t189) (= (_ @t144 @t382) (exists @t24 (and @t191 (= @t5 @t23)))))) % 0.42/0.82 (assume @p262 (forall @t461 (=> (exists @t460 (and (_ @t459 @t382) (_ @t186 @t458))) (exists @t342 (and @t448 (_ @t186 @t339)))))) % 0.42/0.82 (assume @p263 (forall (@list @t463 @t462 @t21 @t126) (=> (= @t463 @t462) (=> (forall @t342 (=> (_ @t341 @t462) @t340)) (= (_ @t377 @t463) (_ @t380 @t462)))))) % 0.42/0.82 (assume @p264 (forall @t461 (=> (forall @t342 (=> (_ @t341 @t382) @t464)) (forall @t460 (=> (_ @t459 @t189) (_ @t186 (_ @t21 @t458))))))) % 0.42/0.82 (assume @p265 (forall (@list @t36 @t189 @t63 @t21) (=> @t446 (=> @t447 @t445)))) % 0.42/0.82 (assume @p266 (forall (@list @t189 @t269 @t36) (=> @t443 (=> @t446 (_ @t272 @t269))))) % 0.42/0.82 (assume @p267 (forall (@list @t189 @t269 @t85) (=> @t443 (=> (_ @t465 @t189) (_ @t465 @t269))))) % 0.42/0.82 (assume @p268 (forall @t444 (=> @t439 (not (=> @t443 (not @t441)))))) % 0.42/0.82 (assume @p269 (forall @t444 (=> @t439 @t443))) % 0.42/0.82 (assume @p270 (forall @t444 (=> @t439 @t441))) % 0.42/0.82 (assume @p271 (= tptp.ord_le701908932omplex (lambda @t470 (forall (@list @t467) (=> (_ @t468 @t469) (_ @t468 @t466)))))) % 0.42/0.82 (assume @p272 (forall @t192 (_ @t442 @t189))) % 0.42/0.82 (assume @p273 (forall @t473 (=> (forall @t342 (=> @t464 (_ @t471 @t338))) @t472))) % 0.42/0.82 (assume @p274 (forall (@list @t189 @t269 @t230) (=> @t443 (=> (_ @t440 @t230) (_ @t442 @t230))))) % 0.42/0.82 (assume @p275 (= @t476 (lambda @t470 (and (_ (_ tptp.ord_le701908932omplex @t469) @t466) (_ (_ tptp.ord_le701908932omplex @t466) @t469))))) % 0.42/0.82 (assume @p276 (forall @t473 (= @t472 (forall @t24 (=> (_ @t186 @t22) (_ @t471 @t22)))))) % 0.42/0.82 (assume @p277 (forall (@list @t189 @t269 @t21) (=> @t443 (_ @t477 (_ @t377 @t269))))) % 0.42/0.82 (assume @p278 (forall (@list @t189 @t21 @t269) (=> (forall @t342 (=> @t448 (_ (_ tptp.member_complex @t339) @t269))) @t478))) % 0.42/0.82 (assume @p279 (forall @t481 (=> @t480 (not (forall (@list @t479) (=> (_ (_ tptp.ord_le701908932omplex @t479) @t189) (not (= @t269 (_ @t377 @t479))))))))) % 0.42/0.82 (assume @p280 (forall (@list @t21 @t189 @t269) (= @t478 (forall @t24 (=> @t191 (_ (_ tptp.member_complex @t23) @t269)))))) % 0.42/0.82 (assume @p281 (forall @t481 (= @t480 (exists (@list @t482) (and (_ (_ tptp.ord_le701908932omplex @t482) @t189) (= @t269 (_ @t377 @t482))))))) % 0.42/0.82 (assume @p282 (forall (@list @t483) (_ @t484 @t483))) % 0.42/0.82 (assume @p283 (forall @t39 (_ @t485 @t38))) % 0.42/0.82 (assume @p284 (forall @t41 (_ @t486 @t40))) % 0.42/0.82 (assume @p285 (forall (@list @t497 @t490 @t495) (=> (forall @t505 (=> @t504 (_ @t497 (_ @t490 @t502)))) (=> (forall @t505 (=> @t504 (forall (@list @t501) (=> (_ @t495 @t501) (and (_ @t388 @t503) (_ (_ tptp.ord_less_eq_real @t503) tptp.one_one_real)))))) (exists (@list @t492) (and (forall @t499 (_ (_ tptp.ord_less_eq_nat @t493) tptp.one_one_nat)) (forall @t499 (=> (and @t498 @t496 (= @t489 tptp.zero_zero_real)) @t500)) (forall @t499 (=> (and @t498 @t496 (= @t489 tptp.one_one_real)) @t494)) (forall @t499 (=> (and @t498 @t496 @t500) (_ (_ tptp.ord_less_eq_real @t489) @t491))) (forall @t499 (=> (and @t498 @t496 @t494) (_ (_ tptp.ord_less_eq_real @t491) @t489))))))))) % 0.42/0.82 (assume @p286 (forall (@list @t506 @t280) (= (_ @t506 (_ @t367 @t280)) (_ @t506 @t280)))) % 0.42/0.82 (assume @p287 (forall (@list @t508 @t507) (= (_ @t508 (_ @t368 @t507)) (_ @t508 @t507)))) % 0.42/0.82 (assume @p288 (forall (@list @t509 @t189) (= (_ @t509 (_ @t369 @t189)) (_ @t509 @t189)))) % 0.42/0.82 (assume @p289 (forall @t43 (_ @t366 @t26))) % 0.42/0.82 (assume @p290 (forall @t452 (=> @t451 (=> (_ (_ tptp.ord_less_eq_nat @t449) @t237) (_ @t450 @t237))))) % 0.42/0.82 (assume @p291 (forall @t250 (=> @t240 @t510))) % 0.42/0.82 (assume @p292 (forall @t250 (=> @t510 (=> @t511 @t240)))) % 0.42/0.82 (assume @p293 (forall @t250 (or @t510 @t511))) % 0.42/0.82 (assume @p294 (forall (@list @t514 @t237 @t70) (=> (_ @t514 @t237) (=> (forall (@list @t515) (=> (_ @t514 @t515) (_ (_ tptp.ord_less_eq_nat @t515) @t70))) (exists (@list @t512) (and (_ @t514 @t512) (forall (@list @t513) (=> (_ @t514 @t513) (_ (_ tptp.ord_less_eq_nat @t513) @t512))))))))) % 0.42/0.82 (assume @p295 (forall (@list @t516 @t517) (=> @t521 (=> @t520 @t518)))) % 0.42/0.82 (assume @p296 (forall (@list @t70 @t54) (=> @t522 (=> @t386 @t93)))) % 0.42/0.82 (assume @p297 (forall (@list @t77 @t57) (=> @t414 (=> @t391 @t102)))) % 0.42/0.82 (assume @p298 (= @t476 (lambda (@list @t524 @t523) (and (_ (_ tptp.ord_le701908932omplex @t523) @t524) (_ (_ tptp.ord_le701908932omplex @t524) @t523))))) % 0.42/0.82 (assume @p299 (= (lambda (@list @t526 @t525) (= @t526 @t525)) (lambda @t197 (and (_ (_ tptp.ord_less_eq_nat @t196) @t195) (_ (_ tptp.ord_less_eq_nat @t195) @t196))))) % 0.42/0.82 (assume @p300 (= (lambda (@list @t528 @t527) (= @t528 @t527)) (lambda @t200 (and (_ (_ tptp.ord_less_eq_real @t199) @t198) (_ (_ tptp.ord_less_eq_real @t198) @t199))))) % 0.42/0.82 (assume @p301 (forall (@list @t516 @t517 @t529) (=> @t521 (=> (_ @t530 @t516) (_ @t530 @t517))))) % 0.42/0.82 (assume @p302 (forall @t201 (=> @t522 (=> (_ @t417 @t70) (_ @t417 @t54))))) % 0.42/0.82 (assume @p303 (forall @t202 (=> @t414 (=> (_ @t412 @t77) (_ @t412 @t57))))) % 0.42/0.82 (assume @p304 (forall (@list @t531 @t54 @t70) (=> (forall @t277 (=> (_ (_ tptp.ord_less_eq_nat @t276) @t274) @t532)) (=> (forall @t277 (=> (_ (_ @t531 @t274) @t276) @t532)) (_ (_ @t531 @t54) @t70))))) % 0.42/0.82 (assume @p305 (forall (@list @t533 @t57 @t77) (=> (forall @t282 (=> (_ (_ tptp.ord_less_eq_real @t281) @t279) @t534)) (=> (forall @t282 (=> (_ (_ @t533 @t279) @t281) @t534)) (_ (_ @t533 @t57) @t77))))) % 0.42/0.82 (assume @p306 (forall (@list @t517) (_ @t519 @t517))) % 0.42/0.82 (assume @p307 (forall @t56 (_ @t385 @t54))) % 0.42/0.82 (assume @p308 (forall @t59 (_ @t390 @t57))) % 0.42/0.82 (assume @p309 (forall (@list @t483 @t536 @t535) (=> (_ @t484 @t536) (=> (_ (_ tptp.ord_le701908932omplex @t536) @t535) (_ @t484 @t535))))) % 0.42/0.82 (assume @p310 (forall (@list @t38 @t352 @t537) (=> (_ @t485 @t352) (=> (_ (_ tptp.ord_less_eq_nat @t352) @t537) (_ @t485 @t537))))) % 0.42/0.82 (assume @p311 (forall (@list @t40 @t213 @t1) (=> @t538 (=> (_ @t434 @t1) (_ @t486 @t1))))) % 0.42/0.82 (assume @p312 (forall (@list @t517 @t516) (=> @t520 (=> @t521 @t518)))) % 0.42/0.82 (assume @p313 (forall @t76 (=> @t386 (=> @t522 @t93)))) % 0.42/0.82 (assume @p314 (forall @t83 (=> @t391 (=> @t414 @t102)))) % 0.42/0.82 (assume @p315 (forall @t148 (=> @t386 (=> (= @t70 @t94) (_ @t385 @t94))))) % 0.42/0.82 (assume @p316 (forall @t151 (=> @t391 (=> (= @t77 @t103) @t539)))) % 0.42/0.82 (assume @p317 (forall @t202 (=> @t414 (=> @t389 (_ (_ tptp.ord_less_eq_real @t120) @t121))))) % 0.42/0.82 (assume @p318 (forall @t202 (=> @t414 (=> @t389 (_ (_ tptp.ord_less_eq_real @t107) @t108))))) % 0.42/0.82 (assume @p319 (forall (@list @t213 @t40) (=> (not @t540) @t538))) % 0.42/0.82 (assume @p320 (forall @t438 (=> (not @t538) @t540))) % 0.42/0.82 (assume @p321 (forall @t151 (=> @t391 (=> (_ @t392 @t103) @t539)))) % 0.42/0.82 (assume @p322 (forall @t41 (=> (_ @t424 @t40) (_ @t388 (_ tptp.ln_ln_real @t40))))) % 0.42/0.82 (assume @p323 (= (_ tptp.ln_ln_complex tptp.one_one_complex) tptp.zero_zero_complex)) % 0.42/0.82 (assume @p324 (forall (@list @t21 @t256 @t5 @t425) (=> @t263 (=> @t260 (=> (_ tptp.topolo2127351575omplex @t256) (=> (forall (@list @t541) (= (_ (_ (_ (_ tptp.compow1098280738omplex @t541) tptp.deriv_complex) @t21) @t5) tptp.zero_zero_complex)) (=> @t259 (=> @t427 (= @t426 tptp.zero_zero_complex))))))))) % 0.42/0.82 (assume @p325 (forall @t542 (= (_ (_ (_ tptp.if_nat false) @t38) @t352) @t352))) % 0.42/0.82 (assume @p326 (forall @t542 (= (_ (_ (_ tptp.if_nat true) @t38) @t352) @t38))) % 0.42/0.82 (assume @p327 (forall @t438 (= (_ (_ (_ tptp.if_real false) @t40) @t213) @t213))) % 0.42/0.82 (assume @p328 (forall @t438 (= (_ (_ (_ tptp.if_real true) @t40) @t213) @t40))) % 0.42/0.82 (assume @p329 (forall (@list @t222) (or (= @t222 true) (= @t222 false)))) % 0.42/0.82 (assume @p330 (forall @t543 (= (_ (_ (_ tptp.if_complex false) @t36) @t209) @t209))) % 0.42/0.82 (assume @p331 (forall @t543 (= (_ (_ (_ tptp.if_complex true) @t36) @t209) @t36))) % 0.42/0.82 (assume @p332 @t545) % 0.42/0.82 (assume @p333 true) % 0.42/0.82 (step @p334 (= tptp.id_real @t546) :rule refl :args (@t546)) % 0.42/0.82 (step @p335 (= tptp.id_complex_complex @t548) :rule refl :args (@t548)) % 0.42/0.82 (step @p336 (= tptp.id_complex @t549) :rule refl :args (@t549)) % 0.42/0.82 (step @p337 (= tptp.comp_c130555887omplex @t552) :rule refl :args (@t552)) % 0.42/0.82 (step @p338 (= tptp.ord_le701908932omplex @t553) :rule refl :args (@t553)) % 0.42/0.82 (step @p339 :rule eq-symm :args (@t554 @t556)) % 0.42/0.82 (step @p340 :rule eq-refl :args (@t549)) % 0.42/0.82 (step @p341 :rule skolem_intro :args (@t555)) % 0.42/0.82 (step @p342 :rule refl :args (@t549)) % 0.42/0.82 (step @p343 :rule cong :premises (@p342 @p341) :args ((= @t549 @t555))) % 0.42/0.82 (step @p344 :rule trans :premises (@p343 @p340)) % 0.42/0.82 (step @p345 :rule true_elim :premises (@p344)) % 0.42/0.82 (step @p346 :rule refl :args (tptp.deriv_complex)) % 0.42/0.82 (step @p347 :rule ho_cong :premises (@p346 @p345)) % 0.42/0.82 (step @p348 :rule eq-refl :args (@t8)) % 0.42/0.82 (step @p349 :rule skolem_intro :args (@t554)) % 0.42/0.82 (step @p350 :rule refl :args (@t8)) % 0.42/0.82 (step @p351 :rule cong :premises (@p350 @p349) :args ((= @t8 @t554))) % 0.42/0.82 (step @p352 :rule trans :premises (@p351 @p348)) % 0.42/0.82 (step @p353 :rule true_elim :premises (@p352)) % 0.42/0.82 (step @p354 :rule cong :premises (@p353 @p347) :args ((= @t8 @t557))) % 0.42/0.82 (step @p355 :rule trans :premises (@p354 @p339)) % 0.42/0.82 (step @p356 :rule eq-symm :args (@t557 @t8)) % 0.42/0.82 (step @p357 :rule ho_cong :premises (@p346 @p336)) % 0.42/0.82 (step @p358 :rule cong :premises (@p357 @p350) :args (@t10)) % 0.42/0.82 (step @p359 :rule trans :premises (@p358 @p356)) % 0.42/0.82 (step @p360 :rule trans :premises (@p359 @p355)) % 0.42/0.82 (step @p361 :rule eq_resolve :premises (@p4 @p360)) % 0.42/0.82 (step @p362 :rule refl :args (@t558)) % 0.42/0.82 (step @p363 :rule refl :args (@t559)) % 0.42/0.82 (step @p364 :rule cong :premises (@p363 @p362) :args ((= @t559 @t558))) % 0.42/0.82 (step @p365 :rule symm :premises (@p364)) % 0.42/0.82 (step @p366 :rule eq_resolve :premises (@p363 @p365)) % 0.42/0.82 (step @p367 :rule refl :args (tptp.w)) % 0.42/0.82 (step @p368 :rule ho_cong :premises (@p347 @p367)) % 0.42/0.82 (step @p369 :rule trans :premises (@p368 @p366)) % 0.42/0.82 (step @p370 :rule refl :args (tptp.one_one_complex)) % 0.42/0.82 (step @p371 :rule cong :premises (@p370 @p369) :args (@t561)) % 0.42/0.82 (step @p372 :rule cong :premises (@p371) :args ((not @t561))) % 0.42/0.82 (step @p373 :rule eq-symm :args (@t560 tptp.one_one_complex)) % 0.42/0.82 (step @p374 :rule cong :premises (@p373) :args ((not (= @t560 tptp.one_one_complex)))) % 0.42/0.82 (step @p375 :rule ho_cong :premises (@p357 @p367)) % 0.42/0.82 (step @p376 :rule cong :premises (@p375 @p370) :args (@t544)) % 0.42/0.82 (step @p377 :rule cong :premises (@p376) :args (@t545)) % 0.42/0.82 (step @p378 :rule trans :premises (@p377 @p374)) % 0.42/0.82 (step @p379 :rule trans :premises (@p378 @p372)) % 0.42/0.82 (step @p380 :rule eq_resolve :premises (@p332 @p379)) % 0.42/0.82 (step @p381 :rule cong :premises (@p370 @p366) :args (@t562)) % 0.42/0.82 (step @p382 :rule refl :args (@t563)) % 0.42/0.82 (step @p383 :rule cong :premises (@p382 @p381) :args ((=> @t563 @t562))) % 0.42/0.82 (step @p384 :rule eq-symm :args (@t559 tptp.one_one_complex)) % 0.42/0.82 (step @p385 :rule cong :premises (@p382 @p384) :args (@t564)) % 0.42/0.82 (step @p386 :rule trans :premises (@p385 @p383)) % 0.42/0.82 ; WARNING: add trust step for TRUST % 0.42/0.82 ; trust TRUST THEORY_LEMMA % 0.42/0.82 (step @p387 :rule trust :premises () :args (@t564)) % 0.42/0.82 (step @p388 :rule eq_resolve :premises (@p387 @p386)) % 0.42/0.82 (step @p389 :rule implies_elim :premises (@p388)) % 0.42/0.82 (step @p390 :rule reordering :premises (@p389) :args ((or @t565 (not @t563)))) % 0.42/0.82 (step @p391 false :rule chain_m_resolution :premises (@p390 @p380 @p361) :args (false (@list true false) (@list @t565 @t563))) % 0.42/0.82 ) % 0.42/0.82 % SZS output end Proof % 0.42/0.82 % cvc5 exiting %------------------------------------------------------------------------------