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