%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP127^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 : n014.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:08 AM UTC 2026 % Result : Theorem 0.46s 0.90s % Output : Proof 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : ITP127^1 : TPTP v9.2.1. Released v7.5.0. % 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.36 % Computer : n014.cluster.edu % 0.18/0.36 % Model : x86_64 x86_64 % 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.36 % Memory : 8042.1875MB % 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.36 % CPULimit : 300 % 0.18/0.36 % WCLimit : 300 % 0.18/0.36 % DateTime : Tue Jun 2 04:15:28 EDT 2026 % 0.18/0.36 % CPUTime : % 0.37/0.61 %----Proving TH0 % 0.46/0.90 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.46/0.90 % SZS status Theorem % 0.46/0.90 % SZS output start Proof % 0.46/0.90 ( % 0.46/0.90 (declare-sort tptp.countable_Set_cset_c 0) % 0.46/0.90 (declare-sort tptp.c 0) % 0.46/0.90 (declare-sort tptp.m 0) % 0.46/0.90 (declare-sort tptp.monomo197243225tT_a_m 0) % 0.46/0.90 (declare-sort tptp.counta191869203tT_a_m 0) % 0.46/0.90 (declare-const tptp.monomo624345106et_a_m (-> tptp.monomo197243225tT_a_m tptp.m)) % 0.46/0.90 (declare-const tptp.monomo412532791tT_m_a (-> tptp.m tptp.monomo197243225tT_a_m)) % 0.46/0.90 (declare-const tptp.ord_le1587667814cset_c (-> tptp.countable_Set_cset_c tptp.countable_Set_cset_c Bool)) % 0.46/0.90 (declare-const tptp.order_1683649299cset_c (-> (-> tptp.countable_Set_cset_c Bool) tptp.countable_Set_cset_c)) % 0.46/0.90 (declare-const tptp.if_c (-> Bool tptp.c tptp.c tptp.c)) % 0.46/0.90 (declare-const tptp.if_Cou1542198912cset_c (-> Bool tptp.countable_Set_cset_c tptp.countable_Set_cset_c tptp.countable_Set_cset_c)) % 0.46/0.90 (declare-const tptp.countable_Set_cin_c (-> tptp.c tptp.countable_Set_cset_c Bool)) % 0.46/0.90 (declare-const tptp.minus_1646763425cset_c (-> tptp.countable_Set_cset_c tptp.countable_Set_cset_c tptp.countable_Set_cset_c)) % 0.46/0.90 (declare-const tptp.comp_m1038691662_a_m_c (-> (-> tptp.m tptp.monomo197243225tT_a_m) (-> tptp.c tptp.m) tptp.c tptp.monomo197243225tT_a_m)) % 0.46/0.90 (declare-const tptp.comp_M750374454_m_m_m (-> (-> tptp.monomo197243225tT_a_m tptp.m) (-> tptp.m tptp.monomo197243225tT_a_m) tptp.m tptp.m)) % 0.46/0.90 (declare-const tptp.comp_c997395372tT_a_m (-> (-> tptp.c tptp.m) (-> tptp.monomo197243225tT_a_m tptp.c) tptp.monomo197243225tT_a_m tptp.m)) % 0.46/0.90 (declare-const tptp.comp_c_c_c (-> (-> tptp.c tptp.c) (-> tptp.c tptp.c) tptp.c tptp.c)) % 0.46/0.90 (declare-const tptp.comp_c_m_m (-> (-> tptp.c tptp.m) (-> tptp.m tptp.c) tptp.m tptp.m)) % 0.46/0.90 (declare-const tptp.counta472291938sert_c (-> tptp.c tptp.countable_Set_cset_c tptp.countable_Set_cset_c)) % 0.46/0.90 (declare-const tptp.comp_M1062614966_m_c_c (-> (-> tptp.monomo197243225tT_a_m tptp.c) (-> tptp.c tptp.monomo197243225tT_a_m) tptp.c tptp.c)) % 0.46/0.90 (declare-const tptp.mergec (-> tptp.countable_Set_cset_c (-> tptp.c tptp.m) tptp.m)) % 0.46/0.90 (declare-const tptp.comp_m_m_m (-> (-> tptp.m tptp.m) (-> tptp.m tptp.m) tptp.m tptp.m)) % 0.46/0.90 (declare-const tptp.bot_bo1320844070cset_c tptp.countable_Set_cset_c) % 0.46/0.90 (declare-const tptp.f (-> tptp.c tptp.monomo197243225tT_a_m)) % 0.46/0.90 (declare-const tptp.x tptp.c) % 0.46/0.90 (declare-const tptp.comp_M864375327_a_m_c (-> (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m) (-> tptp.c tptp.monomo197243225tT_a_m) tptp.c tptp.monomo197243225tT_a_m)) % 0.46/0.90 (declare-const tptp.comp_m_c_c (-> (-> tptp.m tptp.c) (-> tptp.c tptp.m) tptp.c tptp.c)) % 0.46/0.90 (define tptp.comp_M1944986301tT_a_m () (let ((_let_1 (@var "X2" tptp.monomo197243225tT_a_m))) (let ((_let_2 (@var "G" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m)))) (let ((_let_3 (@var "F2" (-> tptp.monomo197243225tT_a_m tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.comp_m263856566tT_a_m () (let ((_let_1 (@var "X2" tptp.monomo197243225tT_a_m))) (let ((_let_2 (@var "G" (-> tptp.monomo197243225tT_a_m tptp.m)))) (let ((_let_3 (@var "F2" (-> tptp.m tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.comp_m_m_c () (let ((_let_1 (@var "X2" tptp.c))) (let ((_let_2 (@var "G" (-> tptp.c tptp.m)))) (let ((_let_3 (@var "F2" (-> tptp.m tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.comp_c1772230468_a_m_c () (let ((_let_1 (@var "X2" tptp.c))) (let ((_let_2 (@var "G" (-> tptp.c tptp.c)))) (let ((_let_3 (@var "F2" (-> tptp.c tptp.monomo197243225tT_a_m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.comp_c_m_c () (let ((_let_1 (@var "X2" tptp.c))) (let ((_let_2 (@var "G" (-> tptp.c tptp.c)))) (let ((_let_3 (@var "F2" (-> tptp.c tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.comp_M750374444_m_m_c () (let ((_let_1 (@var "X2" tptp.c))) (let ((_let_2 (@var "G" (-> tptp.c tptp.monomo197243225tT_a_m)))) (let ((_let_3 (@var "F2" (-> tptp.monomo197243225tT_a_m tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ _let_3 (_ _let_2 _let_1))))))) % 0.46/0.90 (define tptp.monomo2081011572_m_m_a () (let ((_let_1 (@var "F2" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m)))) (let ((_let_2 (@var "A3" tptp.counta191869203tT_a_m))) (let ((_let_3 (@var "Mergec2" (-> tptp.counta191869203tT_a_m (-> tptp.monomo197243225tT_a_m tptp.m) tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ tptp.monomo412532791tT_m_a (_ (_ _let_3 _let_2) (_ (_ tptp.comp_M1944986301tT_a_m tptp.monomo624345106et_a_m) _let_1)))))))) % 0.46/0.90 (define tptp.monomo463139869_c_m_a () (let ((_let_1 (@var "F2" (-> tptp.c tptp.monomo197243225tT_a_m)))) (let ((_let_2 (@var "A3" tptp.countable_Set_cset_c))) (let ((_let_3 (@var "Mergec2" (-> tptp.countable_Set_cset_c (-> tptp.c tptp.m) tptp.m)))) (lambda (@list _let_3 _let_2 _let_1) (_ tptp.monomo412532791tT_m_a (_ (_ _let_3 _let_2) (_ (_ tptp.comp_M750374444_m_m_c tptp.monomo624345106et_a_m) _let_1)))))))) % 0.46/0.90 (define tptp.ord_le15364698cset_c () (let ((_let_1 (@var "Y2" tptp.countable_Set_cset_c))) (let ((_let_2 (@var "X2" tptp.countable_Set_cset_c))) (lambda (@list _let_2 _let_1) (or (_ (_ tptp.ord_le1587667814cset_c _let_2) _let_1) (= _let_2 _let_1)))))) % 0.46/0.90 (define tptp.ord_le1376176871cset_c () (let ((_let_1 (@var "Y6" (-> Bool tptp.countable_Set_cset_c)))) (let ((_let_2 (@var "X5" (-> Bool tptp.countable_Set_cset_c)))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le15364698cset_c (_ _let_2 false)) (_ _let_1 false)) (_ (_ tptp.ord_le15364698cset_c (_ _let_2 true)) (_ _let_1 true))))))) % 0.46/0.90 (define @t1 () (@var "X" tptp.c)) % 0.46/0.90 (define @t2 () (@var "F" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t3 () (_ @t2 @t1)) % 0.46/0.90 (define @t4 () (_ tptp.counta472291938sert_c @t1)) % 0.46/0.90 (define @t5 () (_ @t4 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t6 () (_ (_ tptp.mergec @t5) @t2)) % 0.46/0.90 (define @t7 () (= @t6 @t3)) % 0.46/0.90 (define @t8 () (forall (@list @t1 @t2) @t7)) % 0.46/0.90 (define @t9 () (@var "A" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t10 () (_ @t4 @t9)) % 0.46/0.90 (define @t11 () (@list @t1 @t9)) % 0.46/0.90 (define @t12 () (@var "C" tptp.c)) % 0.46/0.90 (define @t13 () (@var "B" tptp.c)) % 0.46/0.90 (define @t14 () (@var "D" tptp.c)) % 0.46/0.90 (define @t15 () (@var "A2" tptp.c)) % 0.46/0.90 (define @t16 () (_ tptp.counta472291938sert_c @t13)) % 0.46/0.90 (define @t17 () (_ @t16 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t18 () (_ tptp.counta472291938sert_c @t15)) % 0.46/0.90 (define @t19 () (= @t15 @t13)) % 0.46/0.90 (define @t20 () (_ @t18 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t21 () (_ @t18 @t9)) % 0.46/0.90 (define @t22 () (@list @t15 @t9)) % 0.46/0.90 (define @t23 () (@var "Y" tptp.c)) % 0.46/0.90 (define @t24 () (_ tptp.counta472291938sert_c @t23)) % 0.46/0.90 (define @t25 () (@list @t1 @t23 @t9)) % 0.46/0.90 (define @t26 () (@var "F" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t27 () (_ tptp.comp_M750374444_m_m_c tptp.monomo624345106et_a_m)) % 0.46/0.90 (define @t28 () (_ @t27 @t26)) % 0.46/0.90 (define @t29 () (_ (_ tptp.mergec @t9) @t28)) % 0.46/0.90 (define @t30 () (_ tptp.monomo463139869_c_m_a tptp.mergec)) % 0.46/0.90 (define @t31 () (_ (_ @t30 @t9) @t26)) % 0.46/0.90 (define @t32 () (@list @t9 @t26)) % 0.46/0.90 (define @t33 () (@var "NondetT2" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t34 () (@var "NondetT" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t35 () (= @t34 @t33)) % 0.46/0.90 (define @t36 () (_ tptp.monomo624345106et_a_m @t33)) % 0.46/0.90 (define @t37 () (_ tptp.monomo624345106et_a_m @t34)) % 0.46/0.90 (define @t38 () (= @t37 @t36)) % 0.46/0.90 (define @t39 () (@list @t34 @t33)) % 0.46/0.90 (define @t40 () (forall @t39 (=> @t38 @t35))) % 0.46/0.90 (define @t41 () (@var "F" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t42 () (_ tptp.comp_M1944986301tT_a_m tptp.monomo624345106et_a_m)) % 0.46/0.90 (define @t43 () (@var "A" tptp.counta191869203tT_a_m)) % 0.46/0.90 (define @t44 () (@var "Mergec" (-> tptp.counta191869203tT_a_m (-> tptp.monomo197243225tT_a_m tptp.m) tptp.m))) % 0.46/0.90 (define @t45 () (@var "Mergec" (-> tptp.countable_Set_cset_c (-> tptp.c tptp.m) tptp.m))) % 0.46/0.90 (define @t46 () (@var "H" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t47 () (@var "G2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t48 () (_ tptp.comp_c1772230468_a_m_c @t47)) % 0.46/0.90 (define @t49 () (_ @t48 @t46)) % 0.46/0.90 (define @t50 () (@var "F" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t51 () (_ tptp.comp_M750374444_m_m_c @t50)) % 0.46/0.90 (define @t52 () (_ @t51 @t49)) % 0.46/0.90 (define @t53 () (_ @t51 @t47)) % 0.46/0.90 (define @t54 () (_ (_ tptp.comp_c_m_c @t53) @t46)) % 0.46/0.90 (define @t55 () (@var "H" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t56 () (@var "G2" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t57 () (_ tptp.comp_M750374444_m_m_c @t56)) % 0.46/0.90 (define @t58 () (_ @t57 @t55)) % 0.46/0.90 (define @t59 () (@var "F" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t60 () (_ tptp.comp_m_m_c @t59)) % 0.46/0.90 (define @t61 () (_ @t60 @t58)) % 0.46/0.90 (define @t62 () (_ tptp.comp_m263856566tT_a_m @t59)) % 0.46/0.90 (define @t63 () (_ @t62 @t56)) % 0.46/0.90 (define @t64 () (_ (_ tptp.comp_M750374444_m_m_c @t63) @t55)) % 0.46/0.90 (define @t65 () (@var "G2" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t66 () (_ (_ tptp.comp_M864375327_a_m_c @t65) @t55)) % 0.46/0.90 (define @t67 () (_ @t51 @t66)) % 0.46/0.90 (define @t68 () (_ tptp.comp_M1944986301tT_a_m @t50)) % 0.46/0.90 (define @t69 () (_ @t68 @t65)) % 0.46/0.90 (define @t70 () (_ (_ tptp.comp_M750374444_m_m_c @t69) @t55)) % 0.46/0.90 (define @t71 () (@var "H" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t72 () (@var "G2" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t73 () (_ tptp.comp_m_m_c @t72)) % 0.46/0.90 (define @t74 () (_ @t73 @t71)) % 0.46/0.90 (define @t75 () (_ @t60 @t74)) % 0.46/0.90 (define @t76 () (_ tptp.comp_m_m_m @t59)) % 0.46/0.90 (define @t77 () (_ @t76 @t72)) % 0.46/0.90 (define @t78 () (_ (_ tptp.comp_m_m_c @t77) @t71)) % 0.46/0.90 (define @t79 () (@var "G2" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t80 () (_ (_ tptp.comp_m_c_c @t79) @t71)) % 0.46/0.90 (define @t81 () (_ tptp.comp_c_m_c @t2)) % 0.46/0.90 (define @t82 () (_ @t81 @t80)) % 0.46/0.90 (define @t83 () (_ tptp.comp_c_m_m @t2)) % 0.46/0.90 (define @t84 () (_ @t83 @t79)) % 0.46/0.90 (define @t85 () (_ (_ tptp.comp_m_m_c @t84) @t71)) % 0.46/0.90 (define @t86 () (@var "G2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t87 () (_ tptp.comp_c_m_c @t86)) % 0.46/0.90 (define @t88 () (_ @t87 @t46)) % 0.46/0.90 (define @t89 () (_ @t60 @t88)) % 0.46/0.90 (define @t90 () (_ @t60 @t86)) % 0.46/0.90 (define @t91 () (_ (_ tptp.comp_c_m_c @t90) @t46)) % 0.46/0.90 (define @t92 () (@var "G2" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t93 () (_ (_ tptp.comp_c_c_c @t92) @t46)) % 0.46/0.90 (define @t94 () (_ @t81 @t93)) % 0.46/0.90 (define @t95 () (_ @t81 @t92)) % 0.46/0.90 (define @t96 () (_ (_ tptp.comp_c_m_c @t95) @t46)) % 0.46/0.90 (define @t97 () (@var "H" (-> tptp.monomo197243225tT_a_m tptp.c))) % 0.46/0.90 (define @t98 () (_ (_ tptp.comp_c997395372tT_a_m @t86) @t97)) % 0.46/0.90 (define @t99 () (_ (_ tptp.comp_c997395372tT_a_m @t90) @t97)) % 0.46/0.90 (define @t100 () (@var "G2" (-> tptp.monomo197243225tT_a_m tptp.c))) % 0.46/0.90 (define @t101 () (_ (_ tptp.comp_M1062614966_m_c_c @t100) @t55)) % 0.46/0.90 (define @t102 () (_ tptp.comp_c997395372tT_a_m @t2)) % 0.46/0.90 (define @t103 () (_ (_ tptp.comp_M750374444_m_m_c (_ @t102 @t100)) @t55)) % 0.46/0.90 (define @t104 () (@var "H" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t105 () (_ tptp.comp_m263856566tT_a_m @t72)) % 0.46/0.90 (define @t106 () (_ @t62 (_ @t105 @t104))) % 0.46/0.90 (define @t107 () (@var "V" tptp.c)) % 0.46/0.90 (define @t108 () (@var "D" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t109 () (@var "C" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t110 () (_ @t109 (_ @t108 @t107))) % 0.46/0.90 (define @t111 () (@var "B" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t112 () (@var "A2" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t113 () (_ @t112 (_ @t111 @t107))) % 0.46/0.90 (define @t114 () (_ (_ tptp.comp_M750374444_m_m_c @t109) @t108)) % 0.46/0.90 (define @t115 () (_ (_ tptp.comp_M750374444_m_m_c @t112) @t111)) % 0.46/0.90 (define @t116 () (= @t115 @t114)) % 0.46/0.90 (define @t117 () (@var "D" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t118 () (@var "C" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t119 () (_ @t118 (_ @t117 @t107))) % 0.46/0.90 (define @t120 () (@var "B" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t121 () (@var "A2" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t122 () (_ @t121 (_ @t120 @t107))) % 0.46/0.90 (define @t123 () (_ (_ tptp.comp_m_m_c @t118) @t117)) % 0.46/0.90 (define @t124 () (_ (_ tptp.comp_m_m_c @t121) @t120)) % 0.46/0.90 (define @t125 () (= @t124 @t123)) % 0.46/0.90 (define @t126 () (@var "D" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t127 () (_ @t126 @t107)) % 0.46/0.90 (define @t128 () (@var "C" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t129 () (_ @t128 @t127)) % 0.46/0.90 (define @t130 () (_ (_ tptp.comp_c_m_c @t128) @t126)) % 0.46/0.90 (define @t131 () (= @t124 @t130)) % 0.46/0.90 (define @t132 () (@var "B" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t133 () (_ @t132 @t107)) % 0.46/0.90 (define @t134 () (@var "A2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t135 () (_ @t134 @t133)) % 0.46/0.90 (define @t136 () (_ (_ tptp.comp_c_m_c @t134) @t132)) % 0.46/0.90 (define @t137 () (= @t136 @t123)) % 0.46/0.90 (define @t138 () (= @t136 @t130)) % 0.46/0.90 (define @t139 () (= @t115 @t123)) % 0.46/0.90 (define @t140 () (= @t115 @t130)) % 0.46/0.90 (define @t141 () (@var "V" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t142 () (@var "D" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t143 () (@var "B" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t144 () (_ @t121 (_ @t143 @t141))) % 0.46/0.90 (define @t145 () (_ (_ tptp.comp_m263856566tT_a_m @t121) @t143)) % 0.46/0.90 (define @t146 () (= @t145 (_ (_ tptp.comp_m263856566tT_a_m @t118) @t142))) % 0.46/0.90 (define @t147 () (= @t124 @t114)) % 0.46/0.90 (define @t148 () (@var "C" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t149 () (@var "A2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t150 () (_ @t149 @t133)) % 0.46/0.90 (define @t151 () (_ (_ tptp.comp_c1772230468_a_m_c @t149) @t132)) % 0.46/0.90 (define @t152 () (= @t151 (_ (_ tptp.comp_c1772230468_a_m_c @t148) @t126))) % 0.46/0.90 (define @t153 () (@var "V2" tptp.c)) % 0.46/0.90 (define @t154 () (_ @t109 (_ @t108 @t153))) % 0.46/0.90 (define @t155 () (_ @t112 (_ @t111 @t153))) % 0.46/0.90 (define @t156 () (@list @t153)) % 0.46/0.90 (define @t157 () (_ @t118 (_ @t117 @t153))) % 0.46/0.90 (define @t158 () (_ @t121 (_ @t120 @t153))) % 0.46/0.90 (define @t159 () (_ @t126 @t153)) % 0.46/0.90 (define @t160 () (_ @t128 @t159)) % 0.46/0.90 (define @t161 () (_ @t132 @t153)) % 0.46/0.90 (define @t162 () (_ @t134 @t161)) % 0.46/0.90 (define @t163 () (@var "V2" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t164 () (@var "X3" tptp.c)) % 0.46/0.90 (define @t165 () (@var "G3" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t166 () (@var "F3" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t167 () (_ (_ (_ tptp.comp_M750374444_m_m_c @t166) @t165) @t164)) % 0.46/0.90 (define @t168 () (_ @t53 @t1)) % 0.46/0.90 (define @t169 () (_ @t166 (_ @t165 @t164))) % 0.46/0.90 (define @t170 () (_ @t47 @t1)) % 0.46/0.90 (define @t171 () (_ @t50 @t170)) % 0.46/0.90 (define @t172 () (@var "G3" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t173 () (@var "F3" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t174 () (_ (_ (_ tptp.comp_m_m_c @t173) @t172) @t164)) % 0.46/0.90 (define @t175 () (_ @t90 @t1)) % 0.46/0.90 (define @t176 () (_ @t173 (_ @t172 @t164))) % 0.46/0.90 (define @t177 () (_ @t86 @t1)) % 0.46/0.90 (define @t178 () (_ @t59 @t177)) % 0.46/0.90 (define @t179 () (@var "G3" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t180 () (@var "F3" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t181 () (_ (_ (_ tptp.comp_c_m_c @t180) @t179) @t164)) % 0.46/0.90 (define @t182 () (_ @t180 (_ @t179 @t164))) % 0.46/0.90 (define @t183 () (_ @t95 @t1)) % 0.46/0.90 (define @t184 () (_ @t92 @t1)) % 0.46/0.90 (define @t185 () (_ @t2 @t184)) % 0.46/0.90 (define @t186 () (@var "X" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t187 () (_ @t63 @t186)) % 0.46/0.90 (define @t188 () (_ @t59 (_ @t56 @t186))) % 0.46/0.90 (define @t189 () (_ @t109 @t141)) % 0.46/0.90 (define @t190 () (@var "B" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t191 () (_ @t128 @t107)) % 0.46/0.90 (define @t192 () (@var "K" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t193 () (_ (_ (_ tptp.comp_M750374444_m_m_c @t104) @t192) @t1)) % 0.46/0.90 (define @t194 () (_ @t104 (_ @t192 @t1))) % 0.46/0.90 (define @t195 () (@var "K" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t196 () (@var "H" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t197 () (_ (_ (_ tptp.comp_m_m_c @t196) @t195) @t1)) % 0.46/0.90 (define @t198 () (_ @t196 (_ @t195 @t1))) % 0.46/0.90 (define @t199 () (@var "K" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t200 () (_ (_ (_ tptp.comp_c_m_c @t71) @t199) @t1)) % 0.46/0.90 (define @t201 () (_ @t199 @t1)) % 0.46/0.90 (define @t202 () (_ @t71 @t201)) % 0.46/0.90 (define @t203 () (@var "K" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t204 () (_ tptp.comp_c1772230468_a_m_c @t26)) % 0.46/0.90 (define @t205 () (@var "Ya" tptp.m)) % 0.46/0.90 (define @t206 () (@var "X" tptp.m)) % 0.46/0.90 (define @t207 () (_ tptp.monomo412532791tT_m_a @t206)) % 0.46/0.90 (define @t208 () (_ tptp.monomo412532791tT_m_a @t37)) % 0.46/0.90 (define @t209 () (@list @t34)) % 0.46/0.90 (define @t210 () (@var "X4" tptp.m)) % 0.46/0.90 (define @t211 () (@var "Y" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t212 () (@var "P" (-> tptp.monomo197243225tT_a_m Bool))) % 0.46/0.90 (define @t213 () (@var "Xa" tptp.m)) % 0.46/0.90 (define @t214 () (_ tptp.monomo624345106et_a_m @t207)) % 0.46/0.90 (define @t215 () (@list @t206)) % 0.46/0.90 (define @t216 () (forall @t215 (= @t214 @t206))) % 0.46/0.90 (define @t217 () (@var "R2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t218 () (@var "L" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t219 () (_ tptp.comp_M750374444_m_m_c @t218)) % 0.46/0.90 (define @t220 () (_ @t219 @t217)) % 0.46/0.90 (define @t221 () (@var "R1" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t222 () (@var "R2" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t223 () (@var "L" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t224 () (_ tptp.comp_c_m_c @t223)) % 0.46/0.90 (define @t225 () (_ @t224 @t222)) % 0.46/0.90 (define @t226 () (@var "R1" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t227 () (@var "R1" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t228 () (@var "R2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t229 () (@var "L" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t230 () (_ tptp.comp_m_m_c @t229)) % 0.46/0.90 (define @t231 () (_ @t230 @t228)) % 0.46/0.90 (define @t232 () (@var "R1" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t233 () (@var "R1" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t234 () (= (_ @t81 @t233) @t223)) % 0.46/0.90 (define @t235 () (_ (_ tptp.comp_c_c_c @t233) @t222)) % 0.46/0.90 (define @t236 () (@var "R1" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t237 () (= (_ @t76 @t236) @t229)) % 0.46/0.90 (define @t238 () (_ (_ tptp.comp_m_m_c @t236) @t228)) % 0.46/0.90 (define @t239 () (@var "R1" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t240 () (= (_ @t60 @t239) @t223)) % 0.46/0.90 (define @t241 () (_ (_ tptp.comp_c_m_c @t239) @t222)) % 0.46/0.90 (define @t242 () (@var "R" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t243 () (@var "L1" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t244 () (_ tptp.comp_M750374444_m_m_c @t243)) % 0.46/0.90 (define @t245 () (_ @t244 @t242)) % 0.46/0.90 (define @t246 () (@var "L2" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t247 () (@var "R" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t248 () (@var "L1" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t249 () (_ tptp.comp_m_m_c @t248)) % 0.46/0.90 (define @t250 () (_ @t249 @t247)) % 0.46/0.90 (define @t251 () (@var "L2" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t252 () (@var "L2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t253 () (@var "R" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t254 () (@var "L1" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t255 () (_ tptp.comp_c_m_c @t254)) % 0.46/0.90 (define @t256 () (_ @t255 @t253)) % 0.46/0.90 (define @t257 () (@var "L2" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t258 () (@var "L2" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t259 () (= (_ (_ tptp.comp_m_m_c @t258) @t71) @t247)) % 0.46/0.90 (define @t260 () (_ (_ tptp.comp_m_m_m @t248) @t258)) % 0.46/0.90 (define @t261 () (@var "L2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t262 () (= (_ (_ tptp.comp_c_m_c @t261) @t46) @t247)) % 0.46/0.90 (define @t263 () (_ @t249 @t261)) % 0.46/0.90 (define @t264 () (@var "L2" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t265 () (= (_ (_ tptp.comp_c_c_c @t264) @t46) @t253)) % 0.46/0.90 (define @t266 () (_ @t255 @t264)) % 0.46/0.90 (define @t267 () (_ @t51 @t242)) % 0.46/0.90 (define @t268 () (_ @t60 @t247)) % 0.46/0.90 (define @t269 () (_ @t81 @t253)) % 0.46/0.90 (define @t270 () (@var "R" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t271 () (@var "G2" (-> tptp.m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t272 () (_ (_ tptp.comp_M750374454_m_m_m @t50) @t271)) % 0.46/0.90 (define @t273 () (_ tptp.comp_m1038691662_a_m_c @t271)) % 0.46/0.90 (define @t274 () (_ @t273 @t71)) % 0.46/0.90 (define @t275 () (_ @t219 @t55)) % 0.46/0.90 (define @t276 () (_ @t224 @t46)) % 0.46/0.90 (define @t277 () (_ @t230 @t71)) % 0.46/0.90 (define @t278 () (= @t77 @t229)) % 0.46/0.90 (define @t279 () (@var "L" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t280 () (@var "F" (-> tptp.m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t281 () (_ tptp.comp_m1038691662_a_m_c @t280)) % 0.46/0.90 (define @t282 () (@var "N" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t283 () (@var "M" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t284 () (@var "N" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t285 () (@var "M" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t286 () (_ @t46 @t1)) % 0.46/0.90 (define @t287 () (@var "N" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t288 () (_ (_ (_ tptp.comp_c_m_c (_ @t60 @t287)) @t46) @t1)) % 0.46/0.90 (define @t289 () (@var "M" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t290 () (_ @t287 @t286)) % 0.46/0.90 (define @t291 () (@var "N" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t292 () (_ (_ (_ tptp.comp_c_m_c (_ @t81 @t291)) @t46) @t1)) % 0.46/0.90 (define @t293 () (@var "M" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t294 () (_ @t291 @t286)) % 0.46/0.90 (define @t295 () (@var "N" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t296 () (_ @t76 @t295)) % 0.46/0.90 (define @t297 () (@var "M" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t298 () (_ @t60 @t297)) % 0.46/0.90 (define @t299 () (_ (_ (_ tptp.comp_c_m_c @t298) @t92) @t1)) % 0.46/0.90 (define @t300 () (_ @t71 @t1)) % 0.46/0.90 (define @t301 () (_ @t297 @t184)) % 0.46/0.90 (define @t302 () (@var "N" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t303 () (_ @t83 @t302)) % 0.46/0.90 (define @t304 () (@var "M" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t305 () (_ @t81 @t304)) % 0.46/0.90 (define @t306 () (_ (_ (_ tptp.comp_c_m_c @t305) @t92) @t1)) % 0.46/0.90 (define @t307 () (_ @t304 @t184)) % 0.46/0.90 (define @t308 () (_ @t104 @t186)) % 0.46/0.90 (define @t309 () (_ @t100 @t186)) % 0.46/0.90 (define @t310 () (@var "V" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t311 () (@var "V" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t312 () (_ tptp.comp_M1944986301tT_a_m @t56)) % 0.46/0.90 (define @t313 () (@var "V" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t314 () (_ @t73 @t2)) % 0.46/0.90 (define @t315 () (_ @t81 @t311)) % 0.46/0.90 (define @t316 () (@var "F" (-> tptp.m tptp.c))) % 0.46/0.90 (define @t317 () (@var "F" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t318 () (@var "V" (-> tptp.monomo197243225tT_a_m tptp.c))) % 0.46/0.90 (define @t319 () (@var "H2" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t320 () (@list @t319)) % 0.46/0.90 (define @t321 () (@var "Y2" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t322 () (@var "X2" tptp.monomo197243225tT_a_m)) % 0.46/0.90 (define @t323 () (_ @t50 @t322)) % 0.46/0.90 (define @t324 () (= @t323 (_ @t50 @t321))) % 0.46/0.90 (define @t325 () (@list @t322 @t321)) % 0.46/0.90 (define @t326 () (@var "H2" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t327 () (@list @t326)) % 0.46/0.90 (define @t328 () (_ @t56 @t321)) % 0.46/0.90 (define @t329 () (@list @t56 @t50)) % 0.46/0.90 (define @t330 () (@var "Y2" tptp.c)) % 0.46/0.90 (define @t331 () (@var "X2" tptp.c)) % 0.46/0.90 (define @t332 () (_ @t2 @t331)) % 0.46/0.90 (define @t333 () (= @t332 (_ @t2 @t330))) % 0.46/0.90 (define @t334 () (_ @t86 @t330)) % 0.46/0.90 (define @t335 () (@list @t331 @t330)) % 0.46/0.90 (define @t336 () (@list @t86 @t2)) % 0.46/0.90 (define @t337 () (@var "H2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t338 () (@list @t337)) % 0.46/0.90 (define @t339 () (_ @t26 @t331)) % 0.46/0.90 (define @t340 () (= (_ @t92 @t331) (_ @t92 @t330))) % 0.46/0.90 (define @t341 () (@var "H2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t342 () (@list @t341)) % 0.46/0.90 (define @t343 () (_ @t47 @t330)) % 0.46/0.90 (define @t344 () (@var "H2" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t345 () (@list @t321)) % 0.46/0.90 (define @t346 () (@list @t322)) % 0.46/0.90 (define @t347 () (@var "Y2" tptp.m)) % 0.46/0.90 (define @t348 () (_ @t72 @t347)) % 0.46/0.90 (define @t349 () (@list @t347)) % 0.46/0.90 (define @t350 () (@list @t331)) % 0.46/0.90 (define @t351 () (@var "H2" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t352 () (@list @t351)) % 0.46/0.90 (define @t353 () (@list @t330)) % 0.46/0.90 (define @t354 () (_ tptp.minus_1646763425cset_c @t9)) % 0.46/0.90 (define @t355 () (_ @t354 @t20)) % 0.46/0.90 (define @t356 () (_ @t18 @t355)) % 0.46/0.90 (define @t357 () (@var "B2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t358 () (_ @t354 @t357)) % 0.46/0.90 (define @t359 () (_ tptp.minus_1646763425cset_c @t358)) % 0.46/0.90 (define @t360 () (@list @t9 @t357)) % 0.46/0.90 (define @t361 () (@list @t9)) % 0.46/0.90 (define @t362 () (_ @t18 @t357)) % 0.46/0.90 (define @t363 () (_ @t354 @t362)) % 0.46/0.90 (define @t364 () (@list @t9 @t15 @t357)) % 0.46/0.90 (define @t365 () (_ @t4 @t357)) % 0.46/0.90 (define @t366 () (_ tptp.ord_le15364698cset_c @t9)) % 0.46/0.90 (define @t367 () (_ @t366 @t365)) % 0.46/0.90 (define @t368 () (_ @t354 @t5)) % 0.46/0.90 (define @t369 () (_ (_ tptp.ord_le15364698cset_c @t368) @t357)) % 0.46/0.90 (define @t370 () (@list @t9 @t1 @t357)) % 0.46/0.90 (define @t371 () (_ tptp.countable_Set_cin_c @t15)) % 0.46/0.90 (define @t372 () (_ @t371 @t9)) % 0.46/0.90 (define @t373 () (@var "X" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t374 () (_ tptp.ord_le15364698cset_c @t373)) % 0.46/0.90 (define @t375 () (@list @t373)) % 0.46/0.90 (define @t376 () (= @t9 @t357)) % 0.46/0.90 (define @t377 () (_ tptp.ord_le15364698cset_c @t357)) % 0.46/0.90 (define @t378 () (_ @t377 @t9)) % 0.46/0.90 (define @t379 () (_ @t366 @t357)) % 0.46/0.90 (define @t380 () (= @t9 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t381 () (_ (_ tptp.countable_Set_cin_c @t331) @t9)) % 0.46/0.90 (define @t382 () (_ tptp.countable_Set_cin_c @t12)) % 0.46/0.90 (define @t383 () (_ @t371 (_ @t16 @t9))) % 0.46/0.90 (define @t384 () (@list @t15 @t13 @t9)) % 0.46/0.90 (define @t385 () (_ @t16 @t357)) % 0.46/0.90 (define @t386 () (_ @t371 @t385)) % 0.46/0.90 (define @t387 () (_ @t371 @t357)) % 0.46/0.90 (define @t388 () (@list @t15 @t357 @t13)) % 0.46/0.90 (define @t389 () (@var "X4" tptp.c)) % 0.46/0.90 (define @t390 () (_ tptp.countable_Set_cin_c @t389)) % 0.46/0.90 (define @t391 () (_ @t390 @t357)) % 0.46/0.90 (define @t392 () (_ @t390 @t9)) % 0.46/0.90 (define @t393 () (@list @t389)) % 0.46/0.90 (define @t394 () (_ tptp.ord_le15364698cset_c tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t395 () (_ @t382 @t357)) % 0.46/0.90 (define @t396 () (not @t395)) % 0.46/0.90 (define @t397 () (_ @t382 @t9)) % 0.46/0.90 (define @t398 () (_ @t382 @t358)) % 0.46/0.90 (define @t399 () (@list @t12 @t9 @t357)) % 0.46/0.90 (define @t400 () (_ tptp.countable_Set_cin_c @t1)) % 0.46/0.90 (define @t401 () (_ @t400 @t357)) % 0.46/0.90 (define @t402 () (@list @t1 @t9 @t357)) % 0.46/0.90 (define @t403 () (_ tptp.minus_1646763425cset_c @t10)) % 0.46/0.90 (define @t404 () (_ @t403 @t357)) % 0.46/0.90 (define @t405 () (=> @t401 (= @t404 @t358))) % 0.46/0.90 (define @t406 () (@list @t1 @t357 @t9)) % 0.46/0.90 (define @t407 () (_ @t400 @t9)) % 0.46/0.90 (define @t408 () (not @t407)) % 0.46/0.90 (define @t409 () (@var "B" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t410 () (@var "A2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t411 () (= @t410 @t409)) % 0.46/0.90 (define @t412 () (_ tptp.ord_le15364698cset_c @t410)) % 0.46/0.90 (define @t413 () (_ @t412 @t409)) % 0.46/0.90 (define @t414 () (_ tptp.ord_le15364698cset_c @t409)) % 0.46/0.90 (define @t415 () (_ @t414 @t410)) % 0.46/0.90 (define @t416 () (@list @t409 @t410)) % 0.46/0.90 (define @t417 () (@var "B3" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t418 () (@var "A4" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t419 () (_ (_ tptp.ord_le15364698cset_c @t418) @t417)) % 0.46/0.90 (define @t420 () (_ (_ tptp.ord_le15364698cset_c @t417) @t418)) % 0.46/0.90 (define @t421 () (@list @t418 @t417)) % 0.46/0.90 (define @t422 () (@var "Z" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t423 () (@var "Y3" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t424 () (lambda (@list @t423 @t422) (= @t423 @t422))) % 0.46/0.90 (define @t425 () (@var "C" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t426 () (_ tptp.ord_le15364698cset_c @t425)) % 0.46/0.90 (define @t427 () (_ @t426 @t409)) % 0.46/0.90 (define @t428 () (@list @t409 @t410 @t425)) % 0.46/0.90 (define @t429 () (@list @t410)) % 0.46/0.90 (define @t430 () (@var "Z2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t431 () (@var "Y" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t432 () (_ tptp.ord_le15364698cset_c @t431)) % 0.46/0.90 (define @t433 () (_ @t432 @t430)) % 0.46/0.90 (define @t434 () (_ @t374 @t431)) % 0.46/0.90 (define @t435 () (@list @t373 @t431 @t430)) % 0.46/0.90 (define @t436 () (@list @t410 @t409)) % 0.46/0.90 (define @t437 () (_ @t412 @t425)) % 0.46/0.90 (define @t438 () (= @t409 @t425)) % 0.46/0.90 (define @t439 () (@list @t410 @t409 @t425)) % 0.46/0.90 (define @t440 () (_ @t414 @t425)) % 0.46/0.90 (define @t441 () (=> @t440 @t437)) % 0.46/0.90 (define @t442 () (= @t373 @t431)) % 0.46/0.90 (define @t443 () (= @t434 @t442)) % 0.46/0.90 (define @t444 () (_ @t432 @t373)) % 0.46/0.90 (define @t445 () (@list @t431 @t373)) % 0.46/0.90 (define @t446 () (_ tptp.countable_Set_cin_c @t23)) % 0.46/0.90 (define @t447 () (@var "A3" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t448 () (@var "B4" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t449 () (_ (_ tptp.ord_le15364698cset_c @t448) @t447)) % 0.46/0.90 (define @t450 () (_ (_ tptp.ord_le15364698cset_c @t447) @t448)) % 0.46/0.90 (define @t451 () (@list @t447 @t448)) % 0.46/0.90 (define @t452 () (@list @t9 @t357 @t1)) % 0.46/0.90 (define @t453 () (@list @t373 @t431)) % 0.46/0.90 (define @t454 () (@var "Q" Bool)) % 0.46/0.90 (define @t455 () (not @t454)) % 0.46/0.90 (define @t456 () (_ tptp.countable_Set_cin_c @t13)) % 0.46/0.90 (define @t457 () (@var "C2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t458 () (_ @t366 @t457)) % 0.46/0.90 (define @t459 () (_ @t377 @t457)) % 0.46/0.90 (define @t460 () (@list @t9 @t357 @t457)) % 0.46/0.90 (define @t461 () (@list @t9 @t357 @t12)) % 0.46/0.90 (define @t462 () (@var "X2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t463 () (@var "Y2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t464 () (_ (_ tptp.ord_le15364698cset_c @t463) @t462)) % 0.46/0.90 (define @t465 () (_ (_ tptp.ord_le15364698cset_c @t462) @t463)) % 0.46/0.90 (define @t466 () (@list @t462 @t463)) % 0.46/0.90 (define @t467 () (=> @t397 @t395)) % 0.46/0.90 (define @t468 () (@var "F" (-> tptp.countable_Set_cset_c tptp.countable_Set_cset_c))) % 0.46/0.90 (define @t469 () (_ @t468 @t410)) % 0.46/0.90 (define @t470 () (@var "Y4" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t471 () (_ @t468 @t470)) % 0.46/0.90 (define @t472 () (@var "X4" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t473 () (_ @t468 @t472)) % 0.46/0.90 (define @t474 () (@list @t472 @t470)) % 0.46/0.90 (define @t475 () (forall @t474 (=> (_ (_ tptp.ord_le15364698cset_c @t472) @t470) (_ (_ tptp.ord_le15364698cset_c @t473) @t471)))) % 0.46/0.90 (define @t476 () (=> @t475 (_ (_ tptp.ord_le15364698cset_c @t469) @t425))) % 0.46/0.90 (define @t477 () (_ @t468 @t409)) % 0.46/0.90 (define @t478 () (= @t477 @t425)) % 0.46/0.90 (define @t479 () (@list @t410 @t409 @t468 @t425)) % 0.46/0.90 (define @t480 () (_ @t468 @t425)) % 0.46/0.90 (define @t481 () (=> @t440 (=> @t475 (_ @t412 @t480)))) % 0.46/0.90 (define @t482 () (= @t410 @t477)) % 0.46/0.90 (define @t483 () (@list @t410 @t468 @t409 @t425)) % 0.46/0.90 (define @t484 () (_ (_ tptp.ord_le15364698cset_c @t477) @t425)) % 0.46/0.90 (define @t485 () (_ @t412 @t477)) % 0.46/0.90 (define @t486 () (@var "Y4" tptp.c)) % 0.46/0.90 (define @t487 () (@var "B5" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t488 () (@list @t487)) % 0.46/0.90 (define @t489 () (not @t401)) % 0.46/0.90 (define @t490 () (= @t410 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t491 () (_ @t412 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t492 () (@var "D2" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t493 () (_ tptp.ord_le15364698cset_c @t358)) % 0.46/0.90 (define @t494 () (_ tptp.minus_1646763425cset_c @t457)) % 0.46/0.90 (define @t495 () (_ tptp.minus_1646763425cset_c @t357)) % 0.46/0.90 (define @t496 () (=> @t408 @t379)) % 0.46/0.90 (define @t497 () (_ tptp.ord_le1587667814cset_c @t9)) % 0.46/0.90 (define @t498 () (_ @t497 @t357)) % 0.46/0.90 (define @t499 () (@var "P" (-> tptp.countable_Set_cset_c Bool))) % 0.46/0.90 (define @t500 () (_ tptp.order_1683649299cset_c @t499)) % 0.46/0.90 (define @t501 () (forall (@list @t470) (=> (_ @t499 @t470) (_ (_ tptp.ord_le15364698cset_c @t470) @t373)))) % 0.46/0.90 (define @t502 () (_ @t499 @t373)) % 0.46/0.90 (define @t503 () (@var "Q" (-> tptp.countable_Set_cset_c Bool))) % 0.46/0.90 (define @t504 () (@var "Y5" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t505 () (_ tptp.ord_le1587667814cset_c @t410)) % 0.46/0.90 (define @t506 () (_ @t505 @t480)) % 0.46/0.90 (define @t507 () (forall @t474 (=> (_ (_ tptp.ord_le1587667814cset_c @t472) @t470) (_ (_ tptp.ord_le1587667814cset_c @t473) @t471)))) % 0.46/0.90 (define @t508 () (_ tptp.ord_le1587667814cset_c @t409)) % 0.46/0.90 (define @t509 () (_ @t508 @t425)) % 0.46/0.90 (define @t510 () (=> @t509 (=> @t507 @t506))) % 0.46/0.90 (define @t511 () (_ (_ tptp.ord_le1587667814cset_c @t469) @t425)) % 0.46/0.90 (define @t512 () (=> @t507 @t511)) % 0.46/0.90 (define @t513 () (_ @t505 @t409)) % 0.46/0.90 (define @t514 () (_ @t505 @t477)) % 0.46/0.90 (define @t515 () (_ (_ tptp.ord_le1587667814cset_c @t477) @t425)) % 0.46/0.90 (define @t516 () (_ @t508 @t410)) % 0.46/0.90 (define @t517 () (_ @t497 @t457)) % 0.46/0.90 (define @t518 () (=> (_ (_ tptp.ord_le1587667814cset_c @t357) @t457) @t517)) % 0.46/0.90 (define @t519 () (_ tptp.ord_le1587667814cset_c @t373)) % 0.46/0.90 (define @t520 () (_ @t519 @t431)) % 0.46/0.90 (define @t521 () (_ tptp.ord_le1587667814cset_c @t431)) % 0.46/0.90 (define @t522 () (_ @t521 @t373)) % 0.46/0.90 (define @t523 () (_ @t519 @t430)) % 0.46/0.90 (define @t524 () (=> (_ @t521 @t430) @t523)) % 0.46/0.90 (define @t525 () (_ @t505 @t425)) % 0.46/0.90 (define @t526 () (=> @t509 @t525)) % 0.46/0.90 (define @t527 () (@var "P" Bool)) % 0.46/0.90 (define @t528 () (_ tptp.ord_le1587667814cset_c @t425)) % 0.46/0.90 (define @t529 () (_ @t528 @t410)) % 0.46/0.90 (define @t530 () (=> (_ @t528 @t409) @t529)) % 0.46/0.90 (define @t531 () (not @t411)) % 0.46/0.90 (define @t532 () (not @t520)) % 0.46/0.90 (define @t533 () (= @t462 @t463)) % 0.46/0.90 (define @t534 () (= @t418 @t417)) % 0.46/0.90 (define @t535 () (not @t534)) % 0.46/0.90 (define @t536 () (@list @t417 @t418)) % 0.46/0.90 (define @t537 () (= @t447 @t448)) % 0.46/0.90 (define @t538 () (@var "Ys" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t539 () (@var "Xs" tptp.countable_Set_cset_c)) % 0.46/0.90 (define @t540 () (@var "B6" tptp.c)) % 0.46/0.90 (define @t541 () (@list @t1 @t23)) % 0.46/0.90 (define @t542 () (_ tptp.f tptp.x)) % 0.46/0.90 (define @t543 () (_ (_ tptp.counta472291938sert_c tptp.x) tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t544 () (= (_ (_ @t30 @t543) tptp.f) @t542)) % 0.46/0.90 (define @t545 () (not @t544)) % 0.46/0.90 (define @t546 () (@var "G" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t547 () (@var "F2" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t548 () (lambda (@list @t547 @t546 @t322) (_ @t547 (_ @t546 @t322)))) % 0.46/0.90 (define @t549 () (@var "G" (-> tptp.monomo197243225tT_a_m tptp.m))) % 0.46/0.90 (define @t550 () (@var "F2" (-> tptp.m tptp.m))) % 0.46/0.90 (define @t551 () (lambda (@list @t550 @t549 @t322) (_ @t550 (_ @t549 @t322)))) % 0.46/0.90 (define @t552 () (@var "G" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t553 () (lambda (@list @t550 @t552 @t331) (_ @t550 (_ @t552 @t331)))) % 0.46/0.90 (define @t554 () (@var "G" (-> tptp.c tptp.c))) % 0.46/0.90 (define @t555 () (_ @t554 @t331)) % 0.46/0.90 (define @t556 () (@var "F2" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t557 () (lambda (@list @t556 @t554 @t331) (_ @t556 @t555))) % 0.46/0.90 (define @t558 () (@var "F2" (-> tptp.c tptp.m))) % 0.46/0.90 (define @t559 () (lambda (@list @t558 @t554 @t331) (_ @t558 @t555))) % 0.46/0.90 (define @t560 () (@var "G" (-> tptp.c tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t561 () (_ @t560 @t331)) % 0.46/0.90 (define @t562 () (lambda (@list @t547 @t560 @t331) (_ @t547 @t561))) % 0.46/0.90 (define @t563 () (@var "F2" (-> tptp.monomo197243225tT_a_m tptp.monomo197243225tT_a_m))) % 0.46/0.90 (define @t564 () (@var "A3" tptp.counta191869203tT_a_m)) % 0.46/0.90 (define @t565 () (@var "Mergec2" (-> tptp.counta191869203tT_a_m (-> tptp.monomo197243225tT_a_m tptp.m) tptp.m))) % 0.46/0.90 (define @t566 () (lambda (@list @t565 @t564 @t563) (_ tptp.monomo412532791tT_m_a (_ (_ @t565 @t564) (_ @t42 @t563))))) % 0.46/0.90 (define @t567 () (@var "Mergec2" (-> tptp.countable_Set_cset_c (-> tptp.c tptp.m) tptp.m))) % 0.46/0.90 (define @t568 () (_ @t567 @t447)) % 0.46/0.90 (define @t569 () (@list @t567 @t447 @t556)) % 0.46/0.90 (define @t570 () (lambda @t569 (_ tptp.monomo412532791tT_m_a (_ @t568 (_ @t27 @t556))))) % 0.46/0.90 (define @t571 () (@var "Y6" (-> Bool tptp.countable_Set_cset_c))) % 0.46/0.90 (define @t572 () (@var "X5" (-> Bool tptp.countable_Set_cset_c))) % 0.46/0.90 (define @t573 () (lambda (@list @t572 @t571) (and (_ (_ tptp.ord_le15364698cset_c (_ @t572 false)) (_ @t571 false)) (_ (_ tptp.ord_le15364698cset_c (_ @t572 true)) (_ @t571 true))))) % 0.46/0.90 (define @t574 () (lambda @t466 (or (_ (_ tptp.ord_le1587667814cset_c @t462) @t463) @t533))) % 0.46/0.90 (define @t575 () (tptp.monomo624345106et_a_m @t33)) % 0.46/0.90 (define @t576 () (tptp.monomo624345106et_a_m @t34)) % 0.46/0.90 (define @t577 () (not @t38)) % 0.46/0.90 (define @t578 () (or @t577 @t35)) % 0.46/0.90 (define @t579 () (tptp.f @t331)) % 0.46/0.90 (define @t580 () (tptp.monomo624345106et_a_m @t579)) % 0.46/0.90 (define @t581 () (_ tptp.f @t331)) % 0.46/0.90 (define @t582 () (_ tptp.monomo624345106et_a_m @t581)) % 0.46/0.90 (define @t583 () (lambda @t350 @t582)) % 0.46/0.90 (define @t584 () (@purify @t583)) % 0.46/0.90 (define @t585 () (_ @t584 @t331)) % 0.46/0.90 (define @t586 () (= @t582 @t585)) % 0.46/0.90 (define @t587 () (_ @t583 @t331)) % 0.46/0.90 (define @t588 () (= @t585 @t587)) % 0.46/0.90 (define @t589 () (forall @t350 @t588)) % 0.46/0.90 (define @t590 () (_ @t2 @t1)) % 0.46/0.90 (define @t591 () (tptp.counta472291938sert_c @t1 tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t592 () (tptp.mergec @t591 @t2)) % 0.46/0.90 (define @t593 () (tptp.monomo412532791tT_m_a @t206)) % 0.46/0.90 (define @t594 () (tptp.monomo624345106et_a_m @t593)) % 0.46/0.90 (define @t595 () (= @t206 @t214)) % 0.46/0.90 (define @t596 () (tptp.counta472291938sert_c tptp.x tptp.bot_bo1320844070cset_c)) % 0.46/0.90 (define @t597 () (tptp.mergec @t596 @t584)) % 0.46/0.90 (define @t598 () (tptp.f tptp.x)) % 0.46/0.90 (define @t599 () (tptp.monomo412532791tT_m_a @t597)) % 0.46/0.90 (define @t600 () (_ tptp.mergec @t543)) % 0.46/0.90 (define @t601 () (_ @t600 @t584)) % 0.46/0.90 (define @t602 () (_ tptp.monomo412532791tT_m_a (_ @t600 @t583))) % 0.46/0.90 (define @t603 () (= @t542 @t602)) % 0.46/0.90 (define @t604 () (lambda @t350 (_ tptp.monomo624345106et_a_m (_ @t556 @t331)))) % 0.46/0.90 (define @t605 () (lambda (@list @t556) (_ tptp.monomo412532791tT_m_a (_ @t600 @t604)))) % 0.46/0.90 (define @t606 () (lambda (@list @t447 @t556) (_ tptp.monomo412532791tT_m_a (_ (_ tptp.mergec @t447) @t604)))) % 0.46/0.90 (define @t607 () (_ (lambda @t569 (_ tptp.monomo412532791tT_m_a (_ @t568 @t604))) tptp.mergec)) % 0.46/0.90 (define @t608 () (= (_ (_ @t607 @t543) tptp.f) @t542)) % 0.46/0.90 (define @t609 () (lambda (@list @t560 @t331) (_ tptp.monomo624345106et_a_m @t561))) % 0.46/0.90 (define @t610 () (= @t599 @t598)) % 0.46/0.90 (define @t611 () (= (tptp.monomo624345106et_a_m @t599) (tptp.monomo624345106et_a_m @t598))) % 0.46/0.90 (define @t612 () (not @t611)) % 0.46/0.90 (define @t613 () (or @t612 @t610)) % 0.46/0.90 (define @t614 () (not @t613)) % 0.46/0.90 (define @t615 () (@list true false)) % 0.46/0.90 (define @t616 () (forall @t39 (or (not (= @t576 @t575)) @t35))) % 0.46/0.90 (assume @p1 @t8) % 0.46/0.90 (assume @p2 (= tptp.monomo463139869_c_m_a tptp.monomo463139869_c_m_a)) % 0.46/0.90 (assume @p3 (forall @t11 (= (_ @t4 @t10) @t10))) % 0.46/0.90 (assume @p4 (forall (@list @t15 @t13 @t12 @t14) (= (= (_ @t18 @t17) (_ (_ tptp.counta472291938sert_c @t12) (_ (_ tptp.counta472291938sert_c @t14) tptp.bot_bo1320844070cset_c))) (or (and (= @t15 @t12) (= @t13 @t14)) (and (= @t15 @t14) (= @t13 @t12)))))) % 0.46/0.90 (assume @p5 (forall (@list @t15 @t13) (=> (= @t20 @t17) @t19))) % 0.46/0.90 (assume @p6 (forall @t22 (not (= @t21 tptp.bot_bo1320844070cset_c)))) % 0.46/0.90 (assume @p7 (forall @t25 (= (_ @t4 (_ @t24 @t9)) (_ @t24 @t10)))) % 0.46/0.90 (assume @p8 (forall @t32 (= (_ tptp.monomo624345106et_a_m @t31) @t29))) % 0.46/0.90 (assume @p9 @t40) % 0.46/0.90 (assume @p10 (forall (@list @t44 @t43 @t41) (= (_ tptp.monomo624345106et_a_m (_ (_ (_ tptp.monomo2081011572_m_m_a @t44) @t43) @t41)) (_ (_ @t44 @t43) (_ @t42 @t41))))) % 0.46/0.90 (assume @p11 (forall (@list @t45 @t9 @t26) (= (_ tptp.monomo624345106et_a_m (_ (_ (_ tptp.monomo463139869_c_m_a @t45) @t9) @t26)) (_ (_ @t45 @t9) @t28)))) % 0.46/0.90 (assume @p12 (forall @t32 (= @t31 (_ tptp.monomo412532791tT_m_a @t29)))) % 0.46/0.90 (assume @p13 (forall (@list @t50 @t47 @t46) (= @t54 @t52))) % 0.46/0.90 (assume @p14 (forall (@list @t59 @t56 @t55) (= @t64 @t61))) % 0.46/0.90 (assume @p15 (forall (@list @t50 @t65 @t55) (= @t70 @t67))) % 0.46/0.90 (assume @p16 (forall (@list @t59 @t72 @t71) (= @t78 @t75))) % 0.46/0.90 (assume @p17 (forall (@list @t2 @t79 @t71) (= @t85 @t82))) % 0.46/0.90 (assume @p18 (forall (@list @t59 @t86 @t46) (= @t91 @t89))) % 0.46/0.90 (assume @p19 (forall (@list @t2 @t92 @t46) (= @t96 @t94))) % 0.46/0.90 (assume @p20 (forall (@list @t59 @t86 @t97) (= @t99 (_ @t62 @t98)))) % 0.46/0.90 (assume @p21 (forall (@list @t2 @t100 @t55) (= @t103 (_ @t81 @t101)))) % 0.46/0.90 (assume @p22 (forall (@list @t59 @t72 @t104) (= (_ (_ tptp.comp_m263856566tT_a_m @t77) @t104) @t106))) % 0.46/0.90 (assume @p23 (forall (@list @t112 @t111 @t109 @t108 @t107) (=> @t116 (= @t113 @t110)))) % 0.46/0.90 (assume @p24 (forall (@list @t121 @t120 @t118 @t117 @t107) (=> @t125 (= @t122 @t119)))) % 0.46/0.90 (assume @p25 (forall (@list @t121 @t120 @t128 @t126 @t107) (=> @t131 (= @t122 @t129)))) % 0.46/0.90 (assume @p26 (forall (@list @t134 @t132 @t118 @t117 @t107) (=> @t137 (= @t135 @t119)))) % 0.46/0.90 (assume @p27 (forall (@list @t134 @t132 @t128 @t126 @t107) (=> @t138 (= @t135 @t129)))) % 0.46/0.90 (assume @p28 (forall (@list @t112 @t111 @t118 @t117 @t107) (=> @t139 (= @t113 @t119)))) % 0.46/0.90 (assume @p29 (forall (@list @t112 @t111 @t128 @t126 @t107) (=> @t140 (= @t113 @t129)))) % 0.46/0.90 (assume @p30 (forall (@list @t121 @t143 @t118 @t142 @t141) (=> @t146 (= @t144 (_ @t118 (_ @t142 @t141)))))) % 0.46/0.90 (assume @p31 (forall (@list @t121 @t120 @t109 @t108 @t107) (=> @t147 (= @t122 @t110)))) % 0.46/0.90 (assume @p32 (forall (@list @t149 @t132 @t148 @t126 @t107) (=> @t152 (= @t150 (_ @t148 @t127))))) % 0.46/0.90 (assume @p33 (forall (@list @t112 @t111 @t109 @t108) (=> @t116 (forall @t156 (= @t155 @t154))))) % 0.46/0.90 (assume @p34 (forall (@list @t121 @t120 @t118 @t117) (=> @t125 (forall @t156 (= @t158 @t157))))) % 0.46/0.90 (assume @p35 (forall (@list @t121 @t120 @t128 @t126) (=> @t131 (forall @t156 (= @t158 @t160))))) % 0.46/0.90 (assume @p36 (forall (@list @t134 @t132 @t118 @t117) (=> @t137 (forall @t156 (= @t162 @t157))))) % 0.46/0.90 (assume @p37 (forall (@list @t134 @t132 @t128 @t126) (=> @t138 (forall @t156 (= @t162 @t160))))) % 0.46/0.90 (assume @p38 (forall (@list @t112 @t111 @t118 @t117) (=> @t139 (forall @t156 (= @t155 @t157))))) % 0.46/0.90 (assume @p39 (forall (@list @t112 @t111 @t128 @t126) (=> @t140 (forall @t156 (= @t155 @t160))))) % 0.46/0.90 (assume @p40 (forall (@list @t121 @t143 @t118 @t142) (=> @t146 (forall (@list @t163) (= (_ @t121 (_ @t143 @t163)) (_ @t118 (_ @t142 @t163))))))) % 0.46/0.90 (assume @p41 (forall (@list @t121 @t120 @t109 @t108) (=> @t147 (forall @t156 (= @t158 @t154))))) % 0.46/0.90 (assume @p42 (forall (@list @t149 @t132 @t148 @t126) (=> @t152 (forall @t156 (= (_ @t149 @t161) (_ @t148 @t159)))))) % 0.46/0.90 (assume @p43 (forall (@list @t50 @t47 @t1 @t166 @t165 @t164) (=> (= @t171 @t169) (= @t168 @t167)))) % 0.46/0.90 (assume @p44 (forall (@list @t59 @t86 @t1 @t173 @t172 @t164) (=> (= @t178 @t176) (= @t175 @t174)))) % 0.46/0.90 (assume @p45 (forall (@list @t59 @t86 @t1 @t180 @t179 @t164) (=> (= @t178 @t182) (= @t175 @t181)))) % 0.46/0.90 (assume @p46 (forall (@list @t2 @t92 @t1 @t173 @t172 @t164) (=> (= @t185 @t176) (= @t183 @t174)))) % 0.46/0.90 (assume @p47 (forall (@list @t2 @t92 @t1 @t180 @t179 @t164) (=> (= @t185 @t182) (= @t183 @t181)))) % 0.46/0.90 (assume @p48 (forall (@list @t50 @t47 @t1 @t173 @t172 @t164) (=> (= @t171 @t176) (= @t168 @t174)))) % 0.46/0.90 (assume @p49 (forall (@list @t50 @t47 @t1 @t180 @t179 @t164) (=> (= @t171 @t182) (= @t168 @t181)))) % 0.46/0.90 (assume @p50 (forall (@list @t59 @t56 @t186 @t173 @t172 @t164) (=> (= @t188 @t176) (= @t187 @t174)))) % 0.46/0.90 (assume @p51 (forall (@list @t59 @t56 @t186 @t180 @t179 @t164) (=> (= @t188 @t182) (= @t187 @t181)))) % 0.46/0.90 (assume @p52 (forall (@list @t59 @t86 @t1 @t166 @t165 @t164) (=> (= @t178 @t169) (= @t175 @t167)))) % 0.46/0.90 (assume @p53 (forall (@list @t112 @t190 @t109 @t141) (=> (= (_ (_ tptp.comp_M1944986301tT_a_m @t112) @t190) @t109) (= (_ @t112 (_ @t190 @t141)) @t189)))) % 0.46/0.90 (assume @p54 (forall (@list @t121 @t143 @t109 @t141) (=> (= @t145 @t109) (= @t144 @t189)))) % 0.46/0.90 (assume @p55 (forall (@list @t121 @t120 @t128 @t107) (=> (= @t124 @t128) (= @t122 @t191)))) % 0.46/0.90 (assume @p56 (forall (@list @t149 @t132 @t148 @t107) (=> (= @t151 @t148) (= @t150 (_ @t148 @t107))))) % 0.46/0.90 (assume @p57 (forall (@list @t134 @t132 @t128 @t107) (=> (= @t136 @t128) (= @t135 @t191)))) % 0.46/0.90 (assume @p58 (forall (@list @t112 @t111 @t128 @t107) (=> (= @t115 @t128) (= @t113 @t191)))) % 0.46/0.90 (assume @p59 (forall (@list @t50 @t47 @t1 @t104 @t192) (=> (= @t171 @t194) (= @t168 @t193)))) % 0.46/0.90 (assume @p60 (forall (@list @t59 @t86 @t1 @t196 @t195) (=> (= @t178 @t198) (= @t175 @t197)))) % 0.46/0.90 (assume @p61 (forall (@list @t59 @t86 @t1 @t71 @t199) (=> (= @t178 @t202) (= @t175 @t200)))) % 0.46/0.90 (assume @p62 (forall (@list @t2 @t92 @t1 @t196 @t195) (=> (= @t185 @t198) (= @t183 @t197)))) % 0.46/0.90 (assume @p63 (forall (@list @t2 @t92 @t1 @t71 @t199) (=> (= @t185 @t202) (= @t183 @t200)))) % 0.46/0.90 (assume @p64 (forall (@list @t50 @t47 @t1 @t196 @t195) (=> (= @t171 @t198) (= @t168 @t197)))) % 0.46/0.90 (assume @p65 (forall (@list @t50 @t47 @t1 @t71 @t199) (=> (= @t171 @t202) (= @t168 @t200)))) % 0.46/0.90 (assume @p66 (forall (@list @t59 @t56 @t186 @t196 @t203) (=> (= @t188 (_ @t196 (_ @t203 @t186))) (= @t187 (_ (_ (_ tptp.comp_m263856566tT_a_m @t196) @t203) @t186))))) % 0.46/0.90 (assume @p67 (forall (@list @t59 @t86 @t1 @t104 @t192) (=> (= @t178 @t194) (= @t175 @t193)))) % 0.46/0.90 (assume @p68 (forall (@list @t26 @t92 @t1 @t55 @t199) (=> (= (_ @t26 @t184) (_ @t55 @t201)) (= (_ (_ @t204 @t92) @t1) (_ (_ (_ tptp.comp_c1772230468_a_m_c @t55) @t199) @t1))))) % 0.46/0.90 (assume @p69 (forall (@list @t206 @t205) (= (= @t207 (_ tptp.monomo412532791tT_m_a @t205)) (= @t206 @t205)))) % 0.46/0.90 (assume @p70 (forall @t209 (= @t208 @t34))) % 0.46/0.90 (assume @p71 (forall (@list @t211) (not (forall (@list @t210) (not (= @t211 (_ tptp.monomo412532791tT_m_a @t210))))))) % 0.46/0.90 (assume @p72 (forall (@list @t212 @t34) (=> (forall (@list @t213) (_ @t212 (_ tptp.monomo412532791tT_m_a @t213))) (_ @t212 @t34)))) % 0.46/0.90 (assume @p73 (forall @t209 (= @t34 @t208))) % 0.46/0.90 (assume @p74 @t216) % 0.46/0.90 (assume @p75 (forall (@list @t47 @t46 @t221 @t217 @t50 @t218) (=> (= @t49 (_ (_ tptp.comp_M864375327_a_m_c @t221) @t217)) (=> (= (_ @t68 @t221) @t218) (= @t54 @t220))))) % 0.46/0.90 (assume @p76 (forall (@list @t65 @t55 @t226 @t222 @t50 @t223) (=> (= @t66 (_ (_ tptp.comp_c1772230468_a_m_c @t226) @t222)) (=> (= (_ @t51 @t226) @t223) (= @t70 @t225))))) % 0.46/0.90 (assume @p77 (forall (@list @t56 @t55 @t227 @t217 @t59 @t218) (=> (= @t58 (_ (_ tptp.comp_M750374444_m_m_c @t227) @t217)) (=> (= (_ @t62 @t227) @t218) (= @t64 @t220))))) % 0.46/0.90 (assume @p78 (forall (@list @t92 @t46 @t232 @t228 @t2 @t229) (=> (= @t93 (_ (_ tptp.comp_m_c_c @t232) @t228)) (=> (= (_ @t83 @t232) @t229) (= @t96 @t231))))) % 0.46/0.90 (assume @p79 (forall (@list @t79 @t71 @t233 @t222 @t2 @t223) (=> (= @t80 @t235) (=> @t234 (= @t85 @t225))))) % 0.46/0.90 (assume @p80 (forall (@list @t92 @t46 @t233 @t222 @t2 @t223) (=> (= @t93 @t235) (=> @t234 (= @t96 @t225))))) % 0.46/0.90 (assume @p81 (forall (@list @t72 @t71 @t236 @t228 @t59 @t229) (=> (= @t74 @t238) (=> @t237 (= @t78 @t231))))) % 0.46/0.90 (assume @p82 (forall (@list @t72 @t71 @t239 @t222 @t59 @t223) (=> (= @t74 @t241) (=> @t240 (= @t78 @t225))))) % 0.46/0.90 (assume @p83 (forall (@list @t86 @t46 @t236 @t228 @t59 @t229) (=> (= @t88 @t238) (=> @t237 (= @t91 @t231))))) % 0.46/0.90 (assume @p84 (forall (@list @t86 @t46 @t239 @t222 @t59 @t223) (=> (= @t88 @t241) (=> @t240 (= @t91 @t225))))) % 0.46/0.90 (assume @p85 (forall (@list @t59 @t56 @t243 @t246 @t55 @t242) (=> (= @t63 (_ (_ tptp.comp_M1944986301tT_a_m @t243) @t246)) (=> (= (_ (_ tptp.comp_M864375327_a_m_c @t246) @t55) @t242) (= @t61 @t245))))) % 0.46/0.90 (assume @p86 (forall (@list @t50 @t65 @t248 @t251 @t55 @t247) (=> (= @t69 (_ (_ tptp.comp_m263856566tT_a_m @t248) @t251)) (=> (= (_ (_ tptp.comp_M750374444_m_m_c @t251) @t55) @t247) (= @t67 @t250))))) % 0.46/0.90 (assume @p87 (forall (@list @t50 @t47 @t243 @t252 @t46 @t242) (=> (= @t53 (_ @t244 @t252)) (=> (= (_ (_ tptp.comp_c1772230468_a_m_c @t252) @t46) @t242) (= @t52 @t245))))) % 0.46/0.90 (assume @p88 (forall (@list @t59 @t72 @t254 @t257 @t71 @t253) (=> (= @t77 (_ (_ tptp.comp_c_m_m @t254) @t257)) (=> (= (_ (_ tptp.comp_m_c_c @t257) @t71) @t253) (= @t75 @t256))))) % 0.46/0.90 (assume @p89 (forall (@list @t59 @t72 @t248 @t258 @t71 @t247) (=> (= @t77 @t260) (=> @t259 (= @t75 @t250))))) % 0.46/0.90 (assume @p90 (forall (@list @t2 @t79 @t248 @t258 @t71 @t247) (=> (= @t84 @t260) (=> @t259 (= @t82 @t250))))) % 0.46/0.90 (assume @p91 (forall (@list @t59 @t86 @t248 @t261 @t46 @t247) (=> (= @t90 @t263) (=> @t262 (= @t89 @t250))))) % 0.46/0.90 (assume @p92 (forall (@list @t59 @t86 @t254 @t264 @t46 @t253) (=> (= @t90 @t266) (=> @t265 (= @t89 @t256))))) % 0.46/0.90 (assume @p93 (forall (@list @t2 @t92 @t248 @t261 @t46 @t247) (=> (= @t95 @t263) (=> @t262 (= @t94 @t250))))) % 0.46/0.90 (assume @p94 (forall (@list @t2 @t92 @t254 @t264 @t46 @t253) (=> (= @t95 @t266) (=> @t265 (= @t94 @t256))))) % 0.46/0.90 (assume @p95 (forall (@list @t47 @t46 @t242 @t50) (=> (= @t49 @t242) (= @t54 @t267)))) % 0.46/0.90 (assume @p96 (forall (@list @t56 @t55 @t247 @t59) (=> (= @t58 @t247) (= @t64 @t268)))) % 0.46/0.90 (assume @p97 (forall (@list @t65 @t55 @t242 @t50) (=> (= @t66 @t242) (= @t70 @t267)))) % 0.46/0.90 (assume @p98 (forall (@list @t79 @t71 @t253 @t2) (=> (= @t80 @t253) (= @t85 @t269)))) % 0.46/0.90 (assume @p99 (forall (@list @t92 @t46 @t253 @t2) (=> (= @t93 @t253) (= @t96 @t269)))) % 0.46/0.90 (assume @p100 (forall (@list @t72 @t71 @t247 @t59) (=> (= @t74 @t247) (= @t78 @t268)))) % 0.46/0.90 (assume @p101 (forall (@list @t86 @t46 @t247 @t59) (=> (= @t88 @t247) (= @t91 @t268)))) % 0.46/0.90 (assume @p102 (forall (@list @t86 @t97 @t270 @t59) (=> (= @t98 @t270) (= @t99 (_ @t62 @t270))))) % 0.46/0.90 (assume @p103 (forall (@list @t100 @t55 @t253 @t2) (=> (= @t101 @t253) (= @t103 @t269)))) % 0.46/0.90 (assume @p104 (forall (@list @t271 @t71 @t242 @t50) (=> (= @t274 @t242) (= (_ (_ tptp.comp_m_m_c @t272) @t71) @t267)))) % 0.46/0.90 (assume @p105 (forall (@list @t59 @t56 @t218 @t55) (=> (= @t63 @t218) (= @t61 @t275)))) % 0.46/0.90 (assume @p106 (forall (@list @t50 @t47 @t223 @t46) (=> (= @t53 @t223) (= @t52 @t276)))) % 0.46/0.90 (assume @p107 (forall (@list @t50 @t65 @t218 @t55) (=> (= @t69 @t218) (= @t67 @t275)))) % 0.46/0.90 (assume @p108 (forall (@list @t59 @t72 @t229 @t71) (=> @t278 (= @t75 @t277)))) % 0.46/0.90 (assume @p109 (forall (@list @t2 @t79 @t229 @t71) (=> (= @t84 @t229) (= @t82 @t277)))) % 0.46/0.90 (assume @p110 (forall (@list @t59 @t86 @t223 @t46) (=> (= @t90 @t223) (= @t89 @t276)))) % 0.46/0.90 (assume @p111 (forall (@list @t2 @t92 @t223 @t46) (=> (= @t95 @t223) (= @t94 @t276)))) % 0.46/0.90 (assume @p112 (forall (@list @t280 @t86 @t279 @t46) (=> (= (_ @t281 @t86) @t279) (= (_ @t281 @t88) (_ (_ tptp.comp_c1772230468_a_m_c @t279) @t46))))) % 0.46/0.90 (assume @p113 (forall (@list @t50 @t271 @t229 @t71) (=> (= @t272 @t229) (= (_ @t51 @t274) @t277)))) % 0.46/0.90 (assume @p114 (forall (@list @t59 @t72 @t229 @t104) (=> @t278 (= @t106 (_ (_ tptp.comp_m263856566tT_a_m @t229) @t104))))) % 0.46/0.90 (assume @p115 (forall (@list @t283 @t92 @t1 @t282 @t55 @t50) (=> (= (_ @t283 @t184) (_ @t282 (_ @t55 @t1))) (= (_ (_ (_ tptp.comp_c_m_c (_ @t51 @t283)) @t92) @t1) (_ (_ (_ tptp.comp_M750374444_m_m_c (_ @t68 @t282)) @t55) @t1))))) % 0.46/0.90 (assume @p116 (forall (@list @t285 @t47 @t1 @t284 @t46 @t50) (=> (= (_ @t285 @t170) (_ @t284 @t286)) (= (_ (_ (_ tptp.comp_M750374444_m_m_c (_ @t68 @t285)) @t47) @t1) (_ (_ (_ tptp.comp_c_m_c (_ @t51 @t284)) @t46) @t1))))) % 0.46/0.90 (assume @p117 (forall (@list @t289 @t86 @t1 @t287 @t46 @t59) (=> (= (_ @t289 @t177) @t290) (= (_ (_ (_ tptp.comp_m_m_c (_ @t76 @t289)) @t86) @t1) @t288)))) % 0.46/0.90 (assume @p118 (forall (@list @t293 @t86 @t1 @t291 @t46 @t2) (=> (= (_ @t293 @t177) @t294) (= (_ (_ (_ tptp.comp_m_m_c (_ @t83 @t293)) @t86) @t1) @t292)))) % 0.46/0.90 (assume @p119 (forall (@list @t297 @t92 @t1 @t295 @t71 @t59) (=> (= @t301 (_ @t295 @t300)) (= @t299 (_ (_ (_ tptp.comp_m_m_c @t296) @t71) @t1))))) % 0.46/0.90 (assume @p120 (forall (@list @t297 @t92 @t1 @t287 @t46 @t59) (=> (= @t301 @t290) (= @t299 @t288)))) % 0.46/0.90 (assume @p121 (forall (@list @t304 @t92 @t1 @t302 @t71 @t2) (=> (= @t307 (_ @t302 @t300)) (= @t306 (_ (_ (_ tptp.comp_m_m_c @t303) @t71) @t1))))) % 0.46/0.90 (assume @p122 (forall (@list @t304 @t92 @t1 @t291 @t46 @t2) (=> (= @t307 @t294) (= @t306 @t292)))) % 0.46/0.90 (assume @p123 (forall (@list @t297 @t100 @t186 @t295 @t104 @t59) (=> (= (_ @t297 @t309) (_ @t295 @t308)) (= (_ (_ (_ tptp.comp_c997395372tT_a_m @t298) @t100) @t186) (_ (_ (_ tptp.comp_m263856566tT_a_m @t296) @t104) @t186))))) % 0.46/0.90 (assume @p124 (forall (@list @t304 @t100 @t186 @t302 @t104 @t2) (=> (= (_ @t304 @t309) (_ @t302 @t308)) (= (_ (_ (_ tptp.comp_c997395372tT_a_m @t305) @t100) @t186) (_ (_ (_ tptp.comp_m263856566tT_a_m @t303) @t104) @t186))))) % 0.46/0.90 (assume @p125 (forall (@list @t72 @t50 @t310) (= (_ @t73 (_ @t51 @t310)) (_ (_ tptp.comp_M750374444_m_m_c (_ @t105 @t50)) @t310)))) % 0.46/0.90 (assume @p126 (forall (@list @t56 @t26 @t311) (= (_ @t57 (_ @t204 @t311)) (_ (_ tptp.comp_c_m_c (_ @t57 @t26)) @t311)))) % 0.46/0.90 (assume @p127 (forall (@list @t56 @t41 @t310) (= (_ @t57 (_ (_ tptp.comp_M864375327_a_m_c @t41) @t310)) (_ (_ tptp.comp_M750374444_m_m_c (_ @t312 @t41)) @t310)))) % 0.46/0.90 (assume @p128 (forall (@list @t72 @t59 @t313) (= (_ @t73 (_ @t60 @t313)) (_ (_ tptp.comp_m_m_c (_ (_ tptp.comp_m_m_m @t72) @t59)) @t313)))) % 0.46/0.90 (assume @p129 (forall (@list @t72 @t2 @t311) (= (_ @t73 @t315) (_ (_ tptp.comp_c_m_c @t314) @t311)))) % 0.46/0.90 (assume @p130 (forall (@list @t86 @t316 @t313) (= (_ @t87 (_ (_ tptp.comp_m_c_c @t316) @t313)) (_ (_ tptp.comp_m_m_c (_ (_ tptp.comp_c_m_m @t86) @t316)) @t313)))) % 0.46/0.90 (assume @p131 (forall (@list @t86 @t317 @t311) (= (_ @t87 (_ (_ tptp.comp_c_c_c @t317) @t311)) (_ (_ tptp.comp_c_m_c (_ @t87 @t317)) @t311)))) % 0.46/0.90 (assume @p132 (forall (@list @t271 @t2 @t311) (= (_ @t273 @t315) (_ (_ tptp.comp_c1772230468_a_m_c (_ @t273 @t2)) @t311)))) % 0.46/0.90 (assume @p133 (forall (@list @t56 @t280 @t313) (= (_ @t57 (_ @t281 @t313)) (_ (_ tptp.comp_m_m_c (_ (_ tptp.comp_M750374454_m_m_m @t56) @t280)) @t313)))) % 0.46/0.90 (assume @p134 (forall (@list @t72 @t2 @t318) (= (_ @t105 (_ @t102 @t318)) (_ (_ tptp.comp_c997395372tT_a_m @t314) @t318)))) % 0.46/0.90 (assume @p135 (forall (@list @t65 @t50) (= (forall @t325 (=> (= (_ @t65 @t322) (_ @t65 @t321)) @t324)) (exists @t320 (= @t50 (_ (_ tptp.comp_M1944986301tT_a_m @t319) @t65)))))) % 0.46/0.90 (assume @p136 (forall @t329 (= (forall @t325 (=> (= (_ @t56 @t322) @t328) @t324)) (exists @t327 (= @t50 (_ (_ tptp.comp_m263856566tT_a_m @t326) @t56)))))) % 0.46/0.90 (assume @p137 (forall @t336 (= (forall @t335 (=> (= (_ @t86 @t331) @t334) @t333)) (exists @t327 (= @t2 (_ (_ tptp.comp_m_m_c @t326) @t86)))))) % 0.46/0.90 (assume @p138 (forall (@list @t92 @t26) (= (forall @t335 (=> @t340 (= @t339 (_ @t26 @t330)))) (exists @t338 (= @t26 (_ (_ tptp.comp_c1772230468_a_m_c @t337) @t92)))))) % 0.46/0.90 (assume @p139 (forall (@list @t92 @t2) (= (forall @t335 (=> @t340 @t333)) (exists @t342 (= @t2 (_ (_ tptp.comp_c_m_c @t341) @t92)))))) % 0.46/0.90 (assume @p140 (forall (@list @t47 @t2) (= (forall @t335 (=> (= (_ @t47 @t331) @t343) @t333)) (exists @t320 (= @t2 (_ (_ tptp.comp_M750374444_m_m_c @t319) @t47)))))) % 0.46/0.90 (assume @p141 (forall @t329 (= (forall @t346 (exists @t345 (= @t328 @t323))) (exists (@list @t344) (= @t50 (_ @t312 @t344)))))) % 0.46/0.90 (assume @p142 (forall (@list @t72 @t50) (= (forall @t346 (exists @t349 (= @t348 @t323))) (exists @t320 (= @t50 (_ @t105 @t319)))))) % 0.46/0.90 (assume @p143 (forall (@list @t72 @t2) (= (forall @t350 (exists @t349 (= @t348 @t332))) (exists @t342 (= @t2 (_ @t73 @t341)))))) % 0.46/0.90 (assume @p144 (forall (@list @t47 @t26) (= (forall @t350 (exists @t353 (= @t343 @t339))) (exists @t352 (= @t26 (_ @t48 @t351)))))) % 0.46/0.90 (assume @p145 (forall @t336 (= (forall @t350 (exists @t353 (= @t334 @t332))) (exists @t352 (= @t2 (_ @t87 @t351)))))) % 0.46/0.90 (assume @p146 (forall (@list @t56 @t2) (= (forall @t350 (exists @t345 (= @t328 @t332))) (exists @t338 (= @t2 (_ @t57 @t337)))))) % 0.46/0.90 (assume @p147 (forall @t22 (= @t356 @t21))) % 0.46/0.90 (assume @p148 (forall @t360 (= (_ @t359 @t357) @t358))) % 0.46/0.90 (assume @p149 (forall @t361 (= (_ @t354 @t9) tptp.bot_bo1320844070cset_c))) % 0.46/0.90 (assume @p150 (forall @t361 (= (_ @t354 tptp.bot_bo1320844070cset_c) @t9))) % 0.46/0.90 (assume @p151 (forall @t361 (= (_ (_ tptp.minus_1646763425cset_c tptp.bot_bo1320844070cset_c) @t9) tptp.bot_bo1320844070cset_c))) % 0.46/0.90 (assume @p152 (forall @t364 (= @t363 (_ @t359 @t20)))) % 0.46/0.90 (assume @p153 (forall @t364 (= @t363 (_ (_ tptp.minus_1646763425cset_c @t355) @t357)))) % 0.46/0.90 (assume @p154 (forall @t370 (=> @t369 @t367))) % 0.46/0.90 (assume @p155 (forall @t22 (=> @t372 (= @t356 @t9)))) % 0.46/0.90 (assume @p156 (forall @t375 (_ @t374 @t373))) % 0.46/0.90 (assume @p157 (forall @t360 (=> @t379 (=> @t378 @t376)))) % 0.46/0.90 (assume @p158 (forall @t361 (= (forall @t350 (not @t381)) @t380))) % 0.46/0.90 (assume @p159 (forall (@list @t12) (not (_ @t382 tptp.bot_bo1320844070cset_c)))) % 0.46/0.90 (assume @p160 (forall @t384 (= @t383 (or @t19 @t372)))) % 0.46/0.90 (assume @p161 (forall @t388 (=> (=> (not @t387) @t19) @t386))) % 0.46/0.90 (assume @p162 (forall @t360 (=> (forall @t393 (=> @t392 @t391)) @t379))) % 0.46/0.90 (assume @p163 (forall @t375 (_ @t394 @t373))) % 0.46/0.90 (assume @p164 (forall @t361 (= (_ @t366 tptp.bot_bo1320844070cset_c) @t380))) % 0.46/0.90 (assume @p165 (forall @t399 (= @t398 (and @t397 @t396)))) % 0.46/0.90 (assume @p166 (forall @t399 (=> @t397 (=> @t396 @t398)))) % 0.46/0.90 (assume @p167 (forall @t402 (= (_ (_ tptp.ord_le15364698cset_c @t10) @t357) (and @t401 @t379)))) % 0.46/0.90 (assume @p168 (forall @t406 @t405)) % 0.46/0.90 (assume @p169 (forall @t402 (=> @t408 (= @t367 @t379)))) % 0.46/0.90 (assume @p170 (forall @t416 (=> @t415 (=> @t413 @t411)))) % 0.46/0.90 (assume @p171 (= @t424 (lambda @t421 (and @t420 @t419)))) % 0.46/0.90 (assume @p172 (forall @t428 (=> @t415 (=> @t427 (_ @t426 @t410))))) % 0.46/0.90 (assume @p173 (forall @t429 (_ @t412 @t410))) % 0.46/0.90 (assume @p174 (forall @t435 (=> @t434 (=> @t433 (_ @t374 @t430))))) % 0.46/0.90 (assume @p175 (forall @t436 (=> @t413 (=> @t415 @t411)))) % 0.46/0.90 (assume @p176 (forall @t439 (=> @t413 (=> @t438 @t437)))) % 0.46/0.90 (assume @p177 (forall @t439 (=> @t411 @t441))) % 0.46/0.90 (assume @p178 (= @t424 (lambda @t421 (and @t419 @t420)))) % 0.46/0.90 (assume @p179 (forall @t445 (=> @t444 @t443))) % 0.46/0.90 (assume @p180 (forall @t25 (=> (= @t1 @t23) (= @t407 (_ @t446 @t9))))) % 0.46/0.90 (assume @p181 (= @t424 (lambda @t451 (and @t450 @t449)))) % 0.46/0.90 (assume @p182 (forall @t439 (=> @t413 @t441))) % 0.46/0.90 (assume @p183 (forall @t452 (=> @t376 (= @t407 @t401)))) % 0.46/0.90 (assume @p184 (forall @t453 (=> @t442 @t434))) % 0.46/0.90 (assume @p185 (forall (@list @t15 @t454 @t373 @t431) (= (_ @t371 (_ (_ (_ tptp.if_Cou1542198912cset_c @t454) @t373) @t431)) (and (=> @t454 (_ @t371 @t373)) (=> @t455 (_ @t371 @t431)))))) % 0.46/0.90 (assume @p186 (forall (@list @t454 @t1 @t23 @t409) (= (_ (_ tptp.countable_Set_cin_c (_ (_ (_ tptp.if_c @t454) @t1) @t23)) @t409) (and (=> @t454 (_ @t400 @t409)) (=> @t455 (_ @t446 @t409)))))) % 0.46/0.90 (assume @p187 (forall @t384 (=> @t19 (=> (_ @t456 @t9) @t372)))) % 0.46/0.90 (assume @p188 (forall @t460 (=> @t379 (=> @t459 @t458)))) % 0.46/0.90 (assume @p189 (forall @t361 (_ @t366 @t9))) % 0.46/0.90 (assume @p190 (forall @t360 (=> @t376 @t378))) % 0.46/0.90 (assume @p191 (forall @t360 (=> @t376 @t379))) % 0.46/0.90 (assume @p192 (forall @t461 (=> @t376 (=> (=> @t397 @t396) (not (=> (not @t397) @t395)))))) % 0.46/0.90 (assume @p193 (forall @t453 (=> @t434 (=> @t444 @t442)))) % 0.46/0.90 (assume @p194 (forall @t360 (=> @t376 (not (=> @t379 (not @t378)))))) % 0.46/0.90 (assume @p195 (= @t424 (lambda @t466 (and @t465 @t464)))) % 0.46/0.90 (assume @p196 (forall @t461 (=> @t379 @t467))) % 0.46/0.90 (assume @p197 (forall @t360 (=> (forall @t393 (= @t392 @t391)) @t376))) % 0.46/0.90 (assume @p198 (forall @t452 (=> @t379 (=> @t407 @t401)))) % 0.46/0.90 (assume @p199 (forall @t479 (=> @t413 (=> @t478 @t476)))) % 0.46/0.90 (assume @p200 (forall @t483 (=> @t482 @t481))) % 0.46/0.90 (assume @p201 (forall @t479 (=> @t413 (=> @t484 @t476)))) % 0.46/0.90 (assume @p202 (forall @t483 (=> @t485 @t481))) % 0.46/0.90 (assume @p203 (forall @t361 (=> (forall (@list @t486) (not (_ (_ tptp.countable_Set_cin_c @t486) @t9))) @t380))) % 0.46/0.90 (assume @p204 (forall (@list @t9 @t15) (=> @t380 (not @t372)))) % 0.46/0.90 (assume @p205 (forall @t361 (= (exists @t350 @t381) (not @t380)))) % 0.46/0.90 (assume @p206 (forall (@list @t15) (not (_ @t371 tptp.bot_bo1320844070cset_c)))) % 0.46/0.90 (assume @p207 (forall @t22 (=> @t372 (exists @t488 (and (= @t9 (_ @t18 @t487)) (not (_ @t371 @t487))))))) % 0.46/0.90 (assume @p208 (forall @t22 (=> @t372 (= @t21 @t9)))) % 0.46/0.90 (assume @p209 (forall @t402 (=> @t408 (=> @t489 (= (= @t10 @t365) @t376))))) % 0.46/0.90 (assume @p210 (forall @t11 (=> @t407 (not (forall @t488 (=> (= @t9 (_ @t4 @t487)) (_ @t400 @t487))))))) % 0.46/0.90 (assume @p211 (forall @t388 (=> @t387 @t386))) % 0.46/0.90 (assume @p212 (forall (@list @t15 @t357) (_ @t371 @t362))) % 0.46/0.90 (assume @p213 (forall @t384 (=> @t383 (=> (not @t19) @t372)))) % 0.46/0.90 (assume @p214 (forall @t429 (=> @t491 @t490))) % 0.46/0.90 (assume @p215 (forall @t429 (= @t491 @t490))) % 0.46/0.90 (assume @p216 (forall @t429 (_ @t394 @t410))) % 0.46/0.90 (assume @p217 (forall @t399 (=> @t398 @t396))) % 0.46/0.90 (assume @p218 (forall @t399 (=> @t398 @t397))) % 0.46/0.90 (assume @p219 (forall @t399 (=> @t398 (not @t467)))) % 0.46/0.90 (assume @p220 (forall (@list @t9 @t357 @t13) (=> @t379 (_ @t366 @t385)))) % 0.46/0.90 (assume @p221 (forall (@list @t357 @t15) (_ @t377 @t362))) % 0.46/0.90 (assume @p222 (forall (@list @t457 @t492 @t15) (=> (_ (_ tptp.ord_le15364698cset_c @t457) @t492) (_ (_ tptp.ord_le15364698cset_c (_ @t18 @t457)) (_ @t18 @t492))))) % 0.46/0.90 (assume @p223 (forall @t360 (_ @t493 @t9))) % 0.46/0.90 (assume @p224 (forall @t460 (=> @t379 (=> @t459 (= (_ @t495 (_ @t494 @t9)) @t9))))) % 0.46/0.90 (assume @p225 (forall (@list @t9 @t457 @t492 @t357) (=> @t458 (=> (_ (_ tptp.ord_le15364698cset_c @t492) @t357) (_ @t493 (_ @t494 @t492)))))) % 0.46/0.90 (assume @p226 (forall @t370 (= @t367 (and (=> @t407 @t369) @t496)))) % 0.46/0.90 (assume @p227 (forall (@list @t13 @t15) (= (_ @t456 @t20) (= @t13 @t15)))) % 0.46/0.90 (assume @p228 (forall @t406 (and @t405 (=> @t489 (= @t404 (_ @t4 @t358)))))) % 0.46/0.90 (assume @p229 (forall (@list @t9 @t1) (=> (_ @t366 @t5) (or @t380 (= @t9 @t5))))) % 0.46/0.90 (assume @p230 (forall @t11 (=> @t408 (= (_ @t403 @t5) @t9)))) % 0.46/0.90 (assume @p231 (forall @t370 (= (_ @t497 @t365) (and (=> @t401 @t498) (=> @t489 (and (=> @t407 (_ (_ tptp.ord_le1587667814cset_c @t368) @t357)) @t496)))))) % 0.46/0.90 (assume @p232 (forall (@list @t499 @t373) (=> @t502 (=> @t501 (= @t500 @t373))))) % 0.46/0.90 (assume @p233 (forall (@list @t499 @t373 @t503) (=> @t502 (=> @t501 (=> (forall (@list @t472) (=> (_ @t499 @t472) (=> (forall (@list @t504) (=> (_ @t499 @t504) (_ (_ tptp.ord_le15364698cset_c @t504) @t472))) (_ @t503 @t472)))) (_ @t503 @t500)))))) % 0.46/0.90 (assume @p234 (forall @t483 (=> @t482 @t510))) % 0.46/0.90 (assume @p235 (forall @t479 (=> @t513 (=> @t478 @t512)))) % 0.46/0.90 (assume @p236 (forall @t483 (=> @t514 @t510))) % 0.46/0.90 (assume @p237 (forall @t479 (=> @t513 (=> @t515 @t512)))) % 0.46/0.90 (assume @p238 (forall @t436 (=> @t513 (not @t516)))) % 0.46/0.90 (assume @p239 (forall @t460 (=> @t498 @t518))) % 0.46/0.90 (assume @p240 (forall @t453 (=> @t520 (not @t442)))) % 0.46/0.90 (assume @p241 (forall @t453 (=> @t520 (not @t522)))) % 0.46/0.90 (assume @p242 (forall @t435 (=> @t520 @t524))) % 0.46/0.90 (assume @p243 (forall @t375 (not (_ @t519 @t373)))) % 0.46/0.90 (assume @p244 (forall @t439 (=> @t411 @t526))) % 0.46/0.90 (assume @p245 (forall @t439 (=> @t513 (=> @t438 @t525)))) % 0.46/0.90 (assume @p246 (forall @t416 (=> @t516 (not @t513)))) % 0.46/0.90 (assume @p247 (forall @t453 (=> @t520 (not (= @t431 @t373))))) % 0.46/0.90 (assume @p248 (forall (@list @t373 @t431 @t527) (=> @t520 (=> @t522 @t527)))) % 0.46/0.90 (assume @p249 (forall @t429 (not (_ @t505 @t410)))) % 0.46/0.90 (assume @p250 (forall @t439 (=> @t513 @t526))) % 0.46/0.90 (assume @p251 (forall @t428 (=> @t516 @t530))) % 0.46/0.90 (assume @p252 (forall @t436 (=> @t513 @t531))) % 0.46/0.90 (assume @p253 (forall @t416 (=> @t516 @t531))) % 0.46/0.90 (assume @p254 (forall @t445 (=> @t444 @t532))) % 0.46/0.90 (assume @p255 (= tptp.ord_le1587667814cset_c (lambda @t466 (and @t465 (not @t533))))) % 0.46/0.90 (assume @p256 (forall @t483 (=> @t485 @t510))) % 0.46/0.90 (assume @p257 (forall @t479 (=> @t413 (=> @t515 (=> @t475 @t511))))) % 0.46/0.90 (assume @p258 (forall @t483 (=> @t514 (=> @t440 (=> @t475 @t506))))) % 0.46/0.90 (assume @p259 (forall @t479 (=> @t513 (=> @t484 @t512)))) % 0.46/0.90 (assume @p260 (forall @t436 (=> @t413 (=> @t531 @t513)))) % 0.46/0.90 (assume @p261 (forall @t453 (=> @t532 @t443))) % 0.46/0.90 (assume @p262 (forall @t453 (=> @t434 (= @t532 @t442)))) % 0.46/0.90 (assume @p263 (forall @t453 (=> @t520 @t434))) % 0.46/0.90 (assume @p264 (forall @t435 (=> @t434 @t524))) % 0.46/0.90 (assume @p265 (forall @t435 (=> @t520 (=> @t433 @t523)))) % 0.46/0.90 (assume @p266 (forall @t453 (=> @t434 (or @t520 @t442)))) % 0.46/0.90 (assume @p267 (= tptp.ord_le1587667814cset_c (lambda @t466 (and @t465 (not @t464))))) % 0.46/0.90 (assume @p268 (forall @t439 (=> @t413 @t526))) % 0.46/0.90 (assume @p269 (forall @t439 (=> @t513 (=> @t440 @t525)))) % 0.46/0.90 (assume @p270 (= tptp.ord_le15364698cset_c (lambda @t421 (or (_ (_ tptp.ord_le1587667814cset_c @t418) @t417) @t534)))) % 0.46/0.90 (assume @p271 (= tptp.ord_le1587667814cset_c (lambda @t421 (and @t419 @t535)))) % 0.46/0.90 (assume @p272 (forall @t428 (=> @t415 @t530))) % 0.46/0.90 (assume @p273 (forall @t428 (=> @t516 (=> @t427 @t529)))) % 0.46/0.90 (assume @p274 (forall @t436 (=> @t513 @t413))) % 0.46/0.90 (assume @p275 (= tptp.ord_le15364698cset_c (lambda @t536 (or (_ (_ tptp.ord_le1587667814cset_c @t417) @t418) @t534)))) % 0.46/0.90 (assume @p276 (= tptp.ord_le1587667814cset_c (lambda @t536 (and @t420 @t535)))) % 0.46/0.90 (assume @p277 (forall @t416 (=> @t516 @t415))) % 0.46/0.90 (assume @p278 (forall @t436 (=> @t531 (=> @t413 @t513)))) % 0.46/0.90 (assume @p279 (forall @t429 (not (_ @t505 tptp.bot_bo1320844070cset_c)))) % 0.46/0.90 (assume @p280 (forall @t429 (= (not @t490) (_ (_ tptp.ord_le1587667814cset_c tptp.bot_bo1320844070cset_c) @t410)))) % 0.46/0.90 (assume @p281 (forall @t461 (=> @t498 @t467))) % 0.46/0.90 (assume @p282 (forall @t361 (not (_ @t497 tptp.bot_bo1320844070cset_c)))) % 0.46/0.90 (assume @p283 (= tptp.ord_le1587667814cset_c (lambda @t451 (and @t450 (not @t537))))) % 0.46/0.90 (assume @p284 (= tptp.ord_le1587667814cset_c (lambda (@list @t539 @t538) (and (_ (_ tptp.ord_le15364698cset_c @t539) @t538) (not (= @t539 @t538)))))) % 0.46/0.90 (assume @p285 (forall @t360 (=> @t498 @t379))) % 0.46/0.90 (assume @p286 (forall @t460 (=> @t498 (=> @t459 @t517)))) % 0.46/0.90 (assume @p287 (forall @t460 (=> @t379 @t518))) % 0.46/0.90 (assume @p288 (= tptp.ord_le1587667814cset_c (lambda @t451 (and @t450 (not @t449))))) % 0.46/0.90 (assume @p289 (= tptp.ord_le15364698cset_c (lambda @t451 (or (_ (_ tptp.ord_le1587667814cset_c @t447) @t448) @t537)))) % 0.46/0.90 (assume @p290 (forall @t360 (=> @t498 (exists (@list @t540) (_ (_ tptp.countable_Set_cin_c @t540) (_ @t495 @t9)))))) % 0.46/0.90 (assume @p291 (forall @t541 (= (_ (_ (_ tptp.if_c false) @t1) @t23) @t23))) % 0.46/0.90 (assume @p292 (forall @t541 (= (_ (_ (_ tptp.if_c true) @t1) @t23) @t1))) % 0.46/0.90 (assume @p293 (forall (@list @t527) (or (= @t527 true) (= @t527 false)))) % 0.46/0.90 (assume @p294 (forall @t453 (= (_ (_ (_ tptp.if_Cou1542198912cset_c false) @t373) @t431) @t431))) % 0.46/0.90 (assume @p295 (forall @t453 (= (_ (_ (_ tptp.if_Cou1542198912cset_c true) @t373) @t431) @t373))) % 0.46/0.90 (assume @p296 @t545) % 0.46/0.90 (assume @p297 true) % 0.46/0.90 (step @p298 (= tptp.comp_M1944986301tT_a_m @t548) :rule refl :args (@t548)) % 0.46/0.90 (step @p299 (= tptp.comp_m263856566tT_a_m @t551) :rule refl :args (@t551)) % 0.46/0.90 (step @p300 (= tptp.comp_m_m_c @t553) :rule refl :args (@t553)) % 0.46/0.90 (step @p301 (= tptp.comp_c1772230468_a_m_c @t557) :rule refl :args (@t557)) % 0.46/0.90 (step @p302 (= tptp.comp_c_m_c @t559) :rule refl :args (@t559)) % 0.46/0.90 (step @p303 (= tptp.comp_M750374444_m_m_c @t562) :rule refl :args (@t562)) % 0.46/0.90 (step @p304 (= tptp.monomo2081011572_m_m_a @t566) :rule refl :args (@t566)) % 0.46/0.90 (step @p305 (= tptp.monomo463139869_c_m_a @t570) :rule refl :args (@t570)) % 0.46/0.90 (step @p306 (= tptp.ord_le1376176871cset_c @t573) :rule refl :args (@t573)) % 0.46/0.90 (step @p307 (= tptp.ord_le15364698cset_c @t574) :rule refl :args (@t574)) % 0.46/0.90 (step @p308 :rule refl :args (@t35)) % 0.46/0.90 (step @p309 :rule refl :args (@t575)) % 0.46/0.90 (step @p310 :rule refl :args (@t36)) % 0.46/0.90 (step @p311 :rule cong :premises (@p310 @p309) :args ((= @t36 @t575))) % 0.46/0.90 (step @p312 :rule symm :premises (@p311)) % 0.46/0.90 (step @p313 :rule eq_resolve :premises (@p310 @p312)) % 0.46/0.90 (step @p314 :rule refl :args (@t576)) % 0.46/0.90 (step @p315 :rule refl :args (@t37)) % 0.46/0.90 (step @p316 :rule cong :premises (@p315 @p314) :args ((= @t37 @t576))) % 0.46/0.90 (step @p317 :rule symm :premises (@p316)) % 0.46/0.90 (step @p318 :rule eq_resolve :premises (@p315 @p317)) % 0.46/0.90 (step @p319 :rule cong :premises (@p318 @p313) :args (@t38)) % 0.46/0.90 (step @p320 :rule cong :premises (@p319) :args (@t577)) % 0.46/0.90 (step @p321 :rule nary_cong :premises (@p320 @p308) :args (@t578)) % 0.46/0.90 (step @p322 :rule cong :premises (@p321) :args ((forall @t39 @t578))) % 0.46/0.90 (step @p323 :rule bool-impl-elim :args (@t38 @t35)) % 0.46/0.90 (step @p324 :rule cong :premises (@p323) :args (@t40)) % 0.46/0.90 (step @p325 :rule trans :premises (@p324 @p322)) % 0.46/0.90 (step @p326 :rule eq_resolve :premises (@p9 @p325)) % 0.46/0.90 (step @p327 :rule eq-symm :args (@t580 @t585)) % 0.46/0.90 (step @p328 :rule cong :premises (@p327) :args ((forall @t350 (= @t580 @t585)))) % 0.46/0.90 (step @p329 :rule refl :args (@t585)) % 0.46/0.90 (step @p330 :rule refl :args ((tptp.monomo624345106et_a_m @t581))) % 0.46/0.90 (step @p331 :rule refl :args (@t579)) % 0.46/0.90 (step @p332 :rule cong :premises (@p331) :args (@t580)) % 0.46/0.90 (step @p333 :rule trans :premises (@p332 @p330)) % 0.46/0.90 (step @p334 :rule refl :args (tptp.monomo624345106et_a_m)) % 0.46/0.90 (step @p335 :rule ho_cong :premises (@p334 @p331)) % 0.46/0.90 (step @p336 :rule cong :premises (@p335 @p333) :args ((= (_ tptp.monomo624345106et_a_m @t579) @t580))) % 0.46/0.90 (step @p337 :rule symm :premises (@p336)) % 0.46/0.90 (step @p338 :rule refl :args (@t582)) % 0.46/0.90 (step @p339 :rule eq_resolve :premises (@p338 @p337)) % 0.46/0.90 (step @p340 :rule refl :args (@t581)) % 0.46/0.90 (step @p341 :rule cong :premises (@p340 @p331) :args ((= @t581 @t579))) % 0.46/0.90 (step @p342 :rule symm :premises (@p341)) % 0.46/0.90 (step @p343 :rule eq_resolve :premises (@p340 @p342)) % 0.46/0.90 (step @p344 :rule ho_cong :premises (@p334 @p343)) % 0.46/0.90 (step @p345 :rule trans :premises (@p344 @p339)) % 0.46/0.90 (step @p346 :rule cong :premises (@p345 @p329) :args (@t586)) % 0.46/0.90 (step @p347 :rule cong :premises (@p346) :args ((forall @t350 @t586))) % 0.46/0.90 (step @p348 :rule trans :premises (@p347 @p328)) % 0.46/0.90 (step @p349 :rule eq-symm :args (@t585 @t582)) % 0.46/0.90 (step @p350 :rule beta-reduce :args ((= @t587 @t582))) % 0.46/0.90 (step @p351 :rule refl :args (@t585)) % 0.46/0.90 (step @p352 :rule cong :premises (@p351 @p350) :args (@t588)) % 0.46/0.90 (step @p353 :rule trans :premises (@p352 @p349)) % 0.46/0.90 (step @p354 :rule cong :premises (@p353) :args (@t589)) % 0.46/0.90 (step @p355 :rule trans :premises (@p354 @p348)) % 0.46/0.90 (step @p356 :rule quant-unused-vars :args ((= (forall @t350 true) true))) % 0.46/0.90 (step @p357 :rule eq-refl :args (@t587)) % 0.46/0.90 (step @p358 :rule cong :premises (@p357) :args ((forall @t350 (= @t587 @t587)))) % 0.46/0.90 (step @p359 :rule trans :premises (@p358 @p356)) % 0.46/0.90 (step @p360 :rule refl :args (@t587)) % 0.46/0.90 (step @p361 :rule refl :args (@t331)) % 0.46/0.90 (step @p362 :rule skolem_intro :args (@t584)) % 0.46/0.90 (step @p363 :rule ho_cong :premises (@p362 @p361)) % 0.46/0.90 (step @p364 :rule cong :premises (@p363 @p360) :args (@t588)) % 0.46/0.90 (step @p365 :rule cong :premises (@p364) :args (@t589)) % 0.46/0.90 (step @p366 :rule trans :premises (@p365 @p359)) % 0.46/0.90 (step @p367 :rule true_elim :premises (@p366)) % 0.46/0.90 (step @p368 :rule eq_resolve :premises (@p367 @p355)) % 0.46/0.90 (step @p369 :rule instantiate :premises (@p368) :args ((@list tptp.x))) % 0.46/0.90 (step @p370 :rule refl :args (@t590)) % 0.46/0.90 (step @p371 :rule refl :args (@t3)) % 0.46/0.90 (step @p372 :rule cong :premises (@p371 @p370) :args ((= @t3 @t590))) % 0.46/0.90 (step @p373 :rule symm :premises (@p372)) % 0.46/0.90 (step @p374 :rule eq_resolve :premises (@p371 @p373)) % 0.46/0.90 (step @p375 :rule refl :args ((tptp.mergec @t5 @t2))) % 0.46/0.90 (step @p376 :rule refl :args (@t2)) % 0.46/0.90 (step @p377 :rule refl :args (@t591)) % 0.46/0.90 (step @p378 :rule cong :premises (@p377 @p376) :args (@t592)) % 0.46/0.90 (step @p379 :rule trans :premises (@p378 @p375)) % 0.46/0.90 (step @p380 :rule refl :args (tptp.mergec)) % 0.46/0.90 (step @p381 :rule ho_cong :premises (@p380 @p377)) % 0.46/0.90 (step @p382 :rule ho_cong :premises (@p381 @p376)) % 0.46/0.90 (step @p383 :rule cong :premises (@p382 @p379) :args ((= (_ (_ tptp.mergec @t591) @t2) @t592))) % 0.46/0.90 (step @p384 :rule symm :premises (@p383)) % 0.46/0.90 (step @p385 :rule refl :args (@t6)) % 0.46/0.90 (step @p386 :rule eq_resolve :premises (@p385 @p384)) % 0.46/0.90 (step @p387 :rule refl :args (@t5)) % 0.46/0.90 (step @p388 :rule cong :premises (@p387 @p377) :args ((= @t5 @t591))) % 0.46/0.90 (step @p389 :rule symm :premises (@p388)) % 0.46/0.90 (step @p390 :rule eq_resolve :premises (@p387 @p389)) % 0.46/0.90 (step @p391 :rule ho_cong :premises (@p380 @p390)) % 0.46/0.90 (step @p392 :rule ho_cong :premises (@p391 @p376)) % 0.46/0.90 (step @p393 :rule trans :premises (@p392 @p386)) % 0.46/0.90 (step @p394 :rule cong :premises (@p393 @p374) :args (@t7)) % 0.46/0.90 (step @p395 :rule cong :premises (@p394) :args (@t8)) % 0.46/0.90 (step @p396 :rule eq_resolve :premises (@p1 @p395)) % 0.46/0.90 (step @p397 :rule instantiate :premises (@p396) :args ((@list tptp.x @t584))) % 0.46/0.90 (step @p398 :rule refl :args ((tptp.monomo624345106et_a_m @t207))) % 0.46/0.90 (step @p399 :rule refl :args (@t593)) % 0.46/0.90 (step @p400 :rule cong :premises (@p399) :args (@t594)) % 0.46/0.90 (step @p401 :rule trans :premises (@p400 @p398)) % 0.46/0.90 (step @p402 :rule ho_cong :premises (@p334 @p399)) % 0.46/0.90 (step @p403 :rule cong :premises (@p402 @p401) :args ((= (_ tptp.monomo624345106et_a_m @t593) @t594))) % 0.46/0.90 (step @p404 :rule symm :premises (@p403)) % 0.46/0.90 (step @p405 :rule refl :args (@t214)) % 0.46/0.90 (step @p406 :rule eq_resolve :premises (@p405 @p404)) % 0.46/0.90 (step @p407 :rule refl :args (@t207)) % 0.46/0.90 (step @p408 :rule cong :premises (@p407 @p399) :args ((= @t207 @t593))) % 0.46/0.90 (step @p409 :rule symm :premises (@p408)) % 0.46/0.90 (step @p410 :rule eq_resolve :premises (@p407 @p409)) % 0.46/0.90 (step @p411 :rule ho_cong :premises (@p334 @p410)) % 0.46/0.90 (step @p412 :rule trans :premises (@p411 @p406)) % 0.46/0.90 (step @p413 :rule refl :args (@t206)) % 0.46/0.90 (step @p414 :rule cong :premises (@p413 @p412) :args (@t595)) % 0.46/0.90 (step @p415 :rule cong :premises (@p414) :args ((forall @t215 @t595))) % 0.46/0.90 (step @p416 :rule eq-symm :args (@t214 @t206)) % 0.46/0.90 (step @p417 :rule cong :premises (@p416) :args (@t216)) % 0.46/0.90 (step @p418 :rule trans :premises (@p417 @p415)) % 0.46/0.90 (step @p419 :rule eq_resolve :premises (@p74 @p418)) % 0.46/0.90 (step @p420 :rule instantiate :premises (@p419) :args ((@list @t597))) % 0.46/0.90 (step @p421 :rule symm :premises (@p420)) % 0.46/0.90 (step @p422 :rule trans :premises (@p421 @p397 @p369)) % 0.46/0.90 (step @p423 :rule eq-symm :args (@t598 @t599)) % 0.46/0.90 (step @p424 :rule refl :args ((tptp.monomo412532791tT_m_a @t601))) % 0.46/0.90 (step @p425 :rule refl :args ((tptp.mergec @t543 @t584))) % 0.46/0.90 (step @p426 :rule refl :args (@t584)) % 0.46/0.90 (step @p427 :rule refl :args (@t596)) % 0.46/0.90 (step @p428 :rule cong :premises (@p427 @p426) :args (@t597)) % 0.46/0.90 (step @p429 :rule trans :premises (@p428 @p425)) % 0.46/0.90 (step @p430 :rule cong :premises (@p429) :args (@t599)) % 0.46/0.90 (step @p431 :rule trans :premises (@p430 @p424)) % 0.46/0.90 (step @p432 :rule refl :args (tptp.monomo412532791tT_m_a)) % 0.46/0.90 (step @p433 :rule ho_cong :premises (@p432 @p429)) % 0.46/0.90 (step @p434 :rule cong :premises (@p433 @p431) :args ((= (_ tptp.monomo412532791tT_m_a @t597) @t599))) % 0.46/0.90 (step @p435 :rule symm :premises (@p434)) % 0.46/0.90 (step @p436 :rule refl :args ((_ tptp.monomo412532791tT_m_a @t601))) % 0.46/0.90 (step @p437 :rule eq_resolve :premises (@p436 @p435)) % 0.46/0.90 (step @p438 :rule ho_cong :premises (@p380 @p427)) % 0.46/0.90 (step @p439 :rule ho_cong :premises (@p438 @p426)) % 0.46/0.90 (step @p440 :rule cong :premises (@p439 @p429) :args ((= (_ (_ tptp.mergec @t596) @t584) @t597))) % 0.46/0.90 (step @p441 :rule symm :premises (@p440)) % 0.46/0.90 (step @p442 :rule refl :args (@t601)) % 0.46/0.90 (step @p443 :rule eq_resolve :premises (@p442 @p441)) % 0.46/0.90 (step @p444 :rule eq-refl :args (@t583)) % 0.46/0.90 (step @p445 :rule refl :args (@t583)) % 0.46/0.90 (step @p446 :rule cong :premises (@p445 @p362) :args ((= @t583 @t584))) % 0.46/0.90 (step @p447 :rule trans :premises (@p446 @p444)) % 0.46/0.90 (step @p448 :rule true_elim :premises (@p447)) % 0.46/0.90 (step @p449 :rule refl :args (@t543)) % 0.46/0.90 (step @p450 :rule cong :premises (@p449 @p427) :args ((= @t543 @t596))) % 0.46/0.90 (step @p451 :rule symm :premises (@p450)) % 0.46/0.90 (step @p452 :rule eq_resolve :premises (@p449 @p451)) % 0.46/0.90 (step @p453 :rule refl :args (tptp.mergec)) % 0.46/0.90 (step @p454 :rule ho_cong :premises (@p453 @p452)) % 0.46/0.90 (step @p455 :rule ho_cong :premises (@p454 @p448)) % 0.46/0.90 (step @p456 :rule trans :premises (@p455 @p443)) % 0.46/0.90 (step @p457 :rule refl :args (tptp.monomo412532791tT_m_a)) % 0.46/0.90 (step @p458 :rule ho_cong :premises (@p457 @p456)) % 0.46/0.90 (step @p459 :rule trans :premises (@p458 @p437)) % 0.46/0.90 (step @p460 :rule refl :args (@t598)) % 0.46/0.90 (step @p461 :rule refl :args (@t542)) % 0.46/0.90 (step @p462 :rule cong :premises (@p461 @p460) :args ((= @t542 @t598))) % 0.46/0.90 (step @p463 :rule symm :premises (@p462)) % 0.46/0.90 (step @p464 :rule eq_resolve :premises (@p461 @p463)) % 0.46/0.90 (step @p465 :rule cong :premises (@p464 @p459) :args (@t603)) % 0.46/0.90 (step @p466 :rule trans :premises (@p465 @p423)) % 0.46/0.90 (step @p467 :rule cong :premises (@p466) :args ((not @t603))) % 0.46/0.90 (step @p468 :rule eq-symm :args (@t602 @t542)) % 0.46/0.90 (step @p469 :rule refl :args (@t542)) % 0.46/0.90 (step @p470 :rule beta-reduce :args ((= (_ @t605 tptp.f) @t602))) % 0.46/0.90 (step @p471 :rule refl :args (tptp.f)) % 0.46/0.90 (step @p472 :rule beta-reduce :args ((= (_ @t606 @t543) @t605))) % 0.46/0.90 (step @p473 :rule refl :args (@t543)) % 0.46/0.90 (step @p474 :rule beta-reduce :args ((= @t607 @t606))) % 0.46/0.90 (step @p475 :rule ho_cong :premises (@p474 @p473)) % 0.46/0.90 (step @p476 :rule trans :premises (@p475 @p472)) % 0.46/0.90 (step @p477 :rule ho_cong :premises (@p476 @p471)) % 0.46/0.90 (step @p478 :rule trans :premises (@p477 @p470)) % 0.46/0.90 (step @p479 :rule cong :premises (@p478 @p469) :args (@t608)) % 0.46/0.90 (step @p480 :rule trans :premises (@p479 @p468)) % 0.46/0.90 (step @p481 :rule cong :premises (@p480) :args ((not @t608))) % 0.46/0.90 (step @p482 :rule beta-reduce :args ((= (_ @t609 @t556) @t604))) % 0.46/0.90 (step @p483 :rule refl :args (@t556)) % 0.46/0.90 (step @p484 :rule beta-reduce :args ((= (_ @t562 tptp.monomo624345106et_a_m) @t609))) % 0.46/0.90 (step @p485 :rule ho_cong :premises (@p484 @p483)) % 0.46/0.90 (step @p486 :rule trans :premises (@p485 @p482)) % 0.46/0.90 (step @p487 :rule refl :args (@t568)) % 0.46/0.90 (step @p488 :rule ho_cong :premises (@p487 @p486)) % 0.46/0.90 (step @p489 :rule ho_cong :premises (@p457 @p488)) % 0.46/0.90 (step @p490 :rule refl :args (tptp.monomo624345106et_a_m)) % 0.46/0.90 (step @p491 :rule ho_cong :premises (@p303 @p490)) % 0.46/0.90 (step @p492 :rule ho_cong :premises (@p491 @p483)) % 0.46/0.90 (step @p493 :rule ho_cong :premises (@p487 @p492)) % 0.46/0.90 (step @p494 :rule ho_cong :premises (@p457 @p493)) % 0.46/0.90 (step @p495 :rule trans :premises (@p494 @p489)) % 0.46/0.90 (step @p496 :rule cong :premises (@p495) :args (@t570)) % 0.46/0.90 (step @p497 :rule trans :premises (@p305 @p496)) % 0.46/0.90 (step @p498 :rule ho_cong :premises (@p497 @p453)) % 0.46/0.90 (step @p499 :rule ho_cong :premises (@p498 @p473)) % 0.46/0.90 (step @p500 :rule ho_cong :premises (@p499 @p471)) % 0.46/0.90 (step @p501 :rule cong :premises (@p500 @p469) :args (@t544)) % 0.46/0.90 (step @p502 :rule cong :premises (@p501) :args (@t545)) % 0.46/0.90 (step @p503 :rule trans :premises (@p502 @p481)) % 0.46/0.90 (step @p504 :rule trans :premises (@p503 @p467)) % 0.46/0.90 (step @p505 :rule eq_resolve :premises (@p296 @p504)) % 0.46/0.90 (step @p506 :rule cnf_or_pos :args (@t613)) % 0.46/0.90 (step @p507 :rule reordering :premises (@p506) :args ((or @t610 @t612 @t614))) % 0.46/0.90 (step @p508 :rule chain_m_resolution :premises (@p507 @p505 @p422) :args (@t614 @t615 (@list @t610 @t611))) % 0.46/0.90 (assume-push @p515 @t616) % 0.46/0.90 (step @p510 :rule instantiate :premises (@p326) :args ((@list @t599 @t598))) % 0.46/0.90 (step-pop @p516 :rule scope :premises (@p510)) % 0.46/0.90 (step @p511 :rule process_scope :premises (@p516) :args (@t613)) % 0.46/0.90 (step @p513 :rule implies_elim :premises (@p511)) % 0.46/0.90 (step @p514 false :rule chain_m_resolution :premises (@p513 @p508 @p326) :args (false @t615 (@list @t613 @t616))) % 0.46/0.90 ) % 0.46/0.90 % SZS output end Proof % 0.46/0.90 % cvc5 exiting %------------------------------------------------------------------------------