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