%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP108^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n009.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:05 AM UTC 2026 % Result : Theorem 0.44s 0.81s % Output : Proof 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP108^1 : TPTP v9.2.1. Released v7.5.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n009.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:14:29 EDT 2026 % 0.17/0.34 % CPUTime : % 0.41/0.58 %----Proving TH0 % 0.44/0.81 --- 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.44/0.81 % SZS status Theorem % 0.44/0.81 % SZS output start Proof % 0.44/0.81 ( % 0.44/0.81 (declare-sort tptp.set_a 0) % 0.44/0.81 (declare-sort tptp.partia1833973666xt_a_b 0) % 0.44/0.81 (declare-sort tptp.a 0) % 0.44/0.81 (declare-sort tptp.int 0) % 0.44/0.81 (declare-sort tptp.product_prod_a_a 0) % 0.44/0.81 (declare-const tptp.a_inv_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.a)) % 0.44/0.81 (declare-const tptp.add_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.a tptp.a)) % 0.44/0.81 (declare-const tptp.uminus_uminus_int (-> tptp.int tptp.int)) % 0.44/0.81 (declare-const tptp.plus_plus_int (-> tptp.int tptp.int tptp.int)) % 0.44/0.81 (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool)) % 0.44/0.81 (declare-const tptp.uminus_uminus_set_a (-> tptp.set_a tptp.set_a)) % 0.44/0.81 (declare-const tptp.minus_minus_set_a (-> tptp.set_a tptp.set_a tptp.set_a)) % 0.44/0.81 (declare-const tptp.additi2104487374up_a_b (-> tptp.set_a tptp.partia1833973666xt_a_b Bool)) % 0.44/0.81 (declare-const tptp.r2 tptp.a) % 0.44/0.81 (declare-const tptp.locali1648887798ac_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.81 (declare-const tptp.product_snd_a_a (-> tptp.product_prod_a_a tptp.a)) % 0.44/0.81 (declare-const tptp.y tptp.product_prod_a_a) % 0.44/0.81 (declare-const tptp.product_fst_a_a (-> tptp.product_prod_a_a tptp.a)) % 0.44/0.81 (declare-const tptp.a_l_coset_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.set_a tptp.set_a)) % 0.44/0.81 (declare-const tptp.x tptp.product_prod_a_a) % 0.44/0.81 (declare-const tptp.ord_less_eq_int (-> tptp.int tptp.int Bool)) % 0.44/0.81 (declare-const tptp.s2 tptp.a) % 0.44/0.81 (declare-const tptp.locali880295127ng_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.81 (declare-const tptp.s3 tptp.a) % 0.44/0.81 (declare-const tptp.locali425460998xt_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.81 (declare-const tptp.mult_a_ring_ext_a_b (-> tptp.partia1833973666xt_a_b tptp.a tptp.a tptp.a)) % 0.44/0.81 (declare-const tptp.t2 tptp.a) % 0.44/0.81 (declare-const tptp.t tptp.a) % 0.44/0.81 (declare-const tptp.bot_bot_set_a tptp.set_a) % 0.44/0.81 (declare-const tptp.partia1066395285xt_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a)) % 0.44/0.81 (declare-const tptp.add_pow_a_b_int (-> tptp.partia1833973666xt_a_b tptp.int tptp.a tptp.a)) % 0.44/0.81 (declare-const tptp.set_add_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a tptp.set_a tptp.set_a)) % 0.44/0.81 (declare-const tptp.r tptp.partia1833973666xt_a_b) % 0.44/0.81 (declare-const tptp.r3 tptp.a) % 0.44/0.81 (declare-const tptp.locali807230110ng_a_b (-> tptp.partia1833973666xt_a_b tptp.set_a Bool)) % 0.44/0.81 (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a)) % 0.44/0.81 (declare-const tptp.zero_a_b (-> tptp.partia1833973666xt_a_b tptp.a)) % 0.44/0.81 (declare-const tptp.s tptp.set_a) % 0.44/0.81 (declare-const tptp.semiring_a_b (-> tptp.partia1833973666xt_a_b Bool)) % 0.44/0.81 (define tptp.a_minus_a_b () (let ((_let_1 (@var "Y5" tptp.a))) (let ((_let_2 (@var "R2" tptp.partia1833973666xt_a_b))) (let ((_let_3 (@var "X2" tptp.a))) (lambda (@list _let_2 _let_3 _let_1) (_ (_ (_ tptp.add_a_b _let_2) _let_3) (_ (_ tptp.a_inv_a_b _let_2) _let_1))))))) % 0.44/0.81 (define tptp.minus_minus_int () (let ((_let_1 (@var "B2" tptp.int))) (let ((_let_2 (@var "A3" tptp.int))) (lambda (@list _let_2 _let_1) (_ (_ tptp.plus_plus_int _let_2) (_ tptp.uminus_uminus_int _let_1)))))) % 0.44/0.81 (define tptp.ord_less_eq_set_a () (let ((_let_1 (@var "B4" tptp.set_a))) (let ((_let_2 (@var "X2" tptp.a))) (let ((_let_3 (_ tptp.member_a _let_2))) (let ((_let_4 (@var "A4" tptp.set_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.81 (define @t1 () (_ tptp.partia1066395285xt_a_b tptp.r)) % 0.44/0.81 (define @t2 () (_ tptp.member_a tptp.t)) % 0.44/0.81 (define @t3 () (_ @t2 @t1)) % 0.44/0.81 (define @t4 () (_ tptp.member_a tptp.t2)) % 0.44/0.81 (define @t5 () (_ @t4 @t1)) % 0.44/0.81 (define @t6 () (@var "B" tptp.a)) % 0.44/0.81 (define @t7 () (@var "C" tptp.a)) % 0.44/0.81 (define @t8 () (_ tptp.add_a_b tptp.r)) % 0.44/0.81 (define @t9 () (_ @t8 @t7)) % 0.44/0.81 (define @t10 () (@var "A" tptp.a)) % 0.44/0.81 (define @t11 () (= @t10 @t6)) % 0.44/0.81 (define @t12 () (@list @t10 @t6 @t7)) % 0.44/0.81 (define @t13 () (_ tptp.a_minus_a_b tptp.r)) % 0.44/0.81 (define @t14 () (_ @t13 @t7)) % 0.44/0.81 (define @t15 () (_ @t14 @t10)) % 0.44/0.81 (define @t16 () (@var "Z" tptp.a)) % 0.44/0.81 (define @t17 () (@var "Y" tptp.a)) % 0.44/0.81 (define @t18 () (_ tptp.mult_a_ring_ext_a_b tptp.r)) % 0.44/0.81 (define @t19 () (_ @t18 @t17)) % 0.44/0.81 (define @t20 () (_ @t19 @t16)) % 0.44/0.81 (define @t21 () (@var "X" tptp.a)) % 0.44/0.81 (define @t22 () (_ @t18 @t21)) % 0.44/0.81 (define @t23 () (_ @t22 @t20)) % 0.44/0.81 (define @t24 () (_ @t22 @t17)) % 0.44/0.81 (define @t25 () (_ tptp.member_a @t16)) % 0.44/0.81 (define @t26 () (_ @t25 @t1)) % 0.44/0.81 (define @t27 () (_ tptp.member_a @t17)) % 0.44/0.81 (define @t28 () (_ @t27 @t1)) % 0.44/0.81 (define @t29 () (_ tptp.member_a @t21)) % 0.44/0.81 (define @t30 () (_ @t29 @t1)) % 0.44/0.81 (define @t31 () (@list @t21 @t17 @t16)) % 0.44/0.81 (define @t32 () (@list @t21 @t17)) % 0.44/0.81 (define @t33 () (_ @t22 @t16)) % 0.44/0.81 (define @t34 () (_ @t8 @t17)) % 0.44/0.81 (define @t35 () (_ @t8 @t21)) % 0.44/0.81 (define @t36 () (_ @t35 (_ @t34 @t16))) % 0.44/0.81 (define @t37 () (_ @t35 @t17)) % 0.44/0.81 (define @t38 () (_ @t34 @t21)) % 0.44/0.81 (define @t39 () (= @t37 @t38)) % 0.44/0.81 (define @t40 () (_ tptp.product_fst_a_a tptp.x)) % 0.44/0.81 (define @t41 () (_ tptp.product_snd_a_a tptp.y)) % 0.44/0.81 (define @t42 () (_ @t18 @t41)) % 0.44/0.81 (define @t43 () (_ @t42 @t40)) % 0.44/0.81 (define @t44 () (_ @t18 tptp.s2)) % 0.44/0.81 (define @t45 () (_ @t44 tptp.s3)) % 0.44/0.81 (define @t46 () (_ @t18 @t45)) % 0.44/0.81 (define @t47 () (_ @t46 @t43)) % 0.44/0.81 (define @t48 () (_ @t18 tptp.s3)) % 0.44/0.81 (define @t49 () (_ @t48 tptp.r2)) % 0.44/0.81 (define @t50 () (_ tptp.product_snd_a_a tptp.x)) % 0.44/0.81 (define @t51 () (_ @t18 @t50)) % 0.44/0.81 (define @t52 () (_ @t51 @t41)) % 0.44/0.81 (define @t53 () (_ @t18 @t52)) % 0.44/0.81 (define @t54 () (_ @t53 @t49)) % 0.44/0.81 (define @t55 () (_ (_ @t13 @t54) @t47)) % 0.44/0.81 (define @t56 () (_ (_ tptp.member_a @t55) @t1)) % 0.44/0.81 (define @t57 () (_ tptp.product_fst_a_a tptp.y)) % 0.44/0.81 (define @t58 () (_ @t51 @t57)) % 0.44/0.81 (define @t59 () (_ @t46 @t58)) % 0.44/0.81 (define @t60 () (_ @t44 tptp.r3)) % 0.44/0.81 (define @t61 () (_ @t53 @t60)) % 0.44/0.81 (define @t62 () (_ (_ @t13 @t61) @t59)) % 0.44/0.81 (define @t63 () (_ (_ tptp.member_a @t62) @t1)) % 0.44/0.81 (define @t64 () (_ @t18 @t16)) % 0.44/0.81 (define @t65 () (@var "D" tptp.a)) % 0.44/0.81 (define @t66 () (_ @t8 @t10)) % 0.44/0.81 (define @t67 () (_ @t66 @t6)) % 0.44/0.81 (define @t68 () (_ tptp.member_a @t7)) % 0.44/0.81 (define @t69 () (_ @t68 @t1)) % 0.44/0.81 (define @t70 () (_ (_ tptp.member_a @t6) @t1)) % 0.44/0.81 (define @t71 () (_ tptp.member_a @t10)) % 0.44/0.81 (define @t72 () (_ @t71 @t1)) % 0.44/0.81 (define @t73 () (_ @t18 tptp.t2)) % 0.44/0.81 (define @t74 () (_ @t73 tptp.t)) % 0.44/0.81 (define @t75 () (_ @t18 @t74)) % 0.44/0.81 (define @t76 () (_ @t75 @t62)) % 0.44/0.81 (define @t77 () (_ @t75 @t55)) % 0.44/0.81 (define @t78 () (_ (_ @t8 @t77) @t76)) % 0.44/0.81 (define @t79 () (_ @t48 @t57)) % 0.44/0.81 (define @t80 () (_ @t42 tptp.r3)) % 0.44/0.81 (define @t81 () (_ (_ @t13 @t80) @t79)) % 0.44/0.81 (define @t82 () (_ @t18 tptp.t)) % 0.44/0.81 (define @t83 () (_ @t82 @t81)) % 0.44/0.81 (define @t84 () (_ @t73 tptp.s2)) % 0.44/0.81 (define @t85 () (_ (_ @t18 @t84) @t50)) % 0.44/0.81 (define @t86 () (_ @t18 @t85)) % 0.44/0.81 (define @t87 () (_ @t86 @t83)) % 0.44/0.81 (define @t88 () (_ @t44 @t40)) % 0.44/0.81 (define @t89 () (_ @t51 tptp.r2)) % 0.44/0.81 (define @t90 () (_ (_ @t13 @t89) @t88)) % 0.44/0.81 (define @t91 () (_ @t73 @t90)) % 0.44/0.81 (define @t92 () (_ @t82 tptp.s3)) % 0.44/0.81 (define @t93 () (_ (_ @t18 @t92) @t41)) % 0.44/0.81 (define @t94 () (_ @t18 @t93)) % 0.44/0.81 (define @t95 () (_ @t94 @t91)) % 0.44/0.81 (define @t96 () (_ (_ @t8 @t95) @t87)) % 0.44/0.81 (define @t97 () (= @t96 @t78)) % 0.44/0.81 (define @t98 () (_ @t75 (_ (_ @t8 @t55) @t62))) % 0.44/0.81 (define @t99 () (= @t98 @t78)) % 0.44/0.81 (define @t100 () (_ tptp.member_a @t74)) % 0.44/0.81 (define @t101 () (_ @t100 @t1)) % 0.44/0.81 (define @t102 () (=> @t101 @t99)) % 0.44/0.81 (define @t103 () (=> @t63 @t102)) % 0.44/0.81 (define @t104 () (=> @t56 @t103)) % 0.44/0.81 (define @t105 () (_ (_ @t8 @t43) @t58)) % 0.44/0.81 (define @t106 () (_ (_ @t13 (_ @t82 @t80)) (_ @t82 @t79))) % 0.44/0.81 (define @t107 () (_ @t18 (_ @t94 tptp.t2))) % 0.44/0.81 (define @t108 () (_ @t107 @t89)) % 0.44/0.81 (define @t109 () (_ @t75 @t54)) % 0.44/0.81 (define @t110 () (_ @t107 @t88)) % 0.44/0.81 (define @t111 () (_ @t75 @t47)) % 0.44/0.81 (define @t112 () (_ @t8 @t54)) % 0.44/0.81 (define @t113 () (_ @t53 (_ (_ @t8 @t49) @t60))) % 0.44/0.81 (define @t114 () (_ @t18 (_ @t75 @t45))) % 0.44/0.81 (define @t115 () (_ (_ @t13 @t108) @t110)) % 0.44/0.81 (define @t116 () (_ (_ @t13 @t109) @t111)) % 0.44/0.81 (define @t117 () (_ @t18 (_ @t86 tptp.t))) % 0.44/0.81 (define @t118 () (_ @t75 @t59)) % 0.44/0.81 (define @t119 () (_ @t75 @t61)) % 0.44/0.81 (define @t120 () (_ (_ @t13 @t119) @t118)) % 0.44/0.81 (define @t121 () (@var "P" (-> tptp.a Bool))) % 0.44/0.81 (define @t122 () (_ tptp.collect_a @t121)) % 0.44/0.81 (define @t123 () (@var "A2" tptp.set_a)) % 0.44/0.81 (define @t124 () (@var "X2" tptp.a)) % 0.44/0.81 (define @t125 () (_ tptp.member_a @t124)) % 0.44/0.81 (define @t126 () (_ @t125 @t123)) % 0.44/0.81 (define @t127 () (@list @t124)) % 0.44/0.81 (define @t128 () (@list @t123)) % 0.44/0.81 (define @t129 () (@var "Q" (-> tptp.a Bool))) % 0.44/0.81 (define @t130 () (@var "X3" tptp.a)) % 0.44/0.81 (define @t131 () (@list @t130)) % 0.44/0.81 (define @t132 () (_ @t18 (_ @t75 @t52))) % 0.44/0.81 (define @t133 () (_ @t8 @t116)) % 0.44/0.81 (define @t134 () (_ tptp.zero_a_b tptp.r)) % 0.44/0.81 (define @t135 () (_ (_ @t13 @t21) @t17)) % 0.44/0.81 (define @t136 () (_ tptp.member_a @t24)) % 0.44/0.81 (define @t137 () (_ @t136 @t1)) % 0.44/0.81 (define @t138 () (=> @t28 @t137)) % 0.44/0.81 (define @t139 () (forall @t32 (=> @t30 @t138))) % 0.44/0.81 (define @t140 () (_ tptp.a_inv_a_b tptp.r)) % 0.44/0.81 (define @t141 () (_ @t140 @t17)) % 0.44/0.81 (define @t142 () (@var "Q2" tptp.product_prod_a_a)) % 0.44/0.81 (define @t143 () (@var "P2" tptp.product_prod_a_a)) % 0.44/0.81 (define @t144 () (_ tptp.product_snd_a_a @t143)) % 0.44/0.81 (define @t145 () (_ tptp.product_fst_a_a @t143)) % 0.44/0.81 (define @t146 () (@var "Y2" tptp.a)) % 0.44/0.81 (define @t147 () (@var "P" (-> tptp.a tptp.a Bool))) % 0.44/0.81 (define @t148 () (@var "Prod2" tptp.product_prod_a_a)) % 0.44/0.81 (define @t149 () (@var "Prod" tptp.product_prod_a_a)) % 0.44/0.81 (define @t150 () (@var "Y3" tptp.a)) % 0.44/0.81 (define @t151 () (= @t38 @t134)) % 0.44/0.81 (define @t152 () (_ tptp.member_a @t130)) % 0.44/0.81 (define @t153 () (_ @t152 @t1)) % 0.44/0.81 (define @t154 () (@list @t21)) % 0.44/0.81 (define @t155 () (@var "U" tptp.a)) % 0.44/0.81 (define @t156 () (_ @t8 @t130)) % 0.44/0.81 (define @t157 () (= @t37 @t134)) % 0.44/0.81 (define @t158 () (_ @t140 @t24)) % 0.44/0.81 (define @t159 () (_ @t140 @t21)) % 0.44/0.81 (define @t160 () (_ @t8 @t159)) % 0.44/0.81 (define @t161 () (_ @t140 @t37)) % 0.44/0.81 (define @t162 () (= @t6 (_ @t66 @t7))) % 0.44/0.81 (define @t163 () (_ @t8 @t6)) % 0.44/0.81 (define @t164 () (_ @t163 (_ @t140 @t7))) % 0.44/0.81 (define @t165 () (= @t7 (_ @t163 @t10))) % 0.44/0.81 (define @t166 () (_ (_ @t8 (_ @t140 @t6)) @t7)) % 0.44/0.81 (define @t167 () (@var "T" tptp.a)) % 0.44/0.81 (define @t168 () (@var "T2" tptp.a)) % 0.44/0.81 (define @t169 () (_ tptp.member_a @t134)) % 0.44/0.81 (define @t170 () (= @t10 @t134)) % 0.44/0.81 (define @t171 () (_ @t66 @t21)) % 0.44/0.81 (define @t172 () (@list @t21 @t10)) % 0.44/0.81 (define @t173 () (_ @t35 @t10)) % 0.44/0.81 (define @t174 () (@var "T3" tptp.product_prod_a_a)) % 0.44/0.81 (define @t175 () (@var "S" tptp.product_prod_a_a)) % 0.44/0.81 (define @t176 () (@var "Z2" tptp.product_prod_a_a)) % 0.44/0.81 (define @t177 () (@var "Y4" tptp.product_prod_a_a)) % 0.44/0.81 (define @t178 () (@var "I" tptp.int)) % 0.44/0.81 (define @t179 () (_ tptp.add_pow_a_b_int tptp.r)) % 0.44/0.81 (define @t180 () (_ @t179 @t178)) % 0.44/0.81 (define @t181 () (_ @t180 @t21)) % 0.44/0.81 (define @t182 () (_ @t140 @t181)) % 0.44/0.81 (define @t183 () (@list @t21 @t178)) % 0.44/0.81 (define @t184 () (@var "R" tptp.partia1833973666xt_a_b)) % 0.44/0.81 (define @t185 () (_ tptp.zero_a_b @t184)) % 0.44/0.81 (define @t186 () (_ tptp.add_a_b @t184)) % 0.44/0.81 (define @t187 () (_ @t186 @t21)) % 0.44/0.81 (define @t188 () (_ tptp.partia1066395285xt_a_b @t184)) % 0.44/0.81 (define @t189 () (_ @t29 @t188)) % 0.44/0.81 (define @t190 () (_ tptp.semiring_a_b @t184)) % 0.44/0.81 (define @t191 () (@list @t184 @t21)) % 0.44/0.81 (define @t192 () (_ tptp.mult_a_ring_ext_a_b @t184)) % 0.44/0.81 (define @t193 () (_ @t192 @t21)) % 0.44/0.81 (define @t194 () (_ @t192 @t16)) % 0.44/0.81 (define @t195 () (_ @t187 @t17)) % 0.44/0.81 (define @t196 () (_ @t25 @t188)) % 0.44/0.81 (define @t197 () (_ @t27 @t188)) % 0.44/0.81 (define @t198 () (@list @t184 @t21 @t17 @t16)) % 0.44/0.81 (define @t199 () (_ @t18 @t10)) % 0.44/0.81 (define @t200 () (@var "K" tptp.int)) % 0.44/0.81 (define @t201 () (_ @t179 @t200)) % 0.44/0.81 (define @t202 () (_ @t201 (_ @t199 @t6))) % 0.44/0.81 (define @t203 () (@list @t10 @t6 @t200)) % 0.44/0.81 (define @t204 () (_ @t8 @t181)) % 0.44/0.81 (define @t205 () (=> @t30 (=> @t28 (= (_ @t180 @t37) (_ @t204 (_ @t180 @t17)))))) % 0.44/0.81 (define @t206 () (@list @t21 @t17 @t178)) % 0.44/0.81 (define @t207 () (@var "Z" tptp.int)) % 0.44/0.81 (define @t208 () (@var "S2" tptp.set_a)) % 0.44/0.81 (define @t209 () (@var "M" tptp.partia1833973666xt_a_b)) % 0.44/0.81 (define @t210 () (_ (_ tptp.locali425460998xt_a_b @t209) @t208)) % 0.44/0.81 (define @t211 () (@list @t209 @t208)) % 0.44/0.81 (define @t212 () (_ (_ tptp.locali880295127ng_a_b @t184) @t208)) % 0.44/0.81 (define @t213 () (_ (_ tptp.locali807230110ng_a_b @t184) @t208)) % 0.44/0.81 (define @t214 () (@list @t184 @t208)) % 0.44/0.81 (define @t215 () (_ (_ @t192 @t17) @t16)) % 0.44/0.81 (define @t216 () (_ @t193 @t17)) % 0.44/0.81 (define @t217 () (@list @t184 @t21 @t17)) % 0.44/0.81 (define @t218 () (_ @t186 @t17)) % 0.44/0.81 (define @t219 () (_ @t187 (_ @t218 @t16))) % 0.44/0.81 (define @t220 () (@var "M2" tptp.int)) % 0.44/0.81 (define @t221 () (@var "N" tptp.int)) % 0.44/0.81 (define @t222 () (_ tptp.minus_minus_int @t221)) % 0.44/0.81 (define @t223 () (@var "J" tptp.int)) % 0.44/0.81 (define @t224 () (_ tptp.plus_plus_int @t178)) % 0.44/0.81 (define @t225 () (@var "B" tptp.int)) % 0.44/0.81 (define @t226 () (@var "A" tptp.int)) % 0.44/0.81 (define @t227 () (_ tptp.plus_plus_int @t226)) % 0.44/0.81 (define @t228 () (_ @t227 @t225)) % 0.44/0.81 (define @t229 () (_ tptp.uminus_uminus_int @t225)) % 0.44/0.81 (define @t230 () (_ tptp.minus_minus_int @t226)) % 0.44/0.81 (define @t231 () (@list @t226 @t225)) % 0.44/0.81 (define @t232 () (_ tptp.minus_minus_int @t225)) % 0.44/0.81 (define @t233 () (_ @t232 @t226)) % 0.44/0.81 (define @t234 () (_ tptp.uminus_uminus_int @t226)) % 0.44/0.81 (define @t235 () (_ tptp.plus_plus_int @t234)) % 0.44/0.81 (define @t236 () (_ @t235 @t225)) % 0.44/0.81 (define @t237 () (_ @t230 @t225)) % 0.44/0.81 (define @t238 () (_ tptp.plus_plus_int @t225)) % 0.44/0.81 (define @t239 () (_ tptp.ord_less_eq_int @t225)) % 0.44/0.81 (define @t240 () (_ @t239 @t226)) % 0.44/0.81 (define @t241 () (@list @t225 @t226)) % 0.44/0.81 (define @t242 () (_ tptp.plus_plus_int @t237)) % 0.44/0.81 (define @t243 () (= (_ @t242 @t225) @t226)) % 0.44/0.81 (define @t244 () (@var "C" tptp.int)) % 0.44/0.81 (define @t245 () (= @t225 @t244)) % 0.44/0.81 (define @t246 () (_ tptp.plus_plus_int @t244)) % 0.44/0.81 (define @t247 () (_ @t246 @t226)) % 0.44/0.81 (define @t248 () (= (_ @t238 @t226) @t247)) % 0.44/0.81 (define @t249 () (@list @t225 @t226 @t244)) % 0.44/0.81 (define @t250 () (_ @t227 @t244)) % 0.44/0.81 (define @t251 () (= @t228 @t250)) % 0.44/0.81 (define @t252 () (@list @t226 @t225 @t244)) % 0.44/0.81 (define @t253 () (= @t226 @t225)) % 0.44/0.81 (define @t254 () (_ tptp.ord_less_eq_int @t226)) % 0.44/0.81 (define @t255 () (_ @t254 @t225)) % 0.44/0.81 (define @t256 () (_ @t238 @t244)) % 0.44/0.81 (define @t257 () (_ tptp.ord_less_eq_int @t250)) % 0.44/0.81 (define @t258 () (_ @t257 @t256)) % 0.44/0.81 (define @t259 () (@list @t226 @t244 @t225)) % 0.44/0.81 (define @t260 () (_ @t246 @t225)) % 0.44/0.81 (define @t261 () (_ (_ tptp.ord_less_eq_int @t247) @t260)) % 0.44/0.81 (define @t262 () (@list @t244 @t226 @t225)) % 0.44/0.81 (define @t263 () (_ tptp.ord_less_eq_int @t229)) % 0.44/0.81 (define @t264 () (_ @t263 @t234)) % 0.44/0.81 (define @t265 () (_ tptp.minus_minus_int @t228)) % 0.44/0.81 (define @t266 () (_ tptp.minus_minus_int @t250)) % 0.44/0.81 (define @t267 () (_ tptp.uminus_uminus_int @t228)) % 0.44/0.81 (define @t268 () (_ @t227 @t256)) % 0.44/0.81 (define @t269 () (@var "A3" tptp.int)) % 0.44/0.81 (define @t270 () (@var "B2" tptp.int)) % 0.44/0.81 (define @t271 () (@list @t269 @t270)) % 0.44/0.81 (define @t272 () (_ tptp.plus_plus_int @t200)) % 0.44/0.81 (define @t273 () (_ @t272 @t228)) % 0.44/0.81 (define @t274 () (@var "B3" tptp.int)) % 0.44/0.81 (define @t275 () (= @t274 (_ @t272 @t225))) % 0.44/0.81 (define @t276 () (@list @t274 @t200 @t225 @t226)) % 0.44/0.81 (define @t277 () (@var "A2" tptp.int)) % 0.44/0.81 (define @t278 () (= @t277 (_ @t272 @t226))) % 0.44/0.81 (define @t279 () (@list @t277 @t200 @t226 @t225)) % 0.44/0.81 (define @t280 () (@var "L" tptp.int)) % 0.44/0.81 (define @t281 () (_ tptp.plus_plus_int @t223)) % 0.44/0.81 (define @t282 () (_ @t281 @t280)) % 0.44/0.81 (define @t283 () (_ @t224 @t200)) % 0.44/0.81 (define @t284 () (= @t200 @t280)) % 0.44/0.81 (define @t285 () (= @t178 @t223)) % 0.44/0.81 (define @t286 () (@list @t178 @t223 @t200 @t280)) % 0.44/0.81 (define @t287 () (_ (_ tptp.minus_minus_int @t237) @t244)) % 0.44/0.81 (define @t288 () (_ @t230 @t244)) % 0.44/0.81 (define @t289 () (_ (_ tptp.minus_minus_int @t288) @t225)) % 0.44/0.81 (define @t290 () (@var "D" tptp.int)) % 0.44/0.81 (define @t291 () (_ tptp.minus_minus_int @t244)) % 0.44/0.81 (define @t292 () (= @t237 (_ @t291 @t290))) % 0.44/0.81 (define @t293 () (@list @t226 @t225 @t244 @t290)) % 0.44/0.81 (define @t294 () (_ (_ tptp.ord_less_eq_int @t244) @t290)) % 0.44/0.81 (define @t295 () (_ tptp.ord_less_eq_int @t283)) % 0.44/0.81 (define @t296 () (_ @t295 @t282)) % 0.44/0.81 (define @t297 () (_ (_ tptp.ord_less_eq_int @t200) @t280)) % 0.44/0.81 (define @t298 () (_ tptp.ord_less_eq_int @t178)) % 0.44/0.81 (define @t299 () (_ @t298 @t223)) % 0.44/0.81 (define @t300 () (_ @t232 @t244)) % 0.44/0.81 (define @t301 () (_ tptp.ord_less_eq_int @t288)) % 0.44/0.81 (define @t302 () (_ @t291 @t225)) % 0.44/0.81 (define @t303 () (_ @t230 @t256)) % 0.44/0.81 (define @t304 () (_ @t266 @t225)) % 0.44/0.81 (define @t305 () (_ tptp.plus_plus_int (_ tptp.uminus_uminus_int @t200))) % 0.44/0.81 (define @t306 () (_ @t222 @t200)) % 0.44/0.81 (define @t307 () (_ (_ tptp.ord_less_eq_int @t221) (_ @t281 @t200))) % 0.44/0.81 (define @t308 () (_ @t295 @t221)) % 0.44/0.81 (define @t309 () (@var "H" tptp.set_a)) % 0.44/0.81 (define @t310 () (@var "Xa" tptp.a)) % 0.44/0.81 (define @t311 () (_ @t152 @t309)) % 0.44/0.81 (define @t312 () (_ (_ tptp.ord_less_eq_set_a @t309) @t1)) % 0.44/0.81 (define @t313 () (@var "M" tptp.set_a)) % 0.44/0.81 (define @t314 () (_ tptp.a_l_coset_a_b tptp.r)) % 0.44/0.81 (define @t315 () (_ (_ tptp.ord_less_eq_set_a @t313) @t1)) % 0.44/0.81 (define @t316 () (@var "H2" tptp.a)) % 0.44/0.81 (define @t317 () (@var "G" tptp.a)) % 0.44/0.81 (define @t318 () (@var "K2" tptp.set_a)) % 0.44/0.81 (define @t319 () (_ tptp.set_add_a_b tptp.r)) % 0.44/0.81 (define @t320 () (_ (_ @t319 @t309) @t318)) % 0.44/0.81 (define @t321 () (@list @t309 @t318)) % 0.44/0.81 (define @t322 () (@var "B3" tptp.set_a)) % 0.44/0.81 (define @t323 () (_ tptp.ord_less_eq_set_a @t322)) % 0.44/0.81 (define @t324 () (_ tptp.ord_less_eq_set_a @t123)) % 0.44/0.81 (define @t325 () (@list @t123 @t322)) % 0.44/0.81 (define @t326 () (_ @t324 @t322)) % 0.44/0.81 (define @t327 () (_ tptp.minus_minus_set_a @t123)) % 0.44/0.81 (define @t328 () (= @t123 tptp.bot_bot_set_a)) % 0.44/0.81 (define @t329 () (forall @t127 (not (_ @t121 @t124)))) % 0.44/0.81 (define @t330 () (@list @t121)) % 0.44/0.81 (define @t331 () (= @t123 @t322)) % 0.44/0.81 (define @t332 () (_ @t323 @t123)) % 0.44/0.81 (define @t333 () (_ tptp.uminus_uminus_set_a @t322)) % 0.44/0.81 (define @t334 () (_ tptp.uminus_uminus_set_a @t123)) % 0.44/0.81 (define @t335 () (= @t96 @t98)) % 0.44/0.81 (define @t336 () (not @t335)) % 0.44/0.81 (define @t337 () (@var "Y5" tptp.a)) % 0.44/0.81 (define @t338 () (@var "R2" tptp.partia1833973666xt_a_b)) % 0.44/0.81 (define @t339 () (lambda (@list @t338 @t124 @t337) (_ (_ (_ tptp.add_a_b @t338) @t124) (_ (_ tptp.a_inv_a_b @t338) @t337)))) % 0.44/0.81 (define @t340 () (lambda @t271 (_ (_ tptp.plus_plus_int @t269) (_ tptp.uminus_uminus_int @t270)))) % 0.44/0.81 (define @t341 () (@var "B4" tptp.set_a)) % 0.44/0.81 (define @t342 () (@var "A4" tptp.set_a)) % 0.44/0.81 (define @t343 () (lambda (@list @t342 @t341) (forall @t127 (=> (_ @t125 @t342) (_ @t125 @t341))))) % 0.44/0.81 (define @t344 () (tptp.partia1066395285xt_a_b tptp.r)) % 0.44/0.81 (define @t345 () (tptp.mult_a_ring_ext_a_b tptp.r @t21 @t17)) % 0.44/0.81 (define @t346 () (tptp.member_a @t345 @t344)) % 0.44/0.81 (define @t347 () (tptp.member_a @t17 @t344)) % 0.44/0.81 (define @t348 () (not @t28)) % 0.44/0.81 (define @t349 () (tptp.member_a @t21 @t344)) % 0.44/0.81 (define @t350 () (not @t30)) % 0.44/0.81 (define @t351 () (or @t350 @t348 @t137)) % 0.44/0.81 (define @t352 () (tptp.member_a tptp.t2 @t344)) % 0.44/0.81 (define @t353 () (tptp.member_a tptp.t @t344)) % 0.44/0.81 (define @t354 () (_ @t140 @t47)) % 0.44/0.81 (define @t355 () (_ @t112 @t354)) % 0.44/0.81 (define @t356 () (tptp.product_fst_a_a tptp.x)) % 0.44/0.81 (define @t357 () (tptp.product_snd_a_a tptp.y)) % 0.44/0.81 (define @t358 () (tptp.mult_a_ring_ext_a_b tptp.r @t357 @t356)) % 0.44/0.81 (define @t359 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s2 tptp.s3)) % 0.44/0.81 (define @t360 () (tptp.mult_a_ring_ext_a_b tptp.r @t359 @t358)) % 0.44/0.81 (define @t361 () (tptp.a_inv_a_b tptp.r @t360)) % 0.44/0.81 (define @t362 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s3 tptp.r2)) % 0.44/0.81 (define @t363 () (tptp.product_snd_a_a tptp.x)) % 0.44/0.81 (define @t364 () (tptp.mult_a_ring_ext_a_b tptp.r @t363 @t357)) % 0.44/0.81 (define @t365 () (tptp.mult_a_ring_ext_a_b tptp.r @t364 @t362)) % 0.44/0.81 (define @t366 () (tptp.add_a_b tptp.r @t365 @t361)) % 0.44/0.81 (define @t367 () (tptp.member_a @t366 @t344)) % 0.44/0.81 (define @t368 () (_ (_ tptp.member_a @t355) @t1)) % 0.44/0.81 (define @t369 () (_ @t18 @t359)) % 0.44/0.81 (define @t370 () (_ @t18 @t357)) % 0.44/0.81 (define @t371 () (_ @t18 @t364)) % 0.44/0.81 (define @t372 () (_ @t18 @t363)) % 0.44/0.81 (define @t373 () (_ @t140 @t337)) % 0.44/0.81 (define @t374 () (@list @t337)) % 0.44/0.81 (define @t375 () (lambda @t374 (_ @t112 @t373))) % 0.44/0.81 (define @t376 () (lambda (@list @t124 @t337) (_ (_ @t8 @t124) @t373))) % 0.44/0.81 (define @t377 () (_ @t339 tptp.r)) % 0.44/0.81 (define @t378 () (_ @t140 @t59)) % 0.44/0.81 (define @t379 () (_ @t8 @t61)) % 0.44/0.81 (define @t380 () (_ @t379 @t378)) % 0.44/0.81 (define @t381 () (_ (_ @t8 @t355) @t380)) % 0.44/0.81 (define @t382 () (tptp.product_fst_a_a tptp.y)) % 0.44/0.81 (define @t383 () (tptp.mult_a_ring_ext_a_b tptp.r @t363 @t382)) % 0.44/0.81 (define @t384 () (tptp.mult_a_ring_ext_a_b tptp.r @t359 @t383)) % 0.44/0.81 (define @t385 () (tptp.a_inv_a_b tptp.r @t384)) % 0.44/0.81 (define @t386 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s2 tptp.r3)) % 0.44/0.81 (define @t387 () (tptp.mult_a_ring_ext_a_b tptp.r @t364 @t386)) % 0.44/0.81 (define @t388 () (tptp.add_a_b tptp.r @t387 @t385)) % 0.44/0.81 (define @t389 () (tptp.add_a_b tptp.r @t366 @t388)) % 0.44/0.81 (define @t390 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.t2 tptp.t)) % 0.44/0.81 (define @t391 () (tptp.mult_a_ring_ext_a_b tptp.r @t390 @t389)) % 0.44/0.81 (define @t392 () (_ @t18 @t390)) % 0.44/0.81 (define @t393 () (_ @t75 @t381)) % 0.44/0.81 (define @t394 () (_ @t75 @t380)) % 0.44/0.81 (define @t395 () (_ @t75 @t355)) % 0.44/0.81 (define @t396 () (tptp.mult_a_ring_ext_a_b tptp.r @t390 @t388)) % 0.44/0.81 (define @t397 () (tptp.mult_a_ring_ext_a_b tptp.r @t390 @t366)) % 0.44/0.81 (define @t398 () (tptp.add_a_b tptp.r @t397 @t396)) % 0.44/0.81 (define @t399 () (_ (_ @t8 @t395) @t394)) % 0.44/0.81 (define @t400 () (= @t399 @t393)) % 0.44/0.81 (define @t401 () (tptp.member_a @t390 @t344)) % 0.44/0.81 (define @t402 () (=> @t101 @t400)) % 0.44/0.81 (define @t403 () (tptp.member_a @t388 @t344)) % 0.44/0.81 (define @t404 () (_ (_ tptp.member_a @t380) @t1)) % 0.44/0.81 (define @t405 () (=> @t404 @t402)) % 0.44/0.81 (define @t406 () (lambda @t374 (_ @t379 @t373))) % 0.44/0.81 (define @t407 () (_ (_ @t377 @t61) @t59)) % 0.44/0.81 (define @t408 () (_ (_ @t377 @t54) @t47)) % 0.44/0.81 (define @t409 () (_ (_ @t8 (_ @t75 @t408)) (_ @t75 @t407))) % 0.44/0.81 (define @t410 () (_ @t75 (_ (_ @t8 @t408) @t407))) % 0.44/0.81 (define @t411 () (= @t410 @t409)) % 0.44/0.81 (define @t412 () (=> @t101 @t411)) % 0.44/0.81 (define @t413 () (=> (_ (_ tptp.member_a @t407) @t1) @t412)) % 0.44/0.81 (define @t414 () (= @t398 @t391)) % 0.44/0.81 (define @t415 () (=> @t401 @t414)) % 0.44/0.81 (define @t416 () (=> @t403 @t415)) % 0.44/0.81 (define @t417 () (_ @t140 @t79)) % 0.44/0.81 (define @t418 () (_ @t8 @t80)) % 0.44/0.81 (define @t419 () (_ @t418 @t417)) % 0.44/0.81 (define @t420 () (_ @t82 @t419)) % 0.44/0.81 (define @t421 () (_ @t86 @t420)) % 0.44/0.81 (define @t422 () (_ @t140 @t88)) % 0.44/0.81 (define @t423 () (_ @t8 @t89)) % 0.44/0.81 (define @t424 () (_ @t423 @t422)) % 0.44/0.81 (define @t425 () (_ @t73 @t424)) % 0.44/0.81 (define @t426 () (_ @t94 @t425)) % 0.44/0.81 (define @t427 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s3 @t382)) % 0.44/0.81 (define @t428 () (tptp.a_inv_a_b tptp.r @t427)) % 0.44/0.81 (define @t429 () (tptp.mult_a_ring_ext_a_b tptp.r @t357 tptp.r3)) % 0.44/0.81 (define @t430 () (tptp.add_a_b tptp.r @t429 @t428)) % 0.44/0.81 (define @t431 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.t @t430)) % 0.44/0.81 (define @t432 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.t2 tptp.s2)) % 0.44/0.81 (define @t433 () (tptp.mult_a_ring_ext_a_b tptp.r @t432 @t363)) % 0.44/0.81 (define @t434 () (tptp.mult_a_ring_ext_a_b tptp.r @t433 @t431)) % 0.44/0.81 (define @t435 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.s2 @t356)) % 0.44/0.81 (define @t436 () (tptp.a_inv_a_b tptp.r @t435)) % 0.44/0.81 (define @t437 () (tptp.mult_a_ring_ext_a_b tptp.r @t363 tptp.r2)) % 0.44/0.81 (define @t438 () (tptp.add_a_b tptp.r @t437 @t436)) % 0.44/0.81 (define @t439 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.t2 @t438)) % 0.44/0.81 (define @t440 () (tptp.mult_a_ring_ext_a_b tptp.r tptp.t tptp.s3)) % 0.44/0.81 (define @t441 () (tptp.mult_a_ring_ext_a_b tptp.r @t440 @t357)) % 0.44/0.81 (define @t442 () (tptp.mult_a_ring_ext_a_b tptp.r @t441 @t439)) % 0.44/0.81 (define @t443 () (tptp.add_a_b tptp.r @t442 @t434)) % 0.44/0.81 (define @t444 () (_ (_ @t8 @t426) @t421)) % 0.44/0.81 (define @t445 () (= @t444 @t393)) % 0.44/0.81 (define @t446 () (lambda @t374 (_ @t418 @t373))) % 0.44/0.81 (define @t447 () (lambda @t374 (_ @t423 @t373))) % 0.44/0.81 (define @t448 () (_ (_ @t8 (_ @t94 (_ @t73 (_ (_ @t377 @t89) @t88)))) (_ @t86 (_ @t82 (_ (_ @t377 @t80) @t79))))) % 0.44/0.81 (define @t449 () (= @t448 @t410)) % 0.44/0.81 (define @t450 () (not @t401)) % 0.44/0.81 (define @t451 () (@list true false)) % 0.44/0.81 (define @t452 () (not @t353)) % 0.44/0.81 (define @t453 () (not @t352)) % 0.44/0.81 (define @t454 () (or @t453 @t452 @t401)) % 0.44/0.81 (define @t455 () (not @t454)) % 0.44/0.81 (define @t456 () (forall @t32 (or (not @t349) (not @t347) @t346))) % 0.44/0.81 (assume @p1 @t3) % 0.44/0.81 (assume @p2 @t5) % 0.44/0.81 (assume @p3 (forall @t12 (=> @t11 (= (_ @t9 @t10) (_ @t9 @t6))))) % 0.44/0.81 (assume @p4 (forall @t12 (=> @t11 (= @t15 (_ @t14 @t6))))) % 0.44/0.81 (assume @p5 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= (_ (_ @t18 @t24) @t16) @t23)))))) % 0.44/0.81 (assume @p6 (forall @t32 (=> @t30 (=> @t28 (= @t24 (_ @t19 @t21)))))) % 0.44/0.81 (assume @p7 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= @t23 (_ @t19 @t33))))))) % 0.44/0.81 (assume @p8 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= (_ (_ @t8 @t37) @t16) @t36)))))) % 0.44/0.81 (assume @p9 (forall @t32 (=> @t30 (=> @t28 @t39)))) % 0.44/0.81 (assume @p10 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= @t36 (_ @t34 (_ @t35 @t16)))))))) % 0.44/0.81 (assume @p11 (_ (_ tptp.member_a tptp.s3) @t1)) % 0.44/0.81 (assume @p12 (_ (_ tptp.member_a tptp.s2) @t1)) % 0.44/0.81 (assume @p13 @t56) % 0.44/0.81 (assume @p14 @t63) % 0.44/0.81 (assume @p15 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= (_ (_ @t18 @t37) @t16) (_ (_ @t8 @t33) @t20))))))) % 0.44/0.81 (assume @p16 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= (_ @t64 @t37) (_ (_ @t8 (_ @t64 @t21)) (_ @t64 @t17)))))))) % 0.44/0.81 (assume @p17 (forall (@list @t10 @t6 @t7 @t65) (=> @t72 (=> @t70 (=> @t69 (=> (_ (_ tptp.member_a @t65) @t1) (= (_ (_ @t13 (_ (_ @t8 (_ (_ @t13 @t10) @t7)) @t6)) @t65) (_ (_ @t13 (_ (_ @t13 @t67) @t7)) @t65)))))))) % 0.44/0.81 (assume @p18 (forall @t12 (=> @t72 (=> @t70 (=> @t69 (= (_ (_ @t13 @t15) @t6) (_ @t14 @t67))))))) % 0.44/0.81 (assume @p19 (_ (_ tptp.member_a @t41) @t1)) % 0.44/0.81 (assume @p20 @t97) % 0.44/0.81 (assume @p21 (_ (_ tptp.member_a @t40) @t1)) % 0.44/0.81 (assume @p22 @t104) % 0.44/0.81 (assume @p23 (_ (_ tptp.member_a @t45) @t1)) % 0.44/0.81 (assume @p24 (_ (_ tptp.member_a @t52) @t1)) % 0.44/0.81 (assume @p25 (_ (_ tptp.member_a @t79) @t1)) % 0.44/0.81 (assume @p26 (_ (_ tptp.member_a @t88) @t1)) % 0.44/0.81 (assume @p27 (_ (_ tptp.member_a @t89) @t1)) % 0.44/0.81 (assume @p28 (_ (_ tptp.member_a @t80) @t1)) % 0.44/0.81 (assume @p29 (= (_ @t46 @t105) (_ (_ @t8 @t47) @t59))) % 0.44/0.81 (assume @p30 (= @t91 (_ (_ @t13 (_ @t73 @t89)) (_ @t73 @t88)))) % 0.44/0.81 (assume @p31 (= @t83 @t106)) % 0.44/0.81 (assume @p32 (_ (_ tptp.member_a @t43) @t1)) % 0.44/0.81 (assume @p33 (= @t109 @t108)) % 0.44/0.81 (assume @p34 (_ (_ tptp.member_a @t93) @t1)) % 0.44/0.81 (assume @p35 (_ (_ tptp.member_a @t85) @t1)) % 0.44/0.81 (assume @p36 (= @t111 @t110)) % 0.44/0.81 (assume @p37 (= @t113 (_ @t112 @t61))) % 0.44/0.81 (assume @p38 (= (_ @t114 @t105) (_ (_ @t8 (_ @t114 @t43)) (_ @t114 @t58)))) % 0.44/0.81 (assume @p39 (_ (_ tptp.member_a @t54) @t1)) % 0.44/0.81 (assume @p40 (= @t116 @t115)) % 0.44/0.81 (assume @p41 (= @t95 @t115)) % 0.44/0.81 (assume @p42 (= @t95 @t116)) % 0.44/0.81 (assume @p43 (= @t116 @t77)) % 0.44/0.81 (assume @p44 (= @t120 (_ (_ @t13 (_ @t117 @t80)) (_ @t117 @t79)))) % 0.44/0.81 (assume @p45 (= @t87 (_ @t86 @t106))) % 0.44/0.81 (assume @p46 (forall (@list @t10 @t121) (= (_ @t71 @t122) (_ @t121 @t10)))) % 0.44/0.81 (assume @p47 (forall @t128 (= (_ tptp.collect_a (lambda @t127 @t126)) @t123))) % 0.44/0.81 (assume @p48 (forall (@list @t121 @t129) (=> (forall @t131 (= (_ @t121 @t130) (_ @t129 @t130))) (= @t122 (_ tptp.collect_a @t129))))) % 0.44/0.81 (assume @p49 (= @t87 @t120)) % 0.44/0.81 (assume @p50 (= @t120 @t76)) % 0.44/0.81 (assume @p51 (= (_ @t75 @t113) (_ (_ @t8 (_ @t132 @t49)) (_ @t132 @t60)))) % 0.44/0.81 (assume @p52 (_ (_ tptp.member_a @t47) @t1)) % 0.44/0.81 (assume @p53 (= @t78 (_ (_ @t13 (_ @t133 @t119)) @t118))) % 0.44/0.81 (assume @p54 (= @t96 (_ @t133 @t120))) % 0.44/0.81 (assume @p55 (_ (_ tptp.member_a @t77) @t1)) % 0.44/0.81 (assume @p56 (_ (_ tptp.member_a @t116) @t1)) % 0.44/0.81 (assume @p57 (_ (_ tptp.member_a @t76) @t1)) % 0.44/0.81 (assume @p58 (= @t91 @t134)) % 0.44/0.81 (assume @p59 (= @t83 @t134)) % 0.44/0.81 (assume @p60 (forall @t32 (=> @t30 (=> @t28 (_ (_ tptp.member_a @t135) @t1))))) % 0.44/0.81 (assume @p61 (forall @t32 (=> @t30 (=> @t28 (_ (_ tptp.member_a @t37) @t1))))) % 0.44/0.81 (assume @p62 (forall @t31 (=> @t30 (=> @t28 (=> @t26 (= (= @t38 (_ (_ @t8 @t16) @t21)) (= @t17 @t16))))))) % 0.44/0.81 (assume @p63 @t139) % 0.44/0.81 (assume @p64 (_ @t4 tptp.s)) % 0.44/0.81 (assume @p65 (_ @t2 tptp.s)) % 0.44/0.81 (assume @p66 (_ @t100 tptp.s)) % 0.44/0.81 (assume @p67 (_ tptp.semiring_a_b tptp.r)) % 0.44/0.81 (assume @p68 (forall @t32 (= @t135 (_ @t35 @t141)))) % 0.44/0.81 (assume @p69 (forall (@list @t143 @t142) (=> (= @t145 (_ tptp.product_fst_a_a @t142)) (=> (= @t144 (_ tptp.product_snd_a_a @t142)) (= @t143 @t142))))) % 0.44/0.81 (assume @p70 (forall (@list @t147 @t143) (=> (_ (_ @t147 @t144) @t145) (not (forall (@list @t130 @t146) (not (_ (_ @t147 @t146) @t130))))))) % 0.44/0.81 (assume @p71 (forall (@list @t149 @t148) (=> (and (= (_ tptp.product_fst_a_a @t149) (_ tptp.product_fst_a_a @t148)) (= (_ tptp.product_snd_a_a @t149) (_ tptp.product_snd_a_a @t148))) (= @t149 @t148)))) % 0.44/0.81 (assume @p72 (forall (@list @t17 @t21 @t150) (=> @t151 (=> (= (_ @t35 @t150) @t134) (=> @t30 (=> @t28 (=> (_ (_ tptp.member_a @t150) @t1) (= @t17 @t150)))))))) % 0.44/0.81 (assume @p73 (forall @t154 (=> @t30 (exists @t131 (and @t153 (= (_ @t35 @t130) @t134)))))) % 0.44/0.81 (assume @p74 (forall (@list @t155) (=> (_ (_ tptp.member_a @t155) @t1) (=> (forall @t131 (=> @t153 (= (_ (_ @t8 @t155) @t130) @t130))) (= @t155 @t134))))) % 0.44/0.81 (assume @p75 (forall @t154 (=> @t30 (exists @t131 (and @t153 (= (_ @t156 @t21) @t134)))))) % 0.44/0.81 (assume @p76 (forall @t32 (=> @t157 (=> @t30 (=> @t28 @t151))))) % 0.44/0.81 (assume @p77 (forall @t32 (=> @t30 (=> @t28 (= (_ @t22 @t141) @t158))))) % 0.44/0.81 (assume @p78 (forall @t32 (=> @t30 (=> @t28 (= (_ (_ @t18 @t159) @t17) @t158))))) % 0.44/0.81 (assume @p79 (forall @t32 (=> @t30 (=> @t28 (= (_ @t35 (_ @t160 @t17)) @t17))))) % 0.44/0.81 (assume @p80 (forall @t32 (=> @t30 (=> @t28 (= (_ @t160 @t37) @t17))))) % 0.44/0.81 (assume @p81 (forall @t32 (=> @t30 (=> @t28 (= @t161 (_ @t160 @t141)))))) % 0.44/0.81 (assume @p82 (forall @t12 (=> @t72 (=> @t70 (=> @t69 (= (= @t164 @t10) @t162)))))) % 0.44/0.81 (assume @p83 (forall @t12 (=> @t72 (=> @t70 (=> @t69 (= (= @t10 @t164) @t162)))))) % 0.44/0.81 (assume @p84 (forall @t12 (=> @t72 (=> @t70 (=> @t69 (= (= @t166 @t10) @t165)))))) % 0.44/0.81 (assume @p85 (forall @t12 (=> @t72 (=> @t70 (=> @t69 (= (= @t10 @t166) @t165)))))) % 0.44/0.81 (assume @p86 (forall @t32 (=> @t30 (=> @t28 (= @t161 (_ (_ @t8 @t141) @t159)))))) % 0.44/0.81 (assume @p87 (forall @t31 (=> (= @t37 @t16) (=> @t30 (=> @t28 (=> @t26 (= (_ @t160 @t16) @t17))))))) % 0.44/0.81 (assume @p88 (_ (_ tptp.locali1648887798ac_a_b tptp.r) tptp.s)) % 0.44/0.81 (assume @p89 (forall @t32 (=> @t30 (=> @t28 (=> @t157 (= @t21 @t141)))))) % 0.44/0.81 (assume @p90 (forall @t154 (=> @t30 (= (_ @t35 @t159) @t134)))) % 0.44/0.81 (assume @p91 (forall (@list @t17 @t21) (=> @t151 (=> @t30 (=> @t28 (= @t159 @t17)))))) % 0.44/0.81 (assume @p92 (forall @t154 (=> @t30 (= (_ @t160 @t21) @t134)))) % 0.44/0.81 (assume @p93 (forall (@list @t10 @t6) (=> @t72 (=> @t70 (= (_ @t140 @t67) (_ (_ @t13 (_ @t140 @t10)) @t6)))))) % 0.44/0.81 (assume @p94 (not (forall (@list @t167) (=> (_ (_ tptp.member_a @t167) tptp.s) (not (= (_ (_ @t18 @t167) @t90) @t134)))))) % 0.44/0.81 (assume @p95 (not (forall (@list @t168) (=> (_ (_ tptp.member_a @t168) tptp.s) (not (= (_ (_ @t18 @t168) @t81) @t134)))))) % 0.44/0.81 (assume @p96 (_ @t169 @t1)) % 0.44/0.81 (assume @p97 (forall @t154 (=> @t30 (= (_ @t140 @t159) @t21)))) % 0.44/0.81 (assume @p98 (forall @t154 (=> @t30 (_ (_ tptp.member_a @t159) @t1)))) % 0.44/0.81 (assume @p99 (= (_ @t140 @t134) @t134)) % 0.44/0.81 (assume @p100 (forall @t32 (=> (_ @t29 tptp.s) (=> (_ @t27 tptp.s) (_ @t136 tptp.s))))) % 0.44/0.81 (assume @p101 (forall @t154 (=> @t30 (= (_ @t22 @t134) @t134)))) % 0.44/0.81 (assume @p102 (forall @t154 (=> @t30 (= (_ (_ @t18 @t134) @t21) @t134)))) % 0.44/0.81 (assume @p103 (forall @t154 (=> @t30 (= (_ @t35 @t134) @t21)))) % 0.44/0.81 (assume @p104 (forall @t154 (=> @t30 (= (_ (_ @t8 @t134) @t21) @t21)))) % 0.44/0.81 (assume @p105 (forall @t172 (=> @t30 (=> @t72 (= (= @t21 @t171) @t170))))) % 0.44/0.81 (assume @p106 (forall @t172 (=> @t30 (=> @t72 (= (= @t171 @t21) @t170))))) % 0.44/0.81 (assume @p107 (forall @t172 (=> @t30 (=> @t72 (= (= @t21 @t173) @t170))))) % 0.44/0.81 (assume @p108 (forall @t172 (=> @t30 (=> @t72 (= (= @t173 @t21) @t170))))) % 0.44/0.81 (assume @p109 (forall @t154 (=> @t30 (= (= @t159 @t134) (= @t21 @t134))))) % 0.44/0.81 (assume @p110 (_ (_ tptp.locali880295127ng_a_b tptp.r) tptp.s)) % 0.44/0.81 (assume @p111 (_ (_ tptp.locali807230110ng_a_b tptp.r) tptp.s)) % 0.44/0.81 (assume @p112 (= (lambda (@list @t177 @t176) (= @t177 @t176)) (lambda (@list @t175 @t174) (and (= (_ tptp.product_fst_a_a @t175) (_ tptp.product_fst_a_a @t174)) (= (_ tptp.product_snd_a_a @t175) (_ tptp.product_snd_a_a @t174)))))) % 0.44/0.81 (assume @p113 (_ (_ tptp.locali425460998xt_a_b tptp.r) tptp.s)) % 0.44/0.81 (assume @p114 (forall @t183 (=> @t30 (= (_ @t180 @t159) @t182)))) % 0.44/0.81 (assume @p115 (forall @t191 (=> @t190 (=> @t189 (= (_ @t187 @t185) @t21))))) % 0.44/0.81 (assume @p116 (forall @t191 (=> @t190 (=> @t189 (= (_ (_ @t186 @t185) @t21) @t21))))) % 0.44/0.81 (assume @p117 (forall @t191 (=> @t190 (=> @t189 (= (_ (_ @t192 @t185) @t21) @t185))))) % 0.44/0.81 (assume @p118 (forall @t191 (=> @t190 (=> @t189 (= (_ @t193 @t185) @t185))))) % 0.44/0.81 (assume @p119 (forall @t198 (=> @t190 (=> @t189 (=> @t197 (=> @t196 (= (_ @t194 @t195) (_ (_ @t186 (_ @t194 @t21)) (_ @t194 @t17))))))))) % 0.44/0.81 (assume @p120 (forall @t203 (=> @t72 (=> @t70 (= (_ (_ @t18 (_ @t201 @t10)) @t6) @t202))))) % 0.44/0.81 (assume @p121 (forall @t203 (=> @t72 (=> @t70 (= (_ @t199 (_ @t201 @t6)) @t202))))) % 0.44/0.81 (assume @p122 (forall @t206 @t205)) % 0.44/0.81 (assume @p123 (forall @t206 (=> @t39 @t205))) % 0.44/0.81 (assume @p124 (forall @t183 (=> @t30 (_ (_ tptp.member_a @t181) @t1)))) % 0.44/0.81 (assume @p125 (forall (@list @t207) (= (_ (_ @t179 @t207) @t134) @t134))) % 0.44/0.81 (assume @p126 (forall @t211 (=> @t210 @t210))) % 0.44/0.81 (assume @p127 (forall @t214 (=> @t213 @t212))) % 0.44/0.81 (assume @p128 (forall @t214 (=> @t212 (_ (_ tptp.locali425460998xt_a_b @t184) @t208)))) % 0.44/0.81 (assume @p129 (forall @t214 (=> (_ (_ tptp.locali1648887798ac_a_b @t184) @t208) @t213))) % 0.44/0.81 (assume @p130 (forall (@list @t209 @t208 @t21 @t17) (=> @t210 (=> (_ @t29 @t208) (=> (_ @t27 @t208) (_ (_ tptp.member_a (_ (_ (_ tptp.mult_a_ring_ext_a_b @t209) @t21) @t17)) @t208)))))) % 0.44/0.81 (assume @p131 (forall @t198 (=> @t190 (=> @t189 (=> @t197 (=> @t196 (= (_ (_ @t192 @t216) @t16) (_ @t193 @t215)))))))) % 0.44/0.81 (assume @p132 (forall @t217 (=> @t190 (=> @t189 (=> @t197 (_ (_ tptp.member_a @t216) @t188)))))) % 0.44/0.81 (assume @p133 (forall @t198 (=> @t190 (=> @t189 (=> @t197 (=> @t196 (= @t219 (_ @t218 (_ @t187 @t16))))))))) % 0.44/0.81 (assume @p134 (forall @t217 (=> @t190 (=> @t189 (=> @t197 (= @t195 (_ @t218 @t21))))))) % 0.44/0.81 (assume @p135 (forall @t198 (=> @t190 (=> @t189 (=> @t197 (=> @t196 (= (_ (_ @t186 @t195) @t16) @t219))))))) % 0.44/0.81 (assume @p136 (forall @t217 (=> @t190 (=> @t189 (=> @t197 (_ (_ tptp.member_a @t195) @t188)))))) % 0.44/0.81 (assume @p137 (forall (@list @t184) (=> @t190 (_ (_ tptp.member_a @t185) @t188)))) % 0.44/0.81 (assume @p138 (forall @t198 (=> @t190 (=> @t189 (=> @t197 (=> @t196 (= (_ (_ @t192 @t195) @t16) (_ (_ @t186 (_ @t193 @t16)) @t215)))))))) % 0.44/0.81 (assume @p139 (forall (@list @t21 @t221 @t220) (=> @t30 (= (_ (_ @t179 (_ @t222 @t220)) @t21) (_ (_ @t8 (_ (_ @t179 @t221) @t21)) (_ @t140 (_ (_ @t179 @t220) @t21))))))) % 0.44/0.81 (assume @p140 (forall @t183 (=> @t30 (= (_ (_ @t179 (_ tptp.uminus_uminus_int @t178)) @t21) @t182)))) % 0.44/0.81 (assume @p141 (forall (@list @t21 @t178 @t223) (=> @t30 (= (_ (_ @t179 (_ @t224 @t223)) @t21) (_ @t204 (_ (_ @t179 @t223) @t21)))))) % 0.44/0.81 (assume @p142 (_ (_ tptp.ord_less_eq_set_a tptp.s) @t1)) % 0.44/0.81 (assume @p143 (forall @t211 (=> @t210 (_ (_ tptp.ord_less_eq_set_a @t208) (_ tptp.partia1066395285xt_a_b @t209))))) % 0.44/0.81 (assume @p144 (forall @t231 (= (_ @t230 @t229) @t228))) % 0.44/0.81 (assume @p145 (forall @t231 (= @t236 @t233))) % 0.44/0.81 (assume @p146 (forall @t241 (=> @t240 (= (_ @t238 @t237) @t226)))) % 0.44/0.81 (assume @p147 (forall @t241 (=> @t240 @t243))) % 0.44/0.81 (assume @p148 (forall @t249 (= @t248 @t245))) % 0.44/0.81 (assume @p149 (forall @t252 (= @t251 @t245))) % 0.44/0.81 (assume @p150 (forall @t231 (= (= @t234 @t229) @t253))) % 0.44/0.81 (assume @p151 (forall (@list @t226) (= (_ tptp.uminus_uminus_int @t234) @t226))) % 0.44/0.81 (assume @p152 (forall @t259 (= @t258 @t255))) % 0.44/0.81 (assume @p153 (forall @t262 (= @t261 @t255))) % 0.44/0.81 (assume @p154 (forall @t241 (= @t264 @t255))) % 0.44/0.81 (assume @p155 (forall @t231 (= (_ @t265 @t225) @t226))) % 0.44/0.81 (assume @p156 (forall @t259 (= (_ @t266 @t256) @t237))) % 0.44/0.81 (assume @p157 (forall @t231 (= (_ @t265 @t226) @t225))) % 0.44/0.81 (assume @p158 (forall @t262 (= (_ (_ tptp.minus_minus_int @t247) @t260) @t237))) % 0.44/0.81 (assume @p159 (forall @t231 @t243)) % 0.44/0.81 (assume @p160 (forall @t231 (= @t267 (_ @t235 @t229)))) % 0.44/0.81 (assume @p161 (forall @t231 (= (_ @t235 @t228) @t225))) % 0.44/0.81 (assume @p162 (forall @t231 (= (_ @t227 @t236) @t225))) % 0.44/0.81 (assume @p163 (forall @t231 (= (_ tptp.uminus_uminus_int @t237) @t233))) % 0.44/0.81 (assume @p164 (forall @t249 (=> @t248 @t245))) % 0.44/0.81 (assume @p165 (forall @t252 (=> @t251 @t245))) % 0.44/0.81 (assume @p166 (forall @t249 (= (_ @t238 @t250) @t268))) % 0.44/0.81 (assume @p167 (= tptp.plus_plus_int (lambda @t271 (_ (_ tptp.plus_plus_int @t270) @t269)))) % 0.44/0.81 (assume @p168 (forall @t252 (= (_ (_ tptp.plus_plus_int @t228) @t244) @t268))) % 0.44/0.81 (assume @p169 (forall @t276 (=> @t275 (= (_ @t227 @t274) @t273)))) % 0.44/0.81 (assume @p170 (forall @t279 (=> @t278 (= (_ (_ tptp.plus_plus_int @t277) @t225) @t273)))) % 0.44/0.81 (assume @p171 (forall @t286 (=> (and @t285 @t284) (= @t283 @t282)))) % 0.44/0.81 (assume @p172 (forall @t259 (= @t289 @t287))) % 0.44/0.81 (assume @p173 (forall @t293 (=> @t292 (= @t253 (= @t244 @t290))))) % 0.44/0.81 (assume @p174 (forall @t231 (= (= @t234 @t225) (= @t229 @t226)))) % 0.44/0.81 (assume @p175 (forall @t231 (= (= @t226 @t229) (= @t225 @t234)))) % 0.44/0.81 (assume @p176 (forall @t259 (=> @t258 @t255))) % 0.44/0.81 (assume @p177 (forall @t262 (=> @t261 @t255))) % 0.44/0.81 (assume @p178 (forall @t252 (=> @t255 @t258))) % 0.44/0.81 (assume @p179 (forall @t252 (=> @t255 @t261))) % 0.44/0.81 (assume @p180 (forall @t293 (=> @t255 (=> @t294 (_ @t257 (_ @t238 @t290)))))) % 0.44/0.81 (assume @p181 (forall @t286 (=> (and @t299 @t297) @t296))) % 0.44/0.81 (assume @p182 (forall @t286 (=> (and @t285 @t297) @t296))) % 0.44/0.81 (assume @p183 (forall @t286 (=> (and @t299 @t284) @t296))) % 0.44/0.81 (assume @p184 (forall @t293 (=> @t292 (= @t255 @t294)))) % 0.44/0.81 (assume @p185 (forall @t252 (=> @t255 (_ @t301 @t300)))) % 0.44/0.81 (assume @p186 (forall @t249 (=> @t240 (_ (_ tptp.ord_less_eq_int (_ @t291 @t226)) @t302)))) % 0.44/0.81 (assume @p187 (forall (@list @t226 @t225 @t290 @t244) (=> @t255 (=> (_ (_ tptp.ord_less_eq_int @t290) @t244) (_ @t301 (_ @t232 @t290)))))) % 0.44/0.81 (assume @p188 (forall @t231 (=> @t255 @t264))) % 0.44/0.81 (assume @p189 (forall @t231 (= (_ (_ tptp.ord_less_eq_int @t234) @t225) (_ @t263 @t226)))) % 0.44/0.81 (assume @p190 (forall @t231 (= (_ @t254 @t229) (_ @t239 @t234)))) % 0.44/0.81 (assume @p191 (forall (@list @t244 @t225 @t226) (=> (= @t260 @t226) (= @t244 @t237)))) % 0.44/0.81 (assume @p192 (forall @t252 (= @t287 @t303))) % 0.44/0.81 (assume @p193 (forall @t252 (= @t303 @t289))) % 0.44/0.81 (assume @p194 (forall @t252 (= (_ @t242 @t244) @t304))) % 0.44/0.81 (assume @p195 (forall @t252 (= (_ @t230 @t300) @t304))) % 0.44/0.81 (assume @p196 (forall @t252 (= (_ @t227 @t300) (_ @t265 @t244)))) % 0.44/0.81 (assume @p197 (forall @t259 (= (= @t226 @t302) (= @t228 @t244)))) % 0.44/0.81 (assume @p198 (forall @t252 (= (= @t237 @t244) (= @t226 @t260)))) % 0.44/0.81 (assume @p199 (forall @t279 (=> @t278 (= (_ (_ tptp.minus_minus_int @t277) @t225) (_ @t272 @t237))))) % 0.44/0.81 (assume @p200 (forall @t231 (= @t267 (_ (_ tptp.plus_plus_int @t229) @t234)))) % 0.44/0.81 (assume @p201 (forall (@list @t277 @t200 @t226) (=> @t278 (= (_ tptp.uminus_uminus_int @t277) (_ @t305 @t234))))) % 0.44/0.81 (assume @p202 (forall @t241 (= (_ (_ tptp.minus_minus_int @t229) @t226) (_ (_ tptp.minus_minus_int @t234) @t225)))) % 0.44/0.81 (assume @p203 (forall (@list @t178 @t200 @t221 @t223) (=> @t308 (=> @t307 (=> @t308 (=> @t307 (_ (_ tptp.ord_less_eq_int @t306) @t223))))))) % 0.44/0.81 (assume @p204 (forall (@list @t178 @t200 @t221) (=> @t308 (_ @t298 @t306)))) % 0.44/0.81 (assume @p205 (forall @t259 (= (_ @t254 @t302) (_ (_ tptp.ord_less_eq_int @t228) @t244)))) % 0.44/0.81 (assume @p206 (forall @t252 (= (_ (_ tptp.ord_less_eq_int @t237) @t244) (_ @t254 @t260)))) % 0.44/0.81 (assume @p207 (forall @t276 (=> @t275 (= (_ @t230 @t274) (_ @t305 @t237))))) % 0.44/0.81 (assume @p208 (forall (@list @t309) (=> @t312 (=> (not (= @t309 tptp.bot_bot_set_a)) (=> (forall @t131 (=> @t311 (_ (_ tptp.member_a (_ @t140 @t130)) @t309))) (=> (forall @t131 (=> @t311 (forall (@list @t310) (=> (_ (_ tptp.member_a @t310) @t309) (_ (_ tptp.member_a (_ @t156 @t310)) @t309))))) (_ @t169 @t309))))))) % 0.44/0.81 (assume @p209 (forall (@list @t313) (=> @t315 (= (_ (_ @t314 @t134) @t313) @t313)))) % 0.44/0.81 (assume @p210 (forall (@list @t313 @t317 @t316) (=> @t315 (=> (_ (_ tptp.member_a @t317) @t1) (=> (_ (_ tptp.member_a @t316) @t1) (= (_ (_ @t314 @t317) (_ (_ @t314 @t316) @t313)) (_ (_ @t314 (_ (_ @t8 @t317) @t316)) @t313))))))) % 0.44/0.81 (assume @p211 (not (= @t1 tptp.bot_bot_set_a))) % 0.44/0.81 (assume @p212 (forall (@list @t309 @t21) (=> @t312 (=> @t30 (_ (_ tptp.ord_less_eq_set_a (_ (_ @t314 @t21) @t309)) @t1))))) % 0.44/0.81 (assume @p213 (forall @t321 (=> @t312 (=> (_ (_ tptp.ord_less_eq_set_a @t318) @t1) (_ (_ tptp.ord_less_eq_set_a @t320) @t1))))) % 0.44/0.81 (assume @p214 (forall @t325 (=> (_ @t324 @t1) (=> (_ @t323 @t1) (_ (_ tptp.ord_less_eq_set_a (_ (_ @t319 @t123) @t322)) @t1))))) % 0.44/0.81 (assume @p215 (forall @t321 (=> (_ (_ tptp.additi2104487374up_a_b @t309) tptp.r) (=> (_ (_ tptp.additi2104487374up_a_b @t318) tptp.r) (_ (_ tptp.additi2104487374up_a_b @t320) tptp.r))))) % 0.44/0.81 (assume @p216 (forall @t325 (= (= (_ @t327 @t322) tptp.bot_bot_set_a) @t326))) % 0.44/0.81 (assume @p217 (forall (@list @t7) (not (_ @t68 tptp.bot_bot_set_a)))) % 0.44/0.81 (assume @p218 (forall @t128 (= (forall @t127 (not @t126)) @t328))) % 0.44/0.81 (assume @p219 (forall @t330 (= (= @t122 tptp.bot_bot_set_a) @t329))) % 0.44/0.81 (assume @p220 (forall @t330 (= (= tptp.bot_bot_set_a @t122) @t329))) % 0.44/0.81 (assume @p221 (forall @t325 (=> (forall @t131 (=> (_ @t152 @t123) (_ @t152 @t322))) @t326))) % 0.44/0.81 (assume @p222 (forall @t325 (=> @t326 (=> @t332 @t331)))) % 0.44/0.81 (assume @p223 (forall @t325 (= (_ (_ tptp.ord_less_eq_set_a @t334) @t333) @t332))) % 0.44/0.81 (assume @p224 (forall @t325 (=> @t326 (_ (_ tptp.ord_less_eq_set_a @t333) @t334)))) % 0.44/0.81 (assume @p225 (forall @t128 (= (_ @t324 tptp.bot_bot_set_a) @t328))) % 0.44/0.81 (assume @p226 (forall @t128 (_ (_ tptp.ord_less_eq_set_a tptp.bot_bot_set_a) @t123))) % 0.44/0.81 (assume @p227 (forall @t128 (= (_ @t327 tptp.bot_bot_set_a) @t123))) % 0.44/0.81 (assume @p228 (forall @t128 (= (_ (_ tptp.minus_minus_set_a tptp.bot_bot_set_a) @t123) tptp.bot_bot_set_a))) % 0.44/0.81 (assume @p229 (forall @t128 (= (_ @t327 @t123) tptp.bot_bot_set_a))) % 0.44/0.81 (assume @p230 (forall (@list @t10) (not (_ @t71 tptp.bot_bot_set_a)))) % 0.44/0.81 (assume @p231 (forall (@list @t123 @t10) (=> @t328 (not (_ @t71 @t123))))) % 0.44/0.81 (assume @p232 (forall @t128 (=> (forall (@list @t146) (not (_ (_ tptp.member_a @t146) @t123))) @t328))) % 0.44/0.81 (assume @p233 (forall @t128 (= (exists @t127 @t126) (not @t328)))) % 0.44/0.81 (assume @p234 (forall (@list @t123 @t322 @t21) (=> @t326 (=> (_ @t29 @t123) (_ @t29 @t322))))) % 0.44/0.81 (assume @p235 (forall (@list @t123 @t322 @t7) (=> @t326 (=> (_ @t68 @t123) (_ @t68 @t322))))) % 0.44/0.81 (assume @p236 (forall @t325 (=> @t331 (not (=> @t326 (not @t332)))))) % 0.44/0.81 (assume @p237 @t336) % 0.44/0.81 (assume @p238 true) % 0.44/0.81 (step @p239 (= tptp.a_minus_a_b @t339) :rule refl :args (@t339)) % 0.44/0.81 (step @p240 (= tptp.minus_minus_int @t340) :rule refl :args (@t340)) % 0.44/0.81 (step @p241 (= tptp.ord_less_eq_set_a @t343) :rule refl :args (@t343)) % 0.44/0.81 (step @p242 :rule refl :args ((tptp.member_a @t24 @t1))) % 0.44/0.81 (step @p243 :rule refl :args (@t344)) % 0.44/0.81 (step @p244 :rule refl :args (@t345)) % 0.44/0.81 (step @p245 :rule cong :premises (@p244 @p243) :args (@t346)) % 0.44/0.81 (step @p246 :rule trans :premises (@p245 @p242)) % 0.44/0.81 (step @p247 :rule refl :args (tptp.member_a)) % 0.44/0.81 (step @p248 :rule ho_cong :premises (@p247 @p244)) % 0.44/0.81 (step @p249 :rule ho_cong :premises (@p248 @p243)) % 0.44/0.81 (step @p250 :rule cong :premises (@p249 @p246) :args ((= (_ (_ tptp.member_a @t345) @t344) @t346))) % 0.44/0.81 (step @p251 :rule symm :premises (@p250)) % 0.44/0.81 (step @p252 :rule refl :args (@t137)) % 0.44/0.81 (step @p253 :rule eq_resolve :premises (@p252 @p251)) % 0.44/0.81 (step @p254 :rule refl :args (@t1)) % 0.44/0.81 (step @p255 :rule cong :premises (@p254 @p243) :args ((= @t1 @t344))) % 0.44/0.81 (step @p256 :rule symm :premises (@p255)) % 0.44/0.81 (step @p257 :rule eq_resolve :premises (@p254 @p256)) % 0.44/0.81 (step @p258 :rule refl :args (@t24)) % 0.44/0.81 (step @p259 :rule cong :premises (@p258 @p244) :args ((= @t24 @t345))) % 0.44/0.81 (step @p260 :rule symm :premises (@p259)) % 0.44/0.81 (step @p261 :rule eq_resolve :premises (@p258 @p260)) % 0.44/0.81 (step @p262 :rule ho_cong :premises (@p247 @p261)) % 0.44/0.81 (step @p263 :rule ho_cong :premises (@p262 @p257)) % 0.44/0.81 (step @p264 :rule trans :premises (@p263 @p253)) % 0.44/0.81 (step @p265 :rule refl :args ((tptp.member_a @t17 @t1))) % 0.44/0.81 (step @p266 :rule refl :args (@t17)) % 0.44/0.81 (step @p267 :rule cong :premises (@p266 @p243) :args (@t347)) % 0.44/0.81 (step @p268 :rule trans :premises (@p267 @p265)) % 0.44/0.81 (step @p269 :rule refl :args (@t27)) % 0.44/0.81 (step @p270 :rule ho_cong :premises (@p269 @p243)) % 0.44/0.81 (step @p271 :rule cong :premises (@p270 @p268) :args ((= (_ @t27 @t344) @t347))) % 0.44/0.81 (step @p272 :rule symm :premises (@p271)) % 0.44/0.81 (step @p273 :rule refl :args (@t28)) % 0.44/0.81 (step @p274 :rule eq_resolve :premises (@p273 @p272)) % 0.44/0.81 (step @p275 :rule ho_cong :premises (@p269 @p257)) % 0.44/0.81 (step @p276 :rule trans :premises (@p275 @p274)) % 0.44/0.81 (step @p277 :rule cong :premises (@p276) :args (@t348)) % 0.44/0.81 (step @p278 :rule refl :args ((tptp.member_a @t21 @t1))) % 0.44/0.81 (step @p279 :rule refl :args (@t21)) % 0.44/0.81 (step @p280 :rule cong :premises (@p279 @p243) :args (@t349)) % 0.44/0.81 (step @p281 :rule trans :premises (@p280 @p278)) % 0.44/0.81 (step @p282 :rule refl :args (@t29)) % 0.44/0.81 (step @p283 :rule ho_cong :premises (@p282 @p243)) % 0.44/0.81 (step @p284 :rule cong :premises (@p283 @p281) :args ((= (_ @t29 @t344) @t349))) % 0.44/0.81 (step @p285 :rule symm :premises (@p284)) % 0.44/0.81 (step @p286 :rule refl :args (@t30)) % 0.44/0.81 (step @p287 :rule eq_resolve :premises (@p286 @p285)) % 0.44/0.81 (step @p288 :rule ho_cong :premises (@p282 @p257)) % 0.44/0.81 (step @p289 :rule trans :premises (@p288 @p287)) % 0.44/0.81 (step @p290 :rule cong :premises (@p289) :args (@t350)) % 0.44/0.81 (step @p291 :rule nary_cong :premises (@p290 @p277 @p264) :args (@t351)) % 0.44/0.81 (step @p292 :rule cong :premises (@p291) :args ((forall @t32 @t351))) % 0.44/0.81 (step @p293 :rule aci_norm :args ((= (or @t350 (or @t348 @t137)) @t351))) % 0.44/0.81 (step @p294 :rule bool-impl-elim :args (@t28 @t137)) % 0.44/0.81 (step @p295 :rule refl :args (@t350)) % 0.44/0.81 (step @p296 :rule nary_cong :premises (@p295 @p294) :args ((or @t350 @t138))) % 0.44/0.81 (step @p297 :rule trans :premises (@p296 @p293)) % 0.44/0.81 (step @p298 :rule bool-impl-elim :args (@t30 @t138)) % 0.44/0.81 (step @p299 :rule trans :premises (@p298 @p297)) % 0.44/0.81 (step @p300 :rule cong :premises (@p299) :args (@t139)) % 0.44/0.81 (step @p301 :rule trans :premises (@p300 @p292)) % 0.44/0.81 (step @p302 :rule eq_resolve :premises (@p63 @p301)) % 0.44/0.81 (step @p303 :rule refl :args ((tptp.member_a tptp.t2 @t1))) % 0.44/0.81 (step @p304 :rule refl :args (tptp.t2)) % 0.44/0.81 (step @p305 :rule cong :premises (@p304 @p243) :args (@t352)) % 0.44/0.81 (step @p306 :rule trans :premises (@p305 @p303)) % 0.44/0.81 (step @p307 :rule refl :args (@t4)) % 0.44/0.81 (step @p308 :rule ho_cong :premises (@p307 @p243)) % 0.44/0.81 (step @p309 :rule cong :premises (@p308 @p306) :args ((= (_ @t4 @t344) @t352))) % 0.44/0.81 (step @p310 :rule symm :premises (@p309)) % 0.44/0.81 (step @p311 :rule refl :args (@t5)) % 0.44/0.81 (step @p312 :rule eq_resolve :premises (@p311 @p310)) % 0.44/0.81 (step @p313 :rule refl :args (@t4)) % 0.44/0.81 (step @p314 :rule ho_cong :premises (@p313 @p257)) % 0.44/0.81 (step @p315 :rule trans :premises (@p314 @p312)) % 0.44/0.81 (step @p316 :rule eq_resolve :premises (@p2 @p315)) % 0.44/0.81 (step @p317 :rule refl :args ((tptp.member_a tptp.t @t1))) % 0.44/0.81 (step @p318 :rule refl :args (tptp.t)) % 0.44/0.81 (step @p319 :rule cong :premises (@p318 @p243) :args (@t353)) % 0.44/0.81 (step @p320 :rule trans :premises (@p319 @p317)) % 0.44/0.81 (step @p321 :rule refl :args (@t2)) % 0.44/0.81 (step @p322 :rule ho_cong :premises (@p321 @p243)) % 0.44/0.81 (step @p323 :rule cong :premises (@p322 @p320) :args ((= (_ @t2 @t344) @t353))) % 0.44/0.81 (step @p324 :rule symm :premises (@p323)) % 0.44/0.81 (step @p325 :rule refl :args (@t3)) % 0.44/0.81 (step @p326 :rule eq_resolve :premises (@p325 @p324)) % 0.44/0.81 (step @p327 :rule refl :args (@t2)) % 0.44/0.81 (step @p328 :rule ho_cong :premises (@p327 @p257)) % 0.44/0.81 (step @p329 :rule trans :premises (@p328 @p326)) % 0.44/0.81 (step @p330 :rule eq_resolve :premises (@p1 @p329)) % 0.44/0.81 (step @p331 :rule refl :args ((tptp.member_a @t355 @t1))) % 0.44/0.81 (step @p332 :rule refl :args ((tptp.add_a_b tptp.r @t54 @t354))) % 0.44/0.81 (step @p333 :rule refl :args ((tptp.a_inv_a_b tptp.r @t47))) % 0.44/0.81 (step @p334 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t45 @t43))) % 0.44/0.81 (step @p335 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t41 @t40))) % 0.44/0.81 (step @p336 :rule refl :args (@t356)) % 0.44/0.81 (step @p337 :rule refl :args (@t357)) % 0.44/0.81 (step @p338 :rule refl :args (tptp.r)) % 0.44/0.81 (step @p339 :rule cong :premises (@p338 @p337 @p336) :args (@t358)) % 0.44/0.81 (step @p340 :rule trans :premises (@p339 @p335)) % 0.44/0.81 (step @p341 :rule refl :args (@t359)) % 0.44/0.81 (step @p342 :rule cong :premises (@p338 @p341 @p340) :args (@t360)) % 0.44/0.81 (step @p343 :rule trans :premises (@p342 @p334)) % 0.44/0.81 (step @p344 :rule cong :premises (@p338 @p343) :args (@t361)) % 0.44/0.81 (step @p345 :rule trans :premises (@p344 @p333)) % 0.44/0.81 (step @p346 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t52 @t49))) % 0.44/0.81 (step @p347 :rule refl :args (@t362)) % 0.44/0.81 (step @p348 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t50 @t41))) % 0.44/0.81 (step @p349 :rule refl :args (@t363)) % 0.44/0.81 (step @p350 :rule cong :premises (@p338 @p349 @p337) :args (@t364)) % 0.44/0.81 (step @p351 :rule trans :premises (@p350 @p348)) % 0.44/0.81 (step @p352 :rule cong :premises (@p338 @p351 @p347) :args (@t365)) % 0.44/0.81 (step @p353 :rule trans :premises (@p352 @p346)) % 0.44/0.81 (step @p354 :rule cong :premises (@p338 @p353 @p345) :args (@t366)) % 0.44/0.81 (step @p355 :rule trans :premises (@p354 @p332)) % 0.44/0.81 (step @p356 :rule cong :premises (@p355 @p243) :args (@t367)) % 0.44/0.81 (step @p357 :rule trans :premises (@p356 @p331)) % 0.44/0.81 (step @p358 :rule ho_cong :premises (@p247 @p355)) % 0.44/0.81 (step @p359 :rule ho_cong :premises (@p358 @p243)) % 0.44/0.81 (step @p360 :rule cong :premises (@p359 @p357) :args ((= (_ (_ tptp.member_a @t366) @t344) @t367))) % 0.44/0.81 (step @p361 :rule symm :premises (@p360)) % 0.44/0.81 (step @p362 :rule refl :args (@t368)) % 0.44/0.81 (step @p363 :rule eq_resolve :premises (@p362 @p361)) % 0.44/0.81 (step @p364 :rule refl :args (@t8)) % 0.44/0.81 (step @p365 :rule ho_cong :premises (@p364 @p353)) % 0.44/0.81 (step @p366 :rule ho_cong :premises (@p365 @p345)) % 0.44/0.81 (step @p367 :rule cong :premises (@p366 @p355) :args ((= (_ (_ @t8 @t365) @t361) @t366))) % 0.44/0.81 (step @p368 :rule symm :premises (@p367)) % 0.44/0.81 (step @p369 :rule refl :args (@t355)) % 0.44/0.81 (step @p370 :rule eq_resolve :premises (@p369 @p368)) % 0.44/0.81 (step @p371 :rule refl :args (@t140)) % 0.44/0.81 (step @p372 :rule ho_cong :premises (@p371 @p343)) % 0.44/0.81 (step @p373 :rule cong :premises (@p372 @p345) :args ((= (_ @t140 @t360) @t361))) % 0.44/0.81 (step @p374 :rule symm :premises (@p373)) % 0.44/0.81 (step @p375 :rule refl :args (@t354)) % 0.44/0.81 (step @p376 :rule eq_resolve :premises (@p375 @p374)) % 0.44/0.81 (step @p377 :rule refl :args (@t18)) % 0.44/0.81 (step @p378 :rule ho_cong :premises (@p377 @p341)) % 0.44/0.81 (step @p379 :rule ho_cong :premises (@p378 @p340)) % 0.44/0.81 (step @p380 :rule cong :premises (@p379 @p343) :args ((= (_ @t369 @t358) @t360))) % 0.44/0.81 (step @p381 :rule symm :premises (@p380)) % 0.44/0.81 (step @p382 :rule refl :args (@t47)) % 0.44/0.81 (step @p383 :rule eq_resolve :premises (@p382 @p381)) % 0.44/0.81 (step @p384 :rule ho_cong :premises (@p377 @p337)) % 0.44/0.81 (step @p385 :rule ho_cong :premises (@p384 @p336)) % 0.44/0.81 (step @p386 :rule cong :premises (@p385 @p340) :args ((= (_ @t370 @t356) @t358))) % 0.44/0.81 (step @p387 :rule symm :premises (@p386)) % 0.44/0.81 (step @p388 :rule refl :args (@t43)) % 0.44/0.81 (step @p389 :rule eq_resolve :premises (@p388 @p387)) % 0.44/0.81 (step @p390 :rule refl :args (@t40)) % 0.44/0.81 (step @p391 :rule cong :premises (@p390 @p336) :args ((= @t40 @t356))) % 0.44/0.81 (step @p392 :rule symm :premises (@p391)) % 0.44/0.81 (step @p393 :rule eq_resolve :premises (@p390 @p392)) % 0.44/0.81 (step @p394 :rule refl :args (@t41)) % 0.44/0.81 (step @p395 :rule cong :premises (@p394 @p337) :args ((= @t41 @t357))) % 0.44/0.81 (step @p396 :rule symm :premises (@p395)) % 0.44/0.81 (step @p397 :rule eq_resolve :premises (@p394 @p396)) % 0.44/0.81 (step @p398 :rule refl :args (@t18)) % 0.44/0.81 (step @p399 :rule ho_cong :premises (@p398 @p397)) % 0.44/0.81 (step @p400 :rule ho_cong :premises (@p399 @p393)) % 0.44/0.81 (step @p401 :rule trans :premises (@p400 @p389)) % 0.44/0.81 (step @p402 :rule refl :args (@t45)) % 0.44/0.81 (step @p403 :rule cong :premises (@p402 @p341) :args ((= @t45 @t359))) % 0.44/0.81 (step @p404 :rule symm :premises (@p403)) % 0.44/0.81 (step @p405 :rule eq_resolve :premises (@p402 @p404)) % 0.44/0.81 (step @p406 :rule ho_cong :premises (@p398 @p405)) % 0.44/0.81 (step @p407 :rule ho_cong :premises (@p406 @p401)) % 0.44/0.81 (step @p408 :rule trans :premises (@p407 @p383)) % 0.44/0.81 (step @p409 :rule refl :args (@t140)) % 0.44/0.81 (step @p410 :rule ho_cong :premises (@p409 @p408)) % 0.44/0.81 (step @p411 :rule trans :premises (@p410 @p376)) % 0.44/0.81 (step @p412 :rule ho_cong :premises (@p377 @p351)) % 0.44/0.81 (step @p413 :rule ho_cong :premises (@p412 @p347)) % 0.44/0.81 (step @p414 :rule cong :premises (@p413 @p353) :args ((= (_ @t371 @t362) @t365))) % 0.44/0.81 (step @p415 :rule symm :premises (@p414)) % 0.44/0.81 (step @p416 :rule refl :args (@t54)) % 0.44/0.81 (step @p417 :rule eq_resolve :premises (@p416 @p415)) % 0.44/0.81 (step @p418 :rule refl :args (@t49)) % 0.44/0.81 (step @p419 :rule cong :premises (@p418 @p347) :args ((= @t49 @t362))) % 0.44/0.81 (step @p420 :rule symm :premises (@p419)) % 0.44/0.81 (step @p421 :rule eq_resolve :premises (@p418 @p420)) % 0.44/0.81 (step @p422 :rule ho_cong :premises (@p377 @p349)) % 0.44/0.81 (step @p423 :rule ho_cong :premises (@p422 @p337)) % 0.44/0.81 (step @p424 :rule cong :premises (@p423 @p351) :args ((= (_ @t372 @t357) @t364))) % 0.44/0.81 (step @p425 :rule symm :premises (@p424)) % 0.44/0.81 (step @p426 :rule refl :args (@t52)) % 0.44/0.81 (step @p427 :rule eq_resolve :premises (@p426 @p425)) % 0.44/0.81 (step @p428 :rule refl :args (@t50)) % 0.44/0.81 (step @p429 :rule cong :premises (@p428 @p349) :args ((= @t50 @t363))) % 0.44/0.81 (step @p430 :rule symm :premises (@p429)) % 0.44/0.81 (step @p431 :rule eq_resolve :premises (@p428 @p430)) % 0.44/0.81 (step @p432 :rule ho_cong :premises (@p398 @p431)) % 0.44/0.81 (step @p433 :rule ho_cong :premises (@p432 @p397)) % 0.44/0.81 (step @p434 :rule trans :premises (@p433 @p427)) % 0.44/0.81 (step @p435 :rule ho_cong :premises (@p398 @p434)) % 0.44/0.81 (step @p436 :rule ho_cong :premises (@p435 @p421)) % 0.44/0.81 (step @p437 :rule trans :premises (@p436 @p417)) % 0.44/0.81 (step @p438 :rule refl :args (@t8)) % 0.44/0.81 (step @p439 :rule ho_cong :premises (@p438 @p437)) % 0.44/0.81 (step @p440 :rule ho_cong :premises (@p439 @p411)) % 0.44/0.81 (step @p441 :rule trans :premises (@p440 @p370)) % 0.44/0.81 (step @p442 :rule refl :args (tptp.member_a)) % 0.44/0.81 (step @p443 :rule ho_cong :premises (@p442 @p441)) % 0.44/0.81 (step @p444 :rule ho_cong :premises (@p443 @p257)) % 0.44/0.81 (step @p445 :rule trans :premises (@p444 @p363)) % 0.44/0.81 (step @p446 :rule refl :args (@t1)) % 0.44/0.81 (step @p447 :rule beta-reduce :args ((= (_ @t375 @t47) @t355))) % 0.44/0.81 (step @p448 :rule refl :args (@t47)) % 0.44/0.81 (step @p449 :rule beta-reduce :args ((= (_ @t376 @t54) @t375))) % 0.44/0.81 (step @p450 :rule refl :args (@t54)) % 0.44/0.81 (step @p451 :rule beta-reduce :args ((= @t377 @t376))) % 0.44/0.81 (step @p452 :rule ho_cong :premises (@p451 @p450)) % 0.44/0.81 (step @p453 :rule trans :premises (@p452 @p449)) % 0.44/0.81 (step @p454 :rule ho_cong :premises (@p453 @p448)) % 0.44/0.81 (step @p455 :rule trans :premises (@p454 @p447)) % 0.44/0.81 (step @p456 :rule ho_cong :premises (@p442 @p455)) % 0.44/0.81 (step @p457 :rule ho_cong :premises (@p456 @p446)) % 0.44/0.81 (step @p458 :rule refl :args (tptp.r)) % 0.44/0.81 (step @p459 :rule ho_cong :premises (@p239 @p458)) % 0.44/0.81 (step @p460 :rule ho_cong :premises (@p459 @p450)) % 0.44/0.81 (step @p461 :rule ho_cong :premises (@p460 @p448)) % 0.44/0.81 (step @p462 :rule ho_cong :premises (@p442 @p461)) % 0.44/0.81 (step @p463 :rule ho_cong :premises (@p462 @p446)) % 0.44/0.81 (step @p464 :rule trans :premises (@p463 @p457)) % 0.44/0.81 (step @p465 :rule trans :premises (@p464 @p445)) % 0.44/0.81 (step @p466 :rule eq_resolve :premises (@p13 @p465)) % 0.44/0.81 (step @p467 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t74 @t381))) % 0.44/0.81 (step @p468 :rule refl :args ((tptp.add_a_b tptp.r @t355 @t380))) % 0.44/0.81 (step @p469 :rule refl :args ((tptp.add_a_b tptp.r @t61 @t378))) % 0.44/0.81 (step @p470 :rule refl :args ((tptp.a_inv_a_b tptp.r @t59))) % 0.44/0.81 (step @p471 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t45 @t58))) % 0.44/0.81 (step @p472 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t50 @t57))) % 0.44/0.81 (step @p473 :rule refl :args (@t382)) % 0.44/0.81 (step @p474 :rule cong :premises (@p338 @p349 @p473) :args (@t383)) % 0.44/0.81 (step @p475 :rule trans :premises (@p474 @p472)) % 0.44/0.81 (step @p476 :rule cong :premises (@p338 @p341 @p475) :args (@t384)) % 0.44/0.81 (step @p477 :rule trans :premises (@p476 @p471)) % 0.44/0.81 (step @p478 :rule cong :premises (@p338 @p477) :args (@t385)) % 0.44/0.81 (step @p479 :rule trans :premises (@p478 @p470)) % 0.44/0.81 (step @p480 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t52 @t60))) % 0.44/0.81 (step @p481 :rule refl :args (@t386)) % 0.44/0.81 (step @p482 :rule cong :premises (@p338 @p351 @p481) :args (@t387)) % 0.44/0.81 (step @p483 :rule trans :premises (@p482 @p480)) % 0.44/0.81 (step @p484 :rule cong :premises (@p338 @p483 @p479) :args (@t388)) % 0.44/0.81 (step @p485 :rule trans :premises (@p484 @p469)) % 0.44/0.81 (step @p486 :rule cong :premises (@p338 @p355 @p485) :args (@t389)) % 0.44/0.81 (step @p487 :rule trans :premises (@p486 @p468)) % 0.44/0.81 (step @p488 :rule refl :args (@t390)) % 0.44/0.81 (step @p489 :rule cong :premises (@p338 @p488 @p487) :args (@t391)) % 0.44/0.81 (step @p490 :rule trans :premises (@p489 @p467)) % 0.44/0.81 (step @p491 :rule ho_cong :premises (@p377 @p488)) % 0.44/0.81 (step @p492 :rule ho_cong :premises (@p491 @p487)) % 0.44/0.81 (step @p493 :rule cong :premises (@p492 @p490) :args ((= (_ @t392 @t389) @t391))) % 0.44/0.81 (step @p494 :rule symm :premises (@p493)) % 0.44/0.81 (step @p495 :rule refl :args (@t393)) % 0.44/0.81 (step @p496 :rule eq_resolve :premises (@p495 @p494)) % 0.44/0.81 (step @p497 :rule ho_cong :premises (@p364 @p355)) % 0.44/0.81 (step @p498 :rule ho_cong :premises (@p497 @p485)) % 0.44/0.81 (step @p499 :rule cong :premises (@p498 @p487) :args ((= (_ (_ @t8 @t366) @t388) @t389))) % 0.44/0.81 (step @p500 :rule symm :premises (@p499)) % 0.44/0.81 (step @p501 :rule refl :args (@t381)) % 0.44/0.81 (step @p502 :rule eq_resolve :premises (@p501 @p500)) % 0.44/0.81 (step @p503 :rule ho_cong :premises (@p364 @p483)) % 0.44/0.81 (step @p504 :rule ho_cong :premises (@p503 @p479)) % 0.44/0.81 (step @p505 :rule cong :premises (@p504 @p485) :args ((= (_ (_ @t8 @t387) @t385) @t388))) % 0.44/0.81 (step @p506 :rule symm :premises (@p505)) % 0.44/0.81 (step @p507 :rule refl :args (@t380)) % 0.44/0.81 (step @p508 :rule eq_resolve :premises (@p507 @p506)) % 0.44/0.81 (step @p509 :rule ho_cong :premises (@p371 @p477)) % 0.44/0.81 (step @p510 :rule cong :premises (@p509 @p479) :args ((= (_ @t140 @t384) @t385))) % 0.44/0.81 (step @p511 :rule symm :premises (@p510)) % 0.44/0.81 (step @p512 :rule refl :args (@t378)) % 0.44/0.81 (step @p513 :rule eq_resolve :premises (@p512 @p511)) % 0.44/0.81 (step @p514 :rule ho_cong :premises (@p378 @p475)) % 0.44/0.81 (step @p515 :rule cong :premises (@p514 @p477) :args ((= (_ @t369 @t383) @t384))) % 0.44/0.81 (step @p516 :rule symm :premises (@p515)) % 0.44/0.81 (step @p517 :rule refl :args (@t59)) % 0.44/0.81 (step @p518 :rule eq_resolve :premises (@p517 @p516)) % 0.44/0.81 (step @p519 :rule ho_cong :premises (@p422 @p473)) % 0.44/0.81 (step @p520 :rule cong :premises (@p519 @p475) :args ((= (_ @t372 @t382) @t383))) % 0.44/0.81 (step @p521 :rule symm :premises (@p520)) % 0.44/0.81 (step @p522 :rule refl :args (@t58)) % 0.44/0.81 (step @p523 :rule eq_resolve :premises (@p522 @p521)) % 0.44/0.81 (step @p524 :rule refl :args (@t57)) % 0.44/0.81 (step @p525 :rule cong :premises (@p524 @p473) :args ((= @t57 @t382))) % 0.44/0.81 (step @p526 :rule symm :premises (@p525)) % 0.44/0.81 (step @p527 :rule eq_resolve :premises (@p524 @p526)) % 0.44/0.81 (step @p528 :rule ho_cong :premises (@p432 @p527)) % 0.44/0.81 (step @p529 :rule trans :premises (@p528 @p523)) % 0.44/0.81 (step @p530 :rule ho_cong :premises (@p406 @p529)) % 0.44/0.81 (step @p531 :rule trans :premises (@p530 @p518)) % 0.44/0.81 (step @p532 :rule ho_cong :premises (@p409 @p531)) % 0.44/0.81 (step @p533 :rule trans :premises (@p532 @p513)) % 0.44/0.81 (step @p534 :rule ho_cong :premises (@p412 @p481)) % 0.44/0.81 (step @p535 :rule cong :premises (@p534 @p483) :args ((= (_ @t371 @t386) @t387))) % 0.44/0.81 (step @p536 :rule symm :premises (@p535)) % 0.44/0.81 (step @p537 :rule refl :args (@t61)) % 0.44/0.81 (step @p538 :rule eq_resolve :premises (@p537 @p536)) % 0.44/0.81 (step @p539 :rule refl :args (@t60)) % 0.44/0.81 (step @p540 :rule cong :premises (@p539 @p481) :args ((= @t60 @t386))) % 0.44/0.81 (step @p541 :rule symm :premises (@p540)) % 0.44/0.81 (step @p542 :rule eq_resolve :premises (@p539 @p541)) % 0.44/0.81 (step @p543 :rule ho_cong :premises (@p435 @p542)) % 0.44/0.81 (step @p544 :rule trans :premises (@p543 @p538)) % 0.44/0.81 (step @p545 :rule ho_cong :premises (@p438 @p544)) % 0.44/0.81 (step @p546 :rule ho_cong :premises (@p545 @p533)) % 0.44/0.81 (step @p547 :rule trans :premises (@p546 @p508)) % 0.44/0.81 (step @p548 :rule ho_cong :premises (@p438 @p441)) % 0.44/0.81 (step @p549 :rule ho_cong :premises (@p548 @p547)) % 0.44/0.81 (step @p550 :rule trans :premises (@p549 @p502)) % 0.44/0.81 (step @p551 :rule refl :args (@t74)) % 0.44/0.81 (step @p552 :rule cong :premises (@p551 @p488) :args ((= @t74 @t390))) % 0.44/0.81 (step @p553 :rule symm :premises (@p552)) % 0.44/0.81 (step @p554 :rule eq_resolve :premises (@p551 @p553)) % 0.44/0.81 (step @p555 :rule ho_cong :premises (@p398 @p554)) % 0.44/0.81 (step @p556 :rule ho_cong :premises (@p555 @p550)) % 0.44/0.81 (step @p557 :rule trans :premises (@p556 @p496)) % 0.44/0.81 (step @p558 :rule refl :args ((tptp.add_a_b tptp.r @t395 @t394))) % 0.44/0.81 (step @p559 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t74 @t380))) % 0.44/0.81 (step @p560 :rule cong :premises (@p338 @p488 @p485) :args (@t396)) % 0.44/0.81 (step @p561 :rule trans :premises (@p560 @p559)) % 0.44/0.81 (step @p562 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t74 @t355))) % 0.44/0.81 (step @p563 :rule cong :premises (@p338 @p488 @p355) :args (@t397)) % 0.44/0.81 (step @p564 :rule trans :premises (@p563 @p562)) % 0.44/0.81 (step @p565 :rule cong :premises (@p338 @p564 @p561) :args (@t398)) % 0.44/0.81 (step @p566 :rule trans :premises (@p565 @p558)) % 0.44/0.81 (step @p567 :rule ho_cong :premises (@p364 @p564)) % 0.44/0.81 (step @p568 :rule ho_cong :premises (@p567 @p561)) % 0.44/0.81 (step @p569 :rule cong :premises (@p568 @p566) :args ((= (_ (_ @t8 @t397) @t396) @t398))) % 0.44/0.81 (step @p570 :rule symm :premises (@p569)) % 0.44/0.81 (step @p571 :rule refl :args (@t399)) % 0.44/0.81 (step @p572 :rule eq_resolve :premises (@p571 @p570)) % 0.44/0.81 (step @p573 :rule ho_cong :premises (@p491 @p485)) % 0.44/0.81 (step @p574 :rule cong :premises (@p573 @p561) :args ((= (_ @t392 @t388) @t396))) % 0.44/0.81 (step @p575 :rule symm :premises (@p574)) % 0.44/0.81 (step @p576 :rule refl :args (@t394)) % 0.44/0.81 (step @p577 :rule eq_resolve :premises (@p576 @p575)) % 0.44/0.81 (step @p578 :rule ho_cong :premises (@p555 @p547)) % 0.44/0.81 (step @p579 :rule trans :premises (@p578 @p577)) % 0.44/0.81 (step @p580 :rule ho_cong :premises (@p491 @p355)) % 0.44/0.81 (step @p581 :rule cong :premises (@p580 @p564) :args ((= (_ @t392 @t366) @t397))) % 0.44/0.81 (step @p582 :rule symm :premises (@p581)) % 0.44/0.81 (step @p583 :rule refl :args (@t395)) % 0.44/0.81 (step @p584 :rule eq_resolve :premises (@p583 @p582)) % 0.44/0.81 (step @p585 :rule ho_cong :premises (@p555 @p441)) % 0.44/0.81 (step @p586 :rule trans :premises (@p585 @p584)) % 0.44/0.81 (step @p587 :rule ho_cong :premises (@p438 @p586)) % 0.44/0.81 (step @p588 :rule ho_cong :premises (@p587 @p579)) % 0.44/0.81 (step @p589 :rule trans :premises (@p588 @p572)) % 0.44/0.81 (step @p590 :rule cong :premises (@p589 @p557) :args (@t400)) % 0.44/0.81 (step @p591 :rule refl :args ((tptp.member_a @t74 @t1))) % 0.44/0.81 (step @p592 :rule cong :premises (@p488 @p243) :args (@t401)) % 0.44/0.81 (step @p593 :rule trans :premises (@p592 @p591)) % 0.44/0.81 (step @p594 :rule ho_cong :premises (@p247 @p488)) % 0.44/0.81 (step @p595 :rule ho_cong :premises (@p594 @p243)) % 0.44/0.81 (step @p596 :rule cong :premises (@p595 @p593) :args ((= (_ (_ tptp.member_a @t390) @t344) @t401))) % 0.44/0.81 (step @p597 :rule symm :premises (@p596)) % 0.44/0.81 (step @p598 :rule refl :args (@t101)) % 0.44/0.81 (step @p599 :rule eq_resolve :premises (@p598 @p597)) % 0.44/0.81 (step @p600 :rule ho_cong :premises (@p442 @p554)) % 0.44/0.81 (step @p601 :rule ho_cong :premises (@p600 @p257)) % 0.44/0.81 (step @p602 :rule trans :premises (@p601 @p599)) % 0.44/0.81 (step @p603 :rule cong :premises (@p602 @p590) :args (@t402)) % 0.44/0.81 (step @p604 :rule refl :args ((tptp.member_a @t380 @t1))) % 0.44/0.81 (step @p605 :rule cong :premises (@p485 @p243) :args (@t403)) % 0.44/0.81 (step @p606 :rule trans :premises (@p605 @p604)) % 0.44/0.81 (step @p607 :rule ho_cong :premises (@p247 @p485)) % 0.44/0.81 (step @p608 :rule ho_cong :premises (@p607 @p243)) % 0.44/0.81 (step @p609 :rule cong :premises (@p608 @p606) :args ((= (_ (_ tptp.member_a @t388) @t344) @t403))) % 0.44/0.81 (step @p610 :rule symm :premises (@p609)) % 0.44/0.81 (step @p611 :rule refl :args (@t404)) % 0.44/0.81 (step @p612 :rule eq_resolve :premises (@p611 @p610)) % 0.44/0.81 (step @p613 :rule ho_cong :premises (@p442 @p547)) % 0.44/0.81 (step @p614 :rule ho_cong :premises (@p613 @p257)) % 0.44/0.81 (step @p615 :rule trans :premises (@p614 @p612)) % 0.44/0.81 (step @p616 :rule cong :premises (@p615 @p603) :args (@t405)) % 0.44/0.81 (step @p617 :rule cong :premises (@p445 @p616) :args ((=> @t368 @t405))) % 0.44/0.81 (step @p618 :rule eq-symm :args (@t393 @t399)) % 0.44/0.81 (step @p619 :rule beta-reduce :args ((= (_ @t406 @t59) @t380))) % 0.44/0.81 (step @p620 :rule refl :args (@t59)) % 0.44/0.81 (step @p621 :rule beta-reduce :args ((= (_ @t376 @t61) @t406))) % 0.44/0.81 (step @p622 :rule refl :args (@t61)) % 0.44/0.81 (step @p623 :rule ho_cong :premises (@p451 @p622)) % 0.44/0.81 (step @p624 :rule trans :premises (@p623 @p621)) % 0.44/0.81 (step @p625 :rule ho_cong :premises (@p624 @p620)) % 0.44/0.81 (step @p626 :rule trans :premises (@p625 @p619)) % 0.44/0.81 (step @p627 :rule refl :args (@t75)) % 0.44/0.81 (step @p628 :rule ho_cong :premises (@p627 @p626)) % 0.44/0.81 (step @p629 :rule ho_cong :premises (@p627 @p455)) % 0.44/0.81 (step @p630 :rule ho_cong :premises (@p438 @p629)) % 0.44/0.81 (step @p631 :rule ho_cong :premises (@p630 @p628)) % 0.44/0.81 (step @p632 :rule ho_cong :premises (@p438 @p455)) % 0.44/0.81 (step @p633 :rule ho_cong :premises (@p632 @p626)) % 0.44/0.81 (step @p634 :rule ho_cong :premises (@p627 @p633)) % 0.44/0.81 (step @p635 :rule cong :premises (@p634 @p631) :args (@t411)) % 0.44/0.81 (step @p636 :rule trans :premises (@p635 @p618)) % 0.44/0.81 (step @p637 :rule refl :args (@t101)) % 0.44/0.81 (step @p638 :rule cong :premises (@p637 @p636) :args (@t412)) % 0.44/0.81 (step @p639 :rule ho_cong :premises (@p442 @p626)) % 0.44/0.81 (step @p640 :rule ho_cong :premises (@p639 @p446)) % 0.44/0.81 (step @p641 :rule cong :premises (@p640 @p638) :args (@t413)) % 0.44/0.81 (step @p642 :rule cong :premises (@p457 @p641) :args ((=> (_ (_ tptp.member_a @t408) @t1) @t413))) % 0.44/0.81 (step @p643 :rule ho_cong :premises (@p459 @p622)) % 0.44/0.81 (step @p644 :rule ho_cong :premises (@p643 @p620)) % 0.44/0.81 (step @p645 :rule ho_cong :premises (@p627 @p644)) % 0.44/0.81 (step @p646 :rule ho_cong :premises (@p627 @p461)) % 0.44/0.81 (step @p647 :rule ho_cong :premises (@p438 @p646)) % 0.44/0.81 (step @p648 :rule ho_cong :premises (@p647 @p645)) % 0.44/0.81 (step @p649 :rule ho_cong :premises (@p438 @p461)) % 0.44/0.81 (step @p650 :rule ho_cong :premises (@p649 @p644)) % 0.44/0.81 (step @p651 :rule ho_cong :premises (@p627 @p650)) % 0.44/0.81 (step @p652 :rule cong :premises (@p651 @p648) :args (@t99)) % 0.44/0.81 (step @p653 :rule cong :premises (@p637 @p652) :args (@t102)) % 0.44/0.81 (step @p654 :rule ho_cong :premises (@p442 @p644)) % 0.44/0.81 (step @p655 :rule ho_cong :premises (@p654 @p446)) % 0.44/0.81 (step @p656 :rule cong :premises (@p655 @p653) :args (@t103)) % 0.44/0.81 (step @p657 :rule cong :premises (@p463 @p656) :args (@t104)) % 0.44/0.81 (step @p658 :rule trans :premises (@p657 @p642)) % 0.44/0.81 (step @p659 :rule trans :premises (@p658 @p617)) % 0.44/0.81 (step @p660 :rule eq_resolve :premises (@p22 @p659)) % 0.44/0.81 (step @p661 :rule implies_elim :premises (@p660)) % 0.44/0.81 (step @p662 :rule reordering :premises (@p661) :args ((or @t416 (not @t367)))) % 0.44/0.81 (step @p663 :rule chain_m_resolution :premises (@p662 @p466) :args (@t416 (@list false) (@list @t367))) % 0.44/0.81 (step @p664 :rule trans :premises (@p655 @p640)) % 0.44/0.81 (step @p665 :rule trans :premises (@p664 @p615)) % 0.44/0.81 (step @p666 :rule eq_resolve :premises (@p14 @p665)) % 0.44/0.81 (step @p667 :rule cnf_implies_pos :args (@t416)) % 0.44/0.81 (step @p668 :rule reordering :premises (@p667) :args ((or @t415 (not @t403) (not @t416)))) % 0.44/0.81 (step @p669 :rule chain_m_resolution :premises (@p668 @p666 @p663) :args (@t415 (@list false false) (@list @t403 @t416))) % 0.44/0.81 (step @p670 :rule refl :args ((tptp.add_a_b tptp.r @t426 @t421))) % 0.44/0.81 (step @p671 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t85 @t420))) % 0.44/0.81 (step @p672 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r tptp.t @t419))) % 0.44/0.81 (step @p673 :rule refl :args ((tptp.add_a_b tptp.r @t80 @t417))) % 0.44/0.81 (step @p674 :rule refl :args ((tptp.a_inv_a_b tptp.r @t79))) % 0.44/0.81 (step @p675 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r tptp.s3 @t57))) % 0.44/0.81 (step @p676 :rule refl :args (tptp.s3)) % 0.44/0.81 (step @p677 :rule cong :premises (@p338 @p676 @p473) :args (@t427)) % 0.44/0.81 (step @p678 :rule trans :premises (@p677 @p675)) % 0.44/0.81 (step @p679 :rule cong :premises (@p338 @p678) :args (@t428)) % 0.44/0.81 (step @p680 :rule trans :premises (@p679 @p674)) % 0.44/0.81 (step @p681 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t41 tptp.r3))) % 0.44/0.81 (step @p682 :rule refl :args (tptp.r3)) % 0.44/0.81 (step @p683 :rule cong :premises (@p338 @p337 @p682) :args (@t429)) % 0.44/0.81 (step @p684 :rule trans :premises (@p683 @p681)) % 0.44/0.81 (step @p685 :rule cong :premises (@p338 @p684 @p680) :args (@t430)) % 0.44/0.81 (step @p686 :rule trans :premises (@p685 @p673)) % 0.44/0.81 (step @p687 :rule cong :premises (@p338 @p318 @p686) :args (@t431)) % 0.44/0.81 (step @p688 :rule trans :premises (@p687 @p672)) % 0.44/0.81 (step @p689 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t84 @t50))) % 0.44/0.81 (step @p690 :rule refl :args (@t432)) % 0.44/0.81 (step @p691 :rule cong :premises (@p338 @p690 @p349) :args (@t433)) % 0.44/0.81 (step @p692 :rule trans :premises (@p691 @p689)) % 0.44/0.81 (step @p693 :rule cong :premises (@p338 @p692 @p688) :args (@t434)) % 0.44/0.81 (step @p694 :rule trans :premises (@p693 @p671)) % 0.44/0.81 (step @p695 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t93 @t425))) % 0.44/0.81 (step @p696 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r tptp.t2 @t424))) % 0.44/0.81 (step @p697 :rule refl :args ((tptp.add_a_b tptp.r @t89 @t422))) % 0.44/0.81 (step @p698 :rule refl :args ((tptp.a_inv_a_b tptp.r @t88))) % 0.44/0.81 (step @p699 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r tptp.s2 @t40))) % 0.44/0.81 (step @p700 :rule refl :args (tptp.s2)) % 0.44/0.81 (step @p701 :rule cong :premises (@p338 @p700 @p336) :args (@t435)) % 0.44/0.81 (step @p702 :rule trans :premises (@p701 @p699)) % 0.44/0.81 (step @p703 :rule cong :premises (@p338 @p702) :args (@t436)) % 0.44/0.81 (step @p704 :rule trans :premises (@p703 @p698)) % 0.44/0.81 (step @p705 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t50 tptp.r2))) % 0.44/0.81 (step @p706 :rule refl :args (tptp.r2)) % 0.44/0.81 (step @p707 :rule cong :premises (@p338 @p349 @p706) :args (@t437)) % 0.44/0.81 (step @p708 :rule trans :premises (@p707 @p705)) % 0.44/0.81 (step @p709 :rule cong :premises (@p338 @p708 @p704) :args (@t438)) % 0.44/0.81 (step @p710 :rule trans :premises (@p709 @p697)) % 0.44/0.81 (step @p711 :rule cong :premises (@p338 @p304 @p710) :args (@t439)) % 0.44/0.81 (step @p712 :rule trans :premises (@p711 @p696)) % 0.44/0.81 (step @p713 :rule refl :args ((tptp.mult_a_ring_ext_a_b tptp.r @t92 @t41))) % 0.44/0.81 (step @p714 :rule refl :args (@t440)) % 0.44/0.81 (step @p715 :rule cong :premises (@p338 @p714 @p337) :args (@t441)) % 0.44/0.81 (step @p716 :rule trans :premises (@p715 @p713)) % 0.44/0.81 (step @p717 :rule cong :premises (@p338 @p716 @p712) :args (@t442)) % 0.44/0.81 (step @p718 :rule trans :premises (@p717 @p695)) % 0.44/0.81 (step @p719 :rule cong :premises (@p338 @p718 @p694) :args (@t443)) % 0.44/0.81 (step @p720 :rule trans :premises (@p719 @p670)) % 0.44/0.81 (step @p721 :rule ho_cong :premises (@p364 @p718)) % 0.44/0.81 (step @p722 :rule ho_cong :premises (@p721 @p694)) % 0.44/0.81 (step @p723 :rule cong :premises (@p722 @p720) :args ((= (_ (_ @t8 @t442) @t434) @t443))) % 0.44/0.81 (step @p724 :rule symm :premises (@p723)) % 0.44/0.81 (step @p725 :rule refl :args (@t444)) % 0.44/0.81 (step @p726 :rule eq_resolve :premises (@p725 @p724)) % 0.44/0.81 (step @p727 :rule ho_cong :premises (@p377 @p692)) % 0.44/0.81 (step @p728 :rule ho_cong :premises (@p727 @p688)) % 0.44/0.81 (step @p729 :rule cong :premises (@p728 @p694) :args ((= (_ (_ @t18 @t433) @t431) @t434))) % 0.44/0.81 (step @p730 :rule symm :premises (@p729)) % 0.44/0.81 (step @p731 :rule refl :args (@t421)) % 0.44/0.81 (step @p732 :rule eq_resolve :premises (@p731 @p730)) % 0.44/0.81 (step @p733 :rule refl :args (@t82)) % 0.44/0.81 (step @p734 :rule ho_cong :premises (@p733 @p686)) % 0.44/0.81 (step @p735 :rule cong :premises (@p734 @p688) :args ((= (_ @t82 @t430) @t431))) % 0.44/0.81 (step @p736 :rule symm :premises (@p735)) % 0.44/0.81 (step @p737 :rule refl :args (@t420)) % 0.44/0.81 (step @p738 :rule eq_resolve :premises (@p737 @p736)) % 0.44/0.81 (step @p739 :rule ho_cong :premises (@p364 @p684)) % 0.44/0.81 (step @p740 :rule ho_cong :premises (@p739 @p680)) % 0.44/0.81 (step @p741 :rule cong :premises (@p740 @p686) :args ((= (_ (_ @t8 @t429) @t428) @t430))) % 0.44/0.81 (step @p742 :rule symm :premises (@p741)) % 0.44/0.81 (step @p743 :rule refl :args (@t419)) % 0.44/0.81 (step @p744 :rule eq_resolve :premises (@p743 @p742)) % 0.44/0.81 (step @p745 :rule ho_cong :premises (@p371 @p678)) % 0.44/0.81 (step @p746 :rule cong :premises (@p745 @p680) :args ((= (_ @t140 @t427) @t428))) % 0.44/0.81 (step @p747 :rule symm :premises (@p746)) % 0.44/0.81 (step @p748 :rule refl :args (@t417)) % 0.44/0.81 (step @p749 :rule eq_resolve :premises (@p748 @p747)) % 0.44/0.81 (step @p750 :rule refl :args (@t48)) % 0.44/0.81 (step @p751 :rule ho_cong :premises (@p750 @p473)) % 0.44/0.81 (step @p752 :rule cong :premises (@p751 @p678) :args ((= (_ @t48 @t382) @t427))) % 0.44/0.81 (step @p753 :rule symm :premises (@p752)) % 0.44/0.81 (step @p754 :rule refl :args (@t79)) % 0.44/0.81 (step @p755 :rule eq_resolve :premises (@p754 @p753)) % 0.44/0.81 (step @p756 :rule refl :args (@t48)) % 0.44/0.81 (step @p757 :rule ho_cong :premises (@p756 @p527)) % 0.44/0.81 (step @p758 :rule trans :premises (@p757 @p755)) % 0.44/0.81 (step @p759 :rule ho_cong :premises (@p409 @p758)) % 0.44/0.81 (step @p760 :rule trans :premises (@p759 @p749)) % 0.44/0.81 (step @p761 :rule ho_cong :premises (@p384 @p682)) % 0.44/0.81 (step @p762 :rule cong :premises (@p761 @p684) :args ((= (_ @t370 tptp.r3) @t429))) % 0.44/0.81 (step @p763 :rule symm :premises (@p762)) % 0.44/0.81 (step @p764 :rule refl :args (@t80)) % 0.44/0.81 (step @p765 :rule eq_resolve :premises (@p764 @p763)) % 0.44/0.81 (step @p766 :rule refl :args (tptp.r3)) % 0.44/0.81 (step @p767 :rule ho_cong :premises (@p399 @p766)) % 0.44/0.81 (step @p768 :rule trans :premises (@p767 @p765)) % 0.44/0.81 (step @p769 :rule ho_cong :premises (@p438 @p768)) % 0.44/0.81 (step @p770 :rule ho_cong :premises (@p769 @p760)) % 0.44/0.81 (step @p771 :rule trans :premises (@p770 @p744)) % 0.44/0.81 (step @p772 :rule refl :args (@t82)) % 0.44/0.81 (step @p773 :rule ho_cong :premises (@p772 @p771)) % 0.44/0.81 (step @p774 :rule trans :premises (@p773 @p738)) % 0.44/0.81 (step @p775 :rule ho_cong :premises (@p377 @p690)) % 0.44/0.81 (step @p776 :rule ho_cong :premises (@p775 @p349)) % 0.44/0.81 (step @p777 :rule cong :premises (@p776 @p692) :args ((= (_ (_ @t18 @t432) @t363) @t433))) % 0.44/0.81 (step @p778 :rule symm :premises (@p777)) % 0.44/0.81 (step @p779 :rule refl :args (@t85)) % 0.44/0.81 (step @p780 :rule eq_resolve :premises (@p779 @p778)) % 0.44/0.81 (step @p781 :rule refl :args (@t84)) % 0.44/0.81 (step @p782 :rule cong :premises (@p781 @p690) :args ((= @t84 @t432))) % 0.44/0.81 (step @p783 :rule symm :premises (@p782)) % 0.44/0.81 (step @p784 :rule eq_resolve :premises (@p781 @p783)) % 0.44/0.81 (step @p785 :rule ho_cong :premises (@p398 @p784)) % 0.44/0.81 (step @p786 :rule ho_cong :premises (@p785 @p431)) % 0.44/0.81 (step @p787 :rule trans :premises (@p786 @p780)) % 0.44/0.81 (step @p788 :rule ho_cong :premises (@p398 @p787)) % 0.44/0.81 (step @p789 :rule ho_cong :premises (@p788 @p774)) % 0.44/0.81 (step @p790 :rule trans :premises (@p789 @p732)) % 0.44/0.81 (step @p791 :rule ho_cong :premises (@p377 @p716)) % 0.44/0.81 (step @p792 :rule ho_cong :premises (@p791 @p712)) % 0.44/0.81 (step @p793 :rule cong :premises (@p792 @p718) :args ((= (_ (_ @t18 @t441) @t439) @t442))) % 0.44/0.81 (step @p794 :rule symm :premises (@p793)) % 0.44/0.81 (step @p795 :rule refl :args (@t426)) % 0.44/0.81 (step @p796 :rule eq_resolve :premises (@p795 @p794)) % 0.44/0.81 (step @p797 :rule refl :args (@t73)) % 0.44/0.81 (step @p798 :rule ho_cong :premises (@p797 @p710)) % 0.44/0.81 (step @p799 :rule cong :premises (@p798 @p712) :args ((= (_ @t73 @t438) @t439))) % 0.44/0.81 (step @p800 :rule symm :premises (@p799)) % 0.44/0.81 (step @p801 :rule refl :args (@t425)) % 0.44/0.81 (step @p802 :rule eq_resolve :premises (@p801 @p800)) % 0.44/0.81 (step @p803 :rule ho_cong :premises (@p364 @p708)) % 0.44/0.81 (step @p804 :rule ho_cong :premises (@p803 @p704)) % 0.44/0.81 (step @p805 :rule cong :premises (@p804 @p710) :args ((= (_ (_ @t8 @t437) @t436) @t438))) % 0.44/0.81 (step @p806 :rule symm :premises (@p805)) % 0.44/0.81 (step @p807 :rule refl :args (@t424)) % 0.44/0.81 (step @p808 :rule eq_resolve :premises (@p807 @p806)) % 0.44/0.81 (step @p809 :rule ho_cong :premises (@p371 @p702)) % 0.44/0.81 (step @p810 :rule cong :premises (@p809 @p704) :args ((= (_ @t140 @t435) @t436))) % 0.44/0.81 (step @p811 :rule symm :premises (@p810)) % 0.44/0.81 (step @p812 :rule refl :args (@t422)) % 0.44/0.81 (step @p813 :rule eq_resolve :premises (@p812 @p811)) % 0.44/0.81 (step @p814 :rule refl :args (@t44)) % 0.44/0.81 (step @p815 :rule ho_cong :premises (@p814 @p336)) % 0.44/0.81 (step @p816 :rule cong :premises (@p815 @p702) :args ((= (_ @t44 @t356) @t435))) % 0.44/0.81 (step @p817 :rule symm :premises (@p816)) % 0.44/0.81 (step @p818 :rule refl :args (@t88)) % 0.44/0.81 (step @p819 :rule eq_resolve :premises (@p818 @p817)) % 0.44/0.81 (step @p820 :rule refl :args (@t44)) % 0.44/0.81 (step @p821 :rule ho_cong :premises (@p820 @p393)) % 0.44/0.81 (step @p822 :rule trans :premises (@p821 @p819)) % 0.44/0.81 (step @p823 :rule ho_cong :premises (@p409 @p822)) % 0.44/0.81 (step @p824 :rule trans :premises (@p823 @p813)) % 0.44/0.81 (step @p825 :rule ho_cong :premises (@p422 @p706)) % 0.44/0.81 (step @p826 :rule cong :premises (@p825 @p708) :args ((= (_ @t372 tptp.r2) @t437))) % 0.44/0.81 (step @p827 :rule symm :premises (@p826)) % 0.44/0.81 (step @p828 :rule refl :args (@t89)) % 0.44/0.81 (step @p829 :rule eq_resolve :premises (@p828 @p827)) % 0.44/0.81 (step @p830 :rule refl :args (tptp.r2)) % 0.44/0.81 (step @p831 :rule ho_cong :premises (@p432 @p830)) % 0.44/0.81 (step @p832 :rule trans :premises (@p831 @p829)) % 0.44/0.81 (step @p833 :rule ho_cong :premises (@p438 @p832)) % 0.44/0.81 (step @p834 :rule ho_cong :premises (@p833 @p824)) % 0.44/0.81 (step @p835 :rule trans :premises (@p834 @p808)) % 0.44/0.81 (step @p836 :rule refl :args (@t73)) % 0.44/0.81 (step @p837 :rule ho_cong :premises (@p836 @p835)) % 0.44/0.81 (step @p838 :rule trans :premises (@p837 @p802)) % 0.44/0.81 (step @p839 :rule ho_cong :premises (@p377 @p714)) % 0.44/0.81 (step @p840 :rule ho_cong :premises (@p839 @p337)) % 0.44/0.81 (step @p841 :rule cong :premises (@p840 @p716) :args ((= (_ (_ @t18 @t440) @t357) @t441))) % 0.44/0.81 (step @p842 :rule symm :premises (@p841)) % 0.44/0.81 (step @p843 :rule refl :args (@t93)) % 0.44/0.81 (step @p844 :rule eq_resolve :premises (@p843 @p842)) % 0.44/0.81 (step @p845 :rule refl :args (@t92)) % 0.44/0.81 (step @p846 :rule cong :premises (@p845 @p714) :args ((= @t92 @t440))) % 0.44/0.81 (step @p847 :rule symm :premises (@p846)) % 0.44/0.81 (step @p848 :rule eq_resolve :premises (@p845 @p847)) % 0.44/0.81 (step @p849 :rule ho_cong :premises (@p398 @p848)) % 0.44/0.81 (step @p850 :rule ho_cong :premises (@p849 @p397)) % 0.44/0.81 (step @p851 :rule trans :premises (@p850 @p844)) % 0.44/0.81 (step @p852 :rule ho_cong :premises (@p398 @p851)) % 0.44/0.81 (step @p853 :rule ho_cong :premises (@p852 @p838)) % 0.44/0.81 (step @p854 :rule trans :premises (@p853 @p796)) % 0.44/0.81 (step @p855 :rule ho_cong :premises (@p438 @p854)) % 0.44/0.81 (step @p856 :rule ho_cong :premises (@p855 @p790)) % 0.44/0.81 (step @p857 :rule trans :premises (@p856 @p726)) % 0.44/0.81 (step @p858 :rule cong :premises (@p857 @p557) :args (@t445)) % 0.44/0.81 (step @p859 :rule cong :premises (@p858) :args ((not @t445))) % 0.44/0.81 (step @p860 :rule beta-reduce :args ((= (_ @t446 @t79) @t419))) % 0.44/0.81 (step @p861 :rule refl :args (@t79)) % 0.44/0.81 (step @p862 :rule beta-reduce :args ((= (_ @t376 @t80) @t446))) % 0.44/0.81 (step @p863 :rule refl :args (@t80)) % 0.44/0.81 (step @p864 :rule ho_cong :premises (@p451 @p863)) % 0.44/0.81 (step @p865 :rule trans :premises (@p864 @p862)) % 0.44/0.81 (step @p866 :rule ho_cong :premises (@p865 @p861)) % 0.44/0.81 (step @p867 :rule trans :premises (@p866 @p860)) % 0.44/0.81 (step @p868 :rule ho_cong :premises (@p772 @p867)) % 0.44/0.81 (step @p869 :rule refl :args (@t86)) % 0.44/0.81 (step @p870 :rule ho_cong :premises (@p869 @p868)) % 0.44/0.81 (step @p871 :rule beta-reduce :args ((= (_ @t447 @t88) @t424))) % 0.44/0.81 (step @p872 :rule refl :args (@t88)) % 0.44/0.81 (step @p873 :rule beta-reduce :args ((= (_ @t376 @t89) @t447))) % 0.44/0.81 (step @p874 :rule refl :args (@t89)) % 0.44/0.81 (step @p875 :rule ho_cong :premises (@p451 @p874)) % 0.44/0.81 (step @p876 :rule trans :premises (@p875 @p873)) % 0.44/0.81 (step @p877 :rule ho_cong :premises (@p876 @p872)) % 0.44/0.81 (step @p878 :rule trans :premises (@p877 @p871)) % 0.44/0.81 (step @p879 :rule ho_cong :premises (@p836 @p878)) % 0.44/0.81 (step @p880 :rule refl :args (@t94)) % 0.44/0.81 (step @p881 :rule ho_cong :premises (@p880 @p879)) % 0.44/0.81 (step @p882 :rule ho_cong :premises (@p438 @p881)) % 0.44/0.81 (step @p883 :rule ho_cong :premises (@p882 @p870)) % 0.44/0.81 (step @p884 :rule cong :premises (@p883 @p634) :args (@t449)) % 0.44/0.81 (step @p885 :rule cong :premises (@p884) :args ((not @t449))) % 0.44/0.81 (step @p886 :rule ho_cong :premises (@p459 @p863)) % 0.44/0.81 (step @p887 :rule ho_cong :premises (@p886 @p861)) % 0.44/0.81 (step @p888 :rule ho_cong :premises (@p772 @p887)) % 0.44/0.81 (step @p889 :rule ho_cong :premises (@p869 @p888)) % 0.44/0.81 (step @p890 :rule ho_cong :premises (@p459 @p874)) % 0.44/0.81 (step @p891 :rule ho_cong :premises (@p890 @p872)) % 0.44/0.81 (step @p892 :rule ho_cong :premises (@p836 @p891)) % 0.44/0.81 (step @p893 :rule ho_cong :premises (@p880 @p892)) % 0.44/0.81 (step @p894 :rule ho_cong :premises (@p438 @p893)) % 0.44/0.81 (step @p895 :rule ho_cong :premises (@p894 @p889)) % 0.44/0.81 (step @p896 :rule cong :premises (@p895 @p651) :args (@t335)) % 0.44/0.81 (step @p897 :rule cong :premises (@p896) :args (@t336)) % 0.44/0.81 (step @p898 :rule trans :premises (@p897 @p885)) % 0.44/0.81 (step @p899 :rule trans :premises (@p898 @p859)) % 0.44/0.81 (step @p900 :rule eq_resolve :premises (@p237 @p899)) % 0.44/0.81 (step @p901 :rule false_intro :premises (@p900)) % 0.44/0.81 (step @p902 :rule refl :args (@t391)) % 0.44/0.81 (step @p903 :rule eq-symm :args (@t443 @t398)) % 0.44/0.81 (step @p904 :rule cong :premises (@p857 @p589) :args ((= @t444 @t399))) % 0.44/0.81 (step @p905 :rule trans :premises (@p904 @p903)) % 0.44/0.81 (step @p906 :rule cong :premises (@p883 @p631) :args ((= @t448 @t409))) % 0.44/0.81 (step @p907 :rule cong :premises (@p895 @p648) :args (@t97)) % 0.44/0.81 (step @p908 :rule trans :premises (@p907 @p906)) % 0.44/0.81 (step @p909 :rule trans :premises (@p908 @p905)) % 0.44/0.81 (step @p910 :rule eq_resolve :premises (@p20 @p909)) % 0.44/0.81 (step @p911 :rule cong :premises (@p910 @p902) :args (@t414)) % 0.44/0.81 (step @p912 :rule trans :premises (@p911 @p901)) % 0.44/0.81 (step @p913 :rule false_elim :premises (@p912)) % 0.44/0.81 (step @p914 :rule cnf_implies_pos :args (@t415)) % 0.44/0.81 (step @p915 :rule reordering :premises (@p914) :args ((or @t414 @t450 (not @t415)))) % 0.44/0.81 (step @p916 :rule chain_m_resolution :premises (@p915 @p913 @p669) :args (@t450 @t451 (@list @t414 @t415))) % 0.44/0.81 (step @p917 :rule cnf_or_pos :args (@t454)) % 0.44/0.81 (step @p918 :rule reordering :premises (@p917) :args ((or @t401 @t452 @t453 @t455))) % 0.44/0.81 (step @p919 :rule chain_m_resolution :premises (@p918 @p916 @p330 @p316) :args (@t455 (@list true false false) (@list @t401 @t353 @t352))) % 0.44/0.81 (assume-push @p926 @t456) % 0.44/0.81 (step @p921 :rule instantiate :premises (@p302) :args ((@list tptp.t2 tptp.t))) % 0.44/0.81 (step-pop @p927 :rule scope :premises (@p921)) % 0.44/0.81 (step @p922 :rule process_scope :premises (@p927) :args (@t454)) % 0.44/0.81 (step @p924 :rule implies_elim :premises (@p922)) % 0.44/0.81 (step @p925 false :rule chain_m_resolution :premises (@p924 @p919 @p302) :args (false @t451 (@list @t454 @t456))) % 0.44/0.81 ) % 0.44/0.81 % SZS output end Proof % 0.44/0.81 % cvc5 exiting %------------------------------------------------------------------------------