%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP069^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 : n006.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.70s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP069^1 : TPTP v9.2.1. Released v7.5.0. % 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n006.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:13:04 EDT 2026 % 0.16/0.34 % CPUTime : % 0.26/0.55 %----Proving TH0 % 0.38/0.70 --- 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.70 % SZS status Theorem % 0.38/0.70 % SZS output start Proof % 0.38/0.70 ( % 0.38/0.70 (declare-sort tptp.a 0) % 0.38/0.70 (declare-sort tptp.multiset_a 0) % 0.38/0.70 (declare-sort tptp.multiset_multiset_a 0) % 0.38/0.70 (declare-sort tptp.set_multiset_a 0) % 0.38/0.70 (declare-sort tptp.produc1127127335iset_a 0) % 0.38/0.70 (declare-sort tptp.set_Pr158363655iset_a 0) % 0.38/0.70 (declare-sort tptp.set_Product_prod_a_a 0) % 0.38/0.70 (declare-sort tptp.product_prod_a_a 0) % 0.38/0.70 (declare-sort tptp.tree_a 0) % 0.38/0.70 (declare-sort tptp.set_a 0) % 0.38/0.70 (declare-const tptp.zero_zero_multiset_a tptp.multiset_a) % 0.38/0.70 (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.70 (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.70 (declare-const tptp.irrefl_a (-> tptp.set_Product_prod_a_a Bool)) % 0.38/0.70 (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.70 (declare-const tptp.member_multiset_a (-> tptp.multiset_a tptp.set_multiset_a Bool)) % 0.38/0.70 (declare-const tptp.set_mset_multiset_a (-> tptp.multiset_multiset_a tptp.set_multiset_a)) % 0.38/0.70 (declare-const tptp.ord_less_eq_a (-> tptp.a tptp.a Bool)) % 0.38/0.70 (declare-const tptp.t_a (-> tptp.a tptp.tree_a tptp.tree_a tptp.tree_a)) % 0.38/0.70 (declare-const tptp.in_tree_a (-> tptp.a tptp.tree_a Bool)) % 0.38/0.70 (declare-const tptp.heapIm1257206334ight_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.70 (declare-const tptp.val_a (-> tptp.tree_a tptp.a)) % 0.38/0.70 (declare-const tptp.heapIm1140443833left_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.70 (declare-const tptp.heapIm1091024090Down_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.70 (declare-const tptp.set_mset_a (-> tptp.multiset_a tptp.set_a)) % 0.38/0.70 (declare-const tptp.v tptp.a) % 0.38/0.70 (declare-const tptp.heapIm970322378pify_a (-> tptp.tree_a tptp.tree_a)) % 0.38/0.70 (declare-const tptp.e_a tptp.tree_a) % 0.38/0.70 (declare-const tptp.ord_le1199012836iset_a (-> tptp.multiset_a tptp.multiset_a Bool)) % 0.38/0.70 (declare-const tptp.l tptp.tree_a) % 0.38/0.70 (declare-const tptp.mult1_a (-> tptp.set_Product_prod_a_a tptp.set_Pr158363655iset_a)) % 0.38/0.70 (declare-const tptp.is_heap_a (-> tptp.tree_a Bool)) % 0.38/0.70 (declare-const tptp.nO_MAT1617603563iset_a (-> tptp.multiset_a tptp.multiset_a Bool)) % 0.38/0.70 (declare-const tptp.r tptp.tree_a) % 0.38/0.70 (declare-const tptp.mult_a (-> tptp.set_Product_prod_a_a tptp.set_Pr158363655iset_a)) % 0.38/0.70 (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a)) % 0.38/0.70 (declare-const tptp.add_mset_a (-> tptp.a tptp.multiset_a tptp.multiset_a)) % 0.38/0.70 (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool)) % 0.38/0.70 (declare-const tptp.multiset_a2 (-> tptp.tree_a tptp.multiset_a)) % 0.38/0.70 (declare-const tptp.lattic146396397_Max_a (-> tptp.set_a tptp.a)) % 0.38/0.70 (declare-const tptp.trans_a (-> tptp.set_Product_prod_a_a Bool)) % 0.38/0.70 (declare-const tptp.order_Greatest_a (-> (-> tptp.a Bool) tptp.a)) % 0.38/0.70 (declare-const tptp.plus_plus_multiset_a (-> tptp.multiset_a tptp.multiset_a tptp.multiset_a)) % 0.38/0.70 (declare-const tptp.minus_1649712171iset_a (-> tptp.multiset_a tptp.multiset_a tptp.multiset_a)) % 0.38/0.70 (declare-const tptp.member449909584od_a_a (-> tptp.product_prod_a_a tptp.set_Product_prod_a_a Bool)) % 0.38/0.70 (declare-const tptp.product_Pair_a_a (-> tptp.a tptp.a tptp.product_prod_a_a)) % 0.38/0.70 (declare-const tptp.produc2037245207iset_a (-> tptp.multiset_a tptp.multiset_a tptp.produc1127127335iset_a)) % 0.38/0.70 (declare-const tptp.member340150864iset_a (-> tptp.produc1127127335iset_a tptp.set_Pr158363655iset_a Bool)) % 0.38/0.70 (define tptp.is_empty_a () (let ((_let_1 (@var "A6" tptp.multiset_a))) (lambda (@list _let_1) (= _let_1 tptp.zero_zero_multiset_a)))) % 0.38/0.70 (define @t1 () (_ tptp.heapIm970322378pify_a tptp.r)) % 0.38/0.70 (define @t2 () (_ tptp.is_heap_a @t1)) % 0.38/0.70 (define @t3 () (_ tptp.heapIm970322378pify_a tptp.l)) % 0.38/0.70 (define @t4 () (_ tptp.is_heap_a @t3)) % 0.38/0.70 (define @t5 () (_ tptp.t_a tptp.v)) % 0.38/0.70 (define @t6 () (_ (_ @t5 @t3) @t1)) % 0.38/0.70 (define @t7 () (_ tptp.heapIm1091024090Down_a @t6)) % 0.38/0.70 (define @t8 () (_ tptp.is_heap_a @t7)) % 0.38/0.70 (define @t9 () (=> (= @t6 @t6) @t8)) % 0.38/0.70 (define @t10 () (=> @t2 @t9)) % 0.38/0.70 (define @t11 () (=> @t4 @t10)) % 0.38/0.70 (define @t12 () (@var "R" tptp.tree_a)) % 0.38/0.70 (define @t13 () (_ tptp.heapIm970322378pify_a @t12)) % 0.38/0.70 (define @t14 () (@var "L" tptp.tree_a)) % 0.38/0.70 (define @t15 () (_ tptp.heapIm970322378pify_a @t14)) % 0.38/0.70 (define @t16 () (@var "V" tptp.a)) % 0.38/0.70 (define @t17 () (_ tptp.t_a @t16)) % 0.38/0.70 (define @t18 () (_ (_ @t17 @t15) @t13)) % 0.38/0.70 (define @t19 () (_ tptp.heapIm1091024090Down_a @t18)) % 0.38/0.70 (define @t20 () (_ (_ @t17 @t14) @t12)) % 0.38/0.70 (define @t21 () (_ tptp.heapIm970322378pify_a @t20)) % 0.38/0.70 (define @t22 () (= @t21 @t19)) % 0.38/0.70 (define @t23 () (@list @t16 @t14 @t12)) % 0.38/0.70 (define @t24 () (forall @t23 @t22)) % 0.38/0.70 (define @t25 () (@var "T" tptp.tree_a)) % 0.38/0.70 (define @t26 () (_ tptp.heapIm1091024090Down_a @t25)) % 0.38/0.70 (define @t27 () (= @t25 @t20)) % 0.38/0.70 (define @t28 () (@var "Y23" tptp.tree_a)) % 0.38/0.70 (define @t29 () (@var "X23" tptp.tree_a)) % 0.38/0.70 (define @t30 () (@var "Y22" tptp.tree_a)) % 0.38/0.70 (define @t31 () (@var "X22" tptp.tree_a)) % 0.38/0.70 (define @t32 () (@var "Y21" tptp.a)) % 0.38/0.70 (define @t33 () (@var "X21" tptp.a)) % 0.38/0.70 (define @t34 () (_ (_ (_ tptp.t_a @t33) @t31) @t29)) % 0.38/0.70 (define @t35 () (_ @t17 tptp.e_a)) % 0.38/0.70 (define @t36 () (_ @t35 tptp.e_a)) % 0.38/0.70 (define @t37 () (@list @t16)) % 0.38/0.70 (define @t38 () (@var "Vf" tptp.tree_a)) % 0.38/0.70 (define @t39 () (@var "Ve" tptp.tree_a)) % 0.38/0.70 (define @t40 () (@var "Vd" tptp.a)) % 0.38/0.70 (define @t41 () (@var "Vc" tptp.tree_a)) % 0.38/0.70 (define @t42 () (@var "Vb" tptp.tree_a)) % 0.38/0.70 (define @t43 () (@var "Va" tptp.a)) % 0.38/0.70 (define @t44 () (_ (_ (_ tptp.t_a @t43) @t42) @t41)) % 0.38/0.70 (define @t45 () (@var "V2" tptp.a)) % 0.38/0.70 (define @t46 () (_ tptp.t_a @t45)) % 0.38/0.70 (define @t47 () (_ @t46 @t44)) % 0.38/0.70 (define @t48 () (@var "X" tptp.tree_a)) % 0.38/0.70 (define @t49 () (not (forall (@list @t45 @t43 @t42 @t41 @t40 @t39 @t38) (not (= @t48 (_ @t47 (_ (_ (_ tptp.t_a @t40) @t39) @t38))))))) % 0.38/0.70 (define @t50 () (_ @t46 tptp.e_a)) % 0.38/0.70 (define @t51 () (@list @t45 @t43 @t42 @t41)) % 0.38/0.70 (define @t52 () (forall @t51 (not (= @t48 (_ @t50 @t44))))) % 0.38/0.70 (define @t53 () (forall @t51 (not (= @t48 (_ @t47 tptp.e_a))))) % 0.38/0.70 (define @t54 () (forall (@list @t45) (not (= @t48 (_ @t50 tptp.e_a))))) % 0.38/0.70 (define @t55 () (not (= @t48 tptp.e_a))) % 0.38/0.70 (define @t56 () (@list @t48)) % 0.38/0.70 (define @t57 () (_ tptp.in_tree_a @t16)) % 0.38/0.70 (define @t58 () (@var "V3" tptp.a)) % 0.38/0.70 (define @t59 () (@var "T2" tptp.tree_a)) % 0.38/0.70 (define @t60 () (@var "V4" tptp.a)) % 0.38/0.70 (define @t61 () (@var "X232" tptp.tree_a)) % 0.38/0.70 (define @t62 () (@var "X222" tptp.tree_a)) % 0.38/0.70 (define @t63 () (@var "X212" tptp.a)) % 0.38/0.70 (define @t64 () (@var "Y" tptp.tree_a)) % 0.38/0.70 (define @t65 () (@var "Tree" tptp.tree_a)) % 0.38/0.70 (define @t66 () (@var "P" (-> tptp.tree_a Bool))) % 0.38/0.70 (define @t67 () (@var "X3" tptp.tree_a)) % 0.38/0.70 (define @t68 () (@var "X2" tptp.tree_a)) % 0.38/0.70 (define @t69 () (@var "X1" tptp.a)) % 0.38/0.70 (define @t70 () (not (= @t25 tptp.e_a))) % 0.38/0.70 (define @t71 () (@list @t25)) % 0.38/0.70 (define @t72 () (@var "Vc2" tptp.tree_a)) % 0.38/0.70 (define @t73 () (@var "Vb2" tptp.tree_a)) % 0.38/0.70 (define @t74 () (@var "Va2" tptp.a)) % 0.38/0.70 (define @t75 () (_ (_ (_ tptp.t_a @t74) @t73) @t72)) % 0.38/0.70 (define @t76 () (_ tptp.heapIm1091024090Down_a (_ (_ @t17 (_ tptp.heapIm1140443833left_a @t75)) (_ tptp.heapIm1257206334ight_a @t75)))) % 0.38/0.70 (define @t77 () (_ tptp.val_a @t75)) % 0.38/0.70 (define @t78 () (_ tptp.t_a @t77)) % 0.38/0.70 (define @t79 () (_ @t35 @t75)) % 0.38/0.70 (define @t80 () (_ tptp.heapIm1091024090Down_a @t79)) % 0.38/0.70 (define @t81 () (_ tptp.ord_less_eq_a @t77)) % 0.38/0.70 (define @t82 () (_ @t81 @t16)) % 0.38/0.70 (define @t83 () (not @t82)) % 0.38/0.70 (define @t84 () (@list @t74 @t73 @t72 @t16)) % 0.38/0.70 (define @t85 () (_ @t78 @t76)) % 0.38/0.70 (define @t86 () (_ @t17 @t75)) % 0.38/0.70 (define @t87 () (_ @t86 tptp.e_a)) % 0.38/0.70 (define @t88 () (_ tptp.heapIm1091024090Down_a @t87)) % 0.38/0.70 (define @t89 () (@var "Vf2" tptp.tree_a)) % 0.38/0.70 (define @t90 () (@var "Ve2" tptp.tree_a)) % 0.38/0.70 (define @t91 () (@var "Vd2" tptp.a)) % 0.38/0.70 (define @t92 () (_ (_ (_ tptp.t_a @t91) @t90) @t89)) % 0.38/0.70 (define @t93 () (_ (_ @t17 @t92) @t75)) % 0.38/0.70 (define @t94 () (_ tptp.heapIm1091024090Down_a @t93)) % 0.38/0.70 (define @t95 () (= @t94 @t93)) % 0.38/0.70 (define @t96 () (_ tptp.val_a @t92)) % 0.38/0.70 (define @t97 () (_ @t81 @t96)) % 0.38/0.70 (define @t98 () (_ tptp.heapIm1091024090Down_a (_ (_ @t17 (_ tptp.heapIm1140443833left_a @t92)) (_ tptp.heapIm1257206334ight_a @t92)))) % 0.38/0.70 (define @t99 () (_ tptp.t_a @t96)) % 0.38/0.70 (define @t100 () (_ tptp.ord_less_eq_a @t96)) % 0.38/0.70 (define @t101 () (_ @t100 @t16)) % 0.38/0.70 (define @t102 () (not @t101)) % 0.38/0.70 (define @t103 () (_ @t86 @t92)) % 0.38/0.70 (define @t104 () (_ tptp.heapIm1091024090Down_a @t103)) % 0.38/0.70 (define @t105 () (= @t104 @t103)) % 0.38/0.70 (define @t106 () (_ @t100 @t77)) % 0.38/0.70 (define @t107 () (@var "V5" tptp.a)) % 0.38/0.70 (define @t108 () (_ tptp.ord_less_eq_a @t16)) % 0.38/0.70 (define @t109 () (@var "R2" tptp.tree_a)) % 0.38/0.70 (define @t110 () (@var "L2" tptp.tree_a)) % 0.38/0.70 (define @t111 () (_ tptp.is_heap_a @t92)) % 0.38/0.70 (define @t112 () (_ tptp.is_heap_a @t75)) % 0.38/0.70 (define @t113 () (_ tptp.val_a @t25)) % 0.38/0.70 (define @t114 () (_ tptp.is_heap_a @t25)) % 0.38/0.70 (define @t115 () (@var "Uv" tptp.tree_a)) % 0.38/0.70 (define @t116 () (@var "Uu" tptp.tree_a)) % 0.38/0.70 (define @t117 () (and @t82 @t112)) % 0.38/0.70 (define @t118 () (@list @t16 @t74 @t73 @t72)) % 0.38/0.70 (define @t119 () (@var "A" tptp.a)) % 0.38/0.70 (define @t120 () (@var "P" (-> tptp.a Bool))) % 0.38/0.70 (define @t121 () (_ tptp.member_a @t119)) % 0.38/0.70 (define @t122 () (@var "A2" tptp.set_a)) % 0.38/0.70 (define @t123 () (@var "X4" tptp.a)) % 0.38/0.70 (define @t124 () (@var "X" tptp.a)) % 0.38/0.70 (define @t125 () (_ tptp.ord_less_eq_a @t124)) % 0.38/0.70 (define @t126 () (@list @t124)) % 0.38/0.70 (define @t127 () (_ tptp.ord_less_eq_a @t119)) % 0.38/0.70 (define @t128 () (_ tptp.set_mset_a (_ tptp.multiset_a2 @t25))) % 0.38/0.70 (define @t129 () (@var "C" tptp.a)) % 0.38/0.70 (define @t130 () (@var "F" (-> tptp.a tptp.a))) % 0.38/0.70 (define @t131 () (@var "Y2" tptp.a)) % 0.38/0.70 (define @t132 () (@var "X5" tptp.a)) % 0.38/0.70 (define @t133 () (_ tptp.ord_less_eq_a @t132)) % 0.38/0.70 (define @t134 () (forall (@list @t132 @t131) (=> (_ @t133 @t131) (_ (_ tptp.ord_less_eq_a (_ @t130 @t132)) (_ @t130 @t131))))) % 0.38/0.70 (define @t135 () (@var "B" tptp.a)) % 0.38/0.70 (define @t136 () (_ tptp.ord_less_eq_a @t135)) % 0.38/0.70 (define @t137 () (_ @t136 @t129)) % 0.38/0.70 (define @t138 () (=> @t137 (=> @t134 (_ @t127 (_ @t130 @t129))))) % 0.38/0.70 (define @t139 () (_ @t130 @t135)) % 0.38/0.70 (define @t140 () (@list @t119 @t130 @t135 @t129)) % 0.38/0.70 (define @t141 () (=> @t134 (_ (_ tptp.ord_less_eq_a (_ @t130 @t119)) @t129))) % 0.38/0.70 (define @t142 () (_ @t127 @t135)) % 0.38/0.70 (define @t143 () (@list @t119 @t135 @t130 @t129)) % 0.38/0.70 (define @t144 () (@var "Y4" tptp.a)) % 0.38/0.70 (define @t145 () (@var "Z" tptp.a)) % 0.38/0.70 (define @t146 () (@var "Y3" tptp.a)) % 0.38/0.70 (define @t147 () (lambda (@list @t146 @t145) (= @t146 @t145))) % 0.38/0.70 (define @t148 () (@var "Y" tptp.a)) % 0.38/0.70 (define @t149 () (= @t124 @t148)) % 0.38/0.70 (define @t150 () (_ tptp.ord_less_eq_a @t148)) % 0.38/0.70 (define @t151 () (_ @t150 @t124)) % 0.38/0.70 (define @t152 () (_ @t125 @t148)) % 0.38/0.70 (define @t153 () (@list @t124 @t148)) % 0.38/0.70 (define @t154 () (not @t152)) % 0.38/0.70 (define @t155 () (_ @t127 @t129)) % 0.38/0.70 (define @t156 () (=> @t137 @t155)) % 0.38/0.70 (define @t157 () (@list @t119 @t135 @t129)) % 0.38/0.70 (define @t158 () (@var "Z2" tptp.a)) % 0.38/0.70 (define @t159 () (_ tptp.ord_less_eq_a @t158)) % 0.38/0.70 (define @t160 () (_ @t159 @t124)) % 0.38/0.70 (define @t161 () (_ @t150 @t158)) % 0.38/0.70 (define @t162 () (_ @t159 @t148)) % 0.38/0.70 (define @t163 () (_ @t125 @t158)) % 0.38/0.70 (define @t164 () (@list @t124 @t148 @t158)) % 0.38/0.70 (define @t165 () (@var "A3" tptp.a)) % 0.38/0.70 (define @t166 () (@var "B2" tptp.a)) % 0.38/0.70 (define @t167 () (_ (_ tptp.ord_less_eq_a @t166) @t165)) % 0.38/0.70 (define @t168 () (_ (_ tptp.ord_less_eq_a @t165) @t166)) % 0.38/0.70 (define @t169 () (@list @t165 @t166)) % 0.38/0.70 (define @t170 () (= @t119 @t135)) % 0.38/0.70 (define @t171 () (= @t135 @t129)) % 0.38/0.70 (define @t172 () (_ @t136 @t119)) % 0.38/0.70 (define @t173 () (@list @t119 @t135)) % 0.38/0.70 (define @t174 () (@var "P" (-> tptp.a tptp.a Bool))) % 0.38/0.70 (define @t175 () (@var "B3" tptp.a)) % 0.38/0.70 (define @t176 () (@var "A4" tptp.a)) % 0.38/0.70 (define @t177 () (_ (_ @t174 @t176) @t175)) % 0.38/0.70 (define @t178 () (@list @t176 @t175)) % 0.38/0.70 (define @t179 () (_ tptp.ord_less_eq_a @t129)) % 0.38/0.70 (define @t180 () (@var "B4" tptp.multiset_a)) % 0.38/0.70 (define @t181 () (@var "A2" tptp.multiset_a)) % 0.38/0.70 (define @t182 () (_ tptp.add_mset_a @t119)) % 0.38/0.70 (define @t183 () (_ @t182 @t180)) % 0.38/0.70 (define @t184 () (_ @t182 @t181)) % 0.38/0.70 (define @t185 () (@list @t119 @t181 @t180)) % 0.38/0.70 (define @t186 () (@var "M" tptp.multiset_a)) % 0.38/0.70 (define @t187 () (_ tptp.add_mset_a @t124)) % 0.38/0.70 (define @t188 () (_ @t187 @t186)) % 0.38/0.70 (define @t189 () (@var "B5" tptp.multiset_a)) % 0.38/0.70 (define @t190 () (_ tptp.set_mset_a @t181)) % 0.38/0.70 (define @t191 () (_ @t121 @t190)) % 0.38/0.70 (define @t192 () (@list @t119 @t181)) % 0.38/0.70 (define @t193 () (@var "A5" tptp.multiset_a)) % 0.38/0.70 (define @t194 () (_ tptp.set_mset_a @t186)) % 0.38/0.70 (define @t195 () (_ tptp.member_a @t124)) % 0.38/0.70 (define @t196 () (_ @t195 @t194)) % 0.38/0.70 (define @t197 () (@list @t124 @t186)) % 0.38/0.70 (define @t198 () (_ tptp.set_mset_a @t180)) % 0.38/0.70 (define @t199 () (@var "C2" tptp.multiset_a)) % 0.38/0.70 (define @t200 () (_ tptp.add_mset_a @t135)) % 0.38/0.70 (define @t201 () (@var "N" tptp.multiset_a)) % 0.38/0.70 (define @t202 () (= @t188 @t201)) % 0.38/0.70 (define @t203 () (@list @t124 @t186 @t201)) % 0.38/0.70 (define @t204 () (_ tptp.add_mset_a @t148)) % 0.38/0.70 (define @t205 () (@var "K" tptp.multiset_a)) % 0.38/0.70 (define @t206 () (= @t186 @t201)) % 0.38/0.70 (define @t207 () (and @t206 @t170)) % 0.38/0.70 (define @t208 () (_ @t182 @t186)) % 0.38/0.70 (define @t209 () (= @t208 (_ @t200 @t201))) % 0.38/0.70 (define @t210 () (@list @t119 @t186 @t135 @t201)) % 0.38/0.70 (define @t211 () (_ tptp.order_Greatest_a @t120)) % 0.38/0.70 (define @t212 () (forall (@list @t131) (=> (_ @t120 @t131) (_ (_ tptp.ord_less_eq_a @t131) @t124)))) % 0.38/0.70 (define @t213 () (_ @t120 @t124)) % 0.38/0.70 (define @t214 () (@var "Q" (-> tptp.a Bool))) % 0.38/0.70 (define @t215 () (@var "Y5" tptp.a)) % 0.38/0.70 (define @t216 () (@list @t132)) % 0.38/0.70 (define @t217 () (@var "P" (-> tptp.multiset_a Bool))) % 0.38/0.70 (define @t218 () (_ @t217 @t186)) % 0.38/0.70 (define @t219 () (@var "M2" tptp.multiset_a)) % 0.38/0.70 (define @t220 () (_ tptp.add_mset_a @t132)) % 0.38/0.70 (define @t221 () (_ @t217 (_ @t220 @t219))) % 0.38/0.70 (define @t222 () (@var "Xa" tptp.a)) % 0.38/0.70 (define @t223 () (_ tptp.member_a @t222)) % 0.38/0.70 (define @t224 () (_ @t223 (_ tptp.set_mset_a @t219))) % 0.38/0.70 (define @t225 () (@list @t222)) % 0.38/0.70 (define @t226 () (_ @t217 @t219)) % 0.38/0.70 (define @t227 () (@list @t132 @t219)) % 0.38/0.70 (define @t228 () (_ @t217 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t229 () (@list @t217 @t186)) % 0.38/0.70 (define @t230 () (= @t186 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t231 () (_ @t204 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t232 () (and (= @t135 @t119) @t230)) % 0.38/0.70 (define @t233 () (_ @t200 @t186)) % 0.38/0.70 (define @t234 () (_ @t182 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t235 () (@list @t119 @t135 @t186)) % 0.38/0.70 (define @t236 () (_ @t200 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t237 () (@var "N2" tptp.multiset_a)) % 0.38/0.70 (define @t238 () (not @t230)) % 0.38/0.70 (define @t239 () (@list @t186)) % 0.38/0.70 (define @t240 () (@var "P" (-> tptp.multiset_a tptp.multiset_a Bool))) % 0.38/0.70 (define @t241 () (_ tptp.add_mset_a @t176)) % 0.38/0.70 (define @t242 () (_ @t240 @t219)) % 0.38/0.70 (define @t243 () (_ @t242 @t237)) % 0.38/0.70 (define @t244 () (@list @t176 @t219 @t237)) % 0.38/0.70 (define @t245 () (_ tptp.member_a @t132)) % 0.38/0.70 (define @t246 () (@list @t181)) % 0.38/0.70 (define @t247 () (_ @t187 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t248 () (@var "Y" tptp.multiset_a)) % 0.38/0.70 (define @t249 () (@var "X" tptp.multiset_a)) % 0.38/0.70 (define @t250 () (and (= @t249 tptp.zero_zero_multiset_a) (= @t248 tptp.zero_zero_multiset_a))) % 0.38/0.70 (define @t251 () (_ tptp.plus_plus_multiset_a @t249)) % 0.38/0.70 (define @t252 () (_ @t251 @t248)) % 0.38/0.70 (define @t253 () (@list @t249 @t248)) % 0.38/0.70 (define @t254 () (= @t201 tptp.zero_zero_multiset_a)) % 0.38/0.70 (define @t255 () (and @t230 @t254)) % 0.38/0.70 (define @t256 () (_ tptp.plus_plus_multiset_a @t186)) % 0.38/0.70 (define @t257 () (_ @t256 @t201)) % 0.38/0.70 (define @t258 () (@list @t186 @t201)) % 0.38/0.70 (define @t259 () (_ tptp.plus_plus_multiset_a @t181)) % 0.38/0.70 (define @t260 () (_ @t259 @t180)) % 0.38/0.70 (define @t261 () (_ @t182 @t260)) % 0.38/0.70 (define @t262 () (@var "C" tptp.multiset_a)) % 0.38/0.70 (define @t263 () (@var "B" tptp.multiset_a)) % 0.38/0.70 (define @t264 () (_ tptp.plus_plus_multiset_a @t263)) % 0.38/0.70 (define @t265 () (@var "A" tptp.multiset_a)) % 0.38/0.70 (define @t266 () (_ tptp.ord_le1199012836iset_a (_ (_ tptp.plus_plus_multiset_a @t265) @t262))) % 0.38/0.70 (define @t267 () (_ (_ tptp.ord_le1199012836iset_a @t265) @t263)) % 0.38/0.70 (define @t268 () (@list @t265 @t263 @t262)) % 0.38/0.70 (define @t269 () (_ tptp.plus_plus_multiset_a @t262)) % 0.38/0.70 (define @t270 () (@var "D" tptp.multiset_a)) % 0.38/0.70 (define @t271 () (@var "L" tptp.multiset_a)) % 0.38/0.70 (define @t272 () (@var "J" tptp.multiset_a)) % 0.38/0.70 (define @t273 () (@var "K2" tptp.multiset_a)) % 0.38/0.70 (define @t274 () (@var "I" tptp.multiset_a)) % 0.38/0.70 (define @t275 () (_ (_ tptp.ord_le1199012836iset_a (_ (_ tptp.plus_plus_multiset_a @t274) @t273)) (_ (_ tptp.plus_plus_multiset_a @t272) @t271))) % 0.38/0.70 (define @t276 () (_ (_ tptp.ord_le1199012836iset_a @t273) @t271)) % 0.38/0.70 (define @t277 () (_ (_ tptp.ord_le1199012836iset_a @t274) @t272)) % 0.38/0.70 (define @t278 () (@list @t274 @t272 @t273 @t271)) % 0.38/0.70 (define @t279 () (@list @t249)) % 0.38/0.70 (define @t280 () (@var "K3" tptp.multiset_a)) % 0.38/0.70 (define @t281 () (_ tptp.plus_plus_multiset_a @t201)) % 0.38/0.70 (define @t282 () (_ @t281 @t280)) % 0.38/0.70 (define @t283 () (_ @t256 @t282)) % 0.38/0.70 (define @t284 () (@list @t186 @t201 @t280)) % 0.38/0.70 (define @t285 () (_ @t256 @t280)) % 0.38/0.70 (define @t286 () (@var "M3" tptp.multiset_a)) % 0.38/0.70 (define @t287 () (@var "N3" tptp.multiset_a)) % 0.38/0.70 (define @t288 () (_ tptp.plus_plus_multiset_a @t280)) % 0.38/0.70 (define @t289 () (@var "Y6" tptp.multiset_a)) % 0.38/0.70 (define @t290 () (@var "X6" tptp.multiset_a)) % 0.38/0.70 (define @t291 () (@var "A6" tptp.multiset_a)) % 0.38/0.70 (define @t292 () (@list @t119 @t186 @t201)) % 0.38/0.70 (define @t293 () (@var "XS" tptp.multiset_a)) % 0.38/0.70 (define @t294 () (@var "R" tptp.set_Product_prod_a_a)) % 0.38/0.70 (define @t295 () (@var "B6" tptp.a)) % 0.38/0.70 (define @t296 () (_ tptp.product_Pair_a_a @t295)) % 0.38/0.70 (define @t297 () (@var "K4" tptp.multiset_a)) % 0.38/0.70 (define @t298 () (_ tptp.set_mset_a @t297)) % 0.38/0.70 (define @t299 () (_ (_ tptp.member_a @t295) @t298)) % 0.38/0.70 (define @t300 () (@list @t295)) % 0.38/0.70 (define @t301 () (@var "M0" tptp.multiset_a)) % 0.38/0.70 (define @t302 () (@list @t297)) % 0.38/0.70 (define @t303 () (_ tptp.mult1_a @t294)) % 0.38/0.70 (define @t304 () (_ tptp.produc2037245207iset_a @t201)) % 0.38/0.70 (define @t305 () (_ (_ tptp.member340150864iset_a (_ @t304 @t186)) @t303)) % 0.38/0.70 (define @t306 () (_ tptp.set_mset_a @t280)) % 0.38/0.70 (define @t307 () (@var "M02" tptp.multiset_a)) % 0.38/0.70 (define @t308 () (_ tptp.plus_plus_multiset_a @t307)) % 0.38/0.70 (define @t309 () (_ @t182 @t307)) % 0.38/0.70 (define @t310 () (_ tptp.mult_a @t294)) % 0.38/0.70 (define @t311 () (@var "J2" tptp.multiset_a)) % 0.38/0.70 (define @t312 () (@var "I2" tptp.multiset_a)) % 0.38/0.70 (define @t313 () (_ tptp.plus_plus_multiset_a @t312)) % 0.38/0.70 (define @t314 () (_ tptp.produc2037245207iset_a @t186)) % 0.38/0.70 (define @t315 () (@var "D2" tptp.multiset_a)) % 0.38/0.70 (define @t316 () (_ tptp.plus_plus_multiset_a @t199)) % 0.38/0.70 (define @t317 () (@var "Xa2" tptp.a)) % 0.38/0.70 (define @t318 () (@var "X7" tptp.a)) % 0.38/0.70 (define @t319 () (@var "J3" tptp.multiset_a)) % 0.38/0.70 (define @t320 () (@var "I3" tptp.multiset_a)) % 0.38/0.70 (define @t321 () (_ tptp.plus_plus_multiset_a @t320)) % 0.38/0.70 (define @t322 () (@var "X4" tptp.multiset_a)) % 0.38/0.70 (define @t323 () (@var "M" tptp.multiset_multiset_a)) % 0.38/0.70 (define @t324 () (@var "S" tptp.set_Product_prod_a_a)) % 0.38/0.70 (define @t325 () (_ tptp.mult_a @t324)) % 0.38/0.70 (define @t326 () (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t290) @t289)) @t325)) % 0.38/0.70 (define @t327 () (@var "Uu" tptp.a)) % 0.38/0.70 (define @t328 () (_ tptp.add_mset_a @t327)) % 0.38/0.70 (define @t329 () (_ tptp.irrefl_a @t324)) % 0.38/0.70 (define @t330 () (_ tptp.trans_a @t324)) % 0.38/0.70 (define @t331 () (@var "Z3" tptp.multiset_a)) % 0.38/0.70 (define @t332 () (@var "NN" tptp.multiset_multiset_a)) % 0.38/0.70 (define @t333 () (_ tptp.minus_1649712171iset_a @t186)) % 0.38/0.70 (define @t334 () (_ @t333 @t247)) % 0.38/0.70 (define @t335 () (@var "P" tptp.multiset_a)) % 0.38/0.70 (define @t336 () (_ @t333 @t201)) % 0.38/0.70 (define @t337 () (_ tptp.minus_1649712171iset_a @t336)) % 0.38/0.70 (define @t338 () (_ tptp.minus_1649712171iset_a @t188)) % 0.38/0.70 (define @t339 () (_ @t333 @t181)) % 0.38/0.70 (define @t340 () (_ tptp.minus_1649712171iset_a @t233)) % 0.38/0.70 (define @t341 () (_ tptp.minus_1649712171iset_a @t201)) % 0.38/0.70 (define @t342 () (@var "Q" tptp.multiset_a)) % 0.38/0.70 (define @t343 () (_ (_ @t5 tptp.l) tptp.r)) % 0.38/0.70 (define @t344 () (_ tptp.heapIm970322378pify_a @t343)) % 0.38/0.70 (define @t345 () (_ tptp.is_heap_a @t344)) % 0.38/0.70 (define @t346 () (not @t345)) % 0.38/0.70 (define @t347 () (lambda (@list @t291) (= @t291 tptp.zero_zero_multiset_a))) % 0.38/0.70 (define @t348 () (tptp.heapIm970322378pify_a tptp.l)) % 0.38/0.70 (define @t349 () (tptp.is_heap_a @t348)) % 0.38/0.70 (define @t350 () (tptp.heapIm970322378pify_a tptp.r)) % 0.38/0.70 (define @t351 () (tptp.t_a tptp.v @t348 @t350)) % 0.38/0.70 (define @t352 () (tptp.heapIm1091024090Down_a @t351)) % 0.38/0.70 (define @t353 () (tptp.is_heap_a @t352)) % 0.38/0.70 (define @t354 () (tptp.is_heap_a @t350)) % 0.38/0.70 (define @t355 () (=> @t2 @t8)) % 0.38/0.70 (define @t356 () (=> @t354 @t353)) % 0.38/0.70 (define @t357 () (tptp.heapIm970322378pify_a @t12)) % 0.38/0.70 (define @t358 () (tptp.heapIm970322378pify_a @t14)) % 0.38/0.70 (define @t359 () (tptp.t_a @t16 @t358 @t357)) % 0.38/0.70 (define @t360 () (tptp.heapIm1091024090Down_a @t359)) % 0.38/0.70 (define @t361 () (tptp.t_a @t16 @t14 @t12)) % 0.38/0.70 (define @t362 () (tptp.heapIm970322378pify_a @t361)) % 0.38/0.70 (define @t363 () (tptp.t_a tptp.v tptp.l tptp.r)) % 0.38/0.70 (define @t364 () (tptp.heapIm970322378pify_a @t363)) % 0.38/0.70 (define @t365 () (tptp.is_heap_a @t364)) % 0.38/0.70 (assume @p1 @t2) % 0.38/0.70 (assume @p2 @t4) % 0.38/0.70 (assume @p3 @t11) % 0.38/0.70 (assume @p4 @t24) % 0.38/0.70 (assume @p5 (forall (@list @t14 @t12 @t25 @t16) (=> (_ tptp.is_heap_a @t14) (=> (_ tptp.is_heap_a @t12) (=> @t27 (_ tptp.is_heap_a @t26)))))) % 0.38/0.70 (assume @p6 (forall (@list @t33 @t31 @t29 @t32 @t30 @t28) (= (= @t34 (_ (_ (_ tptp.t_a @t32) @t30) @t28)) (and (= @t33 @t32) (= @t31 @t30) (= @t29 @t28))))) % 0.38/0.70 (assume @p7 (forall @t23 (= (_ tptp.heapIm1140443833left_a @t20) @t14))) % 0.38/0.70 (assume @p8 (forall @t23 (= (_ tptp.heapIm1257206334ight_a @t20) @t12))) % 0.38/0.70 (assume @p9 (forall @t37 (_ tptp.is_heap_a @t36))) % 0.38/0.70 (assume @p10 (= (_ tptp.heapIm970322378pify_a tptp.e_a) tptp.e_a)) % 0.38/0.70 (assume @p11 (forall @t56 (=> @t55 (=> @t54 (=> @t53 (=> @t52 @t49)))))) % 0.38/0.70 (assume @p12 (forall (@list @t16 @t58 @t14 @t12) (= (_ @t57 (_ (_ (_ tptp.t_a @t58) @t14) @t12)) (or (= @t16 @t58) (_ @t57 @t14) (_ @t57 @t12))))) % 0.38/0.70 (assume @p13 (forall @t37 (= (_ tptp.heapIm1091024090Down_a @t36) @t36))) % 0.38/0.70 (assume @p14 (forall @t37 (not (_ @t57 tptp.e_a)))) % 0.38/0.70 (assume @p15 (= (_ tptp.heapIm1091024090Down_a tptp.e_a) tptp.e_a)) % 0.38/0.70 (assume @p16 (= tptp.in_tree_a (lambda (@list @t60 @t59) (_ (_ tptp.in_tree_a @t60) (_ tptp.heapIm1091024090Down_a @t59))))) % 0.38/0.70 (assume @p17 (forall @t56 (=> @t55 (=> @t54 (=> @t52 (=> @t53 @t49)))))) % 0.38/0.70 (assume @p18 (forall (@list @t64) (=> (not (= @t64 tptp.e_a)) (not (forall (@list @t63 @t62 @t61) (not (= @t64 (_ (_ (_ tptp.t_a @t63) @t62) @t61)))))))) % 0.38/0.70 (assume @p19 (forall (@list @t66 @t65) (=> (_ @t66 tptp.e_a) (=> (forall (@list @t69 @t68 @t67) (=> (_ @t66 @t68) (=> (_ @t66 @t67) (_ @t66 (_ (_ (_ tptp.t_a @t69) @t68) @t67))))) (_ @t66 @t65))))) % 0.38/0.70 (assume @p20 (forall (@list @t33 @t31 @t29) (not (= tptp.e_a @t34)))) % 0.38/0.70 (assume @p21 (_ tptp.is_heap_a tptp.e_a)) % 0.38/0.70 (assume @p22 (forall @t71 (=> @t70 (_ (_ tptp.in_tree_a (_ tptp.val_a @t26)) @t25)))) % 0.38/0.70 (assume @p23 (forall @t84 (and (=> @t82 (= @t80 @t79)) (=> @t83 (= @t80 (_ (_ @t78 tptp.e_a) @t76)))))) % 0.38/0.70 (assume @p24 (forall @t84 (and (=> @t82 (= @t88 @t87)) (=> @t83 (= @t88 (_ @t85 tptp.e_a)))))) % 0.38/0.70 (assume @p25 (forall (@list @t74 @t73 @t72 @t91 @t90 @t89 @t16) (and (=> @t97 (and (=> @t101 @t95) (=> @t102 (= @t94 (_ (_ @t99 @t98) @t75))))) (=> (not @t97) (and (=> @t82 @t95) (=> @t83 (= @t94 (_ (_ @t78 @t92) @t76)))))))) % 0.38/0.70 (assume @p26 (forall (@list @t91 @t90 @t89 @t74 @t73 @t72 @t16) (and (=> @t106 (and (=> @t82 @t105) (=> @t83 (= @t104 (_ @t85 @t92))))) (=> (not @t106) (and (=> @t101 @t105) (=> @t102 (= @t104 (_ (_ @t99 @t75) @t98)))))))) % 0.38/0.70 (assume @p27 (forall (@list @t25 @t16 @t14 @t12) (=> @t27 (exists (@list @t110 @t107 @t109) (and (= @t26 (_ (_ (_ tptp.t_a @t107) @t110) @t109)) (_ @t108 @t107)))))) % 0.38/0.70 (assume @p28 (forall (@list @t16 @t91 @t90 @t89 @t74 @t73 @t72) (= (_ tptp.is_heap_a @t93) (and @t82 @t112 @t101 @t111)))) % 0.38/0.70 (assume @p29 (forall (@list @t16 @t74 @t73 @t72 @t91 @t90 @t89) (= (_ tptp.is_heap_a @t103) (and @t101 @t111 @t82 @t112)))) % 0.38/0.70 (assume @p30 (forall (@list @t16 @t25) (=> (_ @t57 @t25) (=> @t114 (_ @t108 @t113))))) % 0.38/0.70 (assume @p31 (forall (@list @t16 @t116 @t115) (= (_ tptp.val_a (_ (_ @t17 @t116) @t115)) @t16))) % 0.38/0.70 (assume @p32 (forall @t118 (= (_ tptp.is_heap_a @t87) @t117))) % 0.38/0.70 (assume @p33 (forall @t118 (= (_ tptp.is_heap_a @t79) @t117))) % 0.38/0.70 (assume @p34 (forall (@list @t119 @t120) (= (_ @t121 (_ tptp.collect_a @t120)) (_ @t120 @t119)))) % 0.38/0.70 (assume @p35 (forall (@list @t122) (= (_ tptp.collect_a (lambda (@list @t123) (_ (_ tptp.member_a @t123) @t122))) @t122))) % 0.38/0.70 (assume @p36 (forall @t126 (_ @t125 @t124))) % 0.38/0.70 (assume @p37 (forall (@list @t119 @t25) (=> (_ @t121 @t128) (=> @t114 (_ @t127 @t113))))) % 0.38/0.70 (assume @p38 (forall @t140 (=> (_ @t127 @t139) @t138))) % 0.38/0.70 (assume @p39 (forall @t143 (=> @t142 (=> (_ (_ tptp.ord_less_eq_a @t139) @t129) @t141)))) % 0.38/0.70 (assume @p40 (forall @t140 (=> (= @t119 @t139) @t138))) % 0.38/0.70 (assume @p41 (forall @t143 (=> @t142 (=> (= @t139 @t129) @t141)))) % 0.38/0.70 (assume @p42 (= @t147 (lambda (@list @t123 @t144) (and (_ (_ tptp.ord_less_eq_a @t123) @t144) (_ (_ tptp.ord_less_eq_a @t144) @t123))))) % 0.38/0.70 (assume @p43 (forall @t153 (=> @t152 (=> @t151 @t149)))) % 0.38/0.70 (assume @p44 (forall @t153 (or @t152 @t151))) % 0.38/0.70 (assume @p45 (forall @t153 (=> @t149 @t152))) % 0.38/0.70 (assume @p46 (forall @t153 (=> @t154 @t151))) % 0.38/0.70 (assume @p47 (forall @t157 (=> @t142 @t156))) % 0.38/0.70 (assume @p48 (forall @t164 (=> (=> @t152 (not @t161)) (=> (=> @t151 (not @t163)) (=> (=> @t163 (not @t162)) (=> (=> @t162 (not @t151)) (=> (=> @t161 (not @t160)) (not (=> @t160 @t154))))))))) % 0.38/0.70 (assume @p49 (forall (@list @t148 @t124) (=> @t151 (= @t152 @t149)))) % 0.38/0.70 (assume @p50 (= @t147 (lambda @t169 (and @t168 @t167)))) % 0.38/0.70 (assume @p51 (forall @t157 (=> @t170 @t156))) % 0.38/0.70 (assume @p52 (forall @t157 (=> @t142 (=> @t171 @t155)))) % 0.38/0.70 (assume @p53 (forall @t173 (=> @t142 (=> @t172 @t170)))) % 0.38/0.70 (assume @p54 (forall @t164 (=> @t152 (=> @t161 @t163)))) % 0.38/0.70 (assume @p55 (forall (@list @t119) (_ @t127 @t119))) % 0.38/0.70 (assume @p56 (forall (@list @t174 @t119 @t135) (=> (forall @t178 (=> (_ (_ tptp.ord_less_eq_a @t176) @t175) @t177)) (=> (forall @t178 (=> (_ (_ @t174 @t175) @t176) @t177)) (_ (_ @t174 @t119) @t135))))) % 0.38/0.70 (assume @p57 (forall (@list @t135 @t119 @t129) (=> @t172 (=> (_ @t179 @t135) (_ @t179 @t119))))) % 0.38/0.70 (assume @p58 (= @t147 (lambda @t169 (and @t167 @t168)))) % 0.38/0.70 (assume @p59 (forall (@list @t135 @t119) (=> @t172 (=> @t142 @t170)))) % 0.38/0.70 (assume @p60 (forall @t185 (= (= @t184 @t183) (= @t181 @t180)))) % 0.38/0.70 (assume @p61 (forall (@list @t186 @t124) (not (= @t186 @t188)))) % 0.38/0.70 (assume @p62 (forall @t192 (=> @t191 (not (forall (@list @t189) (not (= @t181 (_ @t182 @t189)))))))) % 0.38/0.70 (assume @p63 (forall @t197 (=> @t196 (exists (@list @t193) (= @t186 (_ @t187 @t193)))))) % 0.38/0.70 (assume @p64 (forall (@list @t135 @t180 @t129 @t199) (=> (= (_ @t200 @t180) (_ (_ tptp.add_mset_a @t129) @t199)) (=> (not @t171) (_ (_ tptp.member_a @t129) @t198))))) % 0.38/0.70 (assume @p65 (forall @t203 (=> @t202 (_ @t195 (_ tptp.set_mset_a @t201))))) % 0.38/0.70 (assume @p66 (forall @t71 (=> @t70 (=> @t114 (= @t113 (_ tptp.lattic146396397_Max_a @t128)))))) % 0.38/0.70 (assume @p67 (forall (@list @t124 @t148 @t186) (= (_ @t187 (_ @t204 @t186)) (_ @t204 @t188)))) % 0.38/0.70 (assume @p68 (forall @t210 (= @t209 (or @t207 (exists (@list @t205) (and (= @t186 (_ @t200 @t205)) (= @t201 (_ @t182 @t205)))))))) % 0.38/0.70 (assume @p69 (forall (@list @t120 @t124) (=> @t213 (=> @t212 (= @t211 @t124))))) % 0.38/0.70 (assume @p70 (forall (@list @t120 @t124 @t214) (=> @t213 (=> @t212 (=> (forall @t216 (=> (_ @t120 @t132) (=> (forall (@list @t215) (=> (_ @t120 @t215) (_ (_ tptp.ord_less_eq_a @t215) @t132))) (_ @t214 @t132)))) (_ @t214 @t211)))))) % 0.38/0.70 (assume @p71 (forall @t229 (=> @t228 (=> (forall @t227 (=> @t226 (=> (forall @t225 (=> @t224 (_ @t133 @t222))) @t221))) @t218)))) % 0.38/0.70 (assume @p72 (forall @t229 (=> @t228 (=> (forall @t227 (=> @t226 (=> (forall @t225 (=> @t224 (_ (_ tptp.ord_less_eq_a @t222) @t132))) @t221))) @t218)))) % 0.38/0.70 (assume @p73 (forall (@list @t124 @t186 @t148) (= (= @t188 @t231) (and @t230 @t149)))) % 0.38/0.70 (assume @p74 (forall @t235 (= (= @t234 @t233) @t232))) % 0.38/0.70 (assume @p75 (forall (@list @t135 @t186 @t119) (= (= @t233 @t234) @t232))) % 0.38/0.70 (assume @p76 (forall @t173 (= (= @t234 @t236) @t170))) % 0.38/0.70 (assume @p77 (forall @t239 (=> @t238 (not (forall (@list @t132 @t237) (not (= @t186 (_ @t220 @t237)))))))) % 0.38/0.70 (assume @p78 (forall @t229 (=> @t228 (=> (forall @t227 (=> @t226 @t221)) @t218)))) % 0.38/0.70 (assume @p79 (forall (@list @t240 @t186 @t201) (=> (_ (_ @t240 tptp.zero_zero_multiset_a) tptp.zero_zero_multiset_a) (=> (forall @t244 (=> @t243 (_ (_ @t240 (_ @t241 @t219)) @t237))) (=> (forall @t244 (=> @t243 (_ @t242 (_ @t241 @t237)))) (_ (_ @t240 @t186) @t201)))))) % 0.38/0.70 (assume @p80 (forall @t192 (not (= tptp.zero_zero_multiset_a @t184)))) % 0.38/0.70 (assume @p81 (forall @t239 (=> @t238 (exists (@list @t193 @t176) (= @t186 (_ @t241 @t193)))))) % 0.38/0.70 (assume @p82 (forall @t246 (=> (not (= @t181 tptp.zero_zero_multiset_a)) (not (forall @t216 (not (_ @t245 @t190))))))) % 0.38/0.70 (assume @p83 (forall @t126 (_ @t195 (_ tptp.set_mset_a @t247)))) % 0.38/0.70 (assume @p84 (= (_ tptp.multiset_a2 tptp.e_a) tptp.zero_zero_multiset_a)) % 0.38/0.70 (assume @p85 (forall @t23 (= (_ tptp.multiset_a2 @t20) (_ (_ tptp.plus_plus_multiset_a (_ (_ tptp.plus_plus_multiset_a (_ tptp.multiset_a2 @t14)) (_ (_ tptp.add_mset_a @t16) tptp.zero_zero_multiset_a))) (_ tptp.multiset_a2 @t12))))) % 0.38/0.70 (assume @p86 (forall @t253 (= (= tptp.zero_zero_multiset_a @t252) @t250))) % 0.38/0.70 (assume @p87 (forall @t253 (= (= @t252 tptp.zero_zero_multiset_a) @t250))) % 0.38/0.70 (assume @p88 (forall @t258 (= (= @t257 tptp.zero_zero_multiset_a) @t255))) % 0.38/0.70 (assume @p89 (forall @t258 (= (= tptp.zero_zero_multiset_a @t257) @t255))) % 0.38/0.70 (assume @p90 (forall (@list @t181 @t119 @t180) (= (_ @t259 @t183) @t261))) % 0.38/0.70 (assume @p91 (forall @t185 (= (_ (_ tptp.plus_plus_multiset_a @t184) @t180) @t261))) % 0.38/0.70 (assume @p92 (forall @t268 (=> @t267 (_ @t266 (_ @t264 @t262))))) % 0.38/0.70 (assume @p93 (forall @t268 (=> @t267 (_ (_ tptp.ord_le1199012836iset_a (_ @t269 @t265)) (_ @t269 @t263))))) % 0.38/0.70 (assume @p94 (forall (@list @t265 @t263 @t262 @t270) (=> @t267 (=> (_ (_ tptp.ord_le1199012836iset_a @t262) @t270) (_ @t266 (_ @t264 @t270)))))) % 0.38/0.70 (assume @p95 (forall @t278 (=> (and @t277 @t276) @t275))) % 0.38/0.70 (assume @p96 (forall @t278 (=> (and (= @t274 @t272) @t276) @t275))) % 0.38/0.70 (assume @p97 (forall @t278 (=> (and @t277 (= @t273 @t271)) @t275))) % 0.38/0.70 (assume @p98 (forall @t279 (= (_ @t251 tptp.zero_zero_multiset_a) @t249))) % 0.38/0.70 (assume @p99 (forall @t279 (= (_ (_ tptp.plus_plus_multiset_a tptp.zero_zero_multiset_a) @t249) @t249))) % 0.38/0.70 (assume @p100 (forall @t185 (= (_ @t121 (_ tptp.set_mset_a @t260)) (or @t191 (_ @t121 @t198))))) % 0.38/0.70 (assume @p101 (forall @t284 (= (_ (_ tptp.plus_plus_multiset_a @t257) @t280) @t283))) % 0.38/0.70 (assume @p102 (forall @t284 (= @t283 (_ @t281 @t285)))) % 0.38/0.70 (assume @p103 (= tptp.plus_plus_multiset_a (lambda (@list @t286 @t287) (_ (_ tptp.plus_plus_multiset_a @t287) @t286)))) % 0.38/0.70 (assume @p104 (forall (@list @t280 @t186 @t201) (= (= (_ @t288 @t186) (_ @t288 @t201)) @t206))) % 0.38/0.70 (assume @p105 (forall (@list @t186 @t280 @t201) (= (= @t285 @t282) @t206))) % 0.38/0.70 (assume @p106 (forall (@list @t181 @t290 @t289) (=> (= (_ @t259 @t290) (_ @t259 @t289)) (= @t290 @t289)))) % 0.38/0.70 (assume @p107 (= tptp.add_mset_a (lambda (@list @t165 @t291) (_ (_ tptp.plus_plus_multiset_a @t291) (_ (_ tptp.add_mset_a @t165) tptp.zero_zero_multiset_a))))) % 0.38/0.70 (assume @p108 (forall (@list @t186 @t201 @t119) (= (= @t257 @t234) (or (and (= @t186 @t234) @t254) (and @t230 (= @t201 @t234)))))) % 0.38/0.70 (assume @p109 (forall @t292 (= (= @t234 @t257) (or (and (= @t234 @t186) @t254) (and @t230 (= @t234 @t201)))))) % 0.38/0.70 (assume @p110 (forall (@list @t124 @t293 @t148) (=> (_ @t195 (_ tptp.set_mset_a @t293)) (_ @t195 (_ tptp.set_mset_a (_ (_ tptp.plus_plus_multiset_a @t231) @t293)))))) % 0.38/0.70 (assume @p111 (forall (@list @t124 @t293) (_ @t195 (_ tptp.set_mset_a (_ (_ tptp.plus_plus_multiset_a @t247) @t293))))) % 0.38/0.70 (assume @p112 (forall (@list @t201 @t186 @t294) (=> @t305 (not (forall (@list @t176 @t301) (=> (= @t186 (_ @t241 @t301)) (forall @t302 (=> (= @t201 (_ (_ tptp.plus_plus_multiset_a @t301) @t297)) (not (forall @t300 (=> @t299 (_ (_ tptp.member449909584od_a_a (_ @t296 @t176)) @t294)))))))))))) % 0.38/0.70 (assume @p113 (forall (@list @t186 @t119 @t307 @t201 @t280 @t294) (=> (= @t186 @t309) (=> (= @t201 (_ @t308 @t280)) (=> (forall (@list @t175) (=> (_ (_ tptp.member_a @t175) @t306) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t175) @t119)) @t294))) @t305))))) % 0.38/0.70 (assume @p114 (forall (@list @t201 @t119 @t307 @t294) (=> (_ (_ tptp.member340150864iset_a (_ @t304 @t309)) @t303) (or (exists (@list @t219) (and (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t219) @t307)) @t303) (= @t201 (_ @t182 @t219)))) (exists @t302 (and (forall @t300 (=> @t299 (_ (_ tptp.member449909584od_a_a (_ @t296 @t119)) @t294))) (= @t201 (_ @t308 @t297)))))))) % 0.38/0.70 (assume @p115 (forall (@list @t311 @t280 @t294 @t312) (=> (not (= @t311 tptp.zero_zero_multiset_a)) (=> (forall @t216 (=> (_ @t245 @t306) (exists @t225 (and (_ @t223 (_ tptp.set_mset_a @t311)) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t132) @t222)) @t294))))) (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ @t313 @t280)) (_ @t313 @t311))) @t310))))) % 0.38/0.70 (assume @p116 (forall (@list @t186 @t294) (not (_ (_ tptp.member340150864iset_a (_ @t314 tptp.zero_zero_multiset_a)) @t303)))) % 0.38/0.70 (assume @p117 (forall (@list @t180 @t315 @t294 @t199) (=> (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a @t180) @t315)) @t303) (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ @t316 @t180)) (_ @t316 @t315))) @t303)))) % 0.38/0.70 (assume @p118 (forall (@list @t294 @t186 @t201) (=> (_ tptp.trans_a @t294) (=> (_ (_ tptp.member340150864iset_a (_ @t314 @t201)) @t310) (exists (@list @t320 @t319) (and (= @t201 (_ @t321 @t319)) (exists @t302 (and (= @t186 (_ @t321 @t297)) (not (= @t319 tptp.zero_zero_multiset_a)) (forall (@list @t318) (=> (_ (_ tptp.member_a @t318) @t298) (exists (@list @t317) (and (_ (_ tptp.member_a @t317) (_ tptp.set_mset_a @t319)) (_ (_ tptp.member449909584od_a_a (_ (_ tptp.product_Pair_a_a @t318) @t317)) @t294))))))))))))) % 0.38/0.70 (assume @p119 (forall (@list @t323) (= (= (_ (_ (_ tptp.comm_m315775925iset_a tptp.plus_plus_multiset_a) tptp.zero_zero_multiset_a) @t323) tptp.zero_zero_multiset_a) (forall (@list @t322) (=> (_ (_ tptp.member_multiset_a @t322) (_ tptp.set_mset_multiset_a @t323)) (= @t322 tptp.zero_zero_multiset_a)))))) % 0.38/0.70 (assume @p120 (forall (@list @t324 @t327 @t290 @t289) (=> @t330 (=> @t329 (= (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ @t328 @t290)) (_ @t328 @t289))) @t325) @t326))))) % 0.38/0.70 (assume @p121 (forall (@list @t324 @t290 @t331 @t289) (=> @t330 (=> @t329 (= (_ (_ tptp.member340150864iset_a (_ (_ tptp.produc2037245207iset_a (_ (_ tptp.plus_plus_multiset_a @t290) @t331)) (_ (_ tptp.plus_plus_multiset_a @t289) @t331))) @t325) @t326))))) % 0.38/0.70 (assume @p122 (forall (@list @t124 @t186 @t332) (= (_ @t195 (_ tptp.set_mset_a (_ (_ (_ tptp.fold_m382157835iset_a tptp.plus_plus_multiset_a) @t186) @t332))) (or @t196 (exists (@list @t287) (and (_ (_ tptp.member_multiset_a @t287) (_ tptp.set_mset_multiset_a @t332)) (_ @t195 (_ tptp.set_mset_a @t287)))))))) % 0.38/0.70 (assume @p123 (= tptp.plus_plus_multiset_a (_ tptp.fold_m364285649iset_a tptp.add_mset_a))) % 0.38/0.70 (assume @p124 (forall (@list @t186 @t119) (=> (_ (_ tptp.nO_MAT1617603563iset_a tptp.zero_zero_multiset_a) @t186) (= @t208 (_ (_ tptp.plus_plus_multiset_a @t234) @t186))))) % 0.38/0.70 (assume @p125 (forall @t197 (=> @t196 (= (_ (_ tptp.plus_plus_multiset_a @t334) @t247) @t186)))) % 0.38/0.70 (assume @p126 (forall (@list @t186 @t201 @t335) (= (_ @t337 @t335) (_ @t333 (_ @t281 @t335))))) % 0.38/0.70 (assume @p127 (forall @t197 (= (_ @t338 @t247) @t186))) % 0.38/0.70 (assume @p128 (forall (@list @t135 @t181 @t186) (=> (not (_ (_ tptp.member_a @t135) @t190)) (= (_ @t340 @t181) (_ @t200 @t339))))) % 0.38/0.70 (assume @p129 (forall (@list @t148 @t186 @t124) (=> (_ (_ tptp.member_a @t148) @t194) (= (_ @t338 @t231) (_ @t187 (_ @t333 @t231)))))) % 0.38/0.70 (assume @p130 (forall @t197 (=> @t196 (= (_ @t187 @t334) @t186)))) % 0.38/0.70 (assume @p131 (forall @t292 (=> (_ @t121 (_ tptp.set_mset_a @t336)) (_ @t121 @t194)))) % 0.38/0.70 (assume @p132 (forall (@list @t119 @t186 @t181) (= (_ (_ tptp.minus_1649712171iset_a @t208) @t184) @t339))) % 0.38/0.70 (assume @p133 (forall @t246 (= (_ (_ tptp.minus_1649712171iset_a @t181) @t181) tptp.zero_zero_multiset_a))) % 0.38/0.70 (assume @p134 (forall @t239 (and (= (_ @t333 tptp.zero_zero_multiset_a) @t186) (= (_ (_ tptp.minus_1649712171iset_a tptp.zero_zero_multiset_a) @t186) tptp.zero_zero_multiset_a)))) % 0.38/0.70 (assume @p135 (forall @t203 (=> @t202 (= @t186 (_ @t341 @t247))))) % 0.38/0.70 (assume @p136 (forall @t210 (= @t209 (or @t207 (and (= @t186 (_ @t200 (_ @t341 @t234))) (= @t201 (_ @t182 (_ @t333 @t236)))))))) % 0.38/0.70 (assume @p137 (forall @t235 (=> (not @t170) (= (_ @t200 (_ @t333 @t234)) (_ @t340 @t234))))) % 0.38/0.70 (assume @p138 (forall @t258 (= (_ (_ tptp.minus_1649712171iset_a @t257) @t201) @t186))) % 0.38/0.70 (assume @p139 (forall (@list @t201 @t186) (= (_ (_ tptp.minus_1649712171iset_a (_ @t281 @t186)) @t201) @t186))) % 0.38/0.70 (assume @p140 (forall (@list @t186 @t201 @t342) (= (_ @t333 (_ @t281 @t342)) (_ @t337 @t342)))) % 0.38/0.70 (assume @p141 (forall @t197 (=> (not @t196) (= @t334 @t186)))) % 0.38/0.70 (assume @p142 @t346) % 0.38/0.70 (assume @p143 true) % 0.38/0.70 (step @p144 (= tptp.is_empty_a @t347) :rule refl :args (@t347)) % 0.38/0.70 (step @p145 :rule evaluate :args ((= false true))) % 0.38/0.70 (step @p146 :rule refl :args ((tptp.is_heap_a @t3))) % 0.38/0.70 (step @p147 :rule refl :args (@t348)) % 0.38/0.70 (step @p148 :rule cong :premises (@p147) :args (@t349)) % 0.38/0.70 (step @p149 :rule trans :premises (@p148 @p146)) % 0.38/0.70 (step @p150 :rule refl :args (tptp.is_heap_a)) % 0.38/0.70 (step @p151 :rule ho_cong :premises (@p150 @p147)) % 0.38/0.70 (step @p152 :rule cong :premises (@p151 @p149) :args ((= (_ tptp.is_heap_a @t348) @t349))) % 0.38/0.70 (step @p153 :rule symm :premises (@p152)) % 0.38/0.70 (step @p154 :rule refl :args (@t4)) % 0.38/0.70 (step @p155 :rule eq_resolve :premises (@p154 @p153)) % 0.38/0.70 (step @p156 :rule refl :args (@t3)) % 0.38/0.70 (step @p157 :rule cong :premises (@p156 @p147) :args ((= @t3 @t348))) % 0.38/0.70 (step @p158 :rule symm :premises (@p157)) % 0.38/0.70 (step @p159 :rule eq_resolve :premises (@p156 @p158)) % 0.38/0.70 (step @p160 :rule refl :args (tptp.is_heap_a)) % 0.38/0.70 (step @p161 :rule ho_cong :premises (@p160 @p159)) % 0.38/0.70 (step @p162 :rule trans :premises (@p161 @p155)) % 0.38/0.70 (step @p163 :rule eq_resolve :premises (@p2 @p162)) % 0.38/0.70 (step @p164 :rule refl :args ((tptp.is_heap_a @t7))) % 0.38/0.70 (step @p165 :rule refl :args ((tptp.heapIm1091024090Down_a @t6))) % 0.38/0.70 (step @p166 :rule refl :args ((tptp.t_a tptp.v @t3 @t1))) % 0.38/0.70 (step @p167 :rule refl :args (@t350)) % 0.38/0.70 (step @p168 :rule refl :args (tptp.v)) % 0.38/0.70 (step @p169 :rule cong :premises (@p168 @p147 @p167) :args (@t351)) % 0.38/0.70 (step @p170 :rule trans :premises (@p169 @p166)) % 0.38/0.70 (step @p171 :rule cong :premises (@p170) :args (@t352)) % 0.38/0.70 (step @p172 :rule trans :premises (@p171 @p165)) % 0.38/0.70 (step @p173 :rule cong :premises (@p172) :args (@t353)) % 0.38/0.70 (step @p174 :rule trans :premises (@p173 @p164)) % 0.38/0.70 (step @p175 :rule ho_cong :premises (@p150 @p172)) % 0.38/0.70 (step @p176 :rule cong :premises (@p175 @p174) :args ((= (_ tptp.is_heap_a @t352) @t353))) % 0.38/0.70 (step @p177 :rule symm :premises (@p176)) % 0.38/0.70 (step @p178 :rule refl :args (@t8)) % 0.38/0.70 (step @p179 :rule eq_resolve :premises (@p178 @p177)) % 0.38/0.70 (step @p180 :rule refl :args (tptp.heapIm1091024090Down_a)) % 0.38/0.70 (step @p181 :rule ho_cong :premises (@p180 @p170)) % 0.38/0.70 (step @p182 :rule cong :premises (@p181 @p172) :args ((= (_ tptp.heapIm1091024090Down_a @t351) @t352))) % 0.38/0.70 (step @p183 :rule symm :premises (@p182)) % 0.38/0.70 (step @p184 :rule refl :args (@t7)) % 0.38/0.70 (step @p185 :rule eq_resolve :premises (@p184 @p183)) % 0.38/0.70 (step @p186 :rule refl :args (@t5)) % 0.38/0.70 (step @p187 :rule ho_cong :premises (@p186 @p147)) % 0.38/0.70 (step @p188 :rule ho_cong :premises (@p187 @p167)) % 0.38/0.70 (step @p189 :rule cong :premises (@p188 @p170) :args ((= (_ (_ @t5 @t348) @t350) @t351))) % 0.38/0.70 (step @p190 :rule symm :premises (@p189)) % 0.38/0.70 (step @p191 :rule refl :args (@t6)) % 0.38/0.70 (step @p192 :rule eq_resolve :premises (@p191 @p190)) % 0.38/0.70 (step @p193 :rule refl :args (@t1)) % 0.38/0.70 (step @p194 :rule cong :premises (@p193 @p167) :args ((= @t1 @t350))) % 0.38/0.70 (step @p195 :rule symm :premises (@p194)) % 0.38/0.70 (step @p196 :rule eq_resolve :premises (@p193 @p195)) % 0.38/0.70 (step @p197 :rule refl :args (@t5)) % 0.38/0.70 (step @p198 :rule ho_cong :premises (@p197 @p159)) % 0.38/0.70 (step @p199 :rule ho_cong :premises (@p198 @p196)) % 0.38/0.70 (step @p200 :rule trans :premises (@p199 @p192)) % 0.38/0.70 (step @p201 :rule refl :args (tptp.heapIm1091024090Down_a)) % 0.38/0.70 (step @p202 :rule ho_cong :premises (@p201 @p200)) % 0.38/0.70 (step @p203 :rule trans :premises (@p202 @p185)) % 0.38/0.70 (step @p204 :rule ho_cong :premises (@p160 @p203)) % 0.38/0.70 (step @p205 :rule trans :premises (@p204 @p179)) % 0.38/0.70 (step @p206 :rule refl :args ((tptp.is_heap_a @t1))) % 0.38/0.70 (step @p207 :rule cong :premises (@p167) :args (@t354)) % 0.38/0.70 (step @p208 :rule trans :premises (@p207 @p206)) % 0.38/0.70 (step @p209 :rule ho_cong :premises (@p150 @p167)) % 0.38/0.70 (step @p210 :rule cong :premises (@p209 @p208) :args ((= (_ tptp.is_heap_a @t350) @t354))) % 0.38/0.70 (step @p211 :rule symm :premises (@p210)) % 0.38/0.70 (step @p212 :rule refl :args (@t2)) % 0.38/0.70 (step @p213 :rule eq_resolve :premises (@p212 @p211)) % 0.38/0.70 (step @p214 :rule ho_cong :premises (@p160 @p196)) % 0.38/0.70 (step @p215 :rule trans :premises (@p214 @p213)) % 0.38/0.70 (step @p216 :rule cong :premises (@p215 @p205) :args (@t355)) % 0.38/0.70 (step @p217 :rule cong :premises (@p162 @p216) :args ((=> @t4 @t355))) % 0.38/0.70 (step @p218 :rule bool-impl-true2 :args (@t8)) % 0.38/0.70 (step @p219 :rule refl :args (@t8)) % 0.38/0.70 (step @p220 :rule eq-refl :args (@t6)) % 0.38/0.70 (step @p221 :rule cong :premises (@p220 @p219) :args (@t9)) % 0.38/0.70 (step @p222 :rule trans :premises (@p221 @p218)) % 0.38/0.70 (step @p223 :rule refl :args (@t2)) % 0.38/0.70 (step @p224 :rule cong :premises (@p223 @p222) :args (@t10)) % 0.38/0.70 (step @p225 :rule refl :args (@t4)) % 0.38/0.70 (step @p226 :rule cong :premises (@p225 @p224) :args (@t11)) % 0.38/0.70 (step @p227 :rule trans :premises (@p226 @p217)) % 0.38/0.70 (step @p228 :rule eq_resolve :premises (@p3 @p227)) % 0.38/0.70 (step @p229 :rule implies_elim :premises (@p228)) % 0.38/0.70 (step @p230 :rule reordering :premises (@p229) :args ((or @t356 (not @t349)))) % 0.38/0.70 (step @p231 :rule chain_m_resolution :premises (@p230 @p163) :args (@t356 (@list false) (@list @t349))) % 0.38/0.70 (step @p232 :rule eq_resolve :premises (@p1 @p215)) % 0.38/0.70 (step @p233 :rule cnf_implies_pos :args (@t356)) % 0.38/0.70 (step @p234 :rule reordering :premises (@p233) :args ((or @t353 (not @t354) (not @t356)))) % 0.38/0.70 (step @p235 :rule chain_m_resolution :premises (@p234 @p232 @p231) :args (@t353 (@list false false) (@list @t354 @t356))) % 0.38/0.70 (step @p236 :rule true_intro :premises (@p235)) % 0.38/0.70 (step @p237 :rule refl :args ((tptp.heapIm1091024090Down_a @t18))) % 0.38/0.70 (step @p238 :rule refl :args ((tptp.t_a @t16 @t15 @t13))) % 0.38/0.70 (step @p239 :rule refl :args (@t357)) % 0.38/0.70 (step @p240 :rule refl :args (@t358)) % 0.38/0.70 (step @p241 :rule refl :args (@t16)) % 0.38/0.70 (step @p242 :rule cong :premises (@p241 @p240 @p239) :args (@t359)) % 0.38/0.70 (step @p243 :rule trans :premises (@p242 @p238)) % 0.38/0.70 (step @p244 :rule cong :premises (@p243) :args (@t360)) % 0.38/0.70 (step @p245 :rule trans :premises (@p244 @p237)) % 0.38/0.70 (step @p246 :rule ho_cong :premises (@p180 @p243)) % 0.38/0.70 (step @p247 :rule cong :premises (@p246 @p245) :args ((= (_ tptp.heapIm1091024090Down_a @t359) @t360))) % 0.38/0.70 (step @p248 :rule symm :premises (@p247)) % 0.38/0.70 (step @p249 :rule refl :args (@t19)) % 0.38/0.70 (step @p250 :rule eq_resolve :premises (@p249 @p248)) % 0.38/0.70 (step @p251 :rule refl :args (@t17)) % 0.38/0.70 (step @p252 :rule ho_cong :premises (@p251 @p240)) % 0.38/0.70 (step @p253 :rule ho_cong :premises (@p252 @p239)) % 0.38/0.70 (step @p254 :rule cong :premises (@p253 @p243) :args ((= (_ (_ @t17 @t358) @t357) @t359))) % 0.38/0.70 (step @p255 :rule symm :premises (@p254)) % 0.38/0.70 (step @p256 :rule refl :args (@t18)) % 0.38/0.70 (step @p257 :rule eq_resolve :premises (@p256 @p255)) % 0.38/0.70 (step @p258 :rule refl :args (@t13)) % 0.38/0.70 (step @p259 :rule cong :premises (@p258 @p239) :args ((= @t13 @t357))) % 0.38/0.70 (step @p260 :rule symm :premises (@p259)) % 0.38/0.70 (step @p261 :rule eq_resolve :premises (@p258 @p260)) % 0.38/0.70 (step @p262 :rule refl :args (@t15)) % 0.38/0.70 (step @p263 :rule cong :premises (@p262 @p240) :args ((= @t15 @t358))) % 0.38/0.70 (step @p264 :rule symm :premises (@p263)) % 0.38/0.70 (step @p265 :rule eq_resolve :premises (@p262 @p264)) % 0.38/0.70 (step @p266 :rule ho_cong :premises (@p251 @p265)) % 0.38/0.70 (step @p267 :rule ho_cong :premises (@p266 @p261)) % 0.38/0.70 (step @p268 :rule trans :premises (@p267 @p257)) % 0.38/0.70 (step @p269 :rule ho_cong :premises (@p180 @p268)) % 0.38/0.70 (step @p270 :rule trans :premises (@p269 @p250)) % 0.38/0.70 (step @p271 :rule refl :args ((tptp.heapIm970322378pify_a @t20))) % 0.38/0.70 (step @p272 :rule refl :args (@t361)) % 0.38/0.70 (step @p273 :rule cong :premises (@p272) :args (@t362)) % 0.38/0.70 (step @p274 :rule trans :premises (@p273 @p271)) % 0.38/0.70 (step @p275 :rule refl :args (tptp.heapIm970322378pify_a)) % 0.38/0.70 (step @p276 :rule ho_cong :premises (@p275 @p272)) % 0.38/0.70 (step @p277 :rule cong :premises (@p276 @p274) :args ((= (_ tptp.heapIm970322378pify_a @t361) @t362))) % 0.38/0.70 (step @p278 :rule symm :premises (@p277)) % 0.38/0.70 (step @p279 :rule refl :args (@t21)) % 0.38/0.70 (step @p280 :rule eq_resolve :premises (@p279 @p278)) % 0.38/0.70 (step @p281 :rule refl :args (@t20)) % 0.38/0.70 (step @p282 :rule cong :premises (@p281 @p272) :args ((= @t20 @t361))) % 0.38/0.70 (step @p283 :rule symm :premises (@p282)) % 0.38/0.70 (step @p284 :rule eq_resolve :premises (@p281 @p283)) % 0.38/0.70 (step @p285 :rule ho_cong :premises (@p275 @p284)) % 0.38/0.70 (step @p286 :rule trans :premises (@p285 @p280)) % 0.38/0.70 (step @p287 :rule cong :premises (@p286 @p270) :args (@t22)) % 0.38/0.70 (step @p288 :rule cong :premises (@p287) :args (@t24)) % 0.38/0.70 (step @p289 :rule eq_resolve :premises (@p4 @p288)) % 0.38/0.70 (step @p290 :rule instantiate :premises (@p289) :args ((@list tptp.v tptp.l tptp.r))) % 0.38/0.70 (step @p291 :rule cong :premises (@p290) :args (@t365)) % 0.38/0.70 (step @p292 :rule refl :args ((tptp.is_heap_a @t344))) % 0.38/0.70 (step @p293 :rule refl :args ((tptp.heapIm970322378pify_a @t343))) % 0.38/0.70 (step @p294 :rule refl :args (@t363)) % 0.38/0.70 (step @p295 :rule cong :premises (@p294) :args (@t364)) % 0.38/0.70 (step @p296 :rule trans :premises (@p295 @p293)) % 0.38/0.70 (step @p297 :rule cong :premises (@p296) :args (@t365)) % 0.38/0.70 (step @p298 :rule trans :premises (@p297 @p292)) % 0.38/0.70 (step @p299 :rule ho_cong :premises (@p150 @p296)) % 0.38/0.70 (step @p300 :rule cong :premises (@p299 @p298) :args ((= (_ tptp.is_heap_a @t364) @t365))) % 0.38/0.70 (step @p301 :rule symm :premises (@p300)) % 0.38/0.70 (step @p302 :rule refl :args (@t345)) % 0.38/0.70 (step @p303 :rule eq_resolve :premises (@p302 @p301)) % 0.38/0.70 (step @p304 :rule ho_cong :premises (@p275 @p294)) % 0.38/0.70 (step @p305 :rule cong :premises (@p304 @p296) :args ((= (_ tptp.heapIm970322378pify_a @t363) @t364))) % 0.38/0.70 (step @p306 :rule symm :premises (@p305)) % 0.38/0.70 (step @p307 :rule refl :args (@t344)) % 0.38/0.70 (step @p308 :rule eq_resolve :premises (@p307 @p306)) % 0.38/0.70 (step @p309 :rule refl :args (@t343)) % 0.38/0.70 (step @p310 :rule cong :premises (@p309 @p294) :args ((= @t343 @t363))) % 0.38/0.70 (step @p311 :rule symm :premises (@p310)) % 0.38/0.70 (step @p312 :rule eq_resolve :premises (@p309 @p311)) % 0.38/0.70 (step @p313 :rule refl :args (tptp.heapIm970322378pify_a)) % 0.38/0.71 (step @p314 :rule ho_cong :premises (@p313 @p312)) % 0.38/0.71 (step @p315 :rule trans :premises (@p314 @p308)) % 0.38/0.71 (step @p316 :rule ho_cong :premises (@p160 @p315)) % 0.38/0.71 (step @p317 :rule trans :premises (@p316 @p303)) % 0.38/0.71 (step @p318 :rule cong :premises (@p317) :args (@t346)) % 0.38/0.71 (step @p319 :rule eq_resolve :premises (@p142 @p318)) % 0.38/0.71 (step @p320 :rule false_intro :premises (@p319)) % 0.38/0.71 (step @p321 :rule symm :premises (@p320)) % 0.38/0.71 (step @p322 :rule trans :premises (@p321 @p291 @p236)) % 0.38/0.71 (step @p323 false :rule eq_resolve :premises (@p322 @p145)) % 0.38/0.71 ) % 0.38/0.71 % SZS output end Proof % 0.38/0.71 % cvc5 exiting %------------------------------------------------------------------------------