%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP032^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:24:51 AM UTC 2026 % Result : Theorem 0.43s 1.01s % Output : Proof 0.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP032^1 : TPTP v9.2.1. Released v7.5.0. % 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.14/0.34 % Computer : n015.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Jun 2 04:11:04 EDT 2026 % 0.14/0.34 % CPUTime : % 0.39/0.58 %----Proving TH0 % 0.43/1.01 --- 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.43/1.01 % SZS status Theorem % 0.43/1.01 % SZS output start Proof % 0.43/1.01 ( % 0.43/1.01 (declare-sort tptp.a 0) % 0.43/1.01 (declare-sort tptp.binary1439146945Tree_a 0) % 0.43/1.01 (declare-sort tptp.int 0) % 0.43/1.01 (declare-sort tptp.set_a 0) % 0.43/1.01 (declare-const tptp.binary945792244etOf_a (-> tptp.binary1439146945Tree_a tptp.set_a)) % 0.43/1.01 (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool)) % 0.43/1.01 (declare-const tptp.binary1721989714Tree_a (-> (-> tptp.a tptp.int) tptp.binary1439146945Tree_a Bool)) % 0.43/1.01 (declare-const tptp.bot_bot_o Bool) % 0.43/1.01 (declare-const tptp.minus_minus_o (-> Bool Bool Bool)) % 0.43/1.01 (declare-const tptp.sup_sup_o (-> Bool Bool Bool)) % 0.43/1.01 (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a)) % 0.43/1.01 (declare-const tptp.sup_sup_int (-> tptp.int tptp.int tptp.int)) % 0.43/1.01 (declare-const tptp.bot_bot_set_a tptp.set_a) % 0.43/1.01 (declare-const tptp.the_a (-> (-> tptp.a Bool) tptp.a)) % 0.43/1.01 (declare-const tptp.binary256242811Tree_a (-> tptp.binary1439146945Tree_a tptp.set_a)) % 0.43/1.01 (declare-const tptp.minus_minus_int (-> tptp.int tptp.int tptp.int)) % 0.43/1.01 (declare-const tptp.binary1452917696Tree_a (-> (-> tptp.a Bool) tptp.binary1439146945Tree_a Bool)) % 0.43/1.01 (declare-const tptp.t1 tptp.binary1439146945Tree_a) % 0.43/1.01 (declare-const tptp.binary476621312_Tip_a tptp.binary1439146945Tree_a) % 0.43/1.01 (declare-const tptp.w tptp.a) % 0.43/1.01 (declare-const tptp.x tptp.a) % 0.43/1.01 (declare-const tptp.t2 tptp.binary1439146945Tree_a) % 0.43/1.01 (declare-const tptp.binary717961607le_T_a (-> tptp.binary1439146945Tree_a tptp.a tptp.binary1439146945Tree_a tptp.binary1439146945Tree_a)) % 0.43/1.01 (declare-const tptp.ord_less_eq_set_a (-> tptp.set_a tptp.set_a Bool)) % 0.43/1.01 (declare-const tptp.binary2053421120memb_a (-> (-> tptp.a tptp.int) tptp.a tptp.binary1439146945Tree_a Bool)) % 0.43/1.01 (declare-const tptp.h (-> tptp.a tptp.int)) % 0.43/1.01 (declare-const tptp.e tptp.a) % 0.43/1.01 (declare-const tptp.ord_less_a_o (-> (-> tptp.a Bool) (-> tptp.a Bool) Bool)) % 0.43/1.01 (declare-const tptp.binary1226383794sert_a (-> (-> tptp.a tptp.int) tptp.a tptp.binary1439146945Tree_a tptp.binary1439146945Tree_a)) % 0.43/1.01 (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.43/1.01 (define tptp.bot_bot_a_o () (lambda (@list (@var "X4" tptp.a)) tptp.bot_bot_o)) % 0.43/1.01 (define tptp.minus_minus_a_o () (let ((_let_1 (@var "X4" tptp.a))) (let ((_let_2 (@var "B6" (-> tptp.a Bool)))) (let ((_let_3 (@var "A5" (-> tptp.a Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.minus_minus_o (_ _let_3 _let_1)) (_ _let_2 _let_1))))))) % 0.43/1.01 (define tptp.sup_sup_a_o () (let ((_let_1 (@var "X4" tptp.a))) (let ((_let_2 (@var "G" (-> tptp.a Bool)))) (let ((_let_3 (@var "F2" (-> tptp.a Bool)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.sup_sup_o (_ _let_3 _let_1)) (_ _let_2 _let_1))))))) % 0.43/1.01 (define tptp.sup_sup_set_a () (let ((_let_1 (@var "B6" 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) (_ tptp.collect_a (lambda (@list _let_2) (or (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))) % 0.43/1.01 (define tptp.ord_less_set_a () (let ((_let_1 (@var "B" tptp.set_a))) (let ((_let_2 (@var "A" tptp.set_a))) (lambda (@list _let_1 _let_2) (and (= _let_2 (_ (_ tptp.sup_sup_set_a _let_2) _let_1)) (not (= _let_2 _let_1))))))) % 0.43/1.01 (define tptp.ord_less_int () (let ((_let_1 (@var "B" tptp.int))) (let ((_let_2 (@var "A" tptp.int))) (lambda (@list _let_1 _let_2) (and (= _let_2 (_ (_ tptp.sup_sup_int _let_2) _let_1)) (not (= _let_2 _let_1))))))) % 0.43/1.01 (define tptp.insert_a () (let ((_let_1 (@var "__flatten_var_0" tptp.set_a))) (let ((_let_2 (@var "A" tptp.a))) (let ((_let_3 (@var "X4" tptp.a))) (lambda (@list _let_2 _let_1) (_ (_ tptp.sup_sup_set_a (_ tptp.collect_a (lambda (@list _let_3) (= _let_3 _let_2)))) _let_1)))))) % 0.43/1.01 (define tptp.binary504661350_eqs_a () (let ((_let_1 (@var "X4" tptp.a))) (let ((_let_2 (@var "H2" (-> tptp.a tptp.int)))) (let ((_let_3 (@var "Y3" tptp.a))) (lambda (@list _let_2 _let_1) (_ tptp.collect_a (lambda (@list _let_3) (= (_ _let_2 _let_3) (_ _let_2 _let_1))))))))) % 0.43/1.01 (define tptp.minus_minus_set_a () (let ((_let_1 (@var "B6" tptp.set_a))) (let ((_let_2 (@var "X4" tptp.a))) (let ((_let_3 (_ tptp.member_a _let_2))) (let ((_let_4 (@list _let_2))) (let ((_let_5 (@var "A5" tptp.set_a))) (lambda (@list _let_5 _let_1) (_ tptp.collect_a (_ (_ tptp.minus_minus_a_o (lambda _let_4 (_ _let_3 _let_5))) (lambda _let_4 (_ _let_3 _let_1))))))))))) % 0.43/1.01 (define tptp.the_elem_a () (let ((_let_1 (@var "X4" tptp.a))) (let ((_let_2 (@var "X5" tptp.set_a))) (lambda (@list _let_2) (_ tptp.the_a (lambda (@list _let_1) (= _let_2 (_ (_ tptp.insert_a _let_1) tptp.bot_bot_set_a)))))))) % 0.43/1.01 (define tptp.is_singleton_a () (let ((_let_1 (@var "A5" tptp.set_a))) (lambda (@list _let_1) (= _let_1 (_ (_ tptp.insert_a (_ tptp.the_elem_a _let_1)) tptp.bot_bot_set_a))))) % 0.43/1.01 (define tptp.remove_a () (let ((_let_1 (@var "X4" tptp.a))) (let ((_let_2 (@var "A5" tptp.set_a))) (lambda (@list _let_1 _let_2) (_ (_ tptp.minus_minus_set_a _let_2) (_ (_ tptp.insert_a _let_1) tptp.bot_bot_set_a)))))) % 0.43/1.01 (define tptp.is_empty_a () (let ((_let_1 (@var "A5" tptp.set_a))) (lambda (@list _let_1) (= _let_1 tptp.bot_bot_set_a)))) % 0.43/1.01 (define @t1 () (_ tptp.binary945792244etOf_a tptp.t1)) % 0.43/1.01 (define @t2 () (_ tptp.member_a tptp.w)) % 0.43/1.01 (define @t3 () (_ @t2 @t1)) % 0.43/1.01 (define @t4 () (_ tptp.binary717961607le_T_a tptp.t1)) % 0.43/1.01 (define @t5 () (_ (_ @t4 tptp.x) tptp.t2)) % 0.43/1.01 (define @t6 () (_ tptp.binary1721989714Tree_a tptp.h)) % 0.43/1.01 (define @t7 () (_ @t6 @t5)) % 0.43/1.01 (define @t8 () (_ @t6 tptp.t2)) % 0.43/1.01 (define @t9 () (_ @t6 tptp.t1)) % 0.43/1.01 (define @t10 () (_ tptp.h tptp.x)) % 0.43/1.01 (define @t11 () (_ tptp.h tptp.e)) % 0.43/1.01 (define @t12 () (_ (_ tptp.binary504661350_eqs_a tptp.h) tptp.e)) % 0.43/1.01 (define @t13 () (@var "Y23" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t14 () (@var "X23" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t15 () (@var "Y22" tptp.a)) % 0.43/1.01 (define @t16 () (@var "X22" tptp.a)) % 0.43/1.01 (define @t17 () (@var "Y21" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t18 () (@var "X21" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t19 () (_ (_ (_ tptp.binary717961607le_T_a @t18) @t16) @t14)) % 0.43/1.01 (define @t20 () (@var "X" tptp.int)) % 0.43/1.01 (define @t21 () (@var "T" tptp.int)) % 0.43/1.01 (define @t22 () (_ (_ tptp.ord_less_int @t21) @t20)) % 0.43/1.01 (define @t23 () (@var "Z" tptp.int)) % 0.43/1.01 (define @t24 () (_ tptp.ord_less_int @t20)) % 0.43/1.01 (define @t25 () (_ @t24 @t23)) % 0.43/1.01 (define @t26 () (@list @t20)) % 0.43/1.01 (define @t27 () (@list @t23)) % 0.43/1.01 (define @t28 () (@list @t21)) % 0.43/1.01 (define @t29 () (_ @t24 @t21)) % 0.43/1.01 (define @t30 () (not (= @t20 @t21))) % 0.43/1.01 (define @t31 () (@var "Q2" (-> tptp.int Bool))) % 0.43/1.01 (define @t32 () (_ @t31 @t20)) % 0.43/1.01 (define @t33 () (@var "P2" (-> tptp.int Bool))) % 0.43/1.01 (define @t34 () (_ @t33 @t20)) % 0.43/1.01 (define @t35 () (@var "Q" (-> tptp.int Bool))) % 0.43/1.01 (define @t36 () (_ @t35 @t20)) % 0.43/1.01 (define @t37 () (@var "P" (-> tptp.int Bool))) % 0.43/1.01 (define @t38 () (_ @t37 @t20)) % 0.43/1.01 (define @t39 () (= (or @t38 @t36) (or @t34 @t32))) % 0.43/1.01 (define @t40 () (@var "X2" tptp.int)) % 0.43/1.01 (define @t41 () (= (_ @t35 @t40) (_ @t31 @t40))) % 0.43/1.01 (define @t42 () (@var "Z2" tptp.int)) % 0.43/1.01 (define @t43 () (_ tptp.ord_less_int @t40)) % 0.43/1.01 (define @t44 () (_ @t43 @t42)) % 0.43/1.01 (define @t45 () (@list @t40)) % 0.43/1.01 (define @t46 () (@list @t42)) % 0.43/1.01 (define @t47 () (exists @t46 (forall @t45 (=> @t44 @t41)))) % 0.43/1.01 (define @t48 () (= (_ @t37 @t40) (_ @t33 @t40))) % 0.43/1.01 (define @t49 () (exists @t46 (forall @t45 (=> @t44 @t48)))) % 0.43/1.01 (define @t50 () (@list @t37 @t33 @t35 @t31)) % 0.43/1.01 (define @t51 () (= (and @t38 @t36) (and @t34 @t32))) % 0.43/1.01 (define @t52 () (_ (_ tptp.binary1226383794sert_a tptp.h) tptp.e)) % 0.43/1.01 (define @t53 () (@var "T2" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t54 () (@var "H" (-> tptp.a tptp.int))) % 0.43/1.01 (define @t55 () (_ tptp.binary1721989714Tree_a @t54)) % 0.43/1.01 (define @t56 () (_ @t55 @t53)) % 0.43/1.01 (define @t57 () (@var "X3" tptp.a)) % 0.43/1.01 (define @t58 () (@var "T1" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t59 () (_ tptp.binary717961607le_T_a @t58)) % 0.43/1.01 (define @t60 () (_ @t59 @t57)) % 0.43/1.01 (define @t61 () (_ @t60 @t53)) % 0.43/1.01 (define @t62 () (_ @t55 @t61)) % 0.43/1.01 (define @t63 () (@list @t54 @t58 @t57 @t53)) % 0.43/1.01 (define @t64 () (_ @t55 @t58)) % 0.43/1.01 (define @t65 () (@var "X4" tptp.a)) % 0.43/1.01 (define @t66 () (_ @t54 @t65)) % 0.43/1.01 (define @t67 () (_ @t54 @t57)) % 0.43/1.01 (define @t68 () (_ tptp.ord_less_int @t67)) % 0.43/1.01 (define @t69 () (_ tptp.binary945792244etOf_a @t53)) % 0.43/1.01 (define @t70 () (_ tptp.member_a @t65)) % 0.43/1.01 (define @t71 () (_ @t70 @t69)) % 0.43/1.01 (define @t72 () (=> @t71 (_ @t68 @t66))) % 0.43/1.01 (define @t73 () (@list @t65)) % 0.43/1.01 (define @t74 () (forall @t73 @t72)) % 0.43/1.01 (define @t75 () (_ tptp.binary945792244etOf_a @t58)) % 0.43/1.01 (define @t76 () (_ @t70 @t75)) % 0.43/1.01 (define @t77 () (=> @t76 (_ (_ tptp.ord_less_int @t66) @t67))) % 0.43/1.01 (define @t78 () (forall @t73 @t77)) % 0.43/1.01 (define @t79 () (and @t64 @t78 @t74 @t56)) % 0.43/1.01 (define @t80 () (= @t62 @t79)) % 0.43/1.01 (define @t81 () (forall @t63 @t80)) % 0.43/1.01 (define @t82 () (_ (_ tptp.ord_less_int @t23) @t20)) % 0.43/1.01 (define @t83 () (_ (_ tptp.ord_less_int @t42) @t40)) % 0.43/1.01 (define @t84 () (exists @t46 (forall @t45 (=> @t83 @t41)))) % 0.43/1.01 (define @t85 () (exists @t46 (forall @t45 (=> @t83 @t48)))) % 0.43/1.01 (define @t86 () (@var "T" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t87 () (_ tptp.member_a @t57)) % 0.43/1.01 (define @t88 () (@var "E" tptp.a)) % 0.43/1.01 (define @t89 () (_ (_ tptp.binary1226383794sert_a @t54) @t88)) % 0.43/1.01 (define @t90 () (_ @t89 @t61)) % 0.43/1.01 (define @t91 () (_ @t54 @t88)) % 0.43/1.01 (define @t92 () (_ @t68 @t91)) % 0.43/1.01 (define @t93 () (_ (_ tptp.ord_less_int @t91) @t67)) % 0.43/1.01 (define @t94 () (@var "X3" tptp.int)) % 0.43/1.01 (define @t95 () (@var "Y" tptp.int)) % 0.43/1.01 (define @t96 () (_ tptp.ord_less_int @t95)) % 0.43/1.01 (define @t97 () (_ @t96 @t94)) % 0.43/1.01 (define @t98 () (_ tptp.ord_less_int @t94)) % 0.43/1.01 (define @t99 () (_ @t98 @t95)) % 0.43/1.01 (define @t100 () (not @t99)) % 0.43/1.01 (define @t101 () (= @t94 @t95)) % 0.43/1.01 (define @t102 () (not @t101)) % 0.43/1.01 (define @t103 () (@list @t94 @t95)) % 0.43/1.01 (define @t104 () (@var "B2" tptp.set_a)) % 0.43/1.01 (define @t105 () (@var "A2" tptp.set_a)) % 0.43/1.01 (define @t106 () (= @t105 @t104)) % 0.43/1.01 (define @t107 () (not @t106)) % 0.43/1.01 (define @t108 () (_ tptp.ord_less_set_a @t104)) % 0.43/1.01 (define @t109 () (_ @t108 @t105)) % 0.43/1.01 (define @t110 () (@list @t104 @t105)) % 0.43/1.01 (define @t111 () (@var "B2" (-> tptp.a Bool))) % 0.43/1.01 (define @t112 () (@var "A2" (-> tptp.a Bool))) % 0.43/1.01 (define @t113 () (= @t112 @t111)) % 0.43/1.01 (define @t114 () (not @t113)) % 0.43/1.01 (define @t115 () (_ tptp.ord_less_a_o @t111)) % 0.43/1.01 (define @t116 () (_ @t115 @t112)) % 0.43/1.01 (define @t117 () (@list @t111 @t112)) % 0.43/1.01 (define @t118 () (@var "B2" tptp.int)) % 0.43/1.01 (define @t119 () (@var "A2" tptp.int)) % 0.43/1.01 (define @t120 () (= @t119 @t118)) % 0.43/1.01 (define @t121 () (not @t120)) % 0.43/1.01 (define @t122 () (_ tptp.ord_less_int @t118)) % 0.43/1.01 (define @t123 () (_ @t122 @t119)) % 0.43/1.01 (define @t124 () (@list @t118 @t119)) % 0.43/1.01 (define @t125 () (_ tptp.ord_less_set_a @t105)) % 0.43/1.01 (define @t126 () (_ @t125 @t104)) % 0.43/1.01 (define @t127 () (@list @t105 @t104)) % 0.43/1.01 (define @t128 () (_ tptp.ord_less_a_o @t112)) % 0.43/1.01 (define @t129 () (_ @t128 @t111)) % 0.43/1.01 (define @t130 () (@list @t112 @t111)) % 0.43/1.01 (define @t131 () (_ tptp.ord_less_int @t119)) % 0.43/1.01 (define @t132 () (_ @t131 @t118)) % 0.43/1.01 (define @t133 () (@list @t119 @t118)) % 0.43/1.01 (define @t134 () (@var "B2" tptp.a)) % 0.43/1.01 (define @t135 () (@var "A2" tptp.a)) % 0.43/1.01 (define @t136 () (@var "C" tptp.int)) % 0.43/1.01 (define @t137 () (@var "F" (-> tptp.int tptp.set_a))) % 0.43/1.01 (define @t138 () (@var "Y2" tptp.int)) % 0.43/1.01 (define @t139 () (_ @t43 @t138)) % 0.43/1.01 (define @t140 () (@list @t40 @t138)) % 0.43/1.01 (define @t141 () (forall @t140 (=> @t139 (_ (_ tptp.ord_less_set_a (_ @t137 @t40)) (_ @t137 @t138))))) % 0.43/1.01 (define @t142 () (_ @t122 @t136)) % 0.43/1.01 (define @t143 () (=> @t142 (=> @t141 (_ @t125 (_ @t137 @t136))))) % 0.43/1.01 (define @t144 () (_ @t137 @t118)) % 0.43/1.01 (define @t145 () (@list @t105 @t137 @t118 @t136)) % 0.43/1.01 (define @t146 () (@var "F" (-> tptp.int tptp.a Bool))) % 0.43/1.01 (define @t147 () (forall @t140 (=> @t139 (_ (_ tptp.ord_less_a_o (_ @t146 @t40)) (_ @t146 @t138))))) % 0.43/1.01 (define @t148 () (=> @t142 (=> @t147 (_ @t128 (_ @t146 @t136))))) % 0.43/1.01 (define @t149 () (_ @t146 @t118)) % 0.43/1.01 (define @t150 () (@list @t112 @t146 @t118 @t136)) % 0.43/1.01 (define @t151 () (@var "C" tptp.set_a)) % 0.43/1.01 (define @t152 () (@var "F" (-> tptp.set_a tptp.int))) % 0.43/1.01 (define @t153 () (@var "Y2" tptp.set_a)) % 0.43/1.01 (define @t154 () (@var "X2" tptp.set_a)) % 0.43/1.01 (define @t155 () (_ (_ tptp.ord_less_set_a @t154) @t153)) % 0.43/1.01 (define @t156 () (@list @t154 @t153)) % 0.43/1.01 (define @t157 () (forall @t156 (=> @t155 (_ (_ tptp.ord_less_int (_ @t152 @t154)) (_ @t152 @t153))))) % 0.43/1.01 (define @t158 () (_ @t108 @t151)) % 0.43/1.01 (define @t159 () (=> @t158 (=> @t157 (_ @t131 (_ @t152 @t151))))) % 0.43/1.01 (define @t160 () (_ @t152 @t104)) % 0.43/1.01 (define @t161 () (@list @t119 @t152 @t104 @t151)) % 0.43/1.01 (define @t162 () (@var "F" (-> tptp.set_a tptp.set_a))) % 0.43/1.01 (define @t163 () (forall @t156 (=> @t155 (_ (_ tptp.ord_less_set_a (_ @t162 @t154)) (_ @t162 @t153))))) % 0.43/1.01 (define @t164 () (=> @t158 (=> @t163 (_ @t125 (_ @t162 @t151))))) % 0.43/1.01 (define @t165 () (_ @t162 @t104)) % 0.43/1.01 (define @t166 () (@list @t105 @t162 @t104 @t151)) % 0.43/1.01 (define @t167 () (@var "F" (-> tptp.set_a tptp.a Bool))) % 0.43/1.01 (define @t168 () (forall @t156 (=> @t155 (_ (_ tptp.ord_less_a_o (_ @t167 @t154)) (_ @t167 @t153))))) % 0.43/1.01 (define @t169 () (=> @t158 (=> @t168 (_ @t128 (_ @t167 @t151))))) % 0.43/1.01 (define @t170 () (_ @t167 @t104)) % 0.43/1.01 (define @t171 () (@list @t112 @t167 @t104 @t151)) % 0.43/1.01 (define @t172 () (@var "C" (-> tptp.a Bool))) % 0.43/1.01 (define @t173 () (@var "F" (-> (-> tptp.a Bool) tptp.int))) % 0.43/1.01 (define @t174 () (@var "Y2" (-> tptp.a Bool))) % 0.43/1.01 (define @t175 () (@var "X2" (-> tptp.a Bool))) % 0.43/1.01 (define @t176 () (_ (_ tptp.ord_less_a_o @t175) @t174)) % 0.43/1.01 (define @t177 () (@list @t175 @t174)) % 0.43/1.01 (define @t178 () (forall @t177 (=> @t176 (_ (_ tptp.ord_less_int (_ @t173 @t175)) (_ @t173 @t174))))) % 0.43/1.01 (define @t179 () (_ @t115 @t172)) % 0.43/1.01 (define @t180 () (=> @t179 (=> @t178 (_ @t131 (_ @t173 @t172))))) % 0.43/1.01 (define @t181 () (_ @t173 @t111)) % 0.43/1.01 (define @t182 () (@list @t119 @t173 @t111 @t172)) % 0.43/1.01 (define @t183 () (@var "F" (-> (-> tptp.a Bool) tptp.set_a))) % 0.43/1.01 (define @t184 () (forall @t177 (=> @t176 (_ (_ tptp.ord_less_set_a (_ @t183 @t175)) (_ @t183 @t174))))) % 0.43/1.01 (define @t185 () (=> @t179 (=> @t184 (_ @t125 (_ @t183 @t172))))) % 0.43/1.01 (define @t186 () (_ @t183 @t111)) % 0.43/1.01 (define @t187 () (@list @t105 @t183 @t111 @t172)) % 0.43/1.01 (define @t188 () (@var "F" (-> (-> tptp.a Bool) tptp.a Bool))) % 0.43/1.01 (define @t189 () (forall @t177 (=> @t176 (_ (_ tptp.ord_less_a_o (_ @t188 @t175)) (_ @t188 @t174))))) % 0.43/1.01 (define @t190 () (=> @t179 (=> @t189 (_ @t128 (_ @t188 @t172))))) % 0.43/1.01 (define @t191 () (_ @t188 @t111)) % 0.43/1.01 (define @t192 () (@list @t112 @t188 @t111 @t172)) % 0.43/1.01 (define @t193 () (@var "F" (-> tptp.int tptp.int))) % 0.43/1.01 (define @t194 () (forall @t140 (=> @t139 (_ (_ tptp.ord_less_int (_ @t193 @t40)) (_ @t193 @t138))))) % 0.43/1.01 (define @t195 () (=> @t142 (=> @t194 (_ @t131 (_ @t193 @t136))))) % 0.43/1.01 (define @t196 () (_ @t193 @t118)) % 0.43/1.01 (define @t197 () (@list @t119 @t193 @t118 @t136)) % 0.43/1.01 (define @t198 () (=> @t141 (_ (_ tptp.ord_less_set_a (_ @t137 @t119)) @t151))) % 0.43/1.01 (define @t199 () (@list @t119 @t118 @t137 @t151)) % 0.43/1.01 (define @t200 () (=> @t147 (_ (_ tptp.ord_less_a_o (_ @t146 @t119)) @t172))) % 0.43/1.01 (define @t201 () (@list @t119 @t118 @t146 @t172)) % 0.43/1.01 (define @t202 () (=> @t157 (_ (_ tptp.ord_less_int (_ @t152 @t105)) @t136))) % 0.43/1.01 (define @t203 () (@list @t105 @t104 @t152 @t136)) % 0.43/1.01 (define @t204 () (=> @t163 (_ (_ tptp.ord_less_set_a (_ @t162 @t105)) @t151))) % 0.43/1.01 (define @t205 () (@list @t105 @t104 @t162 @t151)) % 0.43/1.01 (define @t206 () (=> @t168 (_ (_ tptp.ord_less_a_o (_ @t167 @t105)) @t172))) % 0.43/1.01 (define @t207 () (@list @t105 @t104 @t167 @t172)) % 0.43/1.01 (define @t208 () (=> @t178 (_ (_ tptp.ord_less_int (_ @t173 @t112)) @t136))) % 0.43/1.01 (define @t209 () (@list @t112 @t111 @t173 @t136)) % 0.43/1.01 (define @t210 () (=> @t184 (_ (_ tptp.ord_less_set_a (_ @t183 @t112)) @t151))) % 0.43/1.01 (define @t211 () (@list @t112 @t111 @t183 @t151)) % 0.43/1.01 (define @t212 () (=> @t189 (_ (_ tptp.ord_less_a_o (_ @t188 @t112)) @t172))) % 0.43/1.01 (define @t213 () (@list @t112 @t111 @t188 @t172)) % 0.43/1.01 (define @t214 () (=> @t194 (_ (_ tptp.ord_less_int (_ @t193 @t119)) @t136))) % 0.43/1.01 (define @t215 () (@list @t119 @t118 @t193 @t136)) % 0.43/1.01 (define @t216 () (@list @t94)) % 0.43/1.01 (define @t217 () (@var "X_1" tptp.int)) % 0.43/1.01 (define @t218 () (@var "P" (-> tptp.a Bool))) % 0.43/1.01 (define @t219 () (_ @t218 @t135)) % 0.43/1.01 (define @t220 () (_ tptp.collect_a @t218)) % 0.43/1.01 (define @t221 () (_ tptp.member_a @t135)) % 0.43/1.01 (define @t222 () (_ @t221 @t220)) % 0.43/1.01 (define @t223 () (= @t222 @t219)) % 0.43/1.01 (define @t224 () (@list @t135 @t218)) % 0.43/1.01 (define @t225 () (forall @t224 @t223)) % 0.43/1.01 (define @t226 () (@var "A3" tptp.set_a)) % 0.43/1.01 (define @t227 () (_ @t70 @t226)) % 0.43/1.01 (define @t228 () (@list @t226)) % 0.43/1.01 (define @t229 () (@var "Q" (-> tptp.a Bool))) % 0.43/1.01 (define @t230 () (_ tptp.collect_a @t229)) % 0.43/1.01 (define @t231 () (@var "X2" tptp.a)) % 0.43/1.01 (define @t232 () (@list @t231)) % 0.43/1.01 (define @t233 () (@list @t218 @t229)) % 0.43/1.01 (define @t234 () (@var "Y" tptp.set_a)) % 0.43/1.01 (define @t235 () (@var "X3" tptp.set_a)) % 0.43/1.01 (define @t236 () (_ tptp.ord_less_set_a @t235)) % 0.43/1.01 (define @t237 () (_ @t236 @t234)) % 0.43/1.01 (define @t238 () (@list @t235 @t234)) % 0.43/1.01 (define @t239 () (@var "Y" (-> tptp.a Bool))) % 0.43/1.01 (define @t240 () (@var "X3" (-> tptp.a Bool))) % 0.43/1.01 (define @t241 () (_ tptp.ord_less_a_o @t240)) % 0.43/1.01 (define @t242 () (_ @t241 @t239)) % 0.43/1.01 (define @t243 () (@list @t240 @t239)) % 0.43/1.01 (define @t244 () (_ tptp.ord_less_set_a @t234)) % 0.43/1.01 (define @t245 () (_ @t244 @t235)) % 0.43/1.01 (define @t246 () (_ tptp.ord_less_a_o @t239)) % 0.43/1.01 (define @t247 () (_ @t246 @t240)) % 0.43/1.01 (define @t248 () (not @t97)) % 0.43/1.01 (define @t249 () (@var "Z3" tptp.set_a)) % 0.43/1.01 (define @t250 () (@list @t235 @t234 @t249)) % 0.43/1.01 (define @t251 () (@var "Z3" (-> tptp.a Bool))) % 0.43/1.01 (define @t252 () (@list @t240 @t239 @t251)) % 0.43/1.01 (define @t253 () (@var "Z3" tptp.int)) % 0.43/1.01 (define @t254 () (@list @t94 @t95 @t253)) % 0.43/1.01 (define @t255 () (@list @t235)) % 0.43/1.01 (define @t256 () (@list @t240)) % 0.43/1.01 (define @t257 () (_ @t125 @t151)) % 0.43/1.01 (define @t258 () (=> @t158 @t257)) % 0.43/1.01 (define @t259 () (@list @t105 @t104 @t151)) % 0.43/1.01 (define @t260 () (_ @t128 @t172)) % 0.43/1.01 (define @t261 () (=> @t179 @t260)) % 0.43/1.01 (define @t262 () (@list @t112 @t111 @t172)) % 0.43/1.01 (define @t263 () (_ @t131 @t136)) % 0.43/1.01 (define @t264 () (=> @t142 @t263)) % 0.43/1.01 (define @t265 () (@list @t119 @t118 @t136)) % 0.43/1.01 (define @t266 () (@var "P" Bool)) % 0.43/1.01 (define @t267 () (@list @t105)) % 0.43/1.01 (define @t268 () (@list @t112)) % 0.43/1.01 (define @t269 () (@list @t119)) % 0.43/1.01 (define @t270 () (@var "P" (-> tptp.int tptp.int Bool))) % 0.43/1.01 (define @t271 () (@var "B3" tptp.int)) % 0.43/1.01 (define @t272 () (@var "A4" tptp.int)) % 0.43/1.01 (define @t273 () (_ @t270 @t272)) % 0.43/1.01 (define @t274 () (_ @t273 @t271)) % 0.43/1.01 (define @t275 () (@list @t272 @t271)) % 0.43/1.01 (define @t276 () (_ tptp.ord_less_set_a @t151)) % 0.43/1.01 (define @t277 () (_ @t276 @t105)) % 0.43/1.01 (define @t278 () (_ @t276 @t104)) % 0.43/1.01 (define @t279 () (@list @t104 @t105 @t151)) % 0.43/1.01 (define @t280 () (_ tptp.ord_less_a_o @t172)) % 0.43/1.01 (define @t281 () (_ tptp.ord_less_int @t136)) % 0.43/1.01 (define @t282 () (_ @t281 @t119)) % 0.43/1.01 (define @t283 () (_ @t281 @t118)) % 0.43/1.01 (define @t284 () (@list @t118 @t119 @t136)) % 0.43/1.01 (define @t285 () (_ (_ tptp.insert_a tptp.e) tptp.bot_bot_set_a)) % 0.43/1.01 (define @t286 () (= (_ tptp.binary945792244etOf_a (_ @t52 tptp.t2)) (_ (_ tptp.sup_sup_set_a (_ (_ tptp.minus_minus_set_a (_ tptp.binary945792244etOf_a tptp.t2)) @t12)) @t285))) % 0.43/1.01 (define @t287 () (= (_ tptp.binary945792244etOf_a (_ @t52 tptp.t1)) (_ (_ tptp.sup_sup_set_a (_ (_ tptp.minus_minus_set_a @t1) @t12)) @t285))) % 0.43/1.01 (define @t288 () (@var "Ab" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t289 () (_ tptp.binary1452917696Tree_a @t218)) % 0.43/1.01 (define @t290 () (@var "Aa" tptp.a)) % 0.43/1.01 (define @t291 () (@var "A2" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t292 () (@list @t218)) % 0.43/1.01 (define @t293 () (_ tptp.insert_a @t57)) % 0.43/1.01 (define @t294 () (_ @t293 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t295 () (_ tptp.binary945792244etOf_a tptp.binary476621312_Tip_a)) % 0.43/1.01 (define @t296 () (= @t112 tptp.bot_bot_a_o)) % 0.43/1.01 (define @t297 () (= @t105 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t298 () (@list @t18 @t16 @t14)) % 0.43/1.01 (define @t299 () (@var "Tree" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t300 () (@var "P" (-> tptp.binary1439146945Tree_a Bool))) % 0.43/1.01 (define @t301 () (@var "X32" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t302 () (@var "X24" tptp.a)) % 0.43/1.01 (define @t303 () (@var "X1" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t304 () (@var "X232" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t305 () (@var "X222" tptp.a)) % 0.43/1.01 (define @t306 () (@var "X212" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t307 () (@var "Y" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t308 () (_ tptp.insert_a @t135)) % 0.43/1.01 (define @t309 () (_ @t308 @t226)) % 0.43/1.01 (define @t310 () (_ @t308 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t311 () (_ tptp.minus_minus_set_a @t226)) % 0.43/1.01 (define @t312 () (_ @t311 @t310)) % 0.43/1.01 (define @t313 () (_ @t308 @t312)) % 0.43/1.01 (define @t314 () (@list @t135 @t226)) % 0.43/1.01 (define @t315 () (@var "B4" tptp.set_a)) % 0.43/1.01 (define @t316 () (_ tptp.sup_sup_set_a @t226)) % 0.43/1.01 (define @t317 () (_ @t316 @t315)) % 0.43/1.01 (define @t318 () (_ tptp.minus_minus_set_a @t315)) % 0.43/1.01 (define @t319 () (_ @t318 @t226)) % 0.43/1.01 (define @t320 () (@list @t226 @t315)) % 0.43/1.01 (define @t321 () (_ tptp.sup_sup_set_a @t315)) % 0.43/1.01 (define @t322 () (_ @t311 @t315)) % 0.43/1.01 (define @t323 () (_ @t293 @t315)) % 0.43/1.01 (define @t324 () (_ @t87 @t226)) % 0.43/1.01 (define @t325 () (not @t324)) % 0.43/1.01 (define @t326 () (@list @t57 @t226 @t315)) % 0.43/1.01 (define @t327 () (_ @t293 @t226)) % 0.43/1.01 (define @t328 () (_ tptp.minus_minus_set_a @t327)) % 0.43/1.01 (define @t329 () (_ @t328 @t315)) % 0.43/1.01 (define @t330 () (_ @t87 @t315)) % 0.43/1.01 (define @t331 () (=> @t330 (= @t329 @t322))) % 0.43/1.01 (define @t332 () (@list @t57 @t315 @t226)) % 0.43/1.01 (define @t333 () (@var "C2" tptp.set_a)) % 0.43/1.01 (define @t334 () (_ @t321 @t333)) % 0.43/1.01 (define @t335 () (_ @t308 @t315)) % 0.43/1.01 (define @t336 () (_ @t218 @t65)) % 0.43/1.01 (define @t337 () (forall @t73 (not @t336))) % 0.43/1.01 (define @t338 () (= @t220 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t339 () (= @t226 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t340 () (@var "C" tptp.a)) % 0.43/1.01 (define @t341 () (_ tptp.member_a @t340)) % 0.43/1.01 (define @t342 () (@list @t57 @t226)) % 0.43/1.01 (define @t343 () (_ @t221 @t226)) % 0.43/1.01 (define @t344 () (= @t135 @t134)) % 0.43/1.01 (define @t345 () (_ tptp.insert_a @t134)) % 0.43/1.01 (define @t346 () (_ @t221 (_ @t345 @t226))) % 0.43/1.01 (define @t347 () (@list @t135 @t134 @t226)) % 0.43/1.01 (define @t348 () (_ @t345 @t315)) % 0.43/1.01 (define @t349 () (_ @t221 @t348)) % 0.43/1.01 (define @t350 () (_ @t221 @t315)) % 0.43/1.01 (define @t351 () (@list @t135 @t315 @t134)) % 0.43/1.01 (define @t352 () (_ @t341 @t315)) % 0.43/1.01 (define @t353 () (_ @t341 @t226)) % 0.43/1.01 (define @t354 () (_ @t341 @t317)) % 0.43/1.01 (define @t355 () (@list @t340 @t226 @t315)) % 0.43/1.01 (define @t356 () (not @t352)) % 0.43/1.01 (define @t357 () (@list @t340 @t315 @t226)) % 0.43/1.01 (define @t358 () (_ tptp.minus_minus_set_a @t322)) % 0.43/1.01 (define @t359 () (_ @t341 @t322)) % 0.43/1.01 (define @t360 () (@list @t135)) % 0.43/1.01 (define @t361 () (= @t315 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t362 () (@list @t226 @t135 @t315)) % 0.43/1.01 (define @t363 () (_ tptp.ord_less_set_a @t226)) % 0.43/1.01 (define @t364 () (not @t339)) % 0.43/1.01 (define @t365 () (@var "Y2" tptp.a)) % 0.43/1.01 (define @t366 () (_ (_ tptp.member_a @t365) @t226)) % 0.43/1.01 (define @t367 () (not @t343)) % 0.43/1.01 (define @t368 () (@var "B5" tptp.set_a)) % 0.43/1.01 (define @t369 () (@list @t368)) % 0.43/1.01 (define @t370 () (@var "Y" tptp.a)) % 0.43/1.01 (define @t371 () (_ tptp.insert_a @t370)) % 0.43/1.01 (define @t372 () (@list @t57 @t370 @t226)) % 0.43/1.01 (define @t373 () (@var "C3" tptp.set_a)) % 0.43/1.01 (define @t374 () (_ tptp.member_a @t134)) % 0.43/1.01 (define @t375 () (not @t344)) % 0.43/1.01 (define @t376 () (= @t226 @t315)) % 0.43/1.01 (define @t377 () (not @t330)) % 0.43/1.01 (define @t378 () (_ @t316 @t334)) % 0.43/1.01 (define @t379 () (@list @t226 @t315 @t333)) % 0.43/1.01 (define @t380 () (@var "A5" tptp.set_a)) % 0.43/1.01 (define @t381 () (@var "B6" tptp.set_a)) % 0.43/1.01 (define @t382 () (@list @t380 @t381)) % 0.43/1.01 (define @t383 () (_ @t70 @t315)) % 0.43/1.01 (define @t384 () (_ @t70 @t317)) % 0.43/1.01 (define @t385 () (@list @t226 @t315 @t218)) % 0.43/1.01 (define @t386 () (@var "B3" tptp.a)) % 0.43/1.01 (define @t387 () (_ @t363 @t315)) % 0.43/1.01 (define @t388 () (=> @t353 @t352)) % 0.43/1.01 (define @t389 () (_ @t345 tptp.bot_bot_set_a)) % 0.43/1.01 (define @t390 () (@var "D" tptp.a)) % 0.43/1.01 (define @t391 () (= @t134 @t135)) % 0.43/1.01 (define @t392 () (_ @t374 @t310)) % 0.43/1.01 (define @t393 () (@list @t134 @t135)) % 0.43/1.01 (define @t394 () (_ tptp.sup_sup_set_a tptp.bot_bot_set_a)) % 0.43/1.01 (define @t395 () (= @t315 @t294)) % 0.43/1.01 (define @t396 () (= @t226 @t294)) % 0.43/1.01 (define @t397 () (or (and @t339 @t395) (and @t396 @t361) (and @t396 @t395))) % 0.43/1.01 (define @t398 () (@var "__flatten_var_0" tptp.set_a)) % 0.43/1.01 (define @t399 () (@var "A" tptp.a)) % 0.43/1.01 (define @t400 () (@list @t399 @t398)) % 0.43/1.01 (define @t401 () (_ @t311 @t335)) % 0.43/1.01 (define @t402 () (_ tptp.sup_sup_a_o @t112)) % 0.43/1.01 (define @t403 () (_ tptp.sup_sup_set_a @t105)) % 0.43/1.01 (define @t404 () (and @t296 (= @t111 tptp.bot_bot_a_o))) % 0.43/1.01 (define @t405 () (_ @t402 @t111)) % 0.43/1.01 (define @t406 () (and @t297 (= @t104 tptp.bot_bot_set_a))) % 0.43/1.01 (define @t407 () (_ @t403 @t104)) % 0.43/1.01 (define @t408 () (_ tptp.sup_sup_a_o tptp.bot_bot_a_o)) % 0.43/1.01 (define @t409 () (and (= @t240 tptp.bot_bot_a_o) (= @t239 tptp.bot_bot_a_o))) % 0.43/1.01 (define @t410 () (_ tptp.sup_sup_a_o @t240)) % 0.43/1.01 (define @t411 () (_ @t410 @t239)) % 0.43/1.01 (define @t412 () (and (= @t235 tptp.bot_bot_set_a) (= @t234 tptp.bot_bot_set_a))) % 0.43/1.01 (define @t413 () (_ tptp.sup_sup_set_a @t235)) % 0.43/1.01 (define @t414 () (_ @t413 @t234)) % 0.43/1.01 (define @t415 () (_ tptp.sup_sup_int @t119)) % 0.43/1.01 (define @t416 () (_ tptp.sup_sup_int @t94)) % 0.43/1.01 (define @t417 () (_ @t415 @t118)) % 0.43/1.01 (define @t418 () (_ @t416 @t95)) % 0.43/1.01 (define @t419 () (_ tptp.sup_sup_int @t417)) % 0.43/1.01 (define @t420 () (_ tptp.sup_sup_a_o @t405)) % 0.43/1.01 (define @t421 () (_ tptp.sup_sup_set_a @t407)) % 0.43/1.01 (define @t422 () (_ tptp.sup_sup_int @t95)) % 0.43/1.01 (define @t423 () (_ @t416 (_ @t422 @t253))) % 0.43/1.01 (define @t424 () (_ tptp.sup_sup_a_o @t239)) % 0.43/1.01 (define @t425 () (_ @t410 (_ @t424 @t251))) % 0.43/1.01 (define @t426 () (_ tptp.sup_sup_set_a @t234)) % 0.43/1.01 (define @t427 () (_ @t413 (_ @t426 @t249))) % 0.43/1.01 (define @t428 () (@var "X4" tptp.int)) % 0.43/1.01 (define @t429 () (@var "Y3" tptp.int)) % 0.43/1.01 (define @t430 () (@var "__flatten_var_0" tptp.a)) % 0.43/1.01 (define @t431 () (@var "X4" (-> tptp.a Bool))) % 0.43/1.01 (define @t432 () (@var "Y3" (-> tptp.a Bool))) % 0.43/1.01 (define @t433 () (@var "X4" tptp.set_a)) % 0.43/1.01 (define @t434 () (@var "Y3" tptp.set_a)) % 0.43/1.01 (define @t435 () (@var "K" tptp.int)) % 0.43/1.01 (define @t436 () (_ tptp.sup_sup_int @t435)) % 0.43/1.01 (define @t437 () (_ @t436 @t417)) % 0.43/1.01 (define @t438 () (@var "A3" tptp.int)) % 0.43/1.01 (define @t439 () (@var "K" (-> tptp.a Bool))) % 0.43/1.01 (define @t440 () (_ tptp.sup_sup_a_o @t439)) % 0.43/1.01 (define @t441 () (_ @t440 @t405)) % 0.43/1.01 (define @t442 () (@var "A3" (-> tptp.a Bool))) % 0.43/1.01 (define @t443 () (@var "K" tptp.set_a)) % 0.43/1.01 (define @t444 () (_ tptp.sup_sup_set_a @t443)) % 0.43/1.01 (define @t445 () (_ @t444 @t407)) % 0.43/1.01 (define @t446 () (@var "B4" tptp.int)) % 0.43/1.01 (define @t447 () (@var "B4" (-> tptp.a Bool))) % 0.43/1.01 (define @t448 () (_ (_ tptp.sup_sup_int @t118) @t136)) % 0.43/1.01 (define @t449 () (_ tptp.sup_sup_set_a @t104)) % 0.43/1.01 (define @t450 () (_ @t449 @t151)) % 0.43/1.01 (define @t451 () (_ @t403 @t450)) % 0.43/1.01 (define @t452 () (@var "A" tptp.int)) % 0.43/1.01 (define @t453 () (@var "B" tptp.int)) % 0.43/1.01 (define @t454 () (@var "A" (-> tptp.a Bool))) % 0.43/1.01 (define @t455 () (@var "B" (-> tptp.a Bool))) % 0.43/1.01 (define @t456 () (@var "A" tptp.set_a)) % 0.43/1.01 (define @t457 () (@var "B" tptp.set_a)) % 0.43/1.01 (define @t458 () (_ @t236 @t407)) % 0.43/1.01 (define @t459 () (_ @t98 @t417)) % 0.43/1.01 (define @t460 () (_ @t276 @t407)) % 0.43/1.01 (define @t461 () (_ @t281 @t417)) % 0.43/1.01 (define @t462 () (= @t65 @t135)) % 0.43/1.01 (define @t463 () (@var "Z4" tptp.a)) % 0.43/1.01 (define @t464 () (@var "Y4" tptp.a)) % 0.43/1.01 (define @t465 () (_ @t70 @t381)) % 0.43/1.01 (define @t466 () (lambda @t73 @t465)) % 0.43/1.01 (define @t467 () (_ @t70 @t380)) % 0.43/1.01 (define @t468 () (lambda @t73 @t467)) % 0.43/1.01 (define @t469 () (_ tptp.collect_a (lambda @t73 (and @t462 @t336)))) % 0.43/1.01 (define @t470 () (not @t219)) % 0.43/1.01 (define @t471 () (@list @t218 @t135)) % 0.43/1.01 (define @t472 () (_ tptp.collect_a (lambda @t73 (and (= @t135 @t65) @t336)))) % 0.43/1.01 (define @t473 () (@var "U" tptp.a)) % 0.43/1.01 (define @t474 () (= @t65 @t399)) % 0.43/1.01 (define @t475 () (@list @t57)) % 0.43/1.01 (define @t476 () (@var "S" tptp.set_a)) % 0.43/1.01 (define @t477 () (@var "R" tptp.set_a)) % 0.43/1.01 (define @t478 () (_ tptp.is_singleton_a @t226)) % 0.43/1.01 (define @t479 () (_ (_ tptp.insert_a @t65) tptp.bot_bot_set_a)) % 0.43/1.01 (define @t480 () (@list @t380)) % 0.43/1.01 (define @t481 () (_ tptp.minus_minus_int @t118)) % 0.43/1.01 (define @t482 () (_ tptp.minus_minus_int @t119)) % 0.43/1.01 (define @t483 () (_ tptp.ord_less_int (_ @t482 @t136))) % 0.43/1.01 (define @t484 () (_ tptp.minus_minus_int @t136)) % 0.43/1.01 (define @t485 () (@var "D" tptp.int)) % 0.43/1.01 (define @t486 () (_ tptp.binary256242811Tree_a @t14)) % 0.43/1.01 (define @t487 () (_ tptp.binary256242811Tree_a @t18)) % 0.43/1.01 (define @t488 () (_ tptp.binary256242811Tree_a @t19)) % 0.43/1.01 (define @t489 () (@var "Ya" tptp.a)) % 0.43/1.01 (define @t490 () (_ tptp.member_a @t489)) % 0.43/1.01 (define @t491 () (_ tptp.member_a @t370)) % 0.43/1.01 (define @t492 () (@var "Z32" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t493 () (_ tptp.member_a @t88)) % 0.43/1.01 (define @t494 () (@var "Z22" tptp.a)) % 0.43/1.01 (define @t495 () (@var "Z1" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t496 () (_ tptp.binary717961607le_T_a @t495)) % 0.43/1.01 (define @t497 () (= @t291 (_ (_ @t496 @t494) @t492))) % 0.43/1.01 (define @t498 () (@var "Ya" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t499 () (@var "Pa" (-> tptp.a Bool))) % 0.43/1.01 (define @t500 () (_ tptp.binary1452917696Tree_a @t499)) % 0.43/1.01 (define @t501 () (@var "X3" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t502 () (_ @t289 @t501)) % 0.43/1.01 (define @t503 () (@var "Z" tptp.a)) % 0.43/1.01 (define @t504 () (_ @t499 @t503)) % 0.43/1.01 (define @t505 () (_ @t218 @t503)) % 0.43/1.01 (define @t506 () (_ tptp.member_a @t503)) % 0.43/1.01 (define @t507 () (@list @t503)) % 0.43/1.01 (define @t508 () (@var "B" tptp.a)) % 0.43/1.01 (define @t509 () (@var "H2" (-> tptp.a tptp.int))) % 0.43/1.01 (define @t510 () (@var "T3" tptp.binary1439146945Tree_a)) % 0.43/1.01 (define @t511 () (_ tptp.binary945792244etOf_a @t510)) % 0.43/1.01 (define @t512 () (lambda (@list @t509 @t399 @t508 @t510) (=> (and (_ (_ tptp.binary1721989714Tree_a @t509) @t510) (_ (_ tptp.member_a @t399) @t511) (_ (_ tptp.member_a @t508) @t511) (= (_ @t509 @t399) (_ @t509 @t508))) (= @t399 @t508)))) % 0.43/1.01 (define @t513 () (lambda @t73 tptp.bot_bot_o)) % 0.43/1.01 (define @t514 () (@var "B6" (-> tptp.a Bool))) % 0.43/1.01 (define @t515 () (@var "A5" (-> tptp.a Bool))) % 0.43/1.01 (define @t516 () (lambda (@list @t515 @t514 @t65) (_ (_ tptp.minus_minus_o (_ @t515 @t65)) (_ @t514 @t65)))) % 0.43/1.01 (define @t517 () (@var "G" (-> tptp.a Bool))) % 0.43/1.01 (define @t518 () (@var "F2" (-> tptp.a Bool))) % 0.43/1.01 (define @t519 () (lambda (@list @t518 @t517 @t65) (_ (_ tptp.sup_sup_o (_ @t518 @t65)) (_ @t517 @t65)))) % 0.43/1.01 (define @t520 () (lambda (@list @t457 @t456) (and (= @t456 (_ (_ tptp.sup_sup_set_a @t456) @t457)) (not (= @t456 @t457))))) % 0.43/1.01 (define @t521 () (_ tptp.sup_sup_int @t452)) % 0.43/1.01 (define @t522 () (lambda (@list @t453 @t452) (and (= @t452 (_ @t521 @t453)) (not (= @t452 @t453))))) % 0.43/1.01 (define @t523 () (lambda @t382 (_ tptp.collect_a (lambda @t73 (or @t467 @t465))))) % 0.43/1.01 (define @t524 () (lambda @t400 (_ (_ tptp.sup_sup_set_a (_ tptp.collect_a (lambda @t73 @t474))) @t398))) % 0.43/1.01 (define @t525 () (@var "Y3" tptp.a)) % 0.43/1.01 (define @t526 () (@list @t525)) % 0.43/1.01 (define @t527 () (lambda (@list @t509 @t65) (_ tptp.collect_a (lambda @t526 (= (_ @t509 @t525) (_ @t509 @t65)))))) % 0.43/1.01 (define @t528 () (lambda @t382 (_ tptp.collect_a (_ (_ tptp.minus_minus_a_o @t468) @t466)))) % 0.43/1.01 (define @t529 () (lambda @t480 (= @t380 (_ (_ tptp.insert_a (_ tptp.the_elem_a @t380)) tptp.bot_bot_set_a)))) % 0.43/1.01 (define @t530 () (lambda (@list @t65 @t380) (_ (_ tptp.minus_minus_set_a @t380) @t479))) % 0.43/1.01 (define @t531 () (lambda @t480 (= @t380 tptp.bot_bot_set_a))) % 0.43/1.01 (define @t532 () (@var "X5" tptp.set_a)) % 0.43/1.01 (define @t533 () (lambda (@list @t532) (_ tptp.the_a (lambda @t73 (= @t532 @t479))))) % 0.43/1.01 (define @t534 () (tptp.binary1721989714Tree_a @t54 @t53)) % 0.43/1.01 (define @t535 () (_ @t54 @t65)) % 0.43/1.01 (define @t536 () (_ @t54 @t57)) % 0.43/1.01 (define @t537 () (not (= @t536 @t535))) % 0.43/1.01 (define @t538 () (tptp.sup_sup_int @t535 @t536)) % 0.43/1.01 (define @t539 () (= @t535 @t538)) % 0.43/1.01 (define @t540 () (tptp.binary945792244etOf_a @t53)) % 0.43/1.01 (define @t541 () (tptp.member_a @t65 @t540)) % 0.43/1.01 (define @t542 () (not @t541)) % 0.43/1.01 (define @t543 () (forall @t73 (or @t542 (and @t539 @t537)))) % 0.43/1.01 (define @t544 () (tptp.sup_sup_int @t536 @t535)) % 0.43/1.01 (define @t545 () (= @t536 @t544)) % 0.43/1.01 (define @t546 () (tptp.binary945792244etOf_a @t58)) % 0.43/1.01 (define @t547 () (tptp.member_a @t65 @t546)) % 0.43/1.01 (define @t548 () (not @t547)) % 0.43/1.01 (define @t549 () (forall @t73 (or @t548 (and @t545 @t537)))) % 0.43/1.01 (define @t550 () (tptp.binary1721989714Tree_a @t54 @t58)) % 0.43/1.01 (define @t551 () (and @t64 @t549 @t543 @t56)) % 0.43/1.01 (define @t552 () (tptp.binary717961607le_T_a @t58 @t57 @t53)) % 0.43/1.01 (define @t553 () (tptp.binary1721989714Tree_a @t54 @t552)) % 0.43/1.01 (define @t554 () (= @t62 @t551)) % 0.43/1.01 (define @t555 () (not (= @t535 @t536))) % 0.43/1.01 (define @t556 () (and @t539 @t555)) % 0.43/1.01 (define @t557 () (or @t542 @t556)) % 0.43/1.01 (define @t558 () (= @t66 @t67)) % 0.43/1.01 (define @t559 () (not @t558)) % 0.43/1.01 (define @t560 () (_ (_ tptp.sup_sup_int @t66) @t67)) % 0.43/1.01 (define @t561 () (= @t66 @t560)) % 0.43/1.01 (define @t562 () (and @t561 @t559)) % 0.43/1.01 (define @t563 () (not @t71)) % 0.43/1.01 (define @t564 () (or @t563 @t562)) % 0.43/1.01 (define @t565 () (not (= @t67 @t66))) % 0.43/1.01 (define @t566 () (and @t561 @t565)) % 0.43/1.01 (define @t567 () (= @t452 (_ @t521 @t67))) % 0.43/1.01 (define @t568 () (@list @t452)) % 0.43/1.01 (define @t569 () (not (= @t452 @t67))) % 0.43/1.01 (define @t570 () (and @t567 @t569)) % 0.43/1.01 (define @t571 () (lambda @t568 @t570)) % 0.43/1.01 (define @t572 () (_ @t522 @t67)) % 0.43/1.01 (define @t573 () (=> @t71 (_ @t572 @t66))) % 0.43/1.01 (define @t574 () (forall @t73 @t573)) % 0.43/1.01 (define @t575 () (and @t545 @t555)) % 0.43/1.01 (define @t576 () (or @t548 @t575)) % 0.43/1.01 (define @t577 () (_ (_ tptp.sup_sup_int @t67) @t66)) % 0.43/1.01 (define @t578 () (= @t67 @t577)) % 0.43/1.01 (define @t579 () (and @t578 @t559)) % 0.43/1.01 (define @t580 () (not @t76)) % 0.43/1.01 (define @t581 () (or @t580 @t579)) % 0.43/1.01 (define @t582 () (= @t452 (_ @t521 @t66))) % 0.43/1.01 (define @t583 () (not (= @t452 @t66))) % 0.43/1.01 (define @t584 () (and @t582 @t583)) % 0.43/1.01 (define @t585 () (lambda @t568 @t584)) % 0.43/1.01 (define @t586 () (_ @t522 @t66)) % 0.43/1.01 (define @t587 () (=> @t76 (_ @t586 @t67))) % 0.43/1.01 (define @t588 () (forall @t73 @t587)) % 0.43/1.01 (define @t589 () (and @t64 @t588 @t574 @t56)) % 0.43/1.01 (define @t590 () (= @t62 @t589)) % 0.43/1.01 (define @t591 () (tptp.binary717961607le_T_a tptp.t1 tptp.x tptp.t2)) % 0.43/1.01 (define @t592 () (tptp.binary1721989714Tree_a tptp.h @t591)) % 0.43/1.01 (define @t593 () (tptp.h @t65)) % 0.43/1.01 (define @t594 () (tptp.h tptp.x)) % 0.43/1.01 (define @t595 () (not (= @t594 @t593))) % 0.43/1.01 (define @t596 () (tptp.binary945792244etOf_a tptp.t1)) % 0.43/1.01 (define @t597 () (forall @t73 (or (not (tptp.member_a @t65 @t596)) (and (= @t594 (tptp.sup_sup_int @t594 @t593)) @t595)))) % 0.43/1.01 (define @t598 () (and (tptp.binary1721989714Tree_a tptp.h tptp.t1) @t597 (forall @t73 (or (not (tptp.member_a @t65 (tptp.binary945792244etOf_a tptp.t2))) (and (= @t593 (tptp.sup_sup_int @t593 @t594)) @t595))) (tptp.binary1721989714Tree_a tptp.h tptp.t2))) % 0.43/1.01 (define @t599 () (= @t592 @t598)) % 0.43/1.01 (define @t600 () (@list false false)) % 0.43/1.01 (define @t601 () (@list false)) % 0.43/1.01 (define @t602 () (tptp.member_a tptp.w @t596)) % 0.43/1.01 (define @t603 () (tptp.h @t525)) % 0.43/1.01 (define @t604 () (tptp.h tptp.e)) % 0.43/1.01 (define @t605 () (= @t604 @t603)) % 0.43/1.01 (define @t606 () (_ tptp.h @t525)) % 0.43/1.01 (define @t607 () (= @t11 @t606)) % 0.43/1.01 (define @t608 () (lambda @t526 @t607)) % 0.43/1.01 (define @t609 () (@purify @t608)) % 0.43/1.01 (define @t610 () (_ @t609 @t525)) % 0.43/1.01 (define @t611 () (= @t607 @t610)) % 0.43/1.01 (define @t612 () (_ @t608 @t525)) % 0.43/1.01 (define @t613 () (= @t610 @t612)) % 0.43/1.01 (define @t614 () (forall @t526 @t613)) % 0.43/1.01 (define @t615 () (@list tptp.w)) % 0.43/1.01 (define @t616 () (_ @t218 @t135)) % 0.43/1.01 (define @t617 () (tptp.collect_a @t218)) % 0.43/1.01 (define @t618 () (tptp.member_a @t135 @t617)) % 0.43/1.01 (define @t619 () (_ tptp.collect_a @t609)) % 0.43/1.01 (define @t620 () (tptp.collect_a @t609)) % 0.43/1.01 (define @t621 () (tptp.member_a tptp.w @t620)) % 0.43/1.01 (define @t622 () (lambda @t526 (= @t606 @t11))) % 0.43/1.01 (define @t623 () (lambda @t73 (_ tptp.collect_a (lambda @t526 (= @t606 (_ tptp.h @t65)))))) % 0.43/1.01 (define @t624 () (_ @t609 tptp.w)) % 0.43/1.01 (define @t625 () (= @t621 @t624)) % 0.43/1.01 (define @t626 () (tptp.h tptp.w)) % 0.43/1.01 (define @t627 () (= @t604 @t626)) % 0.43/1.01 (define @t628 () (= @t624 @t627)) % 0.43/1.01 (define @t629 () (= @t594 @t626)) % 0.43/1.01 (define @t630 () (not @t629)) % 0.43/1.01 (define @t631 () (and (= @t594 (tptp.sup_sup_int @t594 @t626)) @t630)) % 0.43/1.01 (define @t632 () (not @t631)) % 0.43/1.01 (define @t633 () (not @t602)) % 0.43/1.01 (define @t634 () (or @t633 @t631)) % 0.43/1.01 (define @t635 () (not @t634)) % 0.43/1.01 (define @t636 () (@list true false)) % 0.43/1.01 (assume @p1 @t3) % 0.43/1.01 (assume @p2 @t7) % 0.43/1.01 (assume @p3 @t8) % 0.43/1.01 (assume @p4 @t9) % 0.43/1.01 (assume @p5 (not (_ (_ tptp.ord_less_int @t11) @t10))) % 0.43/1.01 (assume @p6 (not (_ (_ tptp.ord_less_int @t10) @t11))) % 0.43/1.01 (assume @p7 (_ @t2 @t12)) % 0.43/1.01 (assume @p8 (= @t10 @t11)) % 0.43/1.01 (assume @p9 (forall (@list @t18 @t16 @t14 @t17 @t15 @t13) (= (= @t19 (_ (_ (_ tptp.binary717961607le_T_a @t17) @t15) @t13)) (and (= @t18 @t17) (= @t16 @t15) (= @t14 @t13))))) % 0.43/1.01 (assume @p10 (_ (_ tptp.member_a tptp.x) @t12)) % 0.43/1.01 (assume @p11 (forall @t28 (exists @t27 (forall @t26 (=> @t25 (not @t22)))))) % 0.43/1.01 (assume @p12 (forall @t28 (exists @t27 (forall @t26 (=> @t25 @t29))))) % 0.43/1.01 (assume @p13 (forall @t28 (exists @t27 (forall @t26 (=> @t25 @t30))))) % 0.43/1.01 (assume @p14 (forall @t50 (=> @t49 (=> @t47 (exists @t27 (forall @t26 (=> @t25 @t39))))))) % 0.43/1.01 (assume @p15 (forall @t50 (=> @t49 (=> @t47 (exists @t27 (forall @t26 (=> @t25 @t51))))))) % 0.43/1.01 (assume @p16 (= (_ @t52 @t5) (_ (_ @t4 tptp.e) tptp.t2))) % 0.43/1.01 (assume @p17 (forall @t63 (=> @t62 @t56))) % 0.43/1.01 (assume @p18 (forall @t63 (=> @t62 @t64))) % 0.43/1.01 (assume @p19 @t81) % 0.43/1.01 (assume @p20 (forall @t50 (=> @t85 (=> @t84 (exists @t27 (forall @t26 (=> @t82 @t51))))))) % 0.43/1.01 (assume @p21 (forall @t50 (=> @t85 (=> @t84 (exists @t27 (forall @t26 (=> @t82 @t39))))))) % 0.43/1.01 (assume @p22 (forall @t28 (exists @t27 (forall @t26 (=> @t82 @t30))))) % 0.43/1.01 (assume @p23 (forall @t28 (exists @t27 (forall @t26 (=> @t82 (not @t29)))))) % 0.43/1.01 (assume @p24 (forall @t28 (exists @t27 (forall @t26 (=> @t82 @t22))))) % 0.43/1.01 (assume @p25 (forall (@list @t54 @t86 @t57) (=> (_ @t55 @t86) (= (_ (_ (_ tptp.binary2053421120memb_a @t54) @t57) @t86) (_ @t87 (_ tptp.binary945792244etOf_a @t86)))))) % 0.43/1.01 (assume @p26 (forall (@list @t54 @t88 @t57 @t58 @t53) (and (=> @t93 (= @t90 (_ (_ (_ tptp.binary717961607le_T_a (_ @t89 @t58)) @t57) @t53))) (=> (not @t93) (and (=> @t92 (= @t90 (_ @t60 (_ @t89 @t53)))) (=> (not @t92) (= @t90 (_ (_ @t59 @t88) @t53)))))))) % 0.43/1.01 (assume @p27 (forall @t103 (=> @t102 (=> @t100 @t97)))) % 0.43/1.01 (assume @p28 (forall @t110 (=> @t109 @t107))) % 0.43/1.01 (assume @p29 (forall @t117 (=> @t116 @t114))) % 0.43/1.01 (assume @p30 (forall @t124 (=> @t123 @t121))) % 0.43/1.01 (assume @p31 (forall @t127 (=> @t126 @t107))) % 0.43/1.01 (assume @p32 (forall @t130 (=> @t129 @t114))) % 0.43/1.01 (assume @p33 (forall @t133 (=> @t132 @t121))) % 0.43/1.01 (assume @p34 (forall (@list @t54 @t135 @t134 @t86) (_ (_ (_ (_ tptp.binary670562003pred_a @t54) @t135) @t134) @t86))) % 0.43/1.01 (assume @p35 (forall @t145 (=> (= @t105 @t144) @t143))) % 0.43/1.01 (assume @p36 (forall @t150 (=> (= @t112 @t149) @t148))) % 0.43/1.01 (assume @p37 (forall @t161 (=> (= @t119 @t160) @t159))) % 0.43/1.01 (assume @p38 (forall @t166 (=> (= @t105 @t165) @t164))) % 0.43/1.01 (assume @p39 (forall @t171 (=> (= @t112 @t170) @t169))) % 0.43/1.01 (assume @p40 (forall @t182 (=> (= @t119 @t181) @t180))) % 0.43/1.01 (assume @p41 (forall @t187 (=> (= @t105 @t186) @t185))) % 0.43/1.01 (assume @p42 (forall @t192 (=> (= @t112 @t191) @t190))) % 0.43/1.01 (assume @p43 (forall @t197 (=> (= @t119 @t196) @t195))) % 0.43/1.01 (assume @p44 (forall @t199 (=> @t132 (=> (= @t144 @t151) @t198)))) % 0.43/1.01 (assume @p45 (forall @t201 (=> @t132 (=> (= @t149 @t172) @t200)))) % 0.43/1.01 (assume @p46 (forall @t203 (=> @t126 (=> (= @t160 @t136) @t202)))) % 0.43/1.01 (assume @p47 (forall @t205 (=> @t126 (=> (= @t165 @t151) @t204)))) % 0.43/1.01 (assume @p48 (forall @t207 (=> @t126 (=> (= @t170 @t172) @t206)))) % 0.43/1.01 (assume @p49 (forall @t209 (=> @t129 (=> (= @t181 @t136) @t208)))) % 0.43/1.01 (assume @p50 (forall @t211 (=> @t129 (=> (= @t186 @t151) @t210)))) % 0.43/1.01 (assume @p51 (forall @t213 (=> @t129 (=> (= @t191 @t172) @t212)))) % 0.43/1.01 (assume @p52 (forall @t215 (=> @t132 (=> (= @t196 @t136) @t214)))) % 0.43/1.01 (assume @p53 (forall @t161 (=> (_ @t131 @t160) @t159))) % 0.43/1.01 (assume @p54 (forall @t182 (=> (_ @t131 @t181) @t180))) % 0.43/1.01 (assume @p55 (forall @t145 (=> (_ @t125 @t144) @t143))) % 0.43/1.01 (assume @p56 (forall @t166 (=> (_ @t125 @t165) @t164))) % 0.43/1.01 (assume @p57 (forall @t187 (=> (_ @t125 @t186) @t185))) % 0.43/1.01 (assume @p58 (forall @t150 (=> (_ @t128 @t149) @t148))) % 0.43/1.01 (assume @p59 (forall @t171 (=> (_ @t128 @t170) @t169))) % 0.43/1.01 (assume @p60 (forall @t192 (=> (_ @t128 @t191) @t190))) % 0.43/1.01 (assume @p61 (forall @t197 (=> (_ @t131 @t196) @t195))) % 0.43/1.01 (assume @p62 (forall @t199 (=> @t132 (=> (_ (_ tptp.ord_less_set_a @t144) @t151) @t198)))) % 0.43/1.01 (assume @p63 (forall @t201 (=> @t132 (=> (_ (_ tptp.ord_less_a_o @t149) @t172) @t200)))) % 0.43/1.01 (assume @p64 (forall @t203 (=> @t126 (=> (_ (_ tptp.ord_less_int @t160) @t136) @t202)))) % 0.43/1.01 (assume @p65 (forall @t205 (=> @t126 (=> (_ (_ tptp.ord_less_set_a @t165) @t151) @t204)))) % 0.43/1.01 (assume @p66 (forall @t207 (=> @t126 (=> (_ (_ tptp.ord_less_a_o @t170) @t172) @t206)))) % 0.43/1.01 (assume @p67 (forall @t209 (=> @t129 (=> (_ (_ tptp.ord_less_int @t181) @t136) @t208)))) % 0.43/1.01 (assume @p68 (forall @t211 (=> @t129 (=> (_ (_ tptp.ord_less_set_a @t186) @t151) @t210)))) % 0.43/1.01 (assume @p69 (forall @t213 (=> @t129 (=> (_ (_ tptp.ord_less_a_o @t191) @t172) @t212)))) % 0.43/1.01 (assume @p70 (forall @t215 (=> @t132 (=> (_ (_ tptp.ord_less_int @t196) @t136) @t214)))) % 0.43/1.01 (assume @p71 (forall @t216 (exists (@list @t138) (_ (_ tptp.ord_less_int @t138) @t94)))) % 0.43/1.01 (assume @p72 (forall @t216 (exists (@list @t217) (_ @t98 @t217)))) % 0.43/1.01 (assume @p73 @t225) % 0.43/1.01 (assume @p74 (forall @t228 (= (_ tptp.collect_a (lambda @t73 @t227)) @t226))) % 0.43/1.01 (assume @p75 (forall @t233 (=> (forall @t232 (= (_ @t218 @t231) (_ @t229 @t231))) (= @t220 @t230)))) % 0.43/1.01 (assume @p76 (forall @t103 (= @t102 (or @t99 @t97)))) % 0.43/1.01 (assume @p77 (forall @t127 (=> @t126 (not @t109)))) % 0.43/1.01 (assume @p78 (forall @t130 (=> @t129 (not @t116)))) % 0.43/1.01 (assume @p79 (forall @t133 (=> @t132 (not @t123)))) % 0.43/1.01 (assume @p80 (forall @t238 (=> @t237 (not (= @t235 @t234))))) % 0.43/1.01 (assume @p81 (forall @t243 (=> @t242 (not (= @t240 @t239))))) % 0.43/1.01 (assume @p82 (forall @t103 (=> @t99 @t102))) % 0.43/1.01 (assume @p83 (forall @t238 (=> @t237 (not @t245)))) % 0.43/1.01 (assume @p84 (forall @t243 (=> @t242 (not @t247)))) % 0.43/1.01 (assume @p85 (forall @t103 (=> @t99 @t248))) % 0.43/1.01 (assume @p86 (forall @t250 (=> @t237 (=> (_ @t244 @t249) (_ @t236 @t249))))) % 0.43/1.01 (assume @p87 (forall @t252 (=> @t242 (=> (_ @t246 @t251) (_ @t241 @t251))))) % 0.43/1.01 (assume @p88 (forall @t254 (=> @t99 (=> (_ @t96 @t253) (_ @t98 @t253))))) % 0.43/1.01 (assume @p89 (forall @t103 (or @t99 @t101 @t97))) % 0.43/1.01 (assume @p90 (forall @t255 (not (_ @t236 @t235)))) % 0.43/1.01 (assume @p91 (forall @t256 (not (_ @t241 @t240)))) % 0.43/1.01 (assume @p92 (forall @t216 (not (_ @t98 @t94)))) % 0.43/1.01 (assume @p93 (forall @t259 (=> @t106 @t258))) % 0.43/1.01 (assume @p94 (forall @t262 (=> @t113 @t261))) % 0.43/1.01 (assume @p95 (forall @t265 (=> @t120 @t264))) % 0.43/1.01 (assume @p96 (forall @t259 (=> @t126 (=> (= @t104 @t151) @t257)))) % 0.43/1.01 (assume @p97 (forall @t262 (=> @t129 (=> (= @t111 @t172) @t260)))) % 0.43/1.01 (assume @p98 (forall @t265 (=> @t132 (=> (= @t118 @t136) @t263)))) % 0.43/1.01 (assume @p99 (forall @t110 (=> @t109 (not @t126)))) % 0.43/1.01 (assume @p100 (forall @t117 (=> @t116 (not @t129)))) % 0.43/1.01 (assume @p101 (forall @t124 (=> @t123 (not @t132)))) % 0.43/1.01 (assume @p102 (forall (@list @t95 @t94) (=> @t248 (= @t100 @t101)))) % 0.43/1.01 (assume @p103 (forall @t238 (=> @t237 (not (= @t234 @t235))))) % 0.43/1.01 (assume @p104 (forall @t243 (=> @t242 (not (= @t239 @t240))))) % 0.43/1.01 (assume @p105 (forall @t103 (=> @t99 (not (= @t95 @t94))))) % 0.43/1.01 (assume @p106 (forall (@list @t235 @t234 @t266) (=> @t237 (=> @t245 @t266)))) % 0.43/1.01 (assume @p107 (forall (@list @t240 @t239 @t266) (=> @t242 (=> @t247 @t266)))) % 0.43/1.01 (assume @p108 (forall (@list @t94 @t95 @t266) (=> @t99 (=> @t97 @t266)))) % 0.43/1.01 (assume @p109 (forall @t103 (=> @t100 (=> @t102 @t97)))) % 0.43/1.01 (assume @p110 (forall @t267 (not (_ @t125 @t105)))) % 0.43/1.01 (assume @p111 (forall @t268 (not (_ @t128 @t112)))) % 0.43/1.01 (assume @p112 (forall @t269 (not (_ @t131 @t119)))) % 0.43/1.01 (assume @p113 (forall @t259 (=> @t126 @t258))) % 0.43/1.01 (assume @p114 (forall @t262 (=> @t129 @t261))) % 0.43/1.01 (assume @p115 (forall @t265 (=> @t132 @t264))) % 0.43/1.01 (assume @p116 (forall (@list @t270 @t119 @t118) (=> (forall @t275 (=> (_ (_ tptp.ord_less_int @t272) @t271) @t274)) (=> (forall (@list @t272) (_ @t273 @t272)) (=> (forall @t275 (=> (_ (_ @t270 @t271) @t272) @t274)) (_ (_ @t270 @t119) @t118)))))) % 0.43/1.01 (assume @p117 (forall @t279 (=> @t109 (=> @t278 @t277)))) % 0.43/1.01 (assume @p118 (forall (@list @t111 @t112 @t172) (=> @t116 (=> (_ @t280 @t111) (_ @t280 @t112))))) % 0.43/1.01 (assume @p119 (forall @t284 (=> @t123 (=> @t283 @t282)))) % 0.43/1.01 (assume @p120 (forall @t103 (= @t100 (or @t97 @t101)))) % 0.43/1.01 (assume @p121 (forall (@list @t54 @t88) (= (_ @t89 tptp.binary476621312_Tip_a) (_ (_ (_ tptp.binary717961607le_T_a tptp.binary476621312_Tip_a) @t88) tptp.binary476621312_Tip_a)))) % 0.43/1.01 (assume @p122 @t286) % 0.43/1.01 (assume @p123 @t287) % 0.43/1.01 (assume @p124 (forall (@list @t218 @t291 @t290 @t288) (= (_ @t289 (_ (_ (_ tptp.binary717961607le_T_a @t291) @t290) @t288)) (and (_ @t289 @t291) (_ @t218 @t290) (_ @t289 @t288))))) % 0.43/1.01 (assume @p125 (forall @t292 (_ @t289 tptp.binary476621312_Tip_a))) % 0.43/1.01 (assume @p126 (forall (@list @t58 @t57 @t53) (= (_ tptp.binary945792244etOf_a @t61) (_ (_ tptp.sup_sup_set_a (_ (_ tptp.sup_sup_set_a @t75) @t69)) @t294)))) % 0.43/1.01 (assume @p127 (= @t295 tptp.bot_bot_set_a)) % 0.43/1.01 (assume @p128 (forall @t268 (= (not @t296) (_ (_ tptp.ord_less_a_o tptp.bot_bot_a_o) @t112)))) % 0.43/1.01 (assume @p129 (forall @t267 (= (not @t297) (_ (_ tptp.ord_less_set_a tptp.bot_bot_set_a) @t105)))) % 0.43/1.01 (assume @p130 (forall @t268 (not (_ @t128 tptp.bot_bot_a_o)))) % 0.43/1.01 (assume @p131 (forall @t267 (not (_ @t125 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p132 (forall @t298 (not (= tptp.binary476621312_Tip_a @t19)))) % 0.43/1.01 (assume @p133 (forall (@list @t300 @t299) (=> (_ @t300 tptp.binary476621312_Tip_a) (=> (forall (@list @t303 @t302 @t301) (=> (_ @t300 @t303) (=> (_ @t300 @t301) (_ @t300 (_ (_ (_ tptp.binary717961607le_T_a @t303) @t302) @t301))))) (_ @t300 @t299))))) % 0.43/1.01 (assume @p134 (forall (@list @t307) (=> (not (= @t307 tptp.binary476621312_Tip_a)) (not (forall (@list @t306 @t305 @t304) (not (= @t307 (_ (_ (_ tptp.binary717961607le_T_a @t306) @t305) @t304)))))))) % 0.43/1.01 (assume @p135 (forall (@list @t54) (_ @t55 tptp.binary476621312_Tip_a))) % 0.43/1.01 (assume @p136 (forall @t314 (= @t313 @t309))) % 0.43/1.01 (assume @p137 (forall @t320 (= (_ @t316 @t319) @t317))) % 0.43/1.01 (assume @p138 (forall (@list @t315 @t226) (= (_ (_ tptp.sup_sup_set_a @t319) @t226) (_ @t321 @t226)))) % 0.43/1.01 (assume @p139 (forall @t326 (=> @t325 (= (_ @t311 @t323) @t322)))) % 0.43/1.01 (assume @p140 (forall @t332 @t331)) % 0.43/1.01 (assume @p141 (forall (@list @t135 @t315 @t333) (= (_ (_ tptp.sup_sup_set_a @t335) @t333) (_ @t308 @t334)))) % 0.43/1.01 (assume @p142 (forall @t292 (= (= tptp.bot_bot_set_a @t220) @t337))) % 0.43/1.01 (assume @p143 (forall @t292 (= @t338 @t337))) % 0.43/1.01 (assume @p144 (forall @t228 (= (forall @t73 (not @t227)) @t339))) % 0.43/1.01 (assume @p145 (forall (@list @t340) (not (_ @t341 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p146 (forall @t342 (= (_ @t293 @t327) @t327))) % 0.43/1.01 (assume @p147 (forall @t347 (= @t346 (or @t344 @t343)))) % 0.43/1.01 (assume @p148 (forall @t351 (=> (=> (not @t350) @t344) @t349))) % 0.43/1.01 (assume @p149 (forall @t355 (= @t354 (or @t353 @t352)))) % 0.43/1.01 (assume @p150 (forall @t357 (=> (=> @t356 @t353) @t354))) % 0.43/1.01 (assume @p151 (forall @t320 (= (_ @t358 @t315) @t322))) % 0.43/1.01 (assume @p152 (forall @t355 (= @t359 (and @t353 @t356)))) % 0.43/1.01 (assume @p153 (forall @t355 (=> @t353 (=> @t356 @t359)))) % 0.43/1.01 (assume @p154 (forall @t360 (_ @t221 @t310))) % 0.43/1.01 (assume @p155 (forall @t320 (= (= @t317 tptp.bot_bot_set_a) (and @t339 @t361)))) % 0.43/1.01 (assume @p156 (forall @t228 (= (_ @t311 @t226) tptp.bot_bot_set_a))) % 0.43/1.01 (assume @p157 (forall @t228 (= (_ (_ tptp.minus_minus_set_a tptp.bot_bot_set_a) @t226) tptp.bot_bot_set_a))) % 0.43/1.01 (assume @p158 (forall @t228 (= (_ @t311 tptp.bot_bot_set_a) @t226))) % 0.43/1.01 (assume @p159 (forall @t362 (= (_ @t316 @t335) (_ @t308 @t317)))) % 0.43/1.01 (assume @p160 (= tptp.bot_bot_set_a (_ tptp.collect_a tptp.bot_bot_a_o))) % 0.43/1.01 (assume @p161 (forall @t228 (not (_ @t363 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p162 (forall @t228 (= (exists @t73 @t227) @t364))) % 0.43/1.01 (assume @p163 (forall @t228 (=> (forall (@list @t365) (not @t366)) @t339))) % 0.43/1.01 (assume @p164 (forall (@list @t226 @t135) (=> @t339 @t367))) % 0.43/1.01 (assume @p165 (forall @t360 (not (_ @t221 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p166 (forall @t314 (=> @t343 (exists @t369 (and (= @t226 (_ @t308 @t368)) (not (_ @t221 @t368))))))) % 0.43/1.01 (assume @p167 (forall @t372 (= (_ @t293 (_ @t371 @t226)) (_ @t371 @t327)))) % 0.43/1.01 (assume @p168 (forall (@list @t135 @t226 @t134 @t315) (=> @t367 (=> (not (_ @t374 @t315)) (= (= @t309 @t348) (and (=> @t344 @t376) (=> @t375 (exists (@list @t373) (and (= @t226 (_ @t345 @t373)) (not (_ @t374 @t373)) (= @t315 (_ @t308 @t373)) (not (_ @t221 @t373))))))))))) % 0.43/1.01 (assume @p169 (forall @t314 (=> @t343 (= @t309 @t226)))) % 0.43/1.01 (assume @p170 (forall @t326 (=> @t325 (=> @t377 (= (= @t327 @t323) @t376))))) % 0.43/1.01 (assume @p171 (forall @t342 (=> @t324 (not (forall @t369 (=> (= @t226 (_ @t293 @t368)) (_ @t87 @t368))))))) % 0.43/1.01 (assume @p172 (forall @t351 (=> @t350 @t349))) % 0.43/1.01 (assume @p173 (forall (@list @t135 @t315) (_ @t221 @t335))) % 0.43/1.01 (assume @p174 (forall @t347 (=> @t346 (=> @t375 @t343)))) % 0.43/1.01 (assume @p175 (forall @t379 (= @t378 (_ @t321 (_ @t316 @t333))))) % 0.43/1.01 (assume @p176 (forall @t320 (= (_ @t316 @t317) @t317))) % 0.43/1.01 (assume @p177 (= tptp.sup_sup_set_a (lambda @t382 (_ (_ tptp.sup_sup_set_a @t381) @t380)))) % 0.43/1.01 (assume @p178 (forall @t228 (= (_ @t316 @t226) @t226))) % 0.43/1.01 (assume @p179 (forall @t379 (= (_ (_ tptp.sup_sup_set_a @t317) @t333) @t378))) % 0.43/1.01 (assume @p180 (forall @t385 (= (forall @t73 (=> @t384 @t336)) (and (forall @t73 (=> @t227 @t336)) (forall @t73 (=> @t383 @t336)))))) % 0.43/1.01 (assume @p181 (forall @t385 (= (exists @t73 (and @t384 @t336)) (or (exists @t73 (and @t227 @t336)) (exists @t73 (and @t383 @t336)))))) % 0.43/1.01 (assume @p182 (forall @t357 (=> @t352 @t354))) % 0.43/1.01 (assume @p183 (forall @t355 (=> @t353 @t354))) % 0.43/1.01 (assume @p184 (forall @t355 (=> @t354 (=> (not @t353) @t352)))) % 0.43/1.01 (assume @p185 (forall @t320 (=> @t387 (exists (@list @t386) (_ (_ tptp.member_a @t386) @t319))))) % 0.43/1.01 (assume @p186 (forall @t355 (=> @t359 @t356))) % 0.43/1.01 (assume @p187 (forall @t355 (=> @t359 @t353))) % 0.43/1.01 (assume @p188 (forall @t355 (=> @t359 (not @t388)))) % 0.43/1.01 (assume @p189 (forall (@list @t135 @t134) (=> (= @t310 @t389) @t344))) % 0.43/1.01 (assume @p190 (forall @t314 (not (= @t309 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p191 (forall (@list @t135 @t134 @t340 @t390) (= (= (_ @t308 @t389) (_ (_ tptp.insert_a @t340) (_ (_ tptp.insert_a @t390) tptp.bot_bot_set_a))) (or (and (= @t135 @t340) (= @t134 @t390)) (and (= @t135 @t390) (= @t134 @t340)))))) % 0.43/1.01 (assume @p192 (forall @t393 (= @t392 @t391))) % 0.43/1.01 (assume @p193 (forall @t393 (=> @t392 @t391))) % 0.43/1.01 (assume @p194 (forall @t228 (= (_ @t316 tptp.bot_bot_set_a) @t226))) % 0.43/1.01 (assume @p195 (forall (@list @t315) (= (_ @t394 @t315) @t315))) % 0.43/1.01 (assume @p196 (forall @t332 (and @t331 (=> @t377 (= @t329 (_ @t293 @t322)))))) % 0.43/1.01 (assume @p197 (forall @t379 (= (_ (_ tptp.minus_minus_set_a @t317) @t333) (_ (_ tptp.sup_sup_set_a (_ @t311 @t333)) (_ @t318 @t333))))) % 0.43/1.01 (assume @p198 (forall @t326 (= (= @t294 @t317) @t397))) % 0.43/1.01 (assume @p199 (forall (@list @t226 @t315 @t57) (= (= @t317 @t294) @t397))) % 0.43/1.01 (assume @p200 (= tptp.insert_a (lambda @t400 (_ (_ tptp.sup_sup_set_a (_ (_ tptp.insert_a @t399) tptp.bot_bot_set_a)) @t398)))) % 0.43/1.01 (assume @p201 (forall @t342 (=> @t325 (= (_ @t328 @t294) @t226)))) % 0.43/1.01 (assume @p202 (forall @t362 (= @t401 (_ (_ tptp.minus_minus_set_a @t312) @t315)))) % 0.43/1.01 (assume @p203 (forall @t314 (=> @t343 (= @t313 @t226)))) % 0.43/1.01 (assume @p204 (forall @t362 (= @t401 (_ @t358 @t310)))) % 0.43/1.01 (assume @p205 (forall @t268 (= (_ @t402 tptp.bot_bot_a_o) @t112))) % 0.43/1.01 (assume @p206 (forall @t267 (= (_ @t403 tptp.bot_bot_set_a) @t105))) % 0.43/1.01 (assume @p207 (forall @t130 (= (= tptp.bot_bot_a_o @t405) @t404))) % 0.43/1.01 (assume @p208 (forall @t127 (= (= tptp.bot_bot_set_a @t407) @t406))) % 0.43/1.01 (assume @p209 (forall @t268 (= (_ @t408 @t112) @t112))) % 0.43/1.01 (assume @p210 (forall @t267 (= (_ @t394 @t105) @t105))) % 0.43/1.01 (assume @p211 (forall @t130 (= (= @t405 tptp.bot_bot_a_o) @t404))) % 0.43/1.01 (assume @p212 (forall @t127 (= (= @t407 tptp.bot_bot_set_a) @t406))) % 0.43/1.01 (assume @p213 (forall @t243 (= (= @t411 tptp.bot_bot_a_o) @t409))) % 0.43/1.01 (assume @p214 (forall @t238 (= (= @t414 tptp.bot_bot_set_a) @t412))) % 0.43/1.01 (assume @p215 (forall @t269 (= (_ @t415 @t119) @t119))) % 0.43/1.01 (assume @p216 (forall @t268 (= (_ @t402 @t112) @t112))) % 0.43/1.01 (assume @p217 (forall @t267 (= (_ @t403 @t105) @t105))) % 0.43/1.01 (assume @p218 (forall @t216 (= (_ @t416 @t94) @t94))) % 0.43/1.01 (assume @p219 (forall @t256 (= (_ @t410 @t240) @t240))) % 0.43/1.01 (assume @p220 (forall @t255 (= (_ @t413 @t235) @t235))) % 0.43/1.01 (assume @p221 (forall @t133 (= (_ @t415 @t417) @t417))) % 0.43/1.01 (assume @p222 (forall @t130 (= (_ @t402 @t405) @t405))) % 0.43/1.01 (assume @p223 (forall @t127 (= (_ @t403 @t407) @t407))) % 0.43/1.01 (assume @p224 (forall @t103 (= (_ @t416 @t418) @t418))) % 0.43/1.01 (assume @p225 (forall @t243 (= (_ @t410 @t411) @t411))) % 0.43/1.01 (assume @p226 (forall @t238 (= (_ @t413 @t414) @t414))) % 0.43/1.01 (assume @p227 (forall @t133 (= (_ @t419 @t118) @t417))) % 0.43/1.01 (assume @p228 (forall @t130 (= (_ @t420 @t111) @t405))) % 0.43/1.01 (assume @p229 (forall @t127 (= (_ @t421 @t104) @t407))) % 0.43/1.01 (assume @p230 (forall @t256 (= (_ @t408 @t240) @t240))) % 0.43/1.01 (assume @p231 (forall @t255 (= (_ @t394 @t235) @t235))) % 0.43/1.01 (assume @p232 (forall @t256 (= (_ @t410 tptp.bot_bot_a_o) @t240))) % 0.43/1.01 (assume @p233 (forall @t255 (= (_ @t413 tptp.bot_bot_set_a) @t235))) % 0.43/1.01 (assume @p234 (forall @t243 (= (= tptp.bot_bot_a_o @t411) @t409))) % 0.43/1.01 (assume @p235 (forall @t238 (= (= tptp.bot_bot_set_a @t414) @t412))) % 0.43/1.01 (assume @p236 (forall (@list @t226 @t315 @t340) (=> @t387 @t388))) % 0.43/1.01 (assume @p237 (forall @t379 (=> @t387 (=> (_ (_ tptp.ord_less_set_a @t315) @t333) (_ @t363 @t333))))) % 0.43/1.01 (assume @p238 (forall @t254 (= @t423 (_ @t422 (_ @t416 @t253))))) % 0.43/1.01 (assume @p239 (forall @t252 (= @t425 (_ @t424 (_ @t410 @t251))))) % 0.43/1.01 (assume @p240 (forall @t250 (= @t427 (_ @t426 (_ @t413 @t249))))) % 0.43/1.01 (assume @p241 (forall @t254 (= (_ (_ tptp.sup_sup_int @t418) @t253) @t423))) % 0.43/1.01 (assume @p242 (forall @t252 (= (_ (_ tptp.sup_sup_a_o @t411) @t251) @t425))) % 0.43/1.01 (assume @p243 (forall @t250 (= (_ (_ tptp.sup_sup_set_a @t414) @t249) @t427))) % 0.43/1.01 (assume @p244 (= tptp.sup_sup_int (lambda (@list @t428 @t429) (_ (_ tptp.sup_sup_int @t429) @t428)))) % 0.43/1.01 (assume @p245 (= tptp.sup_sup_a_o (lambda (@list @t431 @t432 @t430) (_ (_ (_ tptp.sup_sup_a_o @t432) @t431) @t430)))) % 0.43/1.01 (assume @p246 (= tptp.sup_sup_set_a (lambda (@list @t433 @t434) (_ (_ tptp.sup_sup_set_a @t434) @t433)))) % 0.43/1.01 (assume @p247 (forall (@list @t438 @t435 @t119 @t118) (=> (= @t438 (_ @t436 @t119)) (= (_ (_ tptp.sup_sup_int @t438) @t118) @t437)))) % 0.43/1.01 (assume @p248 (forall (@list @t442 @t439 @t112 @t111) (=> (= @t442 (_ @t440 @t112)) (= (_ (_ tptp.sup_sup_a_o @t442) @t111) @t441)))) % 0.43/1.01 (assume @p249 (forall (@list @t226 @t443 @t105 @t104) (=> (= @t226 (_ @t444 @t105)) (= (_ @t316 @t104) @t445)))) % 0.43/1.01 (assume @p250 (forall (@list @t446 @t435 @t118 @t119) (=> (= @t446 (_ @t436 @t118)) (= (_ @t415 @t446) @t437)))) % 0.43/1.01 (assume @p251 (forall (@list @t447 @t439 @t111 @t112) (=> (= @t447 (_ @t440 @t111)) (= (_ @t402 @t447) @t441)))) % 0.43/1.01 (assume @p252 (forall (@list @t315 @t443 @t104 @t105) (=> (= @t315 (_ @t444 @t104)) (= (_ @t403 @t315) @t445)))) % 0.43/1.01 (assume @p253 (forall @t265 (= (_ @t419 @t136) (_ @t415 @t448)))) % 0.43/1.01 (assume @p254 (forall @t262 (= (_ @t420 @t172) (_ @t402 (_ (_ tptp.sup_sup_a_o @t111) @t172))))) % 0.43/1.01 (assume @p255 (forall @t259 (= (_ @t421 @t151) @t451))) % 0.43/1.01 (assume @p256 (= tptp.sup_sup_int (lambda (@list @t452 @t453) (_ (_ tptp.sup_sup_int @t453) @t452)))) % 0.43/1.01 (assume @p257 (= tptp.sup_sup_a_o (lambda (@list @t454 @t455 @t430) (_ (_ (_ tptp.sup_sup_a_o @t455) @t454) @t430)))) % 0.43/1.01 (assume @p258 (= tptp.sup_sup_set_a (lambda (@list @t456 @t457) (_ (_ tptp.sup_sup_set_a @t457) @t456)))) % 0.43/1.01 (assume @p259 (forall @t279 (= (_ @t449 (_ @t403 @t151)) @t451))) % 0.43/1.01 (assume @p260 (forall (@list @t235 @t105 @t104) (=> (_ @t236 @t105) @t458))) % 0.43/1.01 (assume @p261 (forall (@list @t94 @t119 @t118) (=> (_ @t98 @t119) @t459))) % 0.43/1.01 (assume @p262 (forall (@list @t235 @t104 @t105) (=> (_ @t236 @t104) @t458))) % 0.43/1.01 (assume @p263 (forall (@list @t94 @t118 @t119) (=> (_ @t98 @t118) @t459))) % 0.43/1.01 (assume @p264 (forall (@list @t104 @t151 @t105) (=> (_ (_ tptp.ord_less_set_a @t450) @t105) (not (=> @t109 (not @t277)))))) % 0.43/1.01 (assume @p265 (forall (@list @t118 @t136 @t119) (=> (_ (_ tptp.ord_less_int @t448) @t119) (not (=> @t123 (not @t282)))))) % 0.43/1.01 (assume @p266 (forall (@list @t151 @t105 @t104) (=> @t277 @t460))) % 0.43/1.01 (assume @p267 (forall (@list @t136 @t119 @t118) (=> @t282 @t461))) % 0.43/1.01 (assume @p268 (forall (@list @t151 @t104 @t105) (=> @t278 @t460))) % 0.43/1.01 (assume @p269 (forall (@list @t136 @t118 @t119) (=> @t283 @t461))) % 0.43/1.01 (assume @p270 (=> @t8 @t286)) % 0.43/1.01 (assume @p271 (=> @t9 @t287)) % 0.43/1.01 (assume @p272 (=> (_ @t6 tptp.binary476621312_Tip_a) (= (_ tptp.binary945792244etOf_a (_ @t52 tptp.binary476621312_Tip_a)) (_ (_ tptp.sup_sup_set_a (_ (_ tptp.minus_minus_set_a @t295) @t12)) @t285)))) % 0.43/1.01 (assume @p273 (forall @t360 (= (_ tptp.collect_a (lambda @t73 @t462)) @t310))) % 0.43/1.01 (assume @p274 (forall @t360 (= (_ tptp.collect_a (_ (lambda (@list @t464 @t463) (= @t464 @t463)) @t135)) @t310))) % 0.43/1.01 (assume @p275 (= tptp.bot_bot_set_a (_ tptp.collect_a (lambda @t73 false)))) % 0.43/1.01 (assume @p276 (= tptp.sup_sup_set_a (lambda @t382 (_ tptp.collect_a (_ (_ tptp.sup_sup_a_o @t468) @t466))))) % 0.43/1.01 (assume @p277 (forall @t471 (and (=> @t219 (= @t469 @t310)) (=> @t470 (= @t469 tptp.bot_bot_set_a))))) % 0.43/1.01 (assume @p278 (forall @t233 (= (_ tptp.collect_a (lambda @t73 (or @t336 (_ @t229 @t65)))) (_ (_ tptp.sup_sup_set_a @t220) @t230)))) % 0.43/1.01 (assume @p279 (forall @t471 (and (=> @t219 (= @t472 @t310)) (=> @t470 (= @t472 tptp.bot_bot_set_a))))) % 0.43/1.01 (assume @p280 (= tptp.ord_less_set_a (lambda @t382 (_ (_ tptp.ord_less_a_o @t468) @t466)))) % 0.43/1.01 (assume @p281 (forall @t224 (= (_ @t308 @t220) (_ tptp.collect_a (lambda (@list @t473) (=> (not (= @t473 @t135)) (_ @t218 @t473))))))) % 0.43/1.01 (assume @p282 (= tptp.insert_a (lambda (@list @t399 @t381) (_ tptp.collect_a (lambda @t73 (or @t474 @t465)))))) % 0.43/1.01 (assume @p283 (= tptp.minus_minus_set_a (lambda @t382 (_ tptp.collect_a (lambda @t73 (and @t467 (not @t465))))))) % 0.43/1.01 (assume @p284 (forall @t475 (= (_ tptp.the_elem_a @t294) @t57))) % 0.43/1.01 (assume @p285 (= tptp.bot_bot_a_o (lambda @t73 (_ @t70 tptp.bot_bot_set_a)))) % 0.43/1.01 (assume @p286 (forall (@list @t477 @t476) (= (_ (_ tptp.sup_sup_a_o (lambda @t73 (_ @t70 @t477))) (lambda @t73 (_ @t70 @t476))) (lambda @t73 (_ @t70 (_ (_ tptp.sup_sup_set_a @t477) @t476)))))) % 0.43/1.01 (assume @p287 (forall @t292 (= @t338 (= @t218 tptp.bot_bot_a_o)))) % 0.43/1.01 (assume @p288 (forall @t475 (_ tptp.is_singleton_a @t294))) % 0.43/1.01 (assume @p289 (forall @t228 (=> @t364 (=> (forall (@list @t231 @t365) (=> (_ (_ tptp.member_a @t231) @t226) (=> @t366 (= @t231 @t365)))) @t478)))) % 0.43/1.01 (assume @p290 (= tptp.is_singleton_a (lambda @t480 (exists @t73 (= @t380 @t479))))) % 0.43/1.01 (assume @p291 (forall @t228 (=> @t478 (not (forall @t232 (not (= @t226 (_ (_ tptp.insert_a @t231) tptp.bot_bot_set_a)))))))) % 0.43/1.01 (assume @p292 (forall @t265 (=> @t132 (_ @t483 (_ @t481 @t136))))) % 0.43/1.01 (assume @p293 (forall @t284 (=> @t123 (_ (_ tptp.ord_less_int (_ @t484 @t119)) (_ @t484 @t118))))) % 0.43/1.01 (assume @p294 (forall (@list @t119 @t118 @t485 @t136) (=> @t132 (=> (_ (_ tptp.ord_less_int @t485) @t136) (_ @t483 (_ @t481 @t485)))))) % 0.43/1.01 (assume @p295 (forall (@list @t119 @t118 @t136 @t485) (=> (= (_ @t482 @t118) (_ @t484 @t485)) (= @t132 (_ @t281 @t485))))) % 0.43/1.01 (assume @p296 (forall @t298 (= @t488 (_ (_ tptp.sup_sup_set_a (_ (_ tptp.sup_sup_set_a @t487) (_ (_ tptp.insert_a @t16) tptp.bot_bot_set_a))) @t486)))) % 0.43/1.01 (assume @p297 (forall @t372 (= (_ @t87 (_ (_ tptp.remove_a @t370) @t226)) (and @t324 (not (= @t57 @t370)))))) % 0.43/1.01 (assume @p298 (= (_ tptp.binary256242811Tree_a tptp.binary476621312_Tip_a) tptp.bot_bot_set_a)) % 0.43/1.01 (assume @p299 (forall (@list @t489 @t14 @t18 @t16) (=> (_ @t490 @t486) (_ @t490 @t488)))) % 0.43/1.01 (assume @p300 (forall (@list @t16 @t18 @t14) (_ (_ tptp.member_a @t16) @t488))) % 0.43/1.01 (assume @p301 (forall (@list @t370 @t18 @t16 @t14) (=> (_ @t491 @t487) (_ @t491 @t488)))) % 0.43/1.01 (assume @p302 (forall (@list @t88 @t291) (=> (_ @t493 (_ tptp.binary256242811Tree_a @t291)) (=> (forall (@list @t495) (=> (exists (@list @t494 @t492) @t497) (not (_ @t493 (_ tptp.binary256242811Tree_a @t495))))) (=> (forall (@list @t495 @t492) (not (= @t291 (_ (_ @t496 @t88) @t492)))) (not (forall (@list @t495 @t494 @t492) (=> @t497 (not (_ @t493 (_ tptp.binary256242811Tree_a @t492))))))))))) % 0.43/1.01 (assume @p303 (forall (@list @t501 @t498 @t218 @t499) (=> (= @t501 @t498) (=> (forall @t507 (=> (_ @t506 (_ tptp.binary256242811Tree_a @t498)) (= @t505 @t504))) (= @t502 (_ @t500 @t498)))))) % 0.43/1.01 (assume @p304 (forall (@list @t218 @t501 @t499) (=> @t502 (=> (forall @t507 (=> (_ @t506 (_ tptp.binary256242811Tree_a @t501)) (=> @t505 @t504))) (_ @t500 @t501))))) % 0.43/1.01 (assume @p305 (forall (@list @t226 @t57 @t315) (= (_ @t363 @t323) (and (=> @t330 @t387) (=> @t377 (and (=> @t324 (_ (_ tptp.ord_less_set_a (_ @t311 @t294)) @t315)) (=> @t325 (_ (_ tptp.ord_less_eq_set_a @t226) @t315)))))))) % 0.43/1.01 (assume @p306 (not (_ (_ tptp.ord_less_int (_ tptp.h tptp.w)) @t10))) % 0.43/1.01 (assume @p307 true) % 0.43/1.01 (step @p308 (= tptp.binary670562003pred_a @t512) :rule refl :args (@t512)) % 0.43/1.01 (step @p309 (= tptp.bot_bot_a_o @t513) :rule refl :args (@t513)) % 0.43/1.01 (step @p310 (= tptp.minus_minus_a_o @t516) :rule refl :args (@t516)) % 0.43/1.01 (step @p311 (= tptp.sup_sup_a_o @t519) :rule refl :args (@t519)) % 0.43/1.01 (step @p312 (= tptp.ord_less_set_a @t520) :rule refl :args (@t520)) % 0.43/1.01 (step @p313 (= tptp.ord_less_int @t522) :rule refl :args (@t522)) % 0.43/1.01 (step @p314 (= tptp.sup_sup_set_a @t523) :rule refl :args (@t523)) % 0.43/1.01 (step @p315 (= tptp.insert_a @t524) :rule refl :args (@t524)) % 0.43/1.01 (step @p316 (= tptp.binary504661350_eqs_a @t527) :rule refl :args (@t527)) % 0.43/1.01 (step @p317 (= tptp.minus_minus_set_a @t528) :rule refl :args (@t528)) % 0.43/1.01 (step @p318 (= tptp.is_singleton_a @t529) :rule refl :args (@t529)) % 0.43/1.01 (step @p319 (= tptp.remove_a @t530) :rule refl :args (@t530)) % 0.43/1.01 (step @p320 (= tptp.is_empty_a @t531) :rule refl :args (@t531)) % 0.43/1.01 (step @p321 (= tptp.the_elem_a @t533) :rule refl :args (@t533)) % 0.43/1.01 (step @p322 :rule refl :args (@t534)) % 0.43/1.01 (step @p323 :rule refl :args (@t56)) % 0.43/1.01 (step @p324 :rule cong :premises (@p323 @p322) :args ((= @t56 @t534))) % 0.43/1.01 (step @p325 :rule symm :premises (@p324)) % 0.43/1.01 (step @p326 :rule eq_resolve :premises (@p323 @p325)) % 0.43/1.01 (step @p327 :rule refl :args (@t543)) % 0.43/1.01 (step @p328 :rule refl :args (@t549)) % 0.43/1.01 (step @p329 :rule refl :args (@t550)) % 0.43/1.01 (step @p330 :rule refl :args (@t64)) % 0.43/1.01 (step @p331 :rule cong :premises (@p330 @p329) :args ((= @t64 @t550))) % 0.43/1.01 (step @p332 :rule symm :premises (@p331)) % 0.43/1.01 (step @p333 :rule eq_resolve :premises (@p330 @p332)) % 0.43/1.01 (step @p334 :rule nary_cong :premises (@p333 @p328 @p327 @p326) :args (@t551)) % 0.43/1.01 (step @p335 :rule refl :args ((tptp.binary1721989714Tree_a @t54 @t61))) % 0.43/1.01 (step @p336 :rule refl :args (@t552)) % 0.43/1.01 (step @p337 :rule refl :args (@t54)) % 0.43/1.01 (step @p338 :rule cong :premises (@p337 @p336) :args (@t553)) % 0.43/1.01 (step @p339 :rule trans :premises (@p338 @p335)) % 0.43/1.01 (step @p340 :rule refl :args (@t55)) % 0.43/1.01 (step @p341 :rule ho_cong :premises (@p340 @p336)) % 0.43/1.01 (step @p342 :rule cong :premises (@p341 @p339) :args ((= (_ @t55 @t552) @t553))) % 0.43/1.01 (step @p343 :rule symm :premises (@p342)) % 0.43/1.01 (step @p344 :rule refl :args (@t62)) % 0.43/1.01 (step @p345 :rule eq_resolve :premises (@p344 @p343)) % 0.43/1.01 (step @p346 :rule refl :args (@t61)) % 0.43/1.01 (step @p347 :rule cong :premises (@p346 @p336) :args ((= @t61 @t552))) % 0.43/1.01 (step @p348 :rule symm :premises (@p347)) % 0.43/1.01 (step @p349 :rule eq_resolve :premises (@p346 @p348)) % 0.43/1.01 (step @p350 :rule ho_cong :premises (@p340 @p349)) % 0.43/1.01 (step @p351 :rule trans :premises (@p350 @p345)) % 0.43/1.01 (step @p352 :rule cong :premises (@p351 @p334) :args (@t554)) % 0.43/1.01 (step @p353 :rule cong :premises (@p352) :args ((forall @t63 @t554))) % 0.43/1.01 (step @p354 :rule refl :args (@t56)) % 0.43/1.01 (step @p355 :rule eq-symm :args (@t535 @t536)) % 0.43/1.01 (step @p356 :rule cong :premises (@p355) :args (@t555)) % 0.43/1.01 (step @p357 :rule refl :args (@t539)) % 0.43/1.01 (step @p358 :rule nary_cong :premises (@p357 @p356) :args (@t556)) % 0.43/1.01 (step @p359 :rule refl :args (@t542)) % 0.43/1.01 (step @p360 :rule nary_cong :premises (@p359 @p358) :args (@t557)) % 0.43/1.01 (step @p361 :rule cong :premises (@p360) :args ((forall @t73 @t557))) % 0.43/1.01 (step @p362 :rule refl :args (@t536)) % 0.43/1.01 (step @p363 :rule refl :args (@t67)) % 0.43/1.01 (step @p364 :rule cong :premises (@p363 @p362) :args ((= @t67 @t536))) % 0.43/1.01 (step @p365 :rule symm :premises (@p364)) % 0.43/1.01 (step @p366 :rule eq_resolve :premises (@p363 @p365)) % 0.43/1.01 (step @p367 :rule refl :args (@t535)) % 0.43/1.01 (step @p368 :rule refl :args (@t66)) % 0.43/1.01 (step @p369 :rule cong :premises (@p368 @p367) :args ((= @t66 @t535))) % 0.43/1.01 (step @p370 :rule symm :premises (@p369)) % 0.43/1.01 (step @p371 :rule eq_resolve :premises (@p368 @p370)) % 0.43/1.01 (step @p372 :rule cong :premises (@p371 @p366) :args (@t558)) % 0.43/1.01 (step @p373 :rule cong :premises (@p372) :args (@t559)) % 0.43/1.01 (step @p374 :rule refl :args ((tptp.sup_sup_int @t66 @t67))) % 0.43/1.01 (step @p375 :rule cong :premises (@p367 @p362) :args (@t538)) % 0.43/1.01 (step @p376 :rule trans :premises (@p375 @p374)) % 0.43/1.01 (step @p377 :rule refl :args (tptp.sup_sup_int)) % 0.43/1.01 (step @p378 :rule ho_cong :premises (@p377 @p367)) % 0.43/1.01 (step @p379 :rule ho_cong :premises (@p378 @p362)) % 0.43/1.01 (step @p380 :rule cong :premises (@p379 @p376) :args ((= (_ (_ tptp.sup_sup_int @t535) @t536) @t538))) % 0.43/1.01 (step @p381 :rule symm :premises (@p380)) % 0.43/1.01 (step @p382 :rule refl :args (@t560)) % 0.43/1.01 (step @p383 :rule eq_resolve :premises (@p382 @p381)) % 0.43/1.01 (step @p384 :rule ho_cong :premises (@p377 @p371)) % 0.43/1.01 (step @p385 :rule ho_cong :premises (@p384 @p366)) % 0.43/1.01 (step @p386 :rule trans :premises (@p385 @p383)) % 0.43/1.01 (step @p387 :rule cong :premises (@p371 @p386) :args (@t561)) % 0.43/1.01 (step @p388 :rule nary_cong :premises (@p387 @p373) :args (@t562)) % 0.43/1.01 (step @p389 :rule refl :args ((tptp.member_a @t65 @t69))) % 0.43/1.01 (step @p390 :rule refl :args (@t540)) % 0.43/1.01 (step @p391 :rule refl :args (@t65)) % 0.43/1.01 (step @p392 :rule cong :premises (@p391 @p390) :args (@t541)) % 0.43/1.01 (step @p393 :rule trans :premises (@p392 @p389)) % 0.43/1.01 (step @p394 :rule refl :args (@t70)) % 0.43/1.01 (step @p395 :rule ho_cong :premises (@p394 @p390)) % 0.43/1.01 (step @p396 :rule cong :premises (@p395 @p393) :args ((= (_ @t70 @t540) @t541))) % 0.43/1.01 (step @p397 :rule symm :premises (@p396)) % 0.43/1.01 (step @p398 :rule refl :args (@t71)) % 0.43/1.01 (step @p399 :rule eq_resolve :premises (@p398 @p397)) % 0.43/1.01 (step @p400 :rule refl :args (@t69)) % 0.43/1.01 (step @p401 :rule cong :premises (@p400 @p390) :args ((= @t69 @t540))) % 0.43/1.01 (step @p402 :rule symm :premises (@p401)) % 0.43/1.01 (step @p403 :rule eq_resolve :premises (@p400 @p402)) % 0.43/1.01 (step @p404 :rule ho_cong :premises (@p394 @p403)) % 0.43/1.01 (step @p405 :rule trans :premises (@p404 @p399)) % 0.43/1.01 (step @p406 :rule cong :premises (@p405) :args (@t563)) % 0.43/1.01 (step @p407 :rule nary_cong :premises (@p406 @p388) :args (@t564)) % 0.43/1.01 (step @p408 :rule cong :premises (@p407) :args ((forall @t73 @t564))) % 0.43/1.01 (step @p409 :rule trans :premises (@p408 @p361)) % 0.43/1.01 (step @p410 :rule bool-impl-elim :args (@t71 @t562)) % 0.43/1.01 (step @p411 :rule cong :premises (@p410) :args ((forall @t73 (=> @t71 @t562)))) % 0.43/1.01 (step @p412 :rule trans :premises (@p411 @p409)) % 0.43/1.01 (step @p413 :rule eq-symm :args (@t67 @t66)) % 0.43/1.01 (step @p414 :rule cong :premises (@p413) :args (@t565)) % 0.43/1.01 (step @p415 :rule refl :args (@t561)) % 0.43/1.01 (step @p416 :rule nary_cong :premises (@p415 @p414) :args (@t566)) % 0.43/1.01 (step @p417 :rule beta-reduce :args ((= (_ (lambda @t568 (and @t567 (not (= @t67 @t452)))) @t66) @t566))) % 0.43/1.01 (step @p418 :rule trans :premises (@p417 @p416)) % 0.43/1.01 (step @p419 :rule refl :args (@t66)) % 0.43/1.01 (step @p420 :rule eq-symm :args (@t452 @t67)) % 0.43/1.01 (step @p421 :rule cong :premises (@p420) :args (@t569)) % 0.43/1.01 (step @p422 :rule refl :args (@t567)) % 0.43/1.01 (step @p423 :rule nary_cong :premises (@p422 @p421) :args (@t570)) % 0.43/1.01 (step @p424 :rule cong :premises (@p423) :args (@t571)) % 0.43/1.01 (step @p425 :rule beta-reduce :args ((= @t572 @t571))) % 0.43/1.01 (step @p426 :rule trans :premises (@p425 @p424)) % 0.43/1.01 (step @p427 :rule ho_cong :premises (@p426 @p419)) % 0.43/1.01 (step @p428 :rule trans :premises (@p427 @p418)) % 0.43/1.01 (step @p429 :rule refl :args (@t71)) % 0.43/1.01 (step @p430 :rule cong :premises (@p429 @p428) :args (@t573)) % 0.43/1.01 (step @p431 :rule cong :premises (@p430) :args (@t574)) % 0.43/1.01 (step @p432 :rule trans :premises (@p431 @p412)) % 0.43/1.01 (step @p433 :rule refl :args (@t545)) % 0.43/1.01 (step @p434 :rule nary_cong :premises (@p433 @p356) :args (@t575)) % 0.43/1.01 (step @p435 :rule refl :args (@t548)) % 0.43/1.01 (step @p436 :rule nary_cong :premises (@p435 @p434) :args (@t576)) % 0.43/1.01 (step @p437 :rule cong :premises (@p436) :args ((forall @t73 @t576))) % 0.43/1.01 (step @p438 :rule refl :args ((tptp.sup_sup_int @t67 @t66))) % 0.43/1.01 (step @p439 :rule cong :premises (@p362 @p367) :args (@t544)) % 0.43/1.01 (step @p440 :rule trans :premises (@p439 @p438)) % 0.43/1.01 (step @p441 :rule ho_cong :premises (@p377 @p362)) % 0.43/1.01 (step @p442 :rule ho_cong :premises (@p441 @p367)) % 0.43/1.01 (step @p443 :rule cong :premises (@p442 @p440) :args ((= (_ (_ tptp.sup_sup_int @t536) @t535) @t544))) % 0.43/1.01 (step @p444 :rule symm :premises (@p443)) % 0.43/1.01 (step @p445 :rule refl :args (@t577)) % 0.43/1.01 (step @p446 :rule eq_resolve :premises (@p445 @p444)) % 0.43/1.01 (step @p447 :rule ho_cong :premises (@p377 @p366)) % 0.43/1.01 (step @p448 :rule ho_cong :premises (@p447 @p371)) % 0.43/1.01 (step @p449 :rule trans :premises (@p448 @p446)) % 0.43/1.01 (step @p450 :rule cong :premises (@p366 @p449) :args (@t578)) % 0.43/1.01 (step @p451 :rule nary_cong :premises (@p450 @p373) :args (@t579)) % 0.43/1.01 (step @p452 :rule refl :args ((tptp.member_a @t65 @t75))) % 0.43/1.01 (step @p453 :rule refl :args (@t546)) % 0.43/1.01 (step @p454 :rule cong :premises (@p391 @p453) :args (@t547)) % 0.43/1.01 (step @p455 :rule trans :premises (@p454 @p452)) % 0.43/1.01 (step @p456 :rule ho_cong :premises (@p394 @p453)) % 0.43/1.01 (step @p457 :rule cong :premises (@p456 @p455) :args ((= (_ @t70 @t546) @t547))) % 0.43/1.01 (step @p458 :rule symm :premises (@p457)) % 0.43/1.01 (step @p459 :rule refl :args (@t76)) % 0.43/1.01 (step @p460 :rule eq_resolve :premises (@p459 @p458)) % 0.43/1.01 (step @p461 :rule refl :args (@t75)) % 0.43/1.01 (step @p462 :rule cong :premises (@p461 @p453) :args ((= @t75 @t546))) % 0.43/1.01 (step @p463 :rule symm :premises (@p462)) % 0.43/1.01 (step @p464 :rule eq_resolve :premises (@p461 @p463)) % 0.43/1.01 (step @p465 :rule ho_cong :premises (@p394 @p464)) % 0.43/1.01 (step @p466 :rule trans :premises (@p465 @p460)) % 0.43/1.01 (step @p467 :rule cong :premises (@p466) :args (@t580)) % 0.43/1.01 (step @p468 :rule nary_cong :premises (@p467 @p451) :args (@t581)) % 0.43/1.01 (step @p469 :rule cong :premises (@p468) :args ((forall @t73 @t581))) % 0.43/1.01 (step @p470 :rule trans :premises (@p469 @p437)) % 0.43/1.01 (step @p471 :rule bool-impl-elim :args (@t76 @t579)) % 0.43/1.01 (step @p472 :rule cong :premises (@p471) :args ((forall @t73 (=> @t76 @t579)))) % 0.43/1.01 (step @p473 :rule trans :premises (@p472 @p470)) % 0.43/1.01 (step @p474 :rule beta-reduce :args ((= (_ (lambda @t568 (and @t582 (not (= @t66 @t452)))) @t67) @t579))) % 0.43/1.01 (step @p475 :rule refl :args (@t67)) % 0.43/1.01 (step @p476 :rule eq-symm :args (@t452 @t66)) % 0.43/1.01 (step @p477 :rule cong :premises (@p476) :args (@t583)) % 0.43/1.01 (step @p478 :rule refl :args (@t582)) % 0.43/1.01 (step @p479 :rule nary_cong :premises (@p478 @p477) :args (@t584)) % 0.43/1.01 (step @p480 :rule cong :premises (@p479) :args (@t585)) % 0.43/1.01 (step @p481 :rule beta-reduce :args ((= @t586 @t585))) % 0.43/1.01 (step @p482 :rule trans :premises (@p481 @p480)) % 0.43/1.01 (step @p483 :rule ho_cong :premises (@p482 @p475)) % 0.43/1.01 (step @p484 :rule trans :premises (@p483 @p474)) % 0.43/1.01 (step @p485 :rule refl :args (@t76)) % 0.43/1.01 (step @p486 :rule cong :premises (@p485 @p484) :args (@t587)) % 0.43/1.01 (step @p487 :rule cong :premises (@p486) :args (@t588)) % 0.43/1.01 (step @p488 :rule trans :premises (@p487 @p473)) % 0.43/1.01 (step @p489 :rule refl :args (@t64)) % 0.43/1.01 (step @p490 :rule nary_cong :premises (@p489 @p488 @p432 @p354) :args (@t589)) % 0.43/1.01 (step @p491 :rule refl :args (@t62)) % 0.43/1.01 (step @p492 :rule cong :premises (@p491 @p490) :args (@t590)) % 0.43/1.01 (step @p493 :rule cong :premises (@p492) :args ((forall @t63 @t590))) % 0.43/1.01 (step @p494 :rule trans :premises (@p493 @p353)) % 0.43/1.01 (step @p495 :rule ho_cong :premises (@p313 @p475)) % 0.43/1.01 (step @p496 :rule ho_cong :premises (@p495 @p419)) % 0.43/1.01 (step @p497 :rule cong :premises (@p429 @p496) :args (@t72)) % 0.43/1.01 (step @p498 :rule cong :premises (@p497) :args (@t74)) % 0.43/1.01 (step @p499 :rule ho_cong :premises (@p313 @p419)) % 0.43/1.01 (step @p500 :rule ho_cong :premises (@p499 @p475)) % 0.43/1.01 (step @p501 :rule cong :premises (@p485 @p500) :args (@t77)) % 0.43/1.01 (step @p502 :rule cong :premises (@p501) :args (@t78)) % 0.43/1.01 (step @p503 :rule nary_cong :premises (@p489 @p502 @p498 @p354) :args (@t79)) % 0.43/1.01 (step @p504 :rule cong :premises (@p491 @p503) :args (@t80)) % 0.43/1.01 (step @p505 :rule cong :premises (@p504) :args (@t81)) % 0.43/1.01 (step @p506 :rule trans :premises (@p505 @p494)) % 0.43/1.01 (step @p507 :rule eq_resolve :premises (@p19 @p506)) % 0.43/1.01 (step @p508 :rule instantiate :premises (@p507) :args ((@list tptp.h tptp.t1 tptp.x tptp.t2))) % 0.43/1.01 (step @p509 :rule refl :args ((tptp.binary1721989714Tree_a tptp.h @t5))) % 0.43/1.01 (step @p510 :rule refl :args (@t591)) % 0.43/1.01 (step @p511 :rule refl :args (tptp.h)) % 0.43/1.01 (step @p512 :rule cong :premises (@p511 @p510) :args (@t592)) % 0.43/1.01 (step @p513 :rule trans :premises (@p512 @p509)) % 0.43/1.01 (step @p514 :rule refl :args (@t6)) % 0.43/1.01 (step @p515 :rule ho_cong :premises (@p514 @p510)) % 0.43/1.01 (step @p516 :rule cong :premises (@p515 @p513) :args ((= (_ @t6 @t591) @t592))) % 0.43/1.01 (step @p517 :rule symm :premises (@p516)) % 0.43/1.01 (step @p518 :rule refl :args (@t7)) % 0.43/1.01 (step @p519 :rule eq_resolve :premises (@p518 @p517)) % 0.43/1.01 (step @p520 :rule refl :args (@t5)) % 0.43/1.01 (step @p521 :rule cong :premises (@p520 @p510) :args ((= @t5 @t591))) % 0.43/1.01 (step @p522 :rule symm :premises (@p521)) % 0.43/1.01 (step @p523 :rule eq_resolve :premises (@p520 @p522)) % 0.43/1.01 (step @p524 :rule refl :args (@t6)) % 0.43/1.01 (step @p525 :rule ho_cong :premises (@p524 @p523)) % 0.43/1.01 (step @p526 :rule trans :premises (@p525 @p519)) % 0.43/1.01 (step @p527 :rule eq_resolve :premises (@p2 @p526)) % 0.43/1.01 (step @p528 :rule cnf_equiv_pos1 :args (@t599)) % 0.43/1.01 (step @p529 :rule reordering :premises (@p528) :args ((or (not @t592) @t598 (not @t599)))) % 0.43/1.01 (step @p530 :rule chain_m_resolution :premises (@p529 @p527 @p508) :args (@t598 @t600 (@list @t592 @t599))) % 0.43/1.01 (step @p531 :rule cnf_and_pos :args (@t598 1)) % 0.43/1.01 (step @p532 :rule reordering :premises (@p531) :args ((or @t597 (not @t598)))) % 0.43/1.01 (step @p533 :rule chain_m_resolution :premises (@p532 @p530) :args (@t597 @t601 (@list @t598))) % 0.43/1.01 (step @p534 :rule refl :args ((tptp.member_a tptp.w @t1))) % 0.43/1.01 (step @p535 :rule refl :args (@t596)) % 0.43/1.01 (step @p536 :rule refl :args (tptp.w)) % 0.43/1.01 (step @p537 :rule cong :premises (@p536 @p535) :args (@t602)) % 0.43/1.01 (step @p538 :rule trans :premises (@p537 @p534)) % 0.43/1.01 (step @p539 :rule refl :args (@t2)) % 0.43/1.01 (step @p540 :rule ho_cong :premises (@p539 @p535)) % 0.43/1.01 (step @p541 :rule cong :premises (@p540 @p538) :args ((= (_ @t2 @t596) @t602))) % 0.43/1.01 (step @p542 :rule symm :premises (@p541)) % 0.43/1.01 (step @p543 :rule refl :args (@t3)) % 0.43/1.01 (step @p544 :rule eq_resolve :premises (@p543 @p542)) % 0.43/1.01 (step @p545 :rule refl :args (@t1)) % 0.43/1.01 (step @p546 :rule cong :premises (@p545 @p535) :args ((= @t1 @t596))) % 0.43/1.01 (step @p547 :rule symm :premises (@p546)) % 0.43/1.01 (step @p548 :rule eq_resolve :premises (@p545 @p547)) % 0.43/1.01 (step @p549 :rule refl :args (@t2)) % 0.43/1.01 (step @p550 :rule ho_cong :premises (@p549 @p548)) % 0.43/1.01 (step @p551 :rule trans :premises (@p550 @p544)) % 0.43/1.01 (step @p552 :rule eq_resolve :premises (@p1 @p551)) % 0.43/1.01 (step @p553 :rule eq-symm :args (@t605 @t610)) % 0.43/1.01 (step @p554 :rule cong :premises (@p553) :args ((forall @t526 (= @t605 @t610)))) % 0.43/1.01 (step @p555 :rule refl :args (@t610)) % 0.43/1.01 (step @p556 :rule refl :args (@t603)) % 0.43/1.01 (step @p557 :rule refl :args (@t606)) % 0.43/1.01 (step @p558 :rule cong :premises (@p557 @p556) :args ((= @t606 @t603))) % 0.43/1.01 (step @p559 :rule symm :premises (@p558)) % 0.43/1.01 (step @p560 :rule eq_resolve :premises (@p557 @p559)) % 0.43/1.01 (step @p561 :rule refl :args (@t604)) % 0.43/1.01 (step @p562 :rule refl :args (@t11)) % 0.43/1.01 (step @p563 :rule cong :premises (@p562 @p561) :args ((= @t11 @t604))) % 0.43/1.01 (step @p564 :rule symm :premises (@p563)) % 0.43/1.01 (step @p565 :rule eq_resolve :premises (@p562 @p564)) % 0.43/1.01 (step @p566 :rule cong :premises (@p565 @p560) :args (@t607)) % 0.43/1.01 (step @p567 :rule cong :premises (@p566 @p555) :args (@t611)) % 0.43/1.01 (step @p568 :rule cong :premises (@p567) :args ((forall @t526 @t611))) % 0.43/1.01 (step @p569 :rule trans :premises (@p568 @p554)) % 0.43/1.01 (step @p570 :rule eq-symm :args (@t610 @t607)) % 0.43/1.01 (step @p571 :rule beta-reduce :args ((= @t612 @t607))) % 0.43/1.01 (step @p572 :rule refl :args (@t610)) % 0.43/1.01 (step @p573 :rule cong :premises (@p572 @p571) :args (@t613)) % 0.43/1.01 (step @p574 :rule trans :premises (@p573 @p570)) % 0.43/1.01 (step @p575 :rule cong :premises (@p574) :args (@t614)) % 0.43/1.01 (step @p576 :rule trans :premises (@p575 @p569)) % 0.43/1.01 (step @p577 :rule quant-unused-vars :args ((= (forall @t526 true) true))) % 0.43/1.01 (step @p578 :rule eq-refl :args (@t612)) % 0.43/1.01 (step @p579 :rule cong :premises (@p578) :args ((forall @t526 (= @t612 @t612)))) % 0.43/1.01 (step @p580 :rule trans :premises (@p579 @p577)) % 0.43/1.01 (step @p581 :rule refl :args (@t612)) % 0.43/1.01 (step @p582 :rule refl :args (@t525)) % 0.43/1.01 (step @p583 :rule skolem_intro :args (@t609)) % 0.43/1.01 (step @p584 :rule ho_cong :premises (@p583 @p582)) % 0.43/1.01 (step @p585 :rule cong :premises (@p584 @p581) :args (@t613)) % 0.43/1.01 (step @p586 :rule cong :premises (@p585) :args (@t614)) % 0.43/1.01 (step @p587 :rule trans :premises (@p586 @p580)) % 0.43/1.01 (step @p588 :rule true_elim :premises (@p587)) % 0.43/1.01 (step @p589 :rule eq_resolve :premises (@p588 @p576)) % 0.43/1.01 (step @p590 :rule instantiate :premises (@p589) :args (@t615)) % 0.43/1.01 (step @p591 :rule refl :args (@t616)) % 0.43/1.01 (step @p592 :rule refl :args (@t219)) % 0.43/1.01 (step @p593 :rule cong :premises (@p592 @p591) :args ((= @t219 @t616))) % 0.43/1.01 (step @p594 :rule symm :premises (@p593)) % 0.43/1.01 (step @p595 :rule eq_resolve :premises (@p592 @p594)) % 0.43/1.01 (step @p596 :rule refl :args ((tptp.member_a @t135 @t220))) % 0.43/1.01 (step @p597 :rule refl :args (@t617)) % 0.43/1.01 (step @p598 :rule refl :args (@t135)) % 0.43/1.01 (step @p599 :rule cong :premises (@p598 @p597) :args (@t618)) % 0.43/1.01 (step @p600 :rule trans :premises (@p599 @p596)) % 0.43/1.01 (step @p601 :rule refl :args (@t221)) % 0.43/1.01 (step @p602 :rule ho_cong :premises (@p601 @p597)) % 0.43/1.01 (step @p603 :rule cong :premises (@p602 @p600) :args ((= (_ @t221 @t617) @t618))) % 0.43/1.01 (step @p604 :rule symm :premises (@p603)) % 0.43/1.01 (step @p605 :rule refl :args (@t222)) % 0.43/1.01 (step @p606 :rule eq_resolve :premises (@p605 @p604)) % 0.43/1.01 (step @p607 :rule refl :args (@t220)) % 0.43/1.01 (step @p608 :rule cong :premises (@p607 @p597) :args ((= @t220 @t617))) % 0.43/1.01 (step @p609 :rule symm :premises (@p608)) % 0.43/1.01 (step @p610 :rule eq_resolve :premises (@p607 @p609)) % 0.43/1.01 (step @p611 :rule ho_cong :premises (@p601 @p610)) % 0.43/1.01 (step @p612 :rule trans :premises (@p611 @p606)) % 0.43/1.01 (step @p613 :rule cong :premises (@p612 @p595) :args (@t223)) % 0.43/1.01 (step @p614 :rule cong :premises (@p613) :args (@t225)) % 0.43/1.01 (step @p615 :rule eq_resolve :premises (@p73 @p614)) % 0.43/1.01 (step @p616 :rule instantiate :premises (@p615) :args ((@list tptp.w @t609))) % 0.43/1.01 (step @p617 :rule refl :args ((tptp.member_a tptp.w @t619))) % 0.43/1.01 (step @p618 :rule refl :args (@t620)) % 0.43/1.01 (step @p619 :rule cong :premises (@p536 @p618) :args (@t621)) % 0.43/1.01 (step @p620 :rule trans :premises (@p619 @p617)) % 0.43/1.01 (step @p621 :rule ho_cong :premises (@p539 @p618)) % 0.43/1.01 (step @p622 :rule cong :premises (@p621 @p620) :args ((= (_ @t2 @t620) @t621))) % 0.43/1.01 (step @p623 :rule symm :premises (@p622)) % 0.43/1.01 (step @p624 :rule refl :args ((_ @t2 @t619))) % 0.43/1.01 (step @p625 :rule eq_resolve :premises (@p624 @p623)) % 0.43/1.01 (step @p626 :rule refl :args (@t619)) % 0.43/1.01 (step @p627 :rule cong :premises (@p626 @p618) :args ((= @t619 @t620))) % 0.43/1.01 (step @p628 :rule symm :premises (@p627)) % 0.43/1.01 (step @p629 :rule eq_resolve :premises (@p626 @p628)) % 0.43/1.01 (step @p630 :rule eq-refl :args (@t608)) % 0.43/1.01 (step @p631 :rule refl :args (@t608)) % 0.43/1.01 (step @p632 :rule cong :premises (@p631 @p583) :args ((= @t608 @t609))) % 0.43/1.01 (step @p633 :rule trans :premises (@p632 @p630)) % 0.43/1.01 (step @p634 :rule true_elim :premises (@p633)) % 0.43/1.01 (step @p635 :rule refl :args (tptp.collect_a)) % 0.43/1.01 (step @p636 :rule ho_cong :premises (@p635 @p634)) % 0.43/1.01 (step @p637 :rule trans :premises (@p636 @p629)) % 0.43/1.01 (step @p638 :rule ho_cong :premises (@p549 @p637)) % 0.43/1.01 (step @p639 :rule trans :premises (@p638 @p625)) % 0.43/1.01 (step @p640 :rule eq-symm :args (@t606 @t11)) % 0.43/1.01 (step @p641 :rule cong :premises (@p640) :args (@t622)) % 0.43/1.01 (step @p642 :rule ho_cong :premises (@p635 @p641)) % 0.43/1.01 (step @p643 :rule beta-reduce :args ((= (_ @t623 tptp.e) (_ tptp.collect_a @t622)))) % 0.43/1.01 (step @p644 :rule trans :premises (@p643 @p642)) % 0.43/1.01 (step @p645 :rule refl :args (tptp.e)) % 0.43/1.01 (step @p646 :rule beta-reduce :args ((= (_ @t527 tptp.h) @t623))) % 0.43/1.01 (step @p647 :rule ho_cong :premises (@p646 @p645)) % 0.43/1.01 (step @p648 :rule trans :premises (@p647 @p644)) % 0.43/1.01 (step @p649 :rule ho_cong :premises (@p549 @p648)) % 0.43/1.01 (step @p650 :rule refl :args (tptp.h)) % 0.43/1.01 (step @p651 :rule ho_cong :premises (@p316 @p650)) % 0.43/1.01 (step @p652 :rule ho_cong :premises (@p651 @p645)) % 0.43/1.01 (step @p653 :rule ho_cong :premises (@p549 @p652)) % 0.43/1.01 (step @p654 :rule trans :premises (@p653 @p649)) % 0.43/1.01 (step @p655 :rule trans :premises (@p654 @p639)) % 0.43/1.01 (step @p656 :rule eq_resolve :premises (@p7 @p655)) % 0.43/1.01 (step @p657 :rule cnf_equiv_pos1 :args (@t625)) % 0.43/1.01 (step @p658 :rule reordering :premises (@p657) :args ((or (not @t621) @t624 (not @t625)))) % 0.43/1.01 (step @p659 :rule chain_m_resolution :premises (@p658 @p656 @p616) :args (@t624 @t600 (@list @t621 @t625))) % 0.43/1.01 (step @p660 :rule cnf_equiv_pos1 :args (@t628)) % 0.43/1.01 (step @p661 :rule reordering :premises (@p660) :args ((or @t627 (not @t624) (not @t628)))) % 0.43/1.01 (step @p662 :rule chain_m_resolution :premises (@p661 @p659 @p590) :args (@t627 @t600 (@list @t624 @t628))) % 0.43/1.01 (step @p663 :rule eq-symm :args (@t604 @t594)) % 0.43/1.01 (step @p664 :rule refl :args (@t594)) % 0.43/1.01 (step @p665 :rule refl :args (@t10)) % 0.43/1.01 (step @p666 :rule cong :premises (@p665 @p664) :args ((= @t10 @t594))) % 0.43/1.01 (step @p667 :rule symm :premises (@p666)) % 0.43/1.01 (step @p668 :rule eq_resolve :premises (@p665 @p667)) % 0.43/1.01 (step @p669 :rule cong :premises (@p565 @p668) :args ((= @t11 @t10))) % 0.43/1.01 (step @p670 :rule trans :premises (@p669 @p663)) % 0.43/1.01 (step @p671 :rule eq-symm :args (@t10 @t11)) % 0.43/1.01 (step @p672 :rule trans :premises (@p671 @p670)) % 0.43/1.01 (step @p673 :rule eq_resolve :premises (@p8 @p672)) % 0.43/1.01 (step @p674 :rule trans :premises (@p673 @p662)) % 0.43/1.01 (step @p675 :rule cnf_and_pos :args (@t631 1)) % 0.43/1.01 (step @p676 :rule reordering :premises (@p675) :args ((or @t630 @t632))) % 0.43/1.01 (step @p677 :rule chain_m_resolution :premises (@p676 @p674) :args (@t632 @t601 (@list @t629))) % 0.43/1.01 (step @p678 :rule cnf_or_pos :args (@t634)) % 0.43/1.01 (step @p679 :rule reordering :premises (@p678) :args ((or @t631 @t633 @t635))) % 0.43/1.01 (step @p680 :rule chain_m_resolution :premises (@p679 @p677 @p552) :args (@t635 @t636 (@list @t631 @t602))) % 0.43/1.01 (assume-push @p687 @t597) % 0.43/1.01 (step @p682 :rule instantiate :premises (@p533) :args (@t615)) % 0.43/1.01 (step-pop @p688 :rule scope :premises (@p682)) % 0.43/1.01 (step @p683 :rule process_scope :premises (@p688) :args (@t634)) % 0.43/1.01 (step @p685 :rule implies_elim :premises (@p683)) % 0.43/1.01 (step @p686 false :rule chain_m_resolution :premises (@p685 @p680 @p533) :args (false @t636 (@list @t634 @t597))) % 0.43/1.01 ) % 0.43/1.01 % SZS output end Proof % 0.43/1.01 % cvc5 exiting %------------------------------------------------------------------------------