%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP068^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.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:57 AM UTC 2026 % Result : Theorem 0.38s 0.77s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP068^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n003.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 04:12:59 EDT 2026 % 0.16/0.34 % CPUTime : % 0.36/0.54 %----Proving TH0 % 0.38/0.77 --- 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.38/0.77 % SZS status Theorem % 0.38/0.77 % SZS output start Proof % 0.38/0.77 ( % 0.38/0.77 (declare-sort tptp.a 0) % 0.38/0.77 (declare-sort tptp.multiset_a 0) % 0.38/0.77 (declare-sort tptp.multiset_multiset_a 0) % 0.38/0.77 (declare-sort tptp.set_multiset_a 0) % 0.38/0.77 (declare-sort tptp.tree_a 0) % 0.38/0.77 (declare-sort tptp.set_a 0) % 0.38/0.77 (declare-sort tptp.product_prod_a_a 0) % 0.38/0.77 (declare-sort tptp.set_Product_prod_a_a 0) % 0.38/0.77 (declare-sort tptp.produc1127127335iset_a 0) % 0.38/0.77 (declare-sort tptp.set_Pr158363655iset_a 0) % 0.38/0.77 (declare-const tptp.ord_less_eq_a (-> tptp.a tptp.a Bool)) % 0.38/0.77 (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool)) % 0.38/0.77 (declare-const tptp.image_mset_a_a (-> (-> tptp.a tptp.a) tptp.multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.irrefl_a (-> tptp.set_Product_prod_a_a Bool)) % 0.38/0.77 (declare-const tptp.set_mset_multiset_a (-> tptp.multiset_multiset_a tptp.set_multiset_a)) % 0.38/0.77 (declare-const tptp.mult_a (-> tptp.set_Product_prod_a_a tptp.set_Pr158363655iset_a)) % 0.38/0.77 (declare-const tptp.mult1_a (-> tptp.set_Product_prod_a_a tptp.set_Pr158363655iset_a)) % 0.38/0.77 (declare-const tptp.ord_le1199012836iset_a (-> tptp.multiset_a tptp.multiset_a Bool)) % 0.38/0.77 (declare-const tptp.subseteq_mset_a (-> tptp.multiset_a tptp.multiset_a Bool)) % 0.38/0.77 (declare-const tptp.plus_plus_multiset_a (-> tptp.multiset_a tptp.multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.zero_zero_multiset_a tptp.multiset_a) % 0.38/0.77 (declare-const tptp.ord_less_eq_a_a_o (-> (-> tptp.a tptp.a Bool) (-> tptp.a tptp.a Bool) Bool)) % 0.38/0.77 (declare-const tptp.fold_m382157835iset_a (-> (-> tptp.multiset_a tptp.multiset_a tptp.multiset_a) tptp.multiset_a tptp.multiset_multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.r1 tptp.tree_a) % 0.38/0.77 (declare-const tptp.va tptp.a) % 0.38/0.77 (declare-const tptp.v1 tptp.a) % 0.38/0.77 (declare-const tptp.nO_MAT1617603563iset_a (-> tptp.multiset_a tptp.multiset_a Bool)) % 0.38/0.77 (declare-const tptp.order_Greatest_o_a (-> (-> (-> Bool tptp.a) Bool) Bool tptp.a)) % 0.38/0.77 (declare-const tptp.image_929116801iset_a (-> (-> tptp.a tptp.multiset_a) tptp.multiset_a tptp.multiset_multiset_a)) % 0.38/0.77 (declare-const tptp.v2 tptp.a) % 0.38/0.77 (declare-const tptp.heapIm1140443833left_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.77 (declare-const tptp.l tptp.tree_a) % 0.38/0.77 (declare-const tptp.l1 tptp.tree_a) % 0.38/0.77 (declare-const tptp.add_mset_a (-> tptp.a tptp.multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.produc2037245207iset_a (-> tptp.multiset_a tptp.multiset_a tptp.produc1127127335iset_a)) % 0.38/0.77 (declare-const tptp.e_a tptp.tree_a) % 0.38/0.77 (declare-const tptp.comm_m315775925iset_a (-> (-> tptp.multiset_a tptp.multiset_a tptp.multiset_a) tptp.multiset_a tptp.multiset_multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.r tptp.tree_a) % 0.38/0.77 (declare-const tptp.heapIm1091024090Down_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.77 (declare-const tptp.heapIm1257206334ight_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.77 (declare-const tptp.order_Greatest_a (-> (-> tptp.a Bool) tptp.a)) % 0.38/0.77 (declare-const tptp.la tptp.tree_a) % 0.38/0.77 (declare-const tptp.member_multiset_a (-> tptp.multiset_a tptp.set_multiset_a Bool)) % 0.38/0.77 (declare-const tptp.is_heap_a (-> tptp.tree_a Bool)) % 0.38/0.77 (declare-const tptp.product_Pair_a_a (-> tptp.a tptp.a tptp.product_prod_a_a)) % 0.38/0.77 (declare-const tptp.t_a (-> tptp.a tptp.tree_a tptp.tree_a tptp.tree_a)) % 0.38/0.77 (declare-const tptp.ra tptp.tree_a) % 0.38/0.77 (declare-const tptp.v tptp.a) % 0.38/0.77 (declare-const tptp.fold_m364285649iset_a (-> (-> tptp.a tptp.multiset_a tptp.multiset_a) tptp.multiset_a tptp.multiset_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.t tptp.tree_a) % 0.38/0.77 (declare-const tptp.member449909584od_a_a (-> tptp.product_prod_a_a tptp.set_Product_prod_a_a Bool)) % 0.38/0.77 (declare-const tptp.val_a (-> tptp.tree_a tptp.a)) % 0.38/0.77 (declare-const tptp.in_tree_a (-> tptp.a tptp.tree_a Bool)) % 0.38/0.77 (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a)) % 0.38/0.77 (declare-const tptp.trans_a (-> tptp.set_Product_prod_a_a Bool)) % 0.38/0.77 (declare-const tptp.rel_Tree_a_a (-> (-> tptp.a tptp.a Bool) tptp.tree_a tptp.tree_a Bool)) % 0.38/0.77 (declare-const tptp.ord_le1530450702ee_a_o (-> (-> tptp.tree_a tptp.tree_a Bool) (-> tptp.tree_a tptp.tree_a Bool) Bool)) % 0.38/0.77 (declare-const tptp.member340150864iset_a (-> tptp.produc1127127335iset_a tptp.set_Pr158363655iset_a Bool)) % 0.38/0.77 (declare-const tptp.multiset_a2 (-> tptp.tree_a tptp.multiset_a)) % 0.38/0.77 (declare-const tptp.set_mset_a (-> tptp.multiset_a tptp.set_a)) % 0.38/0.77 (declare-const tptp.lattic146396397_Max_a (-> tptp.set_a tptp.a)) % 0.38/0.77 (define tptp.ord_less_eq_o_a () (let ((_let_1 (@var "X5" Bool))) (let ((_let_2 (@var "G2" (-> Bool tptp.a)))) (let ((_let_3 (@var "F2" (-> Bool tptp.a)))) (lambda (@list _let_3 _let_2) (forall (@list _let_1) (_ (_ tptp.ord_less_eq_a (_ _let_3 _let_1)) (_ _let_2 _let_1)))))))) % 0.38/0.77 (define tptp.ord_less_eq_o_o_a () (let ((_let_1 (@var "Y6" (-> Bool Bool tptp.a)))) (let ((_let_2 (@var "X6" (-> Bool Bool tptp.a)))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_o_a (_ _let_2 false)) (_ _let_1 false)) (_ (_ tptp.ord_less_eq_o_a (_ _let_2 true)) (_ _let_1 true))))))) % 0.38/0.77 (define tptp.ord_less_eq_set_a () (let ((_let_1 (@var "B7" tptp.set_a))) (let ((_let_2 (@var "X5" tptp.a))) (let ((_let_3 (_ tptp.member_a _let_2))) (let ((_let_4 (@var "A6" tptp.set_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.38/0.77 (define @t1 () (_ tptp.is_heap_a tptp.ra)) % 0.38/0.77 (define @t2 () (_ (_ tptp.ord_less_eq_a tptp.v1) tptp.v2)) % 0.38/0.77 (define @t3 () (_ (_ (_ tptp.t_a tptp.va) tptp.la) tptp.ra)) % 0.38/0.77 (define @t4 () (_ (_ (_ tptp.t_a tptp.v1) tptp.l1) tptp.r1)) % 0.38/0.77 (define @t5 () (_ tptp.t_a tptp.v2)) % 0.38/0.77 (define @t6 () (_ @t5 tptp.e_a)) % 0.38/0.77 (define @t7 () (_ @t6 @t4)) % 0.38/0.77 (define @t8 () (= @t7 @t3)) % 0.38/0.77 (define @t9 () (@var "V" tptp.a)) % 0.38/0.77 (define @t10 () (_ tptp.t_a @t9)) % 0.38/0.77 (define @t11 () (_ @t10 tptp.e_a)) % 0.38/0.77 (define @t12 () (_ @t11 tptp.e_a)) % 0.38/0.77 (define @t13 () (@list @t9)) % 0.38/0.77 (define @t14 () (@var "Vf" tptp.tree_a)) % 0.38/0.77 (define @t15 () (@var "Ve" tptp.tree_a)) % 0.38/0.77 (define @t16 () (@var "Vd" tptp.a)) % 0.38/0.77 (define @t17 () (@var "Vc" tptp.tree_a)) % 0.38/0.77 (define @t18 () (@var "Vb" tptp.tree_a)) % 0.38/0.77 (define @t19 () (@var "Va" tptp.a)) % 0.38/0.77 (define @t20 () (_ (_ (_ tptp.t_a @t19) @t18) @t17)) % 0.38/0.77 (define @t21 () (@var "V2" tptp.a)) % 0.38/0.77 (define @t22 () (_ tptp.t_a @t21)) % 0.38/0.77 (define @t23 () (_ @t22 @t20)) % 0.38/0.77 (define @t24 () (@var "X" tptp.tree_a)) % 0.38/0.77 (define @t25 () (not (forall (@list @t21 @t19 @t18 @t17 @t16 @t15 @t14) (not (= @t24 (_ @t23 (_ (_ (_ tptp.t_a @t16) @t15) @t14))))))) % 0.38/0.77 (define @t26 () (_ @t22 tptp.e_a)) % 0.38/0.77 (define @t27 () (@list @t21 @t19 @t18 @t17)) % 0.38/0.77 (define @t28 () (forall @t27 (not (= @t24 (_ @t26 @t20))))) % 0.38/0.77 (define @t29 () (forall @t27 (not (= @t24 (_ @t23 tptp.e_a))))) % 0.38/0.77 (define @t30 () (forall (@list @t21) (not (= @t24 (_ @t26 tptp.e_a))))) % 0.38/0.77 (define @t31 () (not (= @t24 tptp.e_a))) % 0.38/0.77 (define @t32 () (@list @t24)) % 0.38/0.77 (define @t33 () (@var "V3" tptp.a)) % 0.38/0.77 (define @t34 () (_ tptp.ord_less_eq_a @t9)) % 0.38/0.77 (define @t35 () (@var "R2" tptp.tree_a)) % 0.38/0.77 (define @t36 () (@var "L2" tptp.tree_a)) % 0.38/0.77 (define @t37 () (@var "T" tptp.tree_a)) % 0.38/0.77 (define @t38 () (_ tptp.heapIm1091024090Down_a @t37)) % 0.38/0.77 (define @t39 () (@var "R" tptp.tree_a)) % 0.38/0.77 (define @t40 () (@var "L" tptp.tree_a)) % 0.38/0.77 (define @t41 () (_ (_ @t10 @t40) @t39)) % 0.38/0.77 (define @t42 () (_ (_ @t5 (_ tptp.heapIm1140443833left_a @t4)) (_ tptp.heapIm1257206334ight_a @t4))) % 0.38/0.77 (define @t43 () (@var "Y23" tptp.tree_a)) % 0.38/0.77 (define @t44 () (@var "X23" tptp.tree_a)) % 0.38/0.77 (define @t45 () (@var "Y22" tptp.tree_a)) % 0.38/0.77 (define @t46 () (@var "X22" tptp.tree_a)) % 0.38/0.77 (define @t47 () (@var "Y21" tptp.a)) % 0.38/0.77 (define @t48 () (@var "X21" tptp.a)) % 0.38/0.77 (define @t49 () (and (= @t48 @t47) (= @t46 @t45) (= @t44 @t43))) % 0.38/0.77 (define @t50 () (_ (_ (_ tptp.t_a @t47) @t45) @t43)) % 0.38/0.77 (define @t51 () (_ (_ (_ tptp.t_a @t48) @t46) @t44)) % 0.38/0.77 (define @t52 () (= @t51 @t50)) % 0.38/0.77 (define @t53 () (= @t52 @t49)) % 0.38/0.77 (define @t54 () (@list @t48 @t46 @t44 @t47 @t45 @t43)) % 0.38/0.77 (define @t55 () (forall @t54 @t53)) % 0.38/0.77 (define @t56 () (@var "Tree" tptp.tree_a)) % 0.38/0.77 (define @t57 () (@var "P" (-> tptp.tree_a Bool))) % 0.38/0.77 (define @t58 () (@var "X3" tptp.tree_a)) % 0.38/0.77 (define @t59 () (@var "X2" tptp.tree_a)) % 0.38/0.77 (define @t60 () (@var "X1" tptp.a)) % 0.38/0.77 (define @t61 () (_ (_ (_ tptp.t_a @t60) @t59) @t58)) % 0.38/0.77 (define @t62 () (@list @t60 @t59 @t58)) % 0.38/0.77 (define @t63 () (@var "X232" tptp.tree_a)) % 0.38/0.77 (define @t64 () (@var "X222" tptp.tree_a)) % 0.38/0.77 (define @t65 () (@var "X212" tptp.a)) % 0.38/0.77 (define @t66 () (@var "Y" tptp.tree_a)) % 0.38/0.77 (define @t67 () (@var "T2" tptp.tree_a)) % 0.38/0.77 (define @t68 () (@var "V4" tptp.a)) % 0.38/0.77 (define @t69 () (@list @t9 @t40 @t39)) % 0.38/0.77 (define @t70 () (_ tptp.val_a @t37)) % 0.38/0.77 (define @t71 () (_ tptp.is_heap_a @t37)) % 0.38/0.77 (define @t72 () (_ tptp.in_tree_a @t9)) % 0.38/0.77 (define @t73 () (@var "Uv" tptp.tree_a)) % 0.38/0.77 (define @t74 () (@var "Uu" tptp.tree_a)) % 0.38/0.77 (define @t75 () (_ (_ @t10 @t74) @t73)) % 0.38/0.77 (define @t76 () (_ tptp.val_a @t75)) % 0.38/0.77 (define @t77 () (@list @t9 @t74 @t73)) % 0.38/0.77 (define @t78 () (forall @t77 (= @t76 @t9))) % 0.38/0.77 (define @t79 () (@var "V5" tptp.a)) % 0.38/0.77 (define @t80 () (@var "Vf2" tptp.tree_a)) % 0.38/0.77 (define @t81 () (@var "Ve2" tptp.tree_a)) % 0.38/0.77 (define @t82 () (@var "Vd2" tptp.a)) % 0.38/0.77 (define @t83 () (_ (_ (_ tptp.t_a @t82) @t81) @t80)) % 0.38/0.77 (define @t84 () (_ tptp.heapIm1091024090Down_a (_ (_ @t10 (_ tptp.heapIm1140443833left_a @t83)) (_ tptp.heapIm1257206334ight_a @t83)))) % 0.38/0.77 (define @t85 () (@var "Vc2" tptp.tree_a)) % 0.38/0.77 (define @t86 () (@var "Vb2" tptp.tree_a)) % 0.38/0.77 (define @t87 () (@var "Va2" tptp.a)) % 0.38/0.77 (define @t88 () (_ (_ (_ tptp.t_a @t87) @t86) @t85)) % 0.38/0.77 (define @t89 () (_ tptp.val_a @t83)) % 0.38/0.77 (define @t90 () (_ tptp.t_a @t89)) % 0.38/0.77 (define @t91 () (_ @t10 @t88)) % 0.38/0.77 (define @t92 () (_ @t91 @t83)) % 0.38/0.77 (define @t93 () (_ tptp.heapIm1091024090Down_a @t92)) % 0.38/0.77 (define @t94 () (_ tptp.ord_less_eq_a @t89)) % 0.38/0.77 (define @t95 () (_ @t94 @t9)) % 0.38/0.77 (define @t96 () (not @t95)) % 0.38/0.77 (define @t97 () (= @t93 @t92)) % 0.38/0.77 (define @t98 () (_ tptp.val_a @t88)) % 0.38/0.77 (define @t99 () (_ @t94 @t98)) % 0.38/0.77 (define @t100 () (_ tptp.heapIm1091024090Down_a (_ (_ @t10 (_ tptp.heapIm1140443833left_a @t88)) (_ tptp.heapIm1257206334ight_a @t88)))) % 0.38/0.77 (define @t101 () (_ tptp.t_a @t98)) % 0.38/0.77 (define @t102 () (_ @t101 @t100)) % 0.38/0.77 (define @t103 () (_ tptp.ord_less_eq_a @t98)) % 0.38/0.77 (define @t104 () (_ @t103 @t9)) % 0.38/0.77 (define @t105 () (not @t104)) % 0.38/0.77 (define @t106 () (_ (_ @t10 @t83) @t88)) % 0.38/0.77 (define @t107 () (_ tptp.heapIm1091024090Down_a @t106)) % 0.38/0.77 (define @t108 () (= @t107 @t106)) % 0.38/0.77 (define @t109 () (_ @t103 @t89)) % 0.38/0.77 (define @t110 () (_ tptp.is_heap_a @t88)) % 0.38/0.77 (define @t111 () (_ tptp.is_heap_a @t83)) % 0.38/0.77 (define @t112 () (_ @t91 tptp.e_a)) % 0.38/0.77 (define @t113 () (_ tptp.heapIm1091024090Down_a @t112)) % 0.38/0.77 (define @t114 () (@list @t87 @t86 @t85 @t9)) % 0.38/0.77 (define @t115 () (_ @t11 @t88)) % 0.38/0.77 (define @t116 () (_ tptp.heapIm1091024090Down_a @t115)) % 0.38/0.77 (define @t117 () (= @t116 (_ (_ @t101 tptp.e_a) @t100))) % 0.38/0.77 (define @t118 () (=> @t105 @t117)) % 0.38/0.77 (define @t119 () (=> @t104 (= @t116 @t115))) % 0.38/0.77 (define @t120 () (and @t119 @t118)) % 0.38/0.77 (define @t121 () (forall @t114 @t120)) % 0.38/0.77 (define @t122 () (not (= @t37 tptp.e_a))) % 0.38/0.77 (define @t123 () (@list @t37)) % 0.38/0.77 (define @t124 () (and @t104 @t110)) % 0.38/0.77 (define @t125 () (_ tptp.is_heap_a @t115)) % 0.38/0.77 (define @t126 () (= @t125 @t124)) % 0.38/0.77 (define @t127 () (@list @t9 @t87 @t86 @t85)) % 0.38/0.77 (define @t128 () (forall @t127 @t126)) % 0.38/0.77 (define @t129 () (@var "X" (-> Bool tptp.a))) % 0.38/0.77 (define @t130 () (_ tptp.ord_less_eq_o_a @t129)) % 0.38/0.77 (define @t131 () (@var "X" tptp.a)) % 0.38/0.77 (define @t132 () (_ tptp.ord_less_eq_a @t131)) % 0.38/0.77 (define @t133 () (@list @t131)) % 0.38/0.77 (define @t134 () (@var "X" Bool)) % 0.38/0.77 (define @t135 () (@var "G" (-> Bool tptp.a))) % 0.38/0.77 (define @t136 () (@var "F" (-> Bool tptp.a))) % 0.38/0.77 (define @t137 () (_ (_ tptp.ord_less_eq_o_a @t136) @t135)) % 0.38/0.77 (define @t138 () (@var "X4" Bool)) % 0.38/0.77 (define @t139 () (@var "C" (-> Bool tptp.a))) % 0.38/0.77 (define @t140 () (@var "F" (-> (-> Bool tptp.a) tptp.a))) % 0.38/0.77 (define @t141 () (@var "A" tptp.a)) % 0.38/0.77 (define @t142 () (_ tptp.ord_less_eq_a @t141)) % 0.38/0.77 (define @t143 () (@var "Y2" (-> Bool tptp.a))) % 0.38/0.77 (define @t144 () (@var "X4" (-> Bool tptp.a))) % 0.38/0.77 (define @t145 () (_ (_ tptp.ord_less_eq_o_a @t144) @t143)) % 0.38/0.77 (define @t146 () (@list @t144 @t143)) % 0.38/0.77 (define @t147 () (forall @t146 (=> @t145 (_ (_ tptp.ord_less_eq_a (_ @t140 @t144)) (_ @t140 @t143))))) % 0.38/0.77 (define @t148 () (@var "B" (-> Bool tptp.a))) % 0.38/0.77 (define @t149 () (_ tptp.ord_less_eq_o_a @t148)) % 0.38/0.77 (define @t150 () (_ @t149 @t139)) % 0.38/0.77 (define @t151 () (=> @t150 (=> @t147 (_ @t142 (_ @t140 @t139))))) % 0.38/0.77 (define @t152 () (_ @t140 @t148)) % 0.38/0.77 (define @t153 () (@list @t141 @t140 @t148 @t139)) % 0.38/0.77 (define @t154 () (@var "C" tptp.a)) % 0.38/0.77 (define @t155 () (@var "F" (-> tptp.a Bool tptp.a))) % 0.38/0.77 (define @t156 () (@var "A" (-> Bool tptp.a))) % 0.38/0.77 (define @t157 () (_ tptp.ord_less_eq_o_a @t156)) % 0.38/0.77 (define @t158 () (@var "Y2" tptp.a)) % 0.38/0.77 (define @t159 () (@var "X4" tptp.a)) % 0.38/0.77 (define @t160 () (_ tptp.ord_less_eq_a @t159)) % 0.38/0.77 (define @t161 () (_ @t160 @t158)) % 0.38/0.77 (define @t162 () (@list @t159 @t158)) % 0.38/0.77 (define @t163 () (forall @t162 (=> @t161 (_ (_ tptp.ord_less_eq_o_a (_ @t155 @t159)) (_ @t155 @t158))))) % 0.38/0.77 (define @t164 () (@var "B" tptp.a)) % 0.38/0.77 (define @t165 () (_ tptp.ord_less_eq_a @t164)) % 0.38/0.77 (define @t166 () (_ @t165 @t154)) % 0.38/0.77 (define @t167 () (=> @t166 (=> @t163 (_ @t157 (_ @t155 @t154))))) % 0.38/0.77 (define @t168 () (_ @t155 @t164)) % 0.38/0.77 (define @t169 () (@list @t156 @t155 @t164 @t154)) % 0.38/0.77 (define @t170 () (@var "F" (-> (-> Bool tptp.a) Bool tptp.a))) % 0.38/0.77 (define @t171 () (forall @t146 (=> @t145 (_ (_ tptp.ord_less_eq_o_a (_ @t170 @t144)) (_ @t170 @t143))))) % 0.38/0.77 (define @t172 () (=> @t150 (=> @t171 (_ @t157 (_ @t170 @t139))))) % 0.38/0.77 (define @t173 () (_ @t170 @t148)) % 0.38/0.77 (define @t174 () (@list @t156 @t170 @t148 @t139)) % 0.38/0.77 (define @t175 () (@var "F" (-> tptp.a tptp.a))) % 0.38/0.77 (define @t176 () (forall @t162 (=> @t161 (_ (_ tptp.ord_less_eq_a (_ @t175 @t159)) (_ @t175 @t158))))) % 0.38/0.77 (define @t177 () (=> @t166 (=> @t176 (_ @t142 (_ @t175 @t154))))) % 0.38/0.77 (define @t178 () (_ @t175 @t164)) % 0.38/0.77 (define @t179 () (@list @t141 @t175 @t164 @t154)) % 0.38/0.77 (define @t180 () (=> @t163 (_ (_ tptp.ord_less_eq_o_a (_ @t155 @t141)) @t139))) % 0.38/0.77 (define @t181 () (_ @t142 @t164)) % 0.38/0.77 (define @t182 () (@list @t141 @t164 @t155 @t139)) % 0.38/0.77 (define @t183 () (=> @t147 (_ (_ tptp.ord_less_eq_a (_ @t140 @t156)) @t154))) % 0.38/0.77 (define @t184 () (_ @t157 @t148)) % 0.38/0.77 (define @t185 () (@list @t156 @t148 @t140 @t154)) % 0.38/0.77 (define @t186 () (=> @t171 (_ (_ tptp.ord_less_eq_o_a (_ @t170 @t156)) @t139))) % 0.38/0.77 (define @t187 () (@list @t156 @t148 @t170 @t139)) % 0.38/0.77 (define @t188 () (_ @t175 @t141)) % 0.38/0.77 (define @t189 () (=> @t176 (_ (_ tptp.ord_less_eq_a @t188) @t154))) % 0.38/0.77 (define @t190 () (@list @t141 @t164 @t175 @t154)) % 0.38/0.77 (define @t191 () (_ @t165 @t141)) % 0.38/0.77 (define @t192 () (= @t141 @t164)) % 0.38/0.77 (define @t193 () (@list @t141 @t164)) % 0.38/0.77 (define @t194 () (@var "P" (-> tptp.a Bool))) % 0.38/0.77 (define @t195 () (_ tptp.member_a @t141)) % 0.38/0.77 (define @t196 () (@var "A2" tptp.set_a)) % 0.38/0.77 (define @t197 () (@var "X5" tptp.a)) % 0.38/0.77 (define @t198 () (_ tptp.member_a @t197)) % 0.38/0.77 (define @t199 () (@list @t197)) % 0.38/0.77 (define @t200 () (= @t156 @t148)) % 0.38/0.77 (define @t201 () (_ @t149 @t156)) % 0.38/0.77 (define @t202 () (@var "B2" (-> Bool tptp.a))) % 0.38/0.77 (define @t203 () (@var "A3" (-> Bool tptp.a))) % 0.38/0.77 (define @t204 () (_ (_ tptp.ord_less_eq_o_a @t203) @t202)) % 0.38/0.77 (define @t205 () (_ (_ tptp.ord_less_eq_o_a @t202) @t203)) % 0.38/0.77 (define @t206 () (@list @t203 @t202)) % 0.38/0.77 (define @t207 () (@var "Z" (-> Bool tptp.a))) % 0.38/0.77 (define @t208 () (@var "Y3" (-> Bool tptp.a))) % 0.38/0.77 (define @t209 () (lambda (@list @t208 @t207) (= @t208 @t207))) % 0.38/0.77 (define @t210 () (@var "B2" tptp.a)) % 0.38/0.77 (define @t211 () (@var "A3" tptp.a)) % 0.38/0.77 (define @t212 () (_ (_ tptp.ord_less_eq_a @t211) @t210)) % 0.38/0.77 (define @t213 () (_ (_ tptp.ord_less_eq_a @t210) @t211)) % 0.38/0.77 (define @t214 () (@list @t211 @t210)) % 0.38/0.77 (define @t215 () (@var "Z" tptp.a)) % 0.38/0.77 (define @t216 () (@var "Y3" tptp.a)) % 0.38/0.77 (define @t217 () (lambda (@list @t216 @t215) (= @t216 @t215))) % 0.38/0.77 (define @t218 () (_ tptp.ord_less_eq_o_a @t139)) % 0.38/0.77 (define @t219 () (_ tptp.ord_less_eq_a @t154)) % 0.38/0.77 (define @t220 () (@var "P" (-> tptp.a tptp.a Bool))) % 0.38/0.77 (define @t221 () (@var "B3" tptp.a)) % 0.38/0.77 (define @t222 () (@var "A4" tptp.a)) % 0.38/0.77 (define @t223 () (_ (_ @t220 @t222) @t221)) % 0.38/0.77 (define @t224 () (@list @t222 @t221)) % 0.38/0.77 (define @t225 () (@var "Z2" (-> Bool tptp.a))) % 0.38/0.77 (define @t226 () (@var "Y" (-> Bool tptp.a))) % 0.38/0.77 (define @t227 () (_ tptp.ord_less_eq_o_a @t226)) % 0.38/0.77 (define @t228 () (_ @t130 @t226)) % 0.38/0.77 (define @t229 () (@var "Z2" tptp.a)) % 0.38/0.77 (define @t230 () (_ @t132 @t229)) % 0.38/0.77 (define @t231 () (@var "Y" tptp.a)) % 0.38/0.77 (define @t232 () (_ tptp.ord_less_eq_a @t231)) % 0.38/0.77 (define @t233 () (_ @t232 @t229)) % 0.38/0.77 (define @t234 () (_ @t132 @t231)) % 0.38/0.77 (define @t235 () (@list @t131 @t231 @t229)) % 0.38/0.77 (define @t236 () (_ @t157 @t139)) % 0.38/0.77 (define @t237 () (@list @t156 @t148 @t139)) % 0.38/0.77 (define @t238 () (_ @t142 @t154)) % 0.38/0.77 (define @t239 () (= @t164 @t154)) % 0.38/0.77 (define @t240 () (@list @t141 @t164 @t154)) % 0.38/0.77 (define @t241 () (=> @t150 @t236)) % 0.38/0.77 (define @t242 () (=> @t166 @t238)) % 0.38/0.77 (define @t243 () (= @t129 @t226)) % 0.38/0.77 (define @t244 () (_ @t227 @t129)) % 0.38/0.77 (define @t245 () (= @t131 @t231)) % 0.38/0.77 (define @t246 () (_ @t232 @t131)) % 0.38/0.77 (define @t247 () (not @t234)) % 0.38/0.77 (define @t248 () (_ tptp.ord_less_eq_a @t229)) % 0.38/0.77 (define @t249 () (_ @t248 @t131)) % 0.38/0.77 (define @t250 () (_ @t248 @t231)) % 0.38/0.77 (define @t251 () (@list @t131 @t231)) % 0.38/0.77 (define @t252 () (@list @t129 @t226)) % 0.38/0.77 (define @t253 () (@var "X5" (-> Bool tptp.a))) % 0.38/0.77 (define @t254 () (@var "Y4" (-> Bool tptp.a))) % 0.38/0.77 (define @t255 () (@var "Y4" tptp.a)) % 0.38/0.77 (define @t256 () (@var "P" (-> (-> Bool tptp.a) Bool))) % 0.38/0.77 (define @t257 () (_ tptp.order_Greatest_o_a @t256)) % 0.38/0.77 (define @t258 () (forall (@list @t143) (=> (_ @t256 @t143) (_ (_ tptp.ord_less_eq_o_a @t143) @t129)))) % 0.38/0.77 (define @t259 () (_ @t256 @t129)) % 0.38/0.77 (define @t260 () (_ tptp.order_Greatest_a @t194)) % 0.38/0.77 (define @t261 () (forall (@list @t158) (=> (_ @t194 @t158) (_ (_ tptp.ord_less_eq_a @t158) @t131)))) % 0.38/0.77 (define @t262 () (_ @t194 @t131)) % 0.38/0.77 (define @t263 () (@var "Q" (-> (-> Bool tptp.a) Bool))) % 0.38/0.77 (define @t264 () (@var "Y5" (-> Bool tptp.a))) % 0.38/0.77 (define @t265 () (@var "Q" (-> tptp.a Bool))) % 0.38/0.77 (define @t266 () (@var "Y5" tptp.a)) % 0.38/0.77 (define @t267 () (@list @t159)) % 0.38/0.77 (define @t268 () (@var "Y6" (-> Bool tptp.a))) % 0.38/0.77 (define @t269 () (@var "X6" (-> Bool tptp.a))) % 0.38/0.77 (define @t270 () (@var "Q" (-> tptp.tree_a tptp.tree_a Bool))) % 0.38/0.77 (define @t271 () (@var "B23" tptp.tree_a)) % 0.38/0.77 (define @t272 () (@var "B22" tptp.tree_a)) % 0.38/0.77 (define @t273 () (@var "B21" tptp.a)) % 0.38/0.77 (define @t274 () (@var "A23" tptp.tree_a)) % 0.38/0.77 (define @t275 () (@var "A22" tptp.tree_a)) % 0.38/0.77 (define @t276 () (@var "A21" tptp.a)) % 0.38/0.77 (define @t277 () (@var "R3" (-> tptp.a tptp.a Bool))) % 0.38/0.77 (define @t278 () (_ tptp.rel_Tree_a_a @t277)) % 0.38/0.77 (define @t279 () (@var "Ra" (-> tptp.a tptp.a Bool))) % 0.38/0.77 (define @t280 () (_ tptp.rel_Tree_a_a @t279)) % 0.38/0.77 (define @t281 () (@var "Z" tptp.tree_a)) % 0.38/0.77 (define @t282 () (@var "Y3" tptp.tree_a)) % 0.38/0.77 (define @t283 () (_ (_ @t278 @t44) @t43)) % 0.38/0.77 (define @t284 () (_ (_ @t278 @t46) @t45)) % 0.38/0.77 (define @t285 () (_ (_ @t277 @t48) @t47)) % 0.38/0.77 (define @t286 () (_ (_ @t278 @t51) @t50)) % 0.38/0.77 (define @t287 () (_ @t278 tptp.e_a)) % 0.38/0.77 (define @t288 () (@list @t277 @t47 @t45 @t43)) % 0.38/0.77 (define @t289 () (@var "Y32" tptp.tree_a)) % 0.38/0.77 (define @t290 () (@var "Y24" tptp.tree_a)) % 0.38/0.77 (define @t291 () (@var "Y1" tptp.a)) % 0.38/0.77 (define @t292 () (@var "B" tptp.tree_a)) % 0.38/0.77 (define @t293 () (@var "A" tptp.tree_a)) % 0.38/0.77 (define @t294 () (_ tptp.set_mset_a (_ tptp.multiset_a2 @t37))) % 0.38/0.77 (define @t295 () (@var "B4" tptp.multiset_a)) % 0.38/0.77 (define @t296 () (@var "A2" tptp.multiset_a)) % 0.38/0.77 (define @t297 () (_ tptp.add_mset_a @t141)) % 0.38/0.77 (define @t298 () (_ @t297 @t295)) % 0.38/0.77 (define @t299 () (_ @t297 @t296)) % 0.38/0.77 (define @t300 () (@list @t141 @t296 @t295)) % 0.38/0.77 (define @t301 () (@var "M" tptp.multiset_a)) % 0.38/0.77 (define @t302 () (_ tptp.add_mset_a @t131)) % 0.38/0.77 (define @t303 () (_ @t302 @t301)) % 0.38/0.77 (define @t304 () (@var "B5" tptp.multiset_a)) % 0.38/0.77 (define @t305 () (_ tptp.set_mset_a @t296)) % 0.38/0.77 (define @t306 () (_ @t195 @t305)) % 0.38/0.77 (define @t307 () (@list @t141 @t296)) % 0.38/0.77 (define @t308 () (@var "A5" tptp.multiset_a)) % 0.38/0.77 (define @t309 () (_ tptp.set_mset_a @t301)) % 0.38/0.77 (define @t310 () (_ tptp.member_a @t131)) % 0.38/0.77 (define @t311 () (_ @t310 @t309)) % 0.38/0.77 (define @t312 () (_ tptp.add_mset_a @t231)) % 0.38/0.77 (define @t313 () (@var "K" tptp.multiset_a)) % 0.38/0.77 (define @t314 () (@var "N" tptp.multiset_a)) % 0.38/0.77 (define @t315 () (_ tptp.add_mset_a @t164)) % 0.38/0.77 (define @t316 () (_ @t315 @t314)) % 0.38/0.77 (define @t317 () (_ @t297 @t301)) % 0.38/0.77 (define @t318 () (_ tptp.set_mset_a @t295)) % 0.38/0.77 (define @t319 () (_ tptp.member_a @t154)) % 0.38/0.77 (define @t320 () (@var "C2" tptp.multiset_a)) % 0.38/0.77 (define @t321 () (@var "P" (-> tptp.multiset_a Bool))) % 0.38/0.77 (define @t322 () (_ @t321 @t301)) % 0.38/0.77 (define @t323 () (@var "M2" tptp.multiset_a)) % 0.38/0.77 (define @t324 () (_ tptp.add_mset_a @t159)) % 0.38/0.77 (define @t325 () (_ @t321 (_ @t324 @t323))) % 0.38/0.77 (define @t326 () (@var "Xa" tptp.a)) % 0.38/0.77 (define @t327 () (_ tptp.member_a @t326)) % 0.38/0.77 (define @t328 () (_ @t327 (_ tptp.set_mset_a @t323))) % 0.38/0.77 (define @t329 () (@list @t326)) % 0.38/0.77 (define @t330 () (_ @t321 @t323)) % 0.38/0.77 (define @t331 () (@list @t159 @t323)) % 0.38/0.77 (define @t332 () (_ @t321 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t333 () (@list @t321 @t301)) % 0.38/0.77 (define @t334 () (= @t301 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t335 () (_ @t312 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t336 () (and (= @t164 @t141) @t334)) % 0.38/0.77 (define @t337 () (_ @t315 @t301)) % 0.38/0.77 (define @t338 () (_ @t297 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t339 () (_ @t315 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t340 () (@var "N2" tptp.multiset_a)) % 0.38/0.77 (define @t341 () (not @t334)) % 0.38/0.77 (define @t342 () (@list @t301)) % 0.38/0.77 (define @t343 () (@var "P" (-> tptp.multiset_a tptp.multiset_a Bool))) % 0.38/0.77 (define @t344 () (_ tptp.add_mset_a @t222)) % 0.38/0.77 (define @t345 () (_ @t343 @t323)) % 0.38/0.77 (define @t346 () (_ @t345 @t340)) % 0.38/0.77 (define @t347 () (@list @t222 @t323 @t340)) % 0.38/0.77 (define @t348 () (_ tptp.member_a @t159)) % 0.38/0.77 (define @t349 () (_ @t302 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t350 () (_ tptp.subseteq_mset_a @t338)) % 0.38/0.77 (define @t351 () (_ tptp.plus_plus_multiset_a @t296)) % 0.38/0.77 (define @t352 () (_ @t351 @t295)) % 0.38/0.77 (define @t353 () (_ @t297 @t352)) % 0.38/0.77 (define @t354 () (@var "A" tptp.multiset_a)) % 0.38/0.77 (define @t355 () (_ tptp.plus_plus_multiset_a @t354)) % 0.38/0.77 (define @t356 () (@var "L" tptp.multiset_a)) % 0.38/0.77 (define @t357 () (@var "J" tptp.multiset_a)) % 0.38/0.77 (define @t358 () (@var "K2" tptp.multiset_a)) % 0.38/0.77 (define @t359 () (@var "I" tptp.multiset_a)) % 0.38/0.77 (define @t360 () (_ (_ tptp.ord_le1199012836iset_a (_ (_ tptp.plus_plus_multiset_a @t359) @t358)) (_ (_ tptp.plus_plus_multiset_a @t357) @t356))) % 0.38/0.77 (define @t361 () (_ (_ tptp.ord_le1199012836iset_a @t359) @t357)) % 0.38/0.77 (define @t362 () (@list @t359 @t357 @t358 @t356)) % 0.38/0.77 (define @t363 () (_ (_ tptp.ord_le1199012836iset_a @t358) @t356)) % 0.38/0.77 (define @t364 () (@var "D" tptp.multiset_a)) % 0.38/0.77 (define @t365 () (@var "B" tptp.multiset_a)) % 0.38/0.77 (define @t366 () (_ tptp.plus_plus_multiset_a @t365)) % 0.38/0.77 (define @t367 () (@var "C" tptp.multiset_a)) % 0.38/0.77 (define @t368 () (_ tptp.ord_le1199012836iset_a (_ @t355 @t367))) % 0.38/0.77 (define @t369 () (_ (_ tptp.ord_le1199012836iset_a @t354) @t365)) % 0.38/0.77 (define @t370 () (_ tptp.plus_plus_multiset_a @t367)) % 0.38/0.77 (define @t371 () (@list @t354 @t365 @t367)) % 0.38/0.77 (define @t372 () (_ @t195 @t318)) % 0.38/0.77 (define @t373 () (_ (_ tptp.subseteq_mset_a @t296) @t295)) % 0.38/0.77 (define @t374 () (= @t314 tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t375 () (_ (_ tptp.plus_plus_multiset_a @t301) @t314)) % 0.38/0.77 (define @t376 () (@var "A6" tptp.multiset_a)) % 0.38/0.77 (define @t377 () (@var "F3" tptp.multiset_a)) % 0.38/0.77 (define @t378 () (@var "F4" tptp.multiset_a)) % 0.38/0.77 (define @t379 () (@var "XS" tptp.multiset_a)) % 0.38/0.77 (define @t380 () (@var "R" tptp.set_Product_prod_a_a)) % 0.38/0.77 (define @t381 () (@var "B6" tptp.a)) % 0.38/0.77 (define @t382 () (_ tptp.product_Pair_a_a @t381)) % 0.38/0.77 (define @t383 () (@var "K3" tptp.multiset_a)) % 0.38/0.77 (define @t384 () (_ tptp.set_mset_a @t383)) % 0.38/0.77 (define @t385 () (_ (_ tptp.member_a @t381) @t384)) % 0.38/0.77 (define @t386 () (@list @t381)) % 0.38/0.77 (define @t387 () (@var "M0" tptp.multiset_a)) % 0.38/0.77 (define @t388 () (@list @t383)) % 0.38/0.77 (define @t389 () (_ tptp.mult1_a @t380)) % 0.38/0.77 (define @t390 () (_ tptp.produc2037245207iset_a @t314)) % 0.38/0.77 (define @t391 () (_ (_ tptp.member340150864iset_a (_ @t390 @t301)) @t389)) % 0.38/0.77 (define @t392 () (@var "K4" tptp.multiset_a)) % 0.38/0.77 (define @t393 () (_ tptp.set_mset_a @t392)) % 0.38/0.77 (define @t394 () (@var "M02" tptp.multiset_a)) % 0.38/0.77 (define @t395 () (_ tptp.plus_plus_multiset_a @t394)) % 0.38/0.77 (define @t396 () (_ @t297 @t394)) % 0.38/0.77 (define @t397 () (@var "B4" tptp.set_a)) % 0.38/0.77 (define @t398 () (_ (_ tptp.ord_less_eq_set_a @t196) @t397)) % 0.38/0.77 (define @t399 () (@var "B7" tptp.set_a)) % 0.38/0.77 (define @t400 () (@var "T2" tptp.a)) % 0.38/0.77 (define @t401 () (_ tptp.member_a @t400)) % 0.38/0.77 (define @t402 () (@var "A6" tptp.set_a)) % 0.38/0.77 (define @t403 () (@list @t402 @t399)) % 0.38/0.77 (define @t404 () (_ tptp.mult_a @t380)) % 0.38/0.77 (define @t405 () (@var "J2" tptp.multiset_a)) % 0.38/0.77 (define @t406 () (@var "I2" tptp.multiset_a)) % 0.38/0.77 (define @t407 () (_ tptp.plus_plus_multiset_a @t406)) % 0.38/0.77 (define @t408 () (@var "Xa2" tptp.a)) % 0.38/0.77 (define @t409 () (@var "X7" tptp.a)) % 0.38/0.77 (define @t410 () (@var "J3" tptp.multiset_a)) % 0.38/0.77 (define @t411 () (@var "I3" tptp.multiset_a)) % 0.38/0.77 (define @t412 () (_ tptp.plus_plus_multiset_a @t411)) % 0.38/0.77 (define @t413 () (@var "X5" tptp.multiset_a)) % 0.38/0.77 (define @t414 () (@var "M" tptp.multiset_multiset_a)) % 0.38/0.77 (define @t415 () (_ (_ tptp.comm_m315775925iset_a tptp.plus_plus_multiset_a) tptp.zero_zero_multiset_a)) % 0.38/0.77 (define @t416 () (@var "S" tptp.set_Product_prod_a_a)) % 0.38/0.77 (define @t417 () (_ tptp.mult_a @t416)) % 0.38/0.77 (define @t418 () (@var "Y7" tptp.multiset_a)) % 0.38/0.77 (define @t419 () (@var "X8" tptp.multiset_a)) % 0.38/0.77 (define @t420 () (@var "Uu" tptp.a)) % 0.38/0.77 (define @t421 () (_ tptp.add_mset_a @t420)) % 0.38/0.77 (define @t422 () (@var "N3" tptp.multiset_a)) % 0.38/0.77 (define @t423 () (@var "NN" tptp.multiset_multiset_a)) % 0.38/0.77 (define @t424 () (@var "G" (-> tptp.a tptp.multiset_a))) % 0.38/0.77 (define @t425 () (@var "F" (-> tptp.a tptp.multiset_a))) % 0.38/0.77 (define @t426 () (@var "I4" tptp.a)) % 0.38/0.77 (define @t427 () (_ tptp.image_mset_a_a @t175)) % 0.38/0.77 (define @t428 () (_ @t427 @t301)) % 0.38/0.77 (define @t429 () (_ tptp.add_mset_a @t188)) % 0.38/0.77 (define @t430 () (_ @t427 @t317)) % 0.38/0.77 (define @t431 () (@var "M1" tptp.multiset_a)) % 0.38/0.77 (define @t432 () (@var "N1" tptp.multiset_a)) % 0.38/0.77 (define @t433 () (_ tptp.heapIm1091024090Down_a @t7)) % 0.38/0.77 (define @t434 () (_ tptp.is_heap_a @t433)) % 0.38/0.77 (define @t435 () (not @t434)) % 0.38/0.77 (define @t436 () (@var "X5" Bool)) % 0.38/0.77 (define @t437 () (@var "G2" (-> Bool tptp.a))) % 0.38/0.77 (define @t438 () (@var "F2" (-> Bool tptp.a))) % 0.38/0.77 (define @t439 () (lambda (@list @t438 @t437) (forall (@list @t436) (_ (_ tptp.ord_less_eq_a (_ @t438 @t436)) (_ @t437 @t436))))) % 0.38/0.77 (define @t440 () (@var "Y6" (-> Bool Bool tptp.a))) % 0.38/0.77 (define @t441 () (@var "X6" (-> Bool Bool tptp.a))) % 0.38/0.77 (define @t442 () (lambda (@list @t441 @t440) (and (_ (_ tptp.ord_less_eq_o_a (_ @t441 false)) (_ @t440 false)) (_ (_ tptp.ord_less_eq_o_a (_ @t441 true)) (_ @t440 true))))) % 0.38/0.77 (define @t443 () (lambda @t403 (forall @t199 (=> (_ @t198 @t402) (_ @t198 @t399))))) % 0.38/0.77 (define @t444 () (tptp.t_a @t87 @t86 @t85)) % 0.38/0.77 (define @t445 () (tptp.is_heap_a @t444)) % 0.38/0.77 (define @t446 () (tptp.val_a @t444)) % 0.38/0.77 (define @t447 () (tptp.ord_less_eq_a @t446 @t9)) % 0.38/0.77 (define @t448 () (tptp.t_a @t9 tptp.e_a @t444)) % 0.38/0.77 (define @t449 () (tptp.is_heap_a @t448)) % 0.38/0.77 (define @t450 () (tptp.t_a tptp.v1 tptp.l1 tptp.r1)) % 0.38/0.77 (define @t451 () (tptp.t_a tptp.v2 tptp.e_a @t450)) % 0.38/0.77 (define @t452 () (tptp.heapIm1091024090Down_a @t451)) % 0.38/0.77 (define @t453 () (tptp.is_heap_a @t452)) % 0.38/0.77 (define @t454 () (@var "BOUND_VARIABLE_10151" tptp.tree_a)) % 0.38/0.77 (define @t455 () (@var "BOUND_VARIABLE_10149" tptp.tree_a)) % 0.38/0.77 (define @t456 () (@var "BOUND_VARIABLE_10147" tptp.a)) % 0.38/0.77 (define @t457 () (_ (_ (_ tptp.t_a @t456) @t455) @t454)) % 0.38/0.77 (define @t458 () (_ tptp.heapIm1257206334ight_a @t457)) % 0.38/0.77 (define @t459 () (_ tptp.heapIm1140443833left_a @t457)) % 0.38/0.77 (define @t460 () (@var "BOUND_VARIABLE_10153" tptp.a)) % 0.38/0.77 (define @t461 () (_ tptp.t_a @t460)) % 0.38/0.77 (define @t462 () (_ (_ @t461 @t459) @t458)) % 0.38/0.77 (define @t463 () (_ tptp.heapIm1091024090Down_a @t462)) % 0.38/0.77 (define @t464 () (_ tptp.val_a @t457)) % 0.38/0.77 (define @t465 () (tptp.t_a @t456 @t455 @t454)) % 0.38/0.77 (define @t466 () (tptp.heapIm1257206334ight_a @t465)) % 0.38/0.77 (define @t467 () (tptp.heapIm1140443833left_a @t465)) % 0.38/0.77 (define @t468 () (tptp.t_a @t460 @t467 @t466)) % 0.38/0.77 (define @t469 () (tptp.heapIm1091024090Down_a @t468)) % 0.38/0.77 (define @t470 () (tptp.val_a @t465)) % 0.38/0.77 (define @t471 () (tptp.t_a @t470 tptp.e_a @t469)) % 0.38/0.77 (define @t472 () (_ (_ (_ tptp.t_a @t464) tptp.e_a) @t463)) % 0.38/0.77 (define @t473 () (_ @t461 tptp.e_a)) % 0.38/0.77 (define @t474 () (_ @t473 @t457)) % 0.38/0.77 (define @t475 () (tptp.t_a @t460 tptp.e_a @t465)) % 0.38/0.77 (define @t476 () (tptp.heapIm1091024090Down_a @t475)) % 0.38/0.77 (define @t477 () (_ tptp.heapIm1091024090Down_a @t474)) % 0.38/0.77 (define @t478 () (= @t477 @t472)) % 0.38/0.77 (define @t479 () (tptp.ord_less_eq_a @t470 @t460)) % 0.38/0.77 (define @t480 () (_ (_ tptp.ord_less_eq_a @t464) @t460)) % 0.38/0.77 (define @t481 () (or @t480 @t478)) % 0.38/0.77 (define @t482 () (forall (@list @t456 @t455 @t454 @t460) @t481)) % 0.38/0.77 (define @t483 () (@var "BOUND_VARIABLE_10128" tptp.tree_a)) % 0.38/0.77 (define @t484 () (@var "BOUND_VARIABLE_10126" tptp.tree_a)) % 0.38/0.77 (define @t485 () (@var "BOUND_VARIABLE_10124" tptp.a)) % 0.38/0.77 (define @t486 () (_ (_ (_ tptp.t_a @t485) @t484) @t483)) % 0.38/0.77 (define @t487 () (@var "BOUND_VARIABLE_10130" tptp.a)) % 0.38/0.77 (define @t488 () (_ (_ tptp.t_a @t487) tptp.e_a)) % 0.38/0.77 (define @t489 () (_ @t488 @t486)) % 0.38/0.77 (define @t490 () (tptp.t_a @t485 @t484 @t483)) % 0.38/0.77 (define @t491 () (tptp.t_a @t487 tptp.e_a @t490)) % 0.38/0.77 (define @t492 () (tptp.heapIm1091024090Down_a @t491)) % 0.38/0.77 (define @t493 () (_ tptp.heapIm1091024090Down_a @t489)) % 0.38/0.77 (define @t494 () (= @t489 @t493)) % 0.38/0.77 (define @t495 () (_ tptp.val_a @t486)) % 0.38/0.77 (define @t496 () (tptp.val_a @t490)) % 0.38/0.77 (define @t497 () (tptp.ord_less_eq_a @t496 @t487)) % 0.38/0.77 (define @t498 () (_ (_ tptp.ord_less_eq_a @t495) @t487)) % 0.38/0.77 (define @t499 () (not @t498)) % 0.38/0.77 (define @t500 () (or @t499 @t494)) % 0.38/0.77 (define @t501 () (forall (@list @t485 @t484 @t483 @t487) @t500)) % 0.38/0.77 (define @t502 () (or @t104 @t117)) % 0.38/0.77 (define @t503 () (forall @t114 @t502)) % 0.38/0.77 (define @t504 () (@list @t87 @t86 @t85 @t9)) % 0.38/0.77 (define @t505 () (= @t115 @t116)) % 0.38/0.77 (define @t506 () (or @t105 @t505)) % 0.38/0.77 (define @t507 () (forall @t114 @t506)) % 0.38/0.77 (define @t508 () (and @t507 @t503)) % 0.38/0.77 (define @t509 () (and (=> @t104 @t505) @t118)) % 0.38/0.77 (define @t510 () (tptp.ord_less_eq_a tptp.v1 tptp.v2)) % 0.38/0.77 (define @t511 () (tptp.t_a @t9 @t74 @t73)) % 0.38/0.77 (define @t512 () (tptp.val_a @t511)) % 0.38/0.77 (define @t513 () (= @t9 @t76)) % 0.38/0.77 (define @t514 () (tptp.ord_less_eq_a (tptp.val_a @t450) tptp.v2)) % 0.38/0.77 (define @t515 () (= @t451 @t452)) % 0.38/0.77 (define @t516 () (not @t514)) % 0.38/0.77 (define @t517 () (or @t516 @t515)) % 0.38/0.77 (define @t518 () (@list false false)) % 0.38/0.77 (define @t519 () (tptp.is_heap_a @t451)) % 0.38/0.77 (define @t520 () (tptp.is_heap_a tptp.ra)) % 0.38/0.77 (define @t521 () (tptp.t_a @t47 @t45 @t43)) % 0.38/0.77 (define @t522 () (tptp.t_a @t48 @t46 @t44)) % 0.38/0.77 (define @t523 () (= @t522 @t521)) % 0.38/0.77 (define @t524 () (= tptp.e_a tptp.la)) % 0.38/0.77 (define @t525 () (= tptp.v2 tptp.va)) % 0.38/0.77 (define @t526 () (and @t525 @t524 (= @t450 tptp.ra))) % 0.38/0.77 (define @t527 () (tptp.t_a tptp.va tptp.la tptp.ra)) % 0.38/0.77 (define @t528 () (= @t451 @t527)) % 0.38/0.77 (define @t529 () (forall @t54 (= @t49 @t523))) % 0.38/0.77 (define @t530 () (= @t526 @t528)) % 0.38/0.77 (define @t531 () (= tptp.ra @t450)) % 0.38/0.77 (define @t532 () (and @t525 @t524 @t531)) % 0.38/0.77 (define @t533 () (= @t527 @t451)) % 0.38/0.77 (define @t534 () (= @t533 @t532)) % 0.38/0.77 (define @t535 () (@list false)) % 0.38/0.77 (define @t536 () (tptp.is_heap_a @t450)) % 0.38/0.77 (define @t537 () (and @t514 @t536)) % 0.38/0.77 (define @t538 () (= @t519 @t537)) % 0.38/0.77 (assume @p1 @t1) % 0.38/0.77 (assume @p2 (_ tptp.is_heap_a tptp.la)) % 0.38/0.77 (assume @p3 (_ tptp.is_heap_a tptp.r)) % 0.38/0.77 (assume @p4 (_ tptp.is_heap_a tptp.l)) % 0.38/0.77 (assume @p5 @t2) % 0.38/0.77 (assume @p6 @t8) % 0.38/0.77 (assume @p7 (forall @t13 (= (_ tptp.heapIm1091024090Down_a @t12) @t12))) % 0.38/0.77 (assume @p8 (= (_ tptp.heapIm1091024090Down_a tptp.e_a) tptp.e_a)) % 0.38/0.77 (assume @p9 (forall @t32 (=> @t31 (=> @t30 (=> @t29 (=> @t28 @t25)))))) % 0.38/0.77 (assume @p10 (= tptp.t (_ (_ (_ tptp.t_a tptp.v) tptp.l) tptp.r))) % 0.38/0.77 (assume @p11 (forall @t13 (_ tptp.is_heap_a @t12))) % 0.38/0.77 (assume @p12 (forall (@list @t37 @t9 @t40 @t39) (=> (= @t37 @t41) (exists (@list @t36 @t33 @t35) (and (= @t38 (_ (_ (_ tptp.t_a @t33) @t36) @t35)) (_ @t34 @t33)))))) % 0.38/0.77 (assume @p13 (forall (@list @t40 @t39 @t9) (=> (not (_ (_ tptp.ord_less_eq_a (_ tptp.val_a @t4)) tptp.v2)) (=> (_ tptp.is_heap_a @t40) (=> (_ tptp.is_heap_a @t39) (=> (= @t42 @t41) (_ tptp.is_heap_a (_ tptp.heapIm1091024090Down_a @t42)))))))) % 0.38/0.77 (assume @p14 @t55) % 0.38/0.77 (assume @p15 (_ tptp.is_heap_a tptp.e_a)) % 0.38/0.77 (assume @p16 (forall (@list @t48 @t46 @t44) (not (= tptp.e_a @t51)))) % 0.38/0.77 (assume @p17 (forall (@list @t57 @t56) (=> (_ @t57 tptp.e_a) (=> (forall @t62 (=> (_ @t57 @t59) (=> (_ @t57 @t58) (_ @t57 @t61)))) (_ @t57 @t56))))) % 0.38/0.77 (assume @p18 (forall (@list @t66) (=> (not (= @t66 tptp.e_a)) (not (forall (@list @t65 @t64 @t63) (not (= @t66 (_ (_ (_ tptp.t_a @t65) @t64) @t63)))))))) % 0.38/0.77 (assume @p19 (forall @t32 (=> @t31 (=> @t30 (=> @t28 (=> @t29 @t25)))))) % 0.38/0.77 (assume @p20 (= tptp.in_tree_a (lambda (@list @t68 @t67) (_ (_ tptp.in_tree_a @t68) (_ tptp.heapIm1091024090Down_a @t67))))) % 0.38/0.77 (assume @p21 (forall @t69 (= (_ tptp.heapIm1140443833left_a @t41) @t40))) % 0.38/0.77 (assume @p22 (forall (@list @t9 @t37) (=> (_ @t72 @t37) (=> @t71 (_ @t34 @t70))))) % 0.38/0.77 (assume @p23 @t78) % 0.38/0.77 (assume @p24 (forall (@list @t9 @t79 @t40 @t39) (= (_ @t72 (_ (_ (_ tptp.t_a @t79) @t40) @t39)) (or (= @t9 @t79) (_ @t72 @t40) (_ @t72 @t39))))) % 0.38/0.77 (assume @p25 (forall (@list @t82 @t81 @t80 @t87 @t86 @t85 @t9) (and (=> @t99 (and (=> @t104 @t97) (=> @t105 (= @t93 (_ @t102 @t83))))) (=> (not @t99) (and (=> @t95 @t97) (=> @t96 (= @t93 (_ (_ @t90 @t88) @t84)))))))) % 0.38/0.77 (assume @p26 (forall (@list @t87 @t86 @t85 @t82 @t81 @t80 @t9) (and (=> @t109 (and (=> @t95 @t108) (=> @t96 (= @t107 (_ (_ @t90 @t84) @t88))))) (=> (not @t109) (and (=> @t104 @t108) (=> @t105 (= @t107 (_ (_ @t101 @t83) @t100)))))))) % 0.38/0.77 (assume @p27 (forall @t13 (not (_ @t72 tptp.e_a)))) % 0.38/0.77 (assume @p28 (forall (@list @t9 @t87 @t86 @t85 @t82 @t81 @t80) (= (_ tptp.is_heap_a @t92) (and @t95 @t111 @t104 @t110)))) % 0.38/0.77 (assume @p29 (forall (@list @t9 @t82 @t81 @t80 @t87 @t86 @t85) (= (_ tptp.is_heap_a @t106) (and @t104 @t110 @t95 @t111)))) % 0.38/0.77 (assume @p30 (forall @t114 (and (=> @t104 (= @t113 @t112)) (=> @t105 (= @t113 (_ @t102 tptp.e_a)))))) % 0.38/0.77 (assume @p31 @t121) % 0.38/0.77 (assume @p32 (forall @t123 (=> @t122 (_ (_ tptp.in_tree_a (_ tptp.val_a @t38)) @t37)))) % 0.38/0.77 (assume @p33 @t128) % 0.38/0.77 (assume @p34 (forall @t127 (= (_ tptp.is_heap_a @t112) @t124))) % 0.38/0.77 (assume @p35 (forall @t69 (= (_ tptp.heapIm1257206334ight_a @t41) @t39))) % 0.38/0.77 (assume @p36 (forall (@list @t129) (_ @t130 @t129))) % 0.38/0.77 (assume @p37 (forall @t133 (_ @t132 @t131))) % 0.38/0.77 (assume @p38 (forall (@list @t136 @t135 @t134) (=> @t137 (_ (_ tptp.ord_less_eq_a (_ @t136 @t134)) (_ @t135 @t134))))) % 0.38/0.77 (assume @p39 (forall (@list @t136 @t135) (=> (forall (@list @t138) (_ (_ tptp.ord_less_eq_a (_ @t136 @t138)) (_ @t135 @t138))) @t137))) % 0.38/0.77 (assume @p40 (forall @t153 (=> (_ @t142 @t152) @t151))) % 0.38/0.77 (assume @p41 (forall @t169 (=> (_ @t157 @t168) @t167))) % 0.38/0.77 (assume @p42 (forall @t174 (=> (_ @t157 @t173) @t172))) % 0.38/0.77 (assume @p43 (forall @t179 (=> (_ @t142 @t178) @t177))) % 0.38/0.77 (assume @p44 (forall @t182 (=> @t181 (=> (_ (_ tptp.ord_less_eq_o_a @t168) @t139) @t180)))) % 0.38/0.77 (assume @p45 (forall @t185 (=> @t184 (=> (_ (_ tptp.ord_less_eq_a @t152) @t154) @t183)))) % 0.38/0.77 (assume @p46 (forall @t187 (=> @t184 (=> (_ (_ tptp.ord_less_eq_o_a @t173) @t139) @t186)))) % 0.38/0.77 (assume @p47 (forall @t190 (=> @t181 (=> (_ (_ tptp.ord_less_eq_a @t178) @t154) @t189)))) % 0.38/0.77 (assume @p48 (forall @t193 (or @t192 (not @t181) (not @t191)))) % 0.38/0.77 (assume @p49 (forall @t169 (=> (= @t156 @t168) @t167))) % 0.38/0.77 (assume @p50 (forall @t153 (=> (= @t141 @t152) @t151))) % 0.38/0.77 (assume @p51 (forall @t174 (=> (= @t156 @t173) @t172))) % 0.38/0.77 (assume @p52 (forall @t179 (=> (= @t141 @t178) @t177))) % 0.38/0.77 (assume @p53 (forall @t182 (=> @t181 (=> (= @t168 @t139) @t180)))) % 0.38/0.77 (assume @p54 (forall @t185 (=> @t184 (=> (= @t152 @t154) @t183)))) % 0.38/0.77 (assume @p55 (forall @t187 (=> @t184 (=> (= @t173 @t139) @t186)))) % 0.38/0.77 (assume @p56 (forall @t190 (=> @t181 (=> (= @t178 @t154) @t189)))) % 0.38/0.77 (assume @p57 (forall (@list @t141 @t194) (= (_ @t195 (_ tptp.collect_a @t194)) (_ @t194 @t141)))) % 0.38/0.77 (assume @p58 (forall (@list @t196) (= (_ tptp.collect_a (lambda @t199 (_ @t198 @t196))) @t196))) % 0.38/0.77 (assume @p59 (forall (@list @t148 @t156) (=> @t201 (=> @t184 @t200)))) % 0.38/0.77 (assume @p60 (forall (@list @t164 @t141) (=> @t191 (=> @t181 @t192)))) % 0.38/0.77 (assume @p61 (= @t209 (lambda @t206 (and @t205 @t204)))) % 0.38/0.77 (assume @p62 (= @t217 (lambda @t214 (and @t213 @t212)))) % 0.38/0.77 (assume @p63 (forall (@list @t148 @t156 @t139) (=> @t201 (=> (_ @t218 @t148) (_ @t218 @t156))))) % 0.38/0.77 (assume @p64 (forall (@list @t164 @t141 @t154) (=> @t191 (=> (_ @t219 @t164) (_ @t219 @t141))))) % 0.38/0.77 (assume @p65 (forall (@list @t220 @t141 @t164) (=> (forall @t224 (=> (_ (_ tptp.ord_less_eq_a @t222) @t221) @t223)) (=> (forall @t224 (=> (_ (_ @t220 @t221) @t222) @t223)) (_ (_ @t220 @t141) @t164))))) % 0.38/0.77 (assume @p66 (forall (@list @t156) (_ @t157 @t156))) % 0.38/0.77 (assume @p67 (forall (@list @t141) (_ @t142 @t141))) % 0.38/0.77 (assume @p68 (forall (@list @t129 @t226 @t225) (=> @t228 (=> (_ @t227 @t225) (_ @t130 @t225))))) % 0.38/0.77 (assume @p69 (forall @t235 (=> @t234 (=> @t233 @t230)))) % 0.38/0.77 (assume @p70 (forall (@list @t156 @t148) (=> @t184 (=> @t201 @t200)))) % 0.38/0.77 (assume @p71 (forall @t193 (=> @t181 (=> @t191 @t192)))) % 0.38/0.77 (assume @p72 (forall @t237 (=> @t184 (=> (= @t148 @t139) @t236)))) % 0.38/0.77 (assume @p73 (forall @t240 (=> @t181 (=> @t239 @t238)))) % 0.38/0.77 (assume @p74 (forall @t237 (=> @t200 @t241))) % 0.38/0.77 (assume @p75 (forall @t240 (=> @t192 @t242))) % 0.38/0.77 (assume @p76 (= @t209 (lambda @t206 (and @t204 @t205)))) % 0.38/0.77 (assume @p77 (= @t217 (lambda @t214 (and @t212 @t213)))) % 0.38/0.77 (assume @p78 (forall (@list @t226 @t129) (=> @t244 (= @t228 @t243)))) % 0.38/0.77 (assume @p79 (forall (@list @t231 @t131) (=> @t246 (= @t234 @t245)))) % 0.38/0.77 (assume @p80 (forall @t235 (=> (=> @t234 (not @t233)) (=> (=> @t246 (not @t230)) (=> (=> @t230 (not @t250)) (=> (=> @t250 (not @t246)) (=> (=> @t233 (not @t249)) (not (=> @t249 @t247))))))))) % 0.38/0.77 (assume @p81 (forall @t237 (=> @t184 @t241))) % 0.38/0.77 (assume @p82 (forall @t240 (=> @t181 @t242))) % 0.38/0.77 (assume @p83 (forall @t251 (=> @t247 @t246))) % 0.38/0.77 (assume @p84 (forall @t252 (=> @t243 @t228))) % 0.38/0.77 (assume @p85 (forall @t251 (=> @t245 @t234))) % 0.38/0.77 (assume @p86 (forall @t251 (or @t234 @t246))) % 0.38/0.77 (assume @p87 (forall @t252 (=> @t228 (=> @t244 @t243)))) % 0.38/0.77 (assume @p88 (forall @t251 (=> @t234 (=> @t246 @t245)))) % 0.38/0.77 (assume @p89 (= @t209 (lambda (@list @t253 @t254) (and (_ (_ tptp.ord_less_eq_o_a @t253) @t254) (_ (_ tptp.ord_less_eq_o_a @t254) @t253))))) % 0.38/0.77 (assume @p90 (= @t217 (lambda (@list @t197 @t255) (and (_ (_ tptp.ord_less_eq_a @t197) @t255) (_ (_ tptp.ord_less_eq_a @t255) @t197))))) % 0.38/0.77 (assume @p91 (forall (@list @t256 @t129) (=> @t259 (=> @t258 (= @t257 @t129))))) % 0.38/0.77 (assume @p92 (forall (@list @t194 @t131) (=> @t262 (=> @t261 (= @t260 @t131))))) % 0.38/0.77 (assume @p93 (forall (@list @t256 @t129 @t263) (=> @t259 (=> @t258 (=> (forall (@list @t144) (=> (_ @t256 @t144) (=> (forall (@list @t264) (=> (_ @t256 @t264) (_ (_ tptp.ord_less_eq_o_a @t264) @t144))) (_ @t263 @t144)))) (_ @t263 @t257)))))) % 0.38/0.77 (assume @p94 (forall (@list @t194 @t131 @t265) (=> @t262 (=> @t261 (=> (forall @t267 (=> (_ @t194 @t159) (=> (forall (@list @t266) (=> (_ @t194 @t266) (_ (_ tptp.ord_less_eq_a @t266) @t159))) (_ @t265 @t159)))) (_ @t265 @t260)))))) % 0.38/0.77 (assume @p95 (= tptp.ord_less_eq_o_a (lambda (@list @t269 @t268) (and (_ (_ tptp.ord_less_eq_a (_ @t269 false)) (_ @t268 false)) (_ (_ tptp.ord_less_eq_a (_ @t269 true)) (_ @t268 true)))))) % 0.38/0.77 (assume @p96 (forall (@list @t277 @t24 @t66 @t270) (=> (_ (_ @t278 @t24) @t66) (=> (_ (_ @t270 tptp.e_a) tptp.e_a) (=> (forall (@list @t276 @t275 @t274 @t273 @t272 @t271) (=> (_ (_ @t277 @t276) @t273) (=> (_ (_ @t270 @t275) @t272) (=> (_ (_ @t270 @t274) @t271) (_ (_ @t270 (_ (_ (_ tptp.t_a @t276) @t275) @t274)) (_ (_ (_ tptp.t_a @t273) @t272) @t271)))))) (_ (_ @t270 @t24) @t66)))))) % 0.38/0.77 (assume @p97 (forall (@list @t277 @t279) (=> (_ (_ tptp.ord_less_eq_a_a_o @t277) @t279) (_ (_ tptp.ord_le1530450702ee_a_o @t278) @t280)))) % 0.38/0.77 (assume @p98 (= (_ tptp.rel_Tree_a_a @t217) (lambda (@list @t282 @t281) (= @t282 @t281)))) % 0.38/0.77 (assume @p99 (forall (@list @t279 @t24) (=> (forall @t267 (_ (_ @t279 @t159) @t159)) (_ (_ @t280 @t24) @t24)))) % 0.38/0.77 (assume @p100 (forall (@list @t277 @t48 @t46 @t44 @t47 @t45 @t43) (= @t286 (and @t285 @t284 @t283)))) % 0.38/0.77 (assume @p101 (forall (@list @t277 @t48 @t47 @t46 @t45 @t44 @t43) (=> @t285 (=> @t284 (=> @t283 @t286))))) % 0.38/0.77 (assume @p102 (forall (@list @t277) (_ @t287 tptp.e_a))) % 0.38/0.77 (assume @p103 (forall @t288 (not (_ (_ @t278 @t50) tptp.e_a)))) % 0.38/0.77 (assume @p104 (forall @t288 (not (_ @t287 @t50)))) % 0.38/0.77 (assume @p105 (forall (@list @t277 @t293 @t292) (=> (_ (_ @t278 @t293) @t292) (=> (=> (= @t293 tptp.e_a) (not (= @t292 tptp.e_a))) (not (forall @t62 (=> (= @t293 @t61) (forall (@list @t291 @t290 @t289) (=> (= @t292 (_ (_ (_ tptp.t_a @t291) @t290) @t289)) (=> (_ (_ @t277 @t60) @t291) (=> (_ (_ @t278 @t59) @t290) (not (_ (_ @t278 @t58) @t289))))))))))))) % 0.38/0.77 (assume @p106 (forall (@list @t141 @t37) (=> (_ @t195 @t294) (=> @t71 (_ @t142 @t70))))) % 0.38/0.77 (assume @p107 (forall @t300 (= (= @t299 @t298) (= @t296 @t295)))) % 0.38/0.77 (assume @p108 (forall (@list @t301 @t131) (not (= @t301 @t303)))) % 0.38/0.77 (assume @p109 (forall @t307 (=> @t306 (not (forall (@list @t304) (not (= @t296 (_ @t297 @t304)))))))) % 0.38/0.77 (assume @p110 (forall (@list @t131 @t301) (=> @t311 (exists (@list @t308) (= @t301 (_ @t302 @t308)))))) % 0.38/0.77 (assume @p111 (forall (@list @t131 @t231 @t301) (= (_ @t302 (_ @t312 @t301)) (_ @t312 @t303)))) % 0.38/0.77 (assume @p112 (forall (@list @t141 @t301 @t164 @t314) (= (= @t317 @t316) (or (and (= @t301 @t314) @t192) (exists (@list @t313) (and (= @t301 (_ @t315 @t313)) (= @t314 (_ @t297 @t313)))))))) % 0.38/0.77 (assume @p113 (forall (@list @t131 @t301 @t314) (=> (= @t303 @t314) (_ @t310 (_ tptp.set_mset_a @t314))))) % 0.38/0.77 (assume @p114 (forall (@list @t164 @t295 @t154 @t320) (=> (= (_ @t315 @t295) (_ (_ tptp.add_mset_a @t154) @t320)) (=> (not @t239) (_ @t319 @t318))))) % 0.38/0.77 (assume @p115 (forall @t123 (=> @t122 (=> @t71 (= @t70 (_ tptp.lattic146396397_Max_a @t294)))))) % 0.38/0.77 (assume @p116 (forall @t333 (=> @t332 (=> (forall @t331 (=> @t330 (=> (forall @t329 (=> @t328 (_ (_ tptp.ord_less_eq_a @t326) @t159))) @t325))) @t322)))) % 0.38/0.77 (assume @p117 (forall @t333 (=> @t332 (=> (forall @t331 (=> @t330 (=> (forall @t329 (=> @t328 (_ @t160 @t326))) @t325))) @t322)))) % 0.38/0.77 (assume @p118 (forall (@list @t131 @t301 @t231) (= (= @t303 @t335) (and @t334 @t245)))) % 0.38/0.77 (assume @p119 (forall (@list @t141 @t164 @t301) (= (= @t338 @t337) @t336))) % 0.38/0.77 (assume @p120 (forall (@list @t164 @t301 @t141) (= (= @t337 @t338) @t336))) % 0.38/0.77 (assume @p121 (forall @t193 (= (= @t338 @t339) @t192))) % 0.38/0.77 (assume @p122 (forall @t342 (=> @t341 (not (forall (@list @t159 @t340) (not (= @t301 (_ @t324 @t340)))))))) % 0.38/0.77 (assume @p123 (forall @t333 (=> @t332 (=> (forall @t331 (=> @t330 @t325)) @t322)))) % 0.38/0.77 (assume @p124 (forall (@list @t343 @t301 @t314) (=> (_ (_ @t343 tptp.zero_zero_multiset_a) tptp.zero_zero_multiset_a) (=> (forall @t347 (=> @t346 (_ (_ @t343 (_ @t344 @t323)) @t340))) (=> (forall @t347 (=> @t346 (_ @t345 (_ @t344 @t340)))) (_ (_ @t343 @t301) @t314)))))) % 0.38/0.77 (assume @p125 (forall @t307 (not (= tptp.zero_zero_multiset_a @t299)))) % 0.38/0.77 (assume @p126 (forall (@list @t296) (=> (not (= @t296 tptp.zero_zero_multiset_a)) (not (forall @t267 (not (_ @t348 @t305))))))) % 0.38/0.77 (assume @p127 (forall @t342 (=> @t341 (exists (@list @t308 @t222) (= @t301 (_ @t344 @t308)))))) % 0.38/0.77 (assume @p128 (forall @t133 (_ @t310 (_ tptp.set_mset_a @t349)))) % 0.38/0.77 (assume @p129 (= (_ tptp.multiset_a2 tptp.e_a) tptp.zero_zero_multiset_a)) % 0.38/0.77 (assume @p130 (forall @t69 (= (_ tptp.multiset_a2 @t41) (_ (_ tptp.plus_plus_multiset_a (_ (_ tptp.plus_plus_multiset_a (_ tptp.multiset_a2 @t40)) (_ (_ tptp.add_mset_a @t9) tptp.zero_zero_multiset_a))) (_ tptp.multiset_a2 @t39))))) % 0.38/0.77 (assume @p131 (forall (@list @t141 @t301) (= (_ @t350 @t301) (_ @t195 @t309)))) % 0.38/0.77 (assume @p132 (forall @t300 (= (_ (_ tptp.plus_plus_multiset_a @t299) @t295) @t353))) % 0.38/0.77 (assume @p133 (forall (@list @t296 @t141 @t295) (= (_ @t351 @t298) @t353))) % 0.38/0.77 (assume @p134 (forall (@list @t141 @t301 @t164) (= (_ (_ tptp.subseteq_mset_a @t317) @t339) (and @t334 @t192)))) % 0.38/0.77 (assume @p135 (forall (@list @t354) (= (_ @t355 tptp.zero_zero_multiset_a) @t354))) % 0.38/0.77 (assume @p136 (forall @t362 (=> (and @t361 (= @t358 @t356)) @t360))) % 0.38/0.77 (assume @p137 (forall @t362 (=> (and (= @t359 @t357) @t363) @t360))) % 0.38/0.77 (assume @p138 (forall @t362 (=> (and @t361 @t363) @t360))) % 0.38/0.77 (assume @p139 (forall (@list @t354 @t365 @t367 @t364) (=> @t369 (=> (_ (_ tptp.ord_le1199012836iset_a @t367) @t364) (_ @t368 (_ @t366 @t364)))))) % 0.38/0.77 (assume @p140 (forall @t371 (=> @t369 (_ (_ tptp.ord_le1199012836iset_a (_ @t370 @t354)) (_ @t370 @t365))))) % 0.38/0.77 (assume @p141 (forall @t371 (=> @t369 (_ @t368 (_ @t366 @t367))))) % 0.38/0.77 (assume @p142 (forall @t300 (= (_ @t195 (_ tptp.set_mset_a @t352)) (or @t306 @t372)))) % 0.38/0.77 (assume @p143 (forall (@list @t296 @t295 @t131) (=> @t373 (=> (_ @t310 @t305) (_ @t310 @t318))))) % 0.38/0.77 (assume @p144 (forall @t300 (= (_ (_ tptp.subseteq_mset_a @t299) @t298) @t373))) % 0.38/0.77 (assume @p145 (forall (@list @t296 @t295) (=> @t373 (_ (_ tptp.ord_less_eq_set_a @t305) @t318)))) % 0.38/0.77 (assume @p146 (forall (@list @t141 @t301 @t314) (= (= @t338 @t375) (or (and (= @t338 @t301) @t374) (and @t334 (= @t338 @t314)))))) % 0.38/0.77 (assume @p147 (forall (@list @t301 @t314 @t141) (= (= @t375 @t338) (or (and (= @t301 @t338) @t374) (and @t334 (= @t314 @t338)))))) % 0.38/0.77 (assume @p148 (= tptp.add_mset_a (lambda (@list @t211 @t376) (_ (_ tptp.plus_plus_multiset_a @t376) (_ (_ tptp.add_mset_a @t211) tptp.zero_zero_multiset_a))))) % 0.38/0.77 (assume @p149 (forall (@list @t377 @t296 @t321) (=> (_ (_ tptp.subseteq_mset_a @t377) @t296) (=> @t332 (=> (forall (@list @t222 @t378) (=> (_ (_ tptp.member_a @t222) @t305) (=> (_ @t321 @t378) (_ @t321 (_ @t344 @t378))))) (_ @t321 @t377)))))) % 0.38/0.77 (assume @p150 (forall (@list @t141 @t295) (=> @t372 (_ @t350 @t295)))) % 0.38/0.77 (assume @p151 (forall (@list @t131 @t379 @t231) (=> (_ @t310 (_ tptp.set_mset_a @t379)) (_ @t310 (_ tptp.set_mset_a (_ (_ tptp.plus_plus_multiset_a @t335) @t379)))))) % 0.38/0.77 (assume @p152 (forall (@list @t131 @t379) (_ @t310 (_ tptp.set_mset_a (_ (_ tptp.plus_plus_multiset_a @t349) @t379))))) % 0.38/0.77 (assume @p153 (forall (@list @t314 @t301 @t380) (=> @t391 (not (forall (@list @t222 @t387) (=> (= @t301 (_ @t344 @t387)) (forall @t388 (=> (= @t314 (_ (_ tptp.plus_plus_multiset_a @t387) @t383)) (not (forall @t386 (=> @t385 (_ (_ tptp.member449909584od_a_a (_ @t382 @t222)) @t380)))))))))))) % 0.38/0.77 (assume @p154 (forall (@list @t301 @t141 @t394 @t314 @t392 @t380) (=> (= @t301 @t396) (=> (= @t314 (_ @t395 @t392)) (=> (forall (@list @t221) (=> (_ (_ tptp.member_a @t221) @t393) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t221) @t141)) @t380))) @t391))))) % 0.38/0.77 (assume @p155 (forall (@list @t314 @t141 @t394 @t380) (=> (_ (_ tptp.member340150864iset_a (_ @t390 @t396)) @t389) (or (exists (@list @t323) (and (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t323) @t394)) @t389) (= @t314 (_ @t297 @t323)))) (exists @t388 (and (forall @t386 (=> @t385 (_ (_ tptp.member449909584od_a_a (_ @t382 @t141)) @t380))) (= @t314 (_ @t395 @t383)))))))) % 0.38/0.77 (assume @p156 (forall (@list @t196 @t397) (=> (forall @t267 (=> (_ @t348 @t196) (_ @t348 @t397))) @t398))) % 0.38/0.77 (assume @p157 (forall (@list @t196 @t397 @t131) (=> @t398 (=> (_ @t310 @t196) (_ @t310 @t397))))) % 0.38/0.77 (assume @p158 (forall (@list @t196 @t397 @t154) (=> @t398 (=> (_ @t319 @t196) (_ @t319 @t397))))) % 0.38/0.77 (assume @p159 (= tptp.ord_less_eq_set_a (lambda @t403 (forall (@list @t400) (=> (_ @t401 @t402) (_ @t401 @t399)))))) % 0.38/0.77 (assume @p160 (forall (@list @t405 @t392 @t380 @t406) (=> (not (= @t405 tptp.zero_zero_multiset_a)) (=> (forall @t267 (=> (_ @t348 @t393) (exists @t329 (and (_ @t327 (_ tptp.set_mset_a @t405)) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t159) @t326)) @t380))))) (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ @t407 @t392)) (_ @t407 @t405))) @t404))))) % 0.38/0.77 (assume @p161 (forall (@list @t380 @t301 @t314) (=> (_ tptp.trans_a @t380) (=> (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t301) @t314)) @t404) (exists (@list @t411 @t410) (and (= @t314 (_ @t412 @t410)) (exists @t388 (and (= @t301 (_ @t412 @t383)) (not (= @t410 tptp.zero_zero_multiset_a)) (forall (@list @t409) (=> (_ (_ tptp.member_a @t409) @t384) (exists (@list @t408) (and (_ (_ tptp.member_a @t408) (_ tptp.set_mset_a @t410)) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t409) @t408)) @t380))))))))))))) % 0.38/0.77 (assume @p162 (forall (@list @t414) (= (= (_ @t415 @t414) tptp.zero_zero_multiset_a) (forall (@list @t413) (=> (_ (_ tptp.member_multiset_a @t413) (_ tptp.set_mset_multiset_a @t414)) (= @t413 tptp.zero_zero_multiset_a)))))) % 0.38/0.77 (assume @p163 (forall (@list @t416 @t420 @t419 @t418) (=> (_ tptp.trans_a @t416) (=> (_ tptp.irrefl_a @t416) (= (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ @t421 @t419)) (_ @t421 @t418))) @t417) (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t419) @t418)) @t417)))))) % 0.38/0.77 (assume @p164 (forall (@list @t131 @t301 @t423) (= (_ @t310 (_ tptp.set_mset_a (_ (_ (_ tptp.fold_m382157835iset_a tptp.plus_plus_multiset_a) @t301) @t423))) (or @t311 (exists (@list @t422) (and (_ (_ tptp.member_multiset_a @t422) (_ tptp.set_mset_multiset_a @t423)) (_ @t310 (_ tptp.set_mset_a @t422)))))))) % 0.38/0.77 (assume @p165 (= tptp.plus_plus_multiset_a (_ tptp.fold_m364285649iset_a tptp.add_mset_a))) % 0.38/0.77 (assume @p166 (forall (@list @t301 @t141) (=> (_ (_ tptp.nO_MAT1617603563iset_a tptp.zero_zero_multiset_a) @t301) (= @t317 (_ (_ tptp.plus_plus_multiset_a @t338) @t301))))) % 0.38/0.77 (assume @p167 (forall (@list @t392 @t425 @t424) (=> (forall (@list @t426) (=> (_ (_ tptp.member_a @t426) @t393) (_ (_ tptp.subseteq_mset_a (_ @t425 @t426)) (_ @t424 @t426)))) (_ (_ tptp.subseteq_mset_a (_ @t415 (_ (_ tptp.image_929116801iset_a @t425) @t392))) (_ @t415 (_ (_ tptp.image_929116801iset_a @t424) @t392)))))) % 0.38/0.77 (assume @p168 (forall (@list @t175 @t141 @t301) (= @t430 (_ @t429 @t428)))) % 0.38/0.77 (assume @p169 (forall (@list @t175 @t301 @t164 @t314) (=> (= @t428 @t316) (exists (@list @t431 @t222) (and (= @t301 (_ @t344 @t431)) (= (_ @t175 @t222) @t164) (= (_ @t427 @t431) @t314)))))) % 0.38/0.77 (assume @p170 (forall (@list @t175 @t141 @t301 @t314) (=> (= @t430 @t314) (exists (@list @t432) (and (= @t314 (_ @t429 @t432)) (= @t428 @t432)))))) % 0.38/0.77 (assume @p171 (forall (@list @t175 @t131) (= (_ @t427 @t349) (_ (_ tptp.add_mset_a (_ @t175 @t131)) tptp.zero_zero_multiset_a)))) % 0.38/0.77 (assume @p172 @t435) % 0.38/0.77 (assume @p173 true) % 0.38/0.77 (step @p174 (= tptp.ord_less_eq_o_a @t439) :rule refl :args (@t439)) % 0.38/0.77 (step @p175 (= tptp.ord_less_eq_o_o_a @t442) :rule refl :args (@t442)) % 0.38/0.77 (step @p176 (= tptp.ord_less_eq_set_a @t443) :rule refl :args (@t443)) % 0.38/0.77 (step @p177 :rule refl :args ((tptp.is_heap_a @t88))) % 0.38/0.77 (step @p178 :rule refl :args (@t444)) % 0.38/0.77 (step @p179 :rule cong :premises (@p178) :args (@t445)) % 0.38/0.77 (step @p180 :rule trans :premises (@p179 @p177)) % 0.38/0.77 (step @p181 :rule refl :args (tptp.is_heap_a)) % 0.38/0.77 (step @p182 :rule ho_cong :premises (@p181 @p178)) % 0.38/0.77 (step @p183 :rule cong :premises (@p182 @p180) :args ((= (_ tptp.is_heap_a @t444) @t445))) % 0.38/0.77 (step @p184 :rule symm :premises (@p183)) % 0.38/0.77 (step @p185 :rule refl :args (@t110)) % 0.38/0.77 (step @p186 :rule eq_resolve :premises (@p185 @p184)) % 0.38/0.77 (step @p187 :rule refl :args (@t88)) % 0.38/0.77 (step @p188 :rule cong :premises (@p187 @p178) :args ((= @t88 @t444))) % 0.38/0.77 (step @p189 :rule symm :premises (@p188)) % 0.38/0.77 (step @p190 :rule eq_resolve :premises (@p187 @p189)) % 0.38/0.77 (step @p191 :rule ho_cong :premises (@p181 @p190)) % 0.38/0.77 (step @p192 :rule trans :premises (@p191 @p186)) % 0.38/0.77 (step @p193 :rule refl :args ((tptp.ord_less_eq_a @t98 @t9))) % 0.38/0.77 (step @p194 :rule refl :args (@t9)) % 0.38/0.77 (step @p195 :rule refl :args ((tptp.val_a @t88))) % 0.38/0.77 (step @p196 :rule cong :premises (@p178) :args (@t446)) % 0.38/0.77 (step @p197 :rule trans :premises (@p196 @p195)) % 0.38/0.77 (step @p198 :rule cong :premises (@p197 @p194) :args (@t447)) % 0.38/0.77 (step @p199 :rule trans :premises (@p198 @p193)) % 0.38/0.77 (step @p200 :rule refl :args (tptp.ord_less_eq_a)) % 0.38/0.77 (step @p201 :rule ho_cong :premises (@p200 @p197)) % 0.38/0.77 (step @p202 :rule ho_cong :premises (@p201 @p194)) % 0.38/0.77 (step @p203 :rule cong :premises (@p202 @p199) :args ((= (_ (_ tptp.ord_less_eq_a @t446) @t9) @t447))) % 0.38/0.77 (step @p204 :rule symm :premises (@p203)) % 0.38/0.77 (step @p205 :rule refl :args (@t104)) % 0.38/0.77 (step @p206 :rule eq_resolve :premises (@p205 @p204)) % 0.38/0.77 (step @p207 :rule refl :args (tptp.val_a)) % 0.38/0.77 (step @p208 :rule ho_cong :premises (@p207 @p178)) % 0.38/0.77 (step @p209 :rule cong :premises (@p208 @p197) :args ((= (_ tptp.val_a @t444) @t446))) % 0.38/0.77 (step @p210 :rule symm :premises (@p209)) % 0.38/0.77 (step @p211 :rule refl :args (@t98)) % 0.38/0.77 (step @p212 :rule eq_resolve :premises (@p211 @p210)) % 0.38/0.77 (step @p213 :rule ho_cong :premises (@p207 @p190)) % 0.38/0.77 (step @p214 :rule trans :premises (@p213 @p212)) % 0.38/0.77 (step @p215 :rule ho_cong :premises (@p200 @p214)) % 0.38/0.77 (step @p216 :rule ho_cong :premises (@p215 @p194)) % 0.38/0.77 (step @p217 :rule trans :premises (@p216 @p206)) % 0.38/0.77 (step @p218 :rule nary_cong :premises (@p217 @p192) :args (@t124)) % 0.38/0.77 (step @p219 :rule refl :args ((tptp.is_heap_a @t115))) % 0.38/0.77 (step @p220 :rule refl :args ((tptp.t_a @t9 tptp.e_a @t88))) % 0.38/0.77 (step @p221 :rule refl :args (tptp.e_a)) % 0.38/0.77 (step @p222 :rule cong :premises (@p194 @p221 @p178) :args (@t448)) % 0.38/0.77 (step @p223 :rule trans :premises (@p222 @p220)) % 0.38/0.77 (step @p224 :rule cong :premises (@p223) :args (@t449)) % 0.38/0.77 (step @p225 :rule trans :premises (@p224 @p219)) % 0.38/0.77 (step @p226 :rule ho_cong :premises (@p181 @p223)) % 0.38/0.77 (step @p227 :rule cong :premises (@p226 @p225) :args ((= (_ tptp.is_heap_a @t448) @t449))) % 0.38/0.77 (step @p228 :rule symm :premises (@p227)) % 0.38/0.77 (step @p229 :rule refl :args (@t125)) % 0.38/0.77 (step @p230 :rule eq_resolve :premises (@p229 @p228)) % 0.38/0.77 (step @p231 :rule refl :args (@t11)) % 0.38/0.77 (step @p232 :rule ho_cong :premises (@p231 @p178)) % 0.38/0.77 (step @p233 :rule cong :premises (@p232 @p223) :args ((= (_ @t11 @t444) @t448))) % 0.38/0.77 (step @p234 :rule symm :premises (@p233)) % 0.38/0.77 (step @p235 :rule refl :args (@t115)) % 0.38/0.77 (step @p236 :rule eq_resolve :premises (@p235 @p234)) % 0.38/0.77 (step @p237 :rule ho_cong :premises (@p231 @p190)) % 0.38/0.77 (step @p238 :rule trans :premises (@p237 @p236)) % 0.38/0.77 (step @p239 :rule ho_cong :premises (@p181 @p238)) % 0.38/0.77 (step @p240 :rule trans :premises (@p239 @p230)) % 0.38/0.77 (step @p241 :rule cong :premises (@p240 @p218) :args (@t126)) % 0.38/0.77 (step @p242 :rule cong :premises (@p241) :args (@t128)) % 0.38/0.77 (step @p243 :rule eq_resolve :premises (@p33 @p242)) % 0.38/0.77 (step @p244 :rule instantiate :premises (@p243) :args ((@list tptp.v2 tptp.v1 tptp.l1 tptp.r1))) % 0.38/0.77 (step @p245 :rule refl :args ((tptp.is_heap_a @t433))) % 0.38/0.77 (step @p246 :rule refl :args ((tptp.heapIm1091024090Down_a @t7))) % 0.38/0.77 (step @p247 :rule refl :args ((tptp.t_a tptp.v2 tptp.e_a @t4))) % 0.38/0.77 (step @p248 :rule refl :args (@t450)) % 0.38/0.77 (step @p249 :rule refl :args (tptp.v2)) % 0.38/0.77 (step @p250 :rule cong :premises (@p249 @p221 @p248) :args (@t451)) % 0.38/0.77 (step @p251 :rule trans :premises (@p250 @p247)) % 0.38/0.77 (step @p252 :rule cong :premises (@p251) :args (@t452)) % 0.38/0.77 (step @p253 :rule trans :premises (@p252 @p246)) % 0.38/0.77 (step @p254 :rule cong :premises (@p253) :args (@t453)) % 0.38/0.77 (step @p255 :rule trans :premises (@p254 @p245)) % 0.38/0.77 (step @p256 :rule ho_cong :premises (@p181 @p253)) % 0.38/0.77 (step @p257 :rule cong :premises (@p256 @p255) :args ((= (_ tptp.is_heap_a @t452) @t453))) % 0.38/0.77 (step @p258 :rule symm :premises (@p257)) % 0.38/0.77 (step @p259 :rule refl :args (@t434)) % 0.38/0.77 (step @p260 :rule eq_resolve :premises (@p259 @p258)) % 0.38/0.77 (step @p261 :rule refl :args (tptp.heapIm1091024090Down_a)) % 0.38/0.77 (step @p262 :rule ho_cong :premises (@p261 @p251)) % 0.38/0.77 (step @p263 :rule cong :premises (@p262 @p253) :args ((= (_ tptp.heapIm1091024090Down_a @t451) @t452))) % 0.38/0.77 (step @p264 :rule symm :premises (@p263)) % 0.38/0.77 (step @p265 :rule refl :args (@t433)) % 0.38/0.77 (step @p266 :rule eq_resolve :premises (@p265 @p264)) % 0.38/0.77 (step @p267 :rule refl :args (@t6)) % 0.38/0.77 (step @p268 :rule ho_cong :premises (@p267 @p248)) % 0.38/0.77 (step @p269 :rule cong :premises (@p268 @p251) :args ((= (_ @t6 @t450) @t451))) % 0.38/0.77 (step @p270 :rule symm :premises (@p269)) % 0.38/0.77 (step @p271 :rule refl :args (@t7)) % 0.38/0.77 (step @p272 :rule eq_resolve :premises (@p271 @p270)) % 0.38/0.77 (step @p273 :rule refl :args (@t4)) % 0.38/0.77 (step @p274 :rule cong :premises (@p273 @p248) :args ((= @t4 @t450))) % 0.38/0.77 (step @p275 :rule symm :premises (@p274)) % 0.38/0.77 (step @p276 :rule eq_resolve :premises (@p273 @p275)) % 0.38/0.77 (step @p277 :rule refl :args (@t6)) % 0.38/0.77 (step @p278 :rule ho_cong :premises (@p277 @p276)) % 0.38/0.77 (step @p279 :rule trans :premises (@p278 @p272)) % 0.38/0.77 (step @p280 :rule refl :args (tptp.heapIm1091024090Down_a)) % 0.38/0.77 (step @p281 :rule ho_cong :premises (@p280 @p279)) % 0.38/0.77 (step @p282 :rule trans :premises (@p281 @p266)) % 0.38/0.77 (step @p283 :rule refl :args (tptp.is_heap_a)) % 0.38/0.77 (step @p284 :rule ho_cong :premises (@p283 @p282)) % 0.38/0.77 (step @p285 :rule trans :premises (@p284 @p260)) % 0.38/0.77 (step @p286 :rule cong :premises (@p285) :args (@t435)) % 0.38/0.77 (step @p287 :rule eq_resolve :premises (@p172 @p286)) % 0.38/0.77 (step @p288 :rule false_intro :premises (@p287)) % 0.38/0.77 (step @p289 :rule refl :args ((tptp.t_a @t464 tptp.e_a @t463))) % 0.38/0.77 (step @p290 :rule refl :args ((tptp.heapIm1091024090Down_a @t462))) % 0.38/0.77 (step @p291 :rule refl :args ((tptp.t_a @t460 @t459 @t458))) % 0.38/0.77 (step @p292 :rule refl :args ((tptp.heapIm1257206334ight_a @t457))) % 0.38/0.77 (step @p293 :rule refl :args (@t465)) % 0.38/0.77 (step @p294 :rule cong :premises (@p293) :args (@t466)) % 0.38/0.77 (step @p295 :rule trans :premises (@p294 @p292)) % 0.38/0.77 (step @p296 :rule refl :args ((tptp.heapIm1140443833left_a @t457))) % 0.38/0.77 (step @p297 :rule cong :premises (@p293) :args (@t467)) % 0.38/0.77 (step @p298 :rule trans :premises (@p297 @p296)) % 0.38/0.77 (step @p299 :rule refl :args (@t460)) % 0.38/0.77 (step @p300 :rule cong :premises (@p299 @p298 @p295) :args (@t468)) % 0.38/0.77 (step @p301 :rule trans :premises (@p300 @p291)) % 0.38/0.77 (step @p302 :rule cong :premises (@p301) :args (@t469)) % 0.38/0.77 (step @p303 :rule trans :premises (@p302 @p290)) % 0.38/0.77 (step @p304 :rule refl :args ((tptp.val_a @t457))) % 0.38/0.77 (step @p305 :rule cong :premises (@p293) :args (@t470)) % 0.38/0.77 (step @p306 :rule trans :premises (@p305 @p304)) % 0.38/0.77 (step @p307 :rule cong :premises (@p306 @p221 @p303) :args (@t471)) % 0.38/0.77 (step @p308 :rule trans :premises (@p307 @p289)) % 0.38/0.77 (step @p309 :rule refl :args (tptp.t_a)) % 0.38/0.77 (step @p310 :rule ho_cong :premises (@p309 @p306)) % 0.38/0.77 (step @p311 :rule ho_cong :premises (@p310 @p221)) % 0.38/0.77 (step @p312 :rule ho_cong :premises (@p311 @p303)) % 0.38/0.77 (step @p313 :rule cong :premises (@p312 @p308) :args ((= (_ (_ (_ tptp.t_a @t470) tptp.e_a) @t469) @t471))) % 0.38/0.77 (step @p314 :rule symm :premises (@p313)) % 0.38/0.77 (step @p315 :rule refl :args (@t472)) % 0.38/0.77 (step @p316 :rule eq_resolve :premises (@p315 @p314)) % 0.38/0.77 (step @p317 :rule ho_cong :premises (@p261 @p301)) % 0.38/0.77 (step @p318 :rule cong :premises (@p317 @p303) :args ((= (_ tptp.heapIm1091024090Down_a @t468) @t469))) % 0.38/0.77 (step @p319 :rule symm :premises (@p318)) % 0.38/0.77 (step @p320 :rule refl :args (@t463)) % 0.38/0.77 (step @p321 :rule eq_resolve :premises (@p320 @p319)) % 0.38/0.77 (step @p322 :rule refl :args (@t461)) % 0.38/0.77 (step @p323 :rule ho_cong :premises (@p322 @p298)) % 0.38/0.77 (step @p324 :rule ho_cong :premises (@p323 @p295)) % 0.38/0.77 (step @p325 :rule cong :premises (@p324 @p301) :args ((= (_ (_ @t461 @t467) @t466) @t468))) % 0.38/0.77 (step @p326 :rule symm :premises (@p325)) % 0.38/0.77 (step @p327 :rule refl :args (@t462)) % 0.38/0.77 (step @p328 :rule eq_resolve :premises (@p327 @p326)) % 0.38/0.77 (step @p329 :rule refl :args (tptp.heapIm1257206334ight_a)) % 0.38/0.77 (step @p330 :rule ho_cong :premises (@p329 @p293)) % 0.38/0.77 (step @p331 :rule cong :premises (@p330 @p295) :args ((= (_ tptp.heapIm1257206334ight_a @t465) @t466))) % 0.38/0.77 (step @p332 :rule symm :premises (@p331)) % 0.38/0.77 (step @p333 :rule refl :args (@t458)) % 0.38/0.77 (step @p334 :rule eq_resolve :premises (@p333 @p332)) % 0.38/0.77 (step @p335 :rule refl :args (@t457)) % 0.38/0.77 (step @p336 :rule cong :premises (@p335 @p293) :args ((= @t457 @t465))) % 0.38/0.77 (step @p337 :rule symm :premises (@p336)) % 0.38/0.77 (step @p338 :rule eq_resolve :premises (@p335 @p337)) % 0.38/0.77 (step @p339 :rule ho_cong :premises (@p329 @p338)) % 0.38/0.77 (step @p340 :rule trans :premises (@p339 @p334)) % 0.38/0.77 (step @p341 :rule refl :args (tptp.heapIm1140443833left_a)) % 0.38/0.77 (step @p342 :rule ho_cong :premises (@p341 @p293)) % 0.38/0.77 (step @p343 :rule cong :premises (@p342 @p298) :args ((= (_ tptp.heapIm1140443833left_a @t465) @t467))) % 0.38/0.77 (step @p344 :rule symm :premises (@p343)) % 0.38/0.77 (step @p345 :rule refl :args (@t459)) % 0.38/0.77 (step @p346 :rule eq_resolve :premises (@p345 @p344)) % 0.38/0.77 (step @p347 :rule ho_cong :premises (@p341 @p338)) % 0.38/0.77 (step @p348 :rule trans :premises (@p347 @p346)) % 0.38/0.77 (step @p349 :rule ho_cong :premises (@p322 @p348)) % 0.38/0.77 (step @p350 :rule ho_cong :premises (@p349 @p340)) % 0.38/0.77 (step @p351 :rule trans :premises (@p350 @p328)) % 0.38/0.77 (step @p352 :rule ho_cong :premises (@p261 @p351)) % 0.38/0.77 (step @p353 :rule trans :premises (@p352 @p321)) % 0.38/0.77 (step @p354 :rule ho_cong :premises (@p207 @p293)) % 0.38/0.77 (step @p355 :rule cong :premises (@p354 @p306) :args ((= (_ tptp.val_a @t465) @t470))) % 0.38/0.77 (step @p356 :rule symm :premises (@p355)) % 0.38/0.77 (step @p357 :rule refl :args (@t464)) % 0.38/0.77 (step @p358 :rule eq_resolve :premises (@p357 @p356)) % 0.38/0.77 (step @p359 :rule ho_cong :premises (@p207 @p338)) % 0.38/0.77 (step @p360 :rule trans :premises (@p359 @p358)) % 0.38/0.77 (step @p361 :rule ho_cong :premises (@p309 @p360)) % 0.38/0.77 (step @p362 :rule ho_cong :premises (@p361 @p221)) % 0.38/0.77 (step @p363 :rule ho_cong :premises (@p362 @p353)) % 0.38/0.77 (step @p364 :rule trans :premises (@p363 @p316)) % 0.38/0.77 (step @p365 :rule refl :args ((tptp.heapIm1091024090Down_a @t474))) % 0.38/0.77 (step @p366 :rule refl :args ((tptp.t_a @t460 tptp.e_a @t457))) % 0.38/0.77 (step @p367 :rule cong :premises (@p299 @p221 @p293) :args (@t475)) % 0.38/0.77 (step @p368 :rule trans :premises (@p367 @p366)) % 0.38/0.77 (step @p369 :rule cong :premises (@p368) :args (@t476)) % 0.38/0.77 (step @p370 :rule trans :premises (@p369 @p365)) % 0.38/0.77 (step @p371 :rule ho_cong :premises (@p261 @p368)) % 0.38/0.77 (step @p372 :rule cong :premises (@p371 @p370) :args ((= (_ tptp.heapIm1091024090Down_a @t475) @t476))) % 0.38/0.77 (step @p373 :rule symm :premises (@p372)) % 0.38/0.77 (step @p374 :rule refl :args (@t477)) % 0.38/0.77 (step @p375 :rule eq_resolve :premises (@p374 @p373)) % 0.38/0.77 (step @p376 :rule refl :args (@t473)) % 0.38/0.77 (step @p377 :rule ho_cong :premises (@p376 @p293)) % 0.38/0.77 (step @p378 :rule cong :premises (@p377 @p368) :args ((= (_ @t473 @t465) @t475))) % 0.38/0.77 (step @p379 :rule symm :premises (@p378)) % 0.38/0.77 (step @p380 :rule refl :args (@t474)) % 0.38/0.77 (step @p381 :rule eq_resolve :premises (@p380 @p379)) % 0.38/0.77 (step @p382 :rule ho_cong :premises (@p376 @p338)) % 0.38/0.77 (step @p383 :rule trans :premises (@p382 @p381)) % 0.38/0.77 (step @p384 :rule ho_cong :premises (@p261 @p383)) % 0.38/0.77 (step @p385 :rule trans :premises (@p384 @p375)) % 0.38/0.77 (step @p386 :rule cong :premises (@p385 @p364) :args (@t478)) % 0.38/0.77 (step @p387 :rule refl :args ((tptp.ord_less_eq_a @t464 @t460))) % 0.38/0.77 (step @p388 :rule cong :premises (@p306 @p299) :args (@t479)) % 0.38/0.77 (step @p389 :rule trans :premises (@p388 @p387)) % 0.38/0.77 (step @p390 :rule ho_cong :premises (@p200 @p306)) % 0.38/0.77 (step @p391 :rule ho_cong :premises (@p390 @p299)) % 0.38/0.77 (step @p392 :rule cong :premises (@p391 @p389) :args ((= (_ (_ tptp.ord_less_eq_a @t470) @t460) @t479))) % 0.38/0.77 (step @p393 :rule symm :premises (@p392)) % 0.38/0.77 (step @p394 :rule refl :args (@t480)) % 0.38/0.77 (step @p395 :rule eq_resolve :premises (@p394 @p393)) % 0.38/0.77 (step @p396 :rule ho_cong :premises (@p200 @p360)) % 0.38/0.77 (step @p397 :rule ho_cong :premises (@p396 @p299)) % 0.38/0.77 (step @p398 :rule trans :premises (@p397 @p395)) % 0.38/0.77 (step @p399 :rule nary_cong :premises (@p398 @p386) :args (@t481)) % 0.38/0.77 (step @p400 :rule cong :premises (@p399) :args (@t482)) % 0.38/0.77 (step @p401 :rule refl :args ((tptp.heapIm1091024090Down_a @t489))) % 0.38/0.77 (step @p402 :rule refl :args ((tptp.t_a @t487 tptp.e_a @t486))) % 0.38/0.77 (step @p403 :rule refl :args (@t490)) % 0.38/0.77 (step @p404 :rule refl :args (@t487)) % 0.38/0.77 (step @p405 :rule cong :premises (@p404 @p221 @p403) :args (@t491)) % 0.38/0.77 (step @p406 :rule trans :premises (@p405 @p402)) % 0.38/0.77 (step @p407 :rule cong :premises (@p406) :args (@t492)) % 0.38/0.77 (step @p408 :rule trans :premises (@p407 @p401)) % 0.38/0.77 (step @p409 :rule ho_cong :premises (@p261 @p406)) % 0.38/0.77 (step @p410 :rule cong :premises (@p409 @p408) :args ((= (_ tptp.heapIm1091024090Down_a @t491) @t492))) % 0.38/0.77 (step @p411 :rule symm :premises (@p410)) % 0.38/0.77 (step @p412 :rule refl :args (@t493)) % 0.38/0.77 (step @p413 :rule eq_resolve :premises (@p412 @p411)) % 0.38/0.77 (step @p414 :rule refl :args (@t488)) % 0.38/0.77 (step @p415 :rule ho_cong :premises (@p414 @p403)) % 0.38/0.77 (step @p416 :rule cong :premises (@p415 @p406) :args ((= (_ @t488 @t490) @t491))) % 0.38/0.77 (step @p417 :rule symm :premises (@p416)) % 0.38/0.77 (step @p418 :rule refl :args (@t489)) % 0.38/0.77 (step @p419 :rule eq_resolve :premises (@p418 @p417)) % 0.38/0.77 (step @p420 :rule refl :args (@t486)) % 0.38/0.77 (step @p421 :rule cong :premises (@p420 @p403) :args ((= @t486 @t490))) % 0.38/0.77 (step @p422 :rule symm :premises (@p421)) % 0.38/0.77 (step @p423 :rule eq_resolve :premises (@p420 @p422)) % 0.38/0.77 (step @p424 :rule ho_cong :premises (@p414 @p423)) % 0.38/0.77 (step @p425 :rule trans :premises (@p424 @p419)) % 0.38/0.77 (step @p426 :rule ho_cong :premises (@p261 @p425)) % 0.38/0.77 (step @p427 :rule trans :premises (@p426 @p413)) % 0.38/0.77 (step @p428 :rule cong :premises (@p425 @p427) :args (@t494)) % 0.38/0.77 (step @p429 :rule refl :args ((tptp.ord_less_eq_a @t495 @t487))) % 0.38/0.77 (step @p430 :rule refl :args ((tptp.val_a @t486))) % 0.38/0.77 (step @p431 :rule cong :premises (@p403) :args (@t496)) % 0.38/0.77 (step @p432 :rule trans :premises (@p431 @p430)) % 0.38/0.77 (step @p433 :rule cong :premises (@p432 @p404) :args (@t497)) % 0.38/0.77 (step @p434 :rule trans :premises (@p433 @p429)) % 0.38/0.77 (step @p435 :rule ho_cong :premises (@p200 @p432)) % 0.38/0.77 (step @p436 :rule ho_cong :premises (@p435 @p404)) % 0.38/0.77 (step @p437 :rule cong :premises (@p436 @p434) :args ((= (_ (_ tptp.ord_less_eq_a @t496) @t487) @t497))) % 0.38/0.77 (step @p438 :rule symm :premises (@p437)) % 0.38/0.77 (step @p439 :rule refl :args (@t498)) % 0.38/0.77 (step @p440 :rule eq_resolve :premises (@p439 @p438)) % 0.38/0.77 (step @p441 :rule ho_cong :premises (@p207 @p403)) % 0.38/0.77 (step @p442 :rule cong :premises (@p441 @p432) :args ((= (_ tptp.val_a @t490) @t496))) % 0.38/0.77 (step @p443 :rule symm :premises (@p442)) % 0.38/0.77 (step @p444 :rule refl :args (@t495)) % 0.38/0.77 (step @p445 :rule eq_resolve :premises (@p444 @p443)) % 0.38/0.77 (step @p446 :rule ho_cong :premises (@p207 @p423)) % 0.38/0.77 (step @p447 :rule trans :premises (@p446 @p445)) % 0.38/0.77 (step @p448 :rule ho_cong :premises (@p200 @p447)) % 0.38/0.77 (step @p449 :rule ho_cong :premises (@p448 @p404)) % 0.38/0.77 (step @p450 :rule trans :premises (@p449 @p440)) % 0.38/0.77 (step @p451 :rule cong :premises (@p450) :args (@t499)) % 0.38/0.77 (step @p452 :rule nary_cong :premises (@p451 @p428) :args (@t500)) % 0.38/0.77 (step @p453 :rule cong :premises (@p452) :args (@t501)) % 0.38/0.77 (step @p454 :rule nary_cong :premises (@p453 @p400) :args ((and @t501 @t482))) % 0.38/0.77 (step @p455 :rule alpha_equiv :args (@t503 @t504 (@list @t456 @t455 @t454 @t460))) % 0.38/0.77 (step @p456 :rule alpha_equiv :args (@t507 @t504 (@list @t485 @t484 @t483 @t487))) % 0.38/0.77 (step @p457 :rule nary_cong :premises (@p456 @p455) :args (@t508)) % 0.38/0.77 (step @p458 :rule quant-miniscope-and :args ((= (forall @t114 (and @t506 @t502)) @t508))) % 0.38/0.77 (step @p459 :rule trans :premises (@p458 @p457)) % 0.38/0.77 (step @p460 :rule trans :premises (@p459 @p454)) % 0.38/0.77 (step @p461 :rule refl :args (@t117)) % 0.38/0.77 (step @p462 :rule bool-double-not-elim :args (@t104)) % 0.38/0.77 (step @p463 :rule nary_cong :premises (@p462 @p461) :args ((or (not @t105) @t117))) % 0.38/0.77 (step @p464 :rule bool-impl-elim :args (@t105 @t117)) % 0.38/0.77 (step @p465 :rule trans :premises (@p464 @p463)) % 0.38/0.77 (step @p466 :rule bool-impl-elim :args (@t104 @t505)) % 0.38/0.77 (step @p467 :rule nary_cong :premises (@p466 @p465) :args (@t509)) % 0.38/0.77 (step @p468 :rule cong :premises (@p467) :args ((forall @t114 @t509))) % 0.38/0.77 (step @p469 :rule trans :premises (@p468 @p460)) % 0.38/0.77 (step @p470 :rule refl :args (@t118)) % 0.38/0.77 (step @p471 :rule eq-symm :args (@t116 @t115)) % 0.38/0.77 (step @p472 :rule refl :args (@t104)) % 0.38/0.77 (step @p473 :rule cong :premises (@p472 @p471) :args (@t119)) % 0.38/0.77 (step @p474 :rule nary_cong :premises (@p473 @p470) :args (@t120)) % 0.38/0.77 (step @p475 :rule cong :premises (@p474) :args (@t121)) % 0.38/0.77 (step @p476 :rule trans :premises (@p475 @p469)) % 0.38/0.77 (step @p477 :rule eq_resolve :premises (@p31 @p476)) % 0.38/0.77 (step @p478 :rule and_elim :premises (@p477) :args (0)) % 0.38/0.77 (step @p479 :rule instantiate :premises (@p478) :args ((@list tptp.v1 tptp.l1 tptp.r1 tptp.v2))) % 0.38/0.77 (step @p480 :rule refl :args (@t510)) % 0.38/0.77 (step @p481 :rule refl :args (@t2)) % 0.38/0.77 (step @p482 :rule cong :premises (@p481 @p480) :args ((= @t2 @t510))) % 0.38/0.77 (step @p483 :rule symm :premises (@p482)) % 0.38/0.77 (step @p484 :rule eq_resolve :premises (@p481 @p483)) % 0.38/0.77 (step @p485 :rule eq_resolve :premises (@p5 @p484)) % 0.38/0.77 (step @p486 :rule true_intro :premises (@p485)) % 0.38/0.77 (step @p487 :rule refl :args (tptp.v2)) % 0.38/0.77 (step @p488 :rule refl :args ((tptp.val_a @t75))) % 0.38/0.77 (step @p489 :rule refl :args (@t511)) % 0.38/0.77 (step @p490 :rule cong :premises (@p489) :args (@t512)) % 0.38/0.77 (step @p491 :rule trans :premises (@p490 @p488)) % 0.38/0.77 (step @p492 :rule ho_cong :premises (@p207 @p489)) % 0.38/0.77 (step @p493 :rule cong :premises (@p492 @p491) :args ((= (_ tptp.val_a @t511) @t512))) % 0.38/0.77 (step @p494 :rule symm :premises (@p493)) % 0.38/0.77 (step @p495 :rule refl :args (@t76)) % 0.38/0.77 (step @p496 :rule eq_resolve :premises (@p495 @p494)) % 0.38/0.77 (step @p497 :rule refl :args (@t75)) % 0.38/0.77 (step @p498 :rule cong :premises (@p497 @p489) :args ((= @t75 @t511))) % 0.38/0.77 (step @p499 :rule symm :premises (@p498)) % 0.38/0.77 (step @p500 :rule eq_resolve :premises (@p497 @p499)) % 0.38/0.77 (step @p501 :rule ho_cong :premises (@p207 @p500)) % 0.38/0.77 (step @p502 :rule trans :premises (@p501 @p496)) % 0.38/0.77 (step @p503 :rule cong :premises (@p194 @p502) :args (@t513)) % 0.38/0.77 (step @p504 :rule cong :premises (@p503) :args ((forall @t77 @t513))) % 0.38/0.77 (step @p505 :rule eq-symm :args (@t76 @t9)) % 0.38/0.77 (step @p506 :rule cong :premises (@p505) :args (@t78)) % 0.38/0.77 (step @p507 :rule trans :premises (@p506 @p504)) % 0.38/0.77 (step @p508 :rule eq_resolve :premises (@p23 @p507)) % 0.38/0.77 (step @p509 :rule instantiate :premises (@p508) :args ((@list tptp.v1 tptp.l1 tptp.r1))) % 0.38/0.77 (step @p510 :rule symm :premises (@p509)) % 0.38/0.77 (step @p511 :rule cong :premises (@p510 @p487) :args (@t514)) % 0.38/0.77 (step @p512 :rule trans :premises (@p511 @p486)) % 0.38/0.77 (step @p513 :rule true_elim :premises (@p512)) % 0.38/0.77 (step @p514 :rule cnf_or_pos :args (@t517)) % 0.38/0.77 (step @p515 :rule reordering :premises (@p514) :args ((or @t516 @t515 (not @t517)))) % 0.38/0.77 (step @p516 :rule chain_m_resolution :premises (@p515 @p513 @p479) :args (@t515 @t518 (@list @t514 @t517))) % 0.38/0.77 (step @p517 :rule cong :premises (@p516) :args (@t519)) % 0.38/0.77 (step @p518 :rule trans :premises (@p517 @p288)) % 0.38/0.77 (step @p519 :rule false_elim :premises (@p518)) % 0.38/0.77 (step @p520 :rule refl :args (@t520)) % 0.38/0.77 (step @p521 :rule refl :args (@t1)) % 0.38/0.77 (step @p522 :rule cong :premises (@p521 @p520) :args ((= @t1 @t520))) % 0.38/0.77 (step @p523 :rule symm :premises (@p522)) % 0.38/0.77 (step @p524 :rule eq_resolve :premises (@p521 @p523)) % 0.38/0.77 (step @p525 :rule eq_resolve :premises (@p1 @p524)) % 0.38/0.77 (step @p526 :rule true_intro :premises (@p525)) % 0.38/0.77 (step @p527 :rule eq-symm :args (@t523 @t49)) % 0.38/0.77 (step @p528 :rule cong :premises (@p527) :args ((forall @t54 (= @t523 @t49)))) % 0.38/0.77 (step @p529 :rule refl :args (@t49)) % 0.38/0.77 (step @p530 :rule refl :args (@t521)) % 0.38/0.77 (step @p531 :rule refl :args (@t50)) % 0.38/0.77 (step @p532 :rule cong :premises (@p531 @p530) :args ((= @t50 @t521))) % 0.38/0.77 (step @p533 :rule symm :premises (@p532)) % 0.38/0.77 (step @p534 :rule eq_resolve :premises (@p531 @p533)) % 0.38/0.77 (step @p535 :rule refl :args (@t522)) % 0.38/0.77 (step @p536 :rule refl :args (@t51)) % 0.38/0.77 (step @p537 :rule cong :premises (@p536 @p535) :args ((= @t51 @t522))) % 0.38/0.77 (step @p538 :rule symm :premises (@p537)) % 0.38/0.77 (step @p539 :rule eq_resolve :premises (@p536 @p538)) % 0.38/0.77 (step @p540 :rule cong :premises (@p539 @p534) :args (@t52)) % 0.38/0.77 (step @p541 :rule cong :premises (@p540 @p529) :args (@t53)) % 0.38/0.77 (step @p542 :rule cong :premises (@p541) :args (@t55)) % 0.38/0.77 (step @p543 :rule trans :premises (@p542 @p528)) % 0.38/0.77 (step @p544 :rule eq_resolve :premises (@p14 @p543)) % 0.38/0.77 (step @p545 :rule eq-symm :args (@t450 tptp.ra)) % 0.38/0.77 (step @p546 :rule refl :args (@t524)) % 0.38/0.77 (step @p547 :rule refl :args (@t525)) % 0.38/0.77 (step @p548 :rule nary_cong :premises (@p547 @p546 @p545) :args (@t526)) % 0.38/0.77 (step @p549 :rule eq-symm :args (@t451 @t527)) % 0.38/0.77 (step @p550 :rule cong :premises (@p549 @p548) :args ((= @t528 @t526))) % 0.38/0.77 (step @p551 :rule eq-symm :args (@t526 @t528)) % 0.38/0.77 (step @p552 :rule trans :premises (@p551 @p550)) % 0.38/0.77 (step @p553 :rule refl :args (@t529)) % 0.38/0.77 (step @p554 :rule cong :premises (@p553 @p552) :args ((=> @t529 @t530))) % 0.38/0.77 (assume-push @p586 @t529) % 0.38/0.77 (step @p556 :rule instantiate :premises (@p544) :args ((@list tptp.v2 tptp.e_a @t450 tptp.va tptp.la tptp.ra))) % 0.38/0.77 (step-pop @p587 :rule scope :premises (@p556)) % 0.38/0.77 (step @p557 :rule process_scope :premises (@p587) :args (@t530)) % 0.38/0.77 (step @p559 :rule eq_resolve :premises (@p557 @p554)) % 0.38/0.77 (step @p560 :rule implies_elim :premises (@p559)) % 0.38/0.77 (step @p561 :rule chain_m_resolution :premises (@p560 @p544) :args (@t534 @t535 (@list @t529))) % 0.38/0.77 (step @p562 :rule refl :args (@t527)) % 0.38/0.77 (step @p563 :rule refl :args (@t3)) % 0.38/0.77 (step @p564 :rule cong :premises (@p563 @p562) :args ((= @t3 @t527))) % 0.38/0.77 (step @p565 :rule symm :premises (@p564)) % 0.38/0.77 (step @p566 :rule eq_resolve :premises (@p563 @p565)) % 0.38/0.77 (step @p567 :rule cong :premises (@p279 @p566) :args (@t8)) % 0.38/0.77 (step @p568 :rule trans :premises (@p567 @p549)) % 0.38/0.77 (step @p569 :rule eq_resolve :premises (@p6 @p568)) % 0.38/0.77 (step @p570 :rule cnf_equiv_pos1 :args (@t534)) % 0.38/0.77 (step @p571 :rule reordering :premises (@p570) :args ((or (not @t533) @t532 (not @t534)))) % 0.38/0.77 (step @p572 :rule chain_m_resolution :premises (@p571 @p569 @p561) :args (@t532 @t518 (@list @t533 @t534))) % 0.38/0.77 (step @p573 :rule cnf_and_pos :args (@t532 2)) % 0.38/0.77 (step @p574 :rule reordering :premises (@p573) :args ((or @t531 (not @t532)))) % 0.38/0.77 (step @p575 :rule chain_m_resolution :premises (@p574 @p572) :args (@t531 @t535 (@list @t532))) % 0.38/0.77 (step @p576 :rule symm :premises (@p575)) % 0.38/0.77 (step @p577 :rule cong :premises (@p576) :args (@t536)) % 0.38/0.77 (step @p578 :rule trans :premises (@p577 @p526)) % 0.38/0.77 (step @p579 :rule true_elim :premises (@p578)) % 0.38/0.77 (step @p580 :rule cnf_and_neg :args (@t537)) % 0.38/0.77 (step @p581 :rule reordering :premises (@p580) :args ((or @t516 @t537 (not @t536)))) % 0.38/0.77 (step @p582 :rule chain_m_resolution :premises (@p581 @p513 @p579) :args (@t537 @t518 (@list @t514 @t536))) % 0.38/0.77 (step @p583 :rule cnf_equiv_pos2 :args (@t538)) % 0.38/0.77 (step @p584 :rule reordering :premises (@p583) :args ((or @t519 (not @t537) (not @t538)))) % 0.38/0.77 (step @p585 false :rule chain_m_resolution :premises (@p584 @p582 @p519 @p244) :args (false (@list false true false) (@list @t537 @t519 @t538))) % 0.38/0.77 ) % 0.38/0.77 % SZS output end Proof % 0.38/0.77 % cvc5 exiting %------------------------------------------------------------------------------