%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWW654_2 : TPTP v9.2.1. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n014.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 09:05:25 AM UTC 2026 % Result : Theorem 4.34s 4.53s % Output : Proof 4.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW654_2 : TPTP v9.2.1. Released v6.1.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n014.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue Jun 2 22:22:13 EDT 2026 % 0.18/0.35 % CPUTime : % 0.28/0.52 %----Proving TF0_ARI % 4.34/4.53 --- Run --finite-model-find --decision=internal at 45... % 4.34/4.53 % SZS status Theorem % 4.34/4.53 % SZS output start Proof % 4.34/4.53 ( % 4.34/4.53 (declare-sort tptp.color1 0) % 4.34/4.53 (declare-sort tptp.tuple02 0) % 4.34/4.53 (declare-sort tptp.bool1 0) % 4.34/4.53 (declare-sort tptp.ty 0) % 4.34/4.53 (declare-sort tptp.uni 0) % 4.34/4.53 (declare-sort tptp.tree1 0) % 4.34/4.53 (declare-const tptp.almost_rbtree1 (-> Int tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.memt1 (-> tptp.tree1 Int Int Bool)) % 4.34/4.53 (declare-const tptp.node_proj_51 (-> tptp.tree1 tptp.tree1)) % 4.34/4.53 (declare-const tptp.rbtree1 (-> Int tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.node_proj_31 (-> tptp.tree1 Int)) % 4.34/4.53 (declare-const tptp.gt_tree1 (-> Int tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.witness1 (-> tptp.ty tptp.uni)) % 4.34/4.53 (declare-const tptp.tuple03 tptp.tuple02) % 4.34/4.53 (declare-const tptp.lt_tree1 (-> Int tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.match_tree1 (-> tptp.ty tptp.tree1 tptp.uni tptp.uni tptp.uni)) % 4.34/4.53 (declare-const tptp.node_proj_21 (-> tptp.tree1 tptp.tree1)) % 4.34/4.53 (declare-const tptp.sort1 (-> tptp.ty tptp.uni Bool)) % 4.34/4.53 (declare-const tptp.match_color1 (-> tptp.ty tptp.color1 tptp.uni tptp.uni tptp.uni)) % 4.34/4.53 (declare-const tptp.node_proj_41 (-> tptp.tree1 Int)) % 4.34/4.53 (declare-const tptp.match_bool1 (-> tptp.ty tptp.bool1 tptp.uni tptp.uni tptp.uni)) % 4.34/4.53 (declare-const tptp.node1 (-> tptp.color1 tptp.tree1 Int Int tptp.tree1 tptp.tree1)) % 4.34/4.53 (declare-const tptp.red1 tptp.color1) % 4.34/4.53 (declare-const tptp.true1 tptp.bool1) % 4.34/4.53 (declare-const tptp.is_not_red1 (-> tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.node_proj_11 (-> tptp.tree1 tptp.color1)) % 4.34/4.53 (declare-const tptp.bst1 (-> tptp.tree1 Bool)) % 4.34/4.53 (declare-const tptp.false1 tptp.bool1) % 4.34/4.53 (declare-const tptp.black1 tptp.color1) % 4.34/4.53 (declare-const tptp.leaf1 tptp.tree1) % 4.34/4.53 (define @t1 () (@var "A" tptp.ty)) % 4.34/4.53 (define @t2 () (@var "X2" tptp.uni)) % 4.34/4.53 (define @t3 () (@var "X1" tptp.uni)) % 4.34/4.53 (define @t4 () (@var "X" tptp.bool1)) % 4.34/4.53 (define @t5 () (@var "Z" tptp.uni)) % 4.34/4.53 (define @t6 () (@var "Z1" tptp.uni)) % 4.34/4.53 (define @t7 () (tptp.sort1 @t1 @t5)) % 4.34/4.53 (define @t8 () (@list @t1 @t5 @t6)) % 4.34/4.53 (define @t9 () (tptp.sort1 @t1 @t6)) % 4.34/4.53 (define @t10 () (@var "U" tptp.bool1)) % 4.34/4.53 (define @t11 () (@var "U" tptp.tuple02)) % 4.34/4.53 (define @t12 () (@var "X" tptp.color1)) % 4.34/4.53 (define @t13 () (@var "U" tptp.color1)) % 4.34/4.53 (define @t14 () (@var "X" tptp.tree1)) % 4.34/4.53 (define @t15 () (@var "U4" tptp.tree1)) % 4.34/4.53 (define @t16 () (@var "U3" Int)) % 4.34/4.53 (define @t17 () (@var "U2" Int)) % 4.34/4.53 (define @t18 () (@var "U1" tptp.tree1)) % 4.34/4.53 (define @t19 () (tptp.node1 @t13 @t18 @t17 @t16 @t15)) % 4.34/4.53 (define @t20 () (@var "V4" tptp.tree1)) % 4.34/4.53 (define @t21 () (@var "V3" Int)) % 4.34/4.53 (define @t22 () (@var "V2" Int)) % 4.34/4.53 (define @t23 () (@var "V1" tptp.tree1)) % 4.34/4.53 (define @t24 () (@var "V" tptp.color1)) % 4.34/4.53 (define @t25 () (@list @t13 @t18 @t17 @t16 @t15)) % 4.34/4.53 (define @t26 () (@var "U" tptp.tree1)) % 4.34/4.53 (define @t27 () (@var "V" Int)) % 4.34/4.53 (define @t28 () (@var "K" Int)) % 4.34/4.53 (define @t29 () (@var "X4" tptp.tree1)) % 4.34/4.53 (define @t30 () (@var "X1" tptp.tree1)) % 4.34/4.53 (define @t31 () (@var "X3" Int)) % 4.34/4.53 (define @t32 () (@var "X2" Int)) % 4.34/4.53 (define @t33 () (tptp.node1 @t12 @t30 @t32 @t31 @t29)) % 4.34/4.53 (define @t34 () (@list @t12 @t30 @t32 @t31 @t29)) % 4.34/4.53 (define @t35 () (@list @t28 @t27)) % 4.34/4.53 (define @t36 () (@var "Vqt" Int)) % 4.34/4.53 (define @t37 () (@var "Kqt" Int)) % 4.34/4.53 (define @t38 () (@var "R" tptp.tree1)) % 4.34/4.53 (define @t39 () (@var "L" tptp.tree1)) % 4.34/4.53 (define @t40 () (@var "Cqt" tptp.color1)) % 4.34/4.53 (define @t41 () (tptp.node1 @t40 @t39 @t28 @t27 @t38)) % 4.34/4.53 (define @t42 () (@var "C" tptp.color1)) % 4.34/4.53 (define @t43 () (tptp.node1 @t42 @t39 @t28 @t27 @t38)) % 4.34/4.53 (define @t44 () (@var "Z" Int)) % 4.34/4.53 (define @t45 () (@var "Y" Int)) % 4.34/4.53 (define @t46 () (@var "X" Int)) % 4.34/4.53 (define @t47 () (@var "T" tptp.tree1)) % 4.34/4.53 (define @t48 () (tptp.memt1 @t47 @t28 @t27)) % 4.34/4.53 (define @t49 () (tptp.lt_tree1 @t46 @t47)) % 4.34/4.53 (define @t50 () (@list @t46 @t47)) % 4.34/4.53 (define @t51 () (tptp.gt_tree1 @t46 @t47)) % 4.34/4.53 (define @t52 () (@list @t46)) % 4.34/4.53 (define @t53 () (tptp.node1 @t42 @t39 @t45 @t27 @t38)) % 4.34/4.53 (define @t54 () (tptp.lt_tree1 @t46 @t53)) % 4.34/4.53 (define @t55 () (< @t45 @t46)) % 4.34/4.53 (define @t56 () (tptp.lt_tree1 @t46 @t38)) % 4.34/4.53 (define @t57 () (tptp.lt_tree1 @t46 @t39)) % 4.34/4.53 (define @t58 () (@list @t46 @t45 @t27 @t39 @t38 @t42)) % 4.34/4.53 (define @t59 () (tptp.gt_tree1 @t46 @t53)) % 4.34/4.53 (define @t60 () (< @t46 @t45)) % 4.34/4.53 (define @t61 () (tptp.gt_tree1 @t46 @t38)) % 4.34/4.53 (define @t62 () (tptp.gt_tree1 @t46 @t39)) % 4.34/4.53 (define @t63 () (forall (@list @t27) (not (tptp.memt1 @t47 @t46 @t27)))) % 4.34/4.53 (define @t64 () (@list @t47)) % 4.34/4.53 (define @t65 () (@list @t46 @t45)) % 4.34/4.53 (define @t66 () (forall @t34 (= (tptp.bst1 @t33) (and (tptp.bst1 @t30) (tptp.bst1 @t29) (tptp.lt_tree1 @t32 @t30) (tptp.gt_tree1 @t32 @t29))))) % 4.34/4.53 (define @t67 () (tptp.bst1 tptp.leaf1)) % 4.34/4.53 (define @t68 () (tptp.bst1 @t39)) % 4.34/4.53 (define @t69 () (tptp.bst1 @t43)) % 4.34/4.53 (define @t70 () (@list @t28 @t27 @t39 @t38 @t42)) % 4.34/4.53 (define @t71 () (tptp.bst1 @t38)) % 4.34/4.53 (define @t72 () (tptp.bst1 @t41)) % 4.34/4.53 (define @t73 () (forall (@list @t42 @t40 @t28 @t27 @t39 @t38) (=> @t69 @t72))) % 4.34/4.53 (define @t74 () (@var "C" tptp.tree1)) % 4.34/4.53 (define @t75 () (@var "Vy" Int)) % 4.34/4.53 (define @t76 () (@var "Ky" Int)) % 4.34/4.53 (define @t77 () (@var "B" tptp.tree1)) % 4.34/4.53 (define @t78 () (@var "Vx" Int)) % 4.34/4.53 (define @t79 () (@var "Kx" Int)) % 4.34/4.53 (define @t80 () (@var "A" tptp.tree1)) % 4.34/4.53 (define @t81 () (@var "C4" tptp.color1)) % 4.34/4.53 (define @t82 () (@var "C3" tptp.color1)) % 4.34/4.53 (define @t83 () (tptp.bst1 (tptp.node1 @t82 (tptp.node1 @t81 @t80 @t79 @t78 @t77) @t76 @t75 @t74))) % 4.34/4.53 (define @t84 () (@var "C2" tptp.color1)) % 4.34/4.53 (define @t85 () (@var "C1" tptp.color1)) % 4.34/4.53 (define @t86 () (tptp.bst1 (tptp.node1 @t85 @t80 @t79 @t78 (tptp.node1 @t84 @t77 @t76 @t75 @t74)))) % 4.34/4.53 (define @t87 () (@list @t79 @t76 @t78 @t75 @t80 @t77 @t74 @t85 @t84 @t82 @t81)) % 4.34/4.53 (define @t88 () (forall @t87 (=> @t86 @t83))) % 4.34/4.53 (define @t89 () (forall @t87 (=> @t83 @t86))) % 4.34/4.53 (define @t90 () (tptp.is_not_red1 @t33)) % 4.34/4.53 (define @t91 () (= @t12 tptp.black1)) % 4.34/4.53 (define @t92 () (= @t12 tptp.red1)) % 4.34/4.53 (define @t93 () (@var "N" Int)) % 4.34/4.53 (define @t94 () (- @t93 1)) % 4.34/4.53 (define @t95 () (and (tptp.rbtree1 @t94 @t30) (tptp.rbtree1 @t94 @t29))) % 4.34/4.53 (define @t96 () (tptp.rbtree1 @t93 @t33)) % 4.34/4.53 (define @t97 () (tptp.rbtree1 @t93 @t29)) % 4.34/4.53 (define @t98 () (tptp.rbtree1 @t93 @t30)) % 4.34/4.53 (define @t99 () (= @t93 0)) % 4.34/4.53 (define @t100 () (@list @t93)) % 4.34/4.53 (define @t101 () (exists @t100 (tptp.rbtree1 @t93 (tptp.node1 @t42 @t39 @t46 @t27 @t38)))) % 4.34/4.53 (define @t102 () (@list @t46 @t27 @t39 @t38 @t42)) % 4.34/4.53 (define @t103 () (tptp.almost_rbtree1 @t93 @t33)) % 4.34/4.53 (define @t104 () (@var "S" tptp.tree1)) % 4.34/4.53 (define @t105 () (tptp.node1 tptp.black1 @t39 @t46 @t27 @t38)) % 4.34/4.53 (define @t106 () (tptp.node1 tptp.black1 @t29 @t28 @t27 @t38)) % 4.34/4.53 (define @t107 () (@var "X14" tptp.tree1)) % 4.34/4.53 (define @t108 () (@var "X13" Int)) % 4.34/4.53 (define @t109 () (@var "X12" Int)) % 4.34/4.53 (define @t110 () (@var "X11" tptp.tree1)) % 4.34/4.53 (define @t111 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t110 @t109 @t108 @t107) @t32 @t31 @t106))) % 4.34/4.53 (define @t112 () (=> @t92 @t111)) % 4.34/4.53 (define @t113 () (@var "X10" tptp.color1)) % 4.34/4.53 (define @t114 () (= @t113 tptp.red1)) % 4.34/4.53 (define @t115 () (=> @t114 @t112)) % 4.34/4.53 (define @t116 () (= @t30 (tptp.node1 @t113 @t110 @t109 @t108 @t107))) % 4.34/4.53 (define @t117 () (=> @t116 @t115)) % 4.34/4.53 (define @t118 () (@list @t113 @t110 @t109 @t108 @t107)) % 4.34/4.53 (define @t119 () (forall @t118 @t117)) % 4.34/4.53 (define @t120 () (@var "X5" tptp.color1)) % 4.34/4.53 (define @t121 () (=> (= @t120 tptp.black1) @t119)) % 4.34/4.53 (define @t122 () (@var "X9" tptp.tree1)) % 4.34/4.53 (define @t123 () (@var "X8" Int)) % 4.34/4.53 (define @t124 () (@var "X7" Int)) % 4.34/4.53 (define @t125 () (@var "X6" tptp.tree1)) % 4.34/4.53 (define @t126 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t30 @t32 @t31 @t125) @t124 @t123 (tptp.node1 tptp.black1 @t122 @t28 @t27 @t38)))) % 4.34/4.53 (define @t127 () (=> @t92 @t126)) % 4.34/4.53 (define @t128 () (=> (= @t113 tptp.black1) @t127)) % 4.34/4.53 (define @t129 () (and @t115 @t128)) % 4.34/4.53 (define @t130 () (=> @t116 @t129)) % 4.34/4.53 (define @t131 () (forall @t118 @t130)) % 4.34/4.53 (define @t132 () (=> (= @t30 tptp.leaf1) @t127)) % 4.34/4.53 (define @t133 () (and @t132 @t131)) % 4.34/4.53 (define @t134 () (= @t120 tptp.red1)) % 4.34/4.53 (define @t135 () (=> @t134 @t133)) % 4.34/4.53 (define @t136 () (and @t135 @t121)) % 4.34/4.53 (define @t137 () (tptp.node1 @t120 @t125 @t124 @t123 @t122)) % 4.34/4.53 (define @t138 () (= @t29 @t137)) % 4.34/4.53 (define @t139 () (=> @t138 @t136)) % 4.34/4.53 (define @t140 () (@list @t120 @t125 @t124 @t123 @t122)) % 4.34/4.53 (define @t141 () (forall @t140 @t139)) % 4.34/4.53 (define @t142 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t125 @t124 @t123 @t122) @t32 @t31 @t106))) % 4.34/4.53 (define @t143 () (=> @t92 @t142)) % 4.34/4.53 (define @t144 () (=> @t134 @t143)) % 4.34/4.53 (define @t145 () (= @t30 @t137)) % 4.34/4.53 (define @t146 () (=> @t145 @t144)) % 4.34/4.53 (define @t147 () (forall @t140 @t146)) % 4.34/4.53 (define @t148 () (=> (= @t29 tptp.leaf1) @t147)) % 4.34/4.53 (define @t149 () (and @t148 @t141)) % 4.34/4.53 (define @t150 () (=> (= @t39 @t33) @t149)) % 4.34/4.53 (define @t151 () (forall @t34 @t150)) % 4.34/4.53 (define @t152 () (tptp.gt_tree1 @t28 @t38)) % 4.34/4.53 (define @t153 () (tptp.lt_tree1 @t28 @t39)) % 4.34/4.53 (define @t154 () (and @t153 @t152 @t68 @t71)) % 4.34/4.53 (define @t155 () (=> @t154 @t151)) % 4.34/4.53 (define @t156 () (@list @t39 @t28 @t27 @t38)) % 4.34/4.53 (define @t157 () (forall @t156 @t155)) % 4.34/4.53 (define @t158 () (not @t157)) % 4.34/4.53 (define @t159 () (@var "BOUND_VARIABLE_8776" tptp.tree1)) % 4.34/4.53 (define @t160 () (tptp.node1 tptp.black1 @t159 @t28 @t27 @t38)) % 4.34/4.53 (define @t161 () (@var "BOUND_VARIABLE_8774" Int)) % 4.34/4.53 (define @t162 () (@var "BOUND_VARIABLE_8772" Int)) % 4.34/4.53 (define @t163 () (@var "BOUND_VARIABLE_8812" tptp.tree1)) % 4.34/4.53 (define @t164 () (@var "BOUND_VARIABLE_8810" Int)) % 4.34/4.53 (define @t165 () (@var "BOUND_VARIABLE_8808" Int)) % 4.34/4.53 (define @t166 () (@var "BOUND_VARIABLE_8806" tptp.tree1)) % 4.34/4.53 (define @t167 () (@var "BOUND_VARIABLE_8770" tptp.tree1)) % 4.34/4.53 (define @t168 () (@var "BOUND_VARIABLE_8768" tptp.color1)) % 4.34/4.53 (define @t169 () (not (= tptp.red1 @t168))) % 4.34/4.53 (define @t170 () (@var "BOUND_VARIABLE_8786" tptp.color1)) % 4.34/4.53 (define @t171 () (@var "BOUND_VARIABLE_8794" tptp.tree1)) % 4.34/4.53 (define @t172 () (@var "BOUND_VARIABLE_8792" Int)) % 4.34/4.53 (define @t173 () (@var "BOUND_VARIABLE_8790" Int)) % 4.34/4.53 (define @t174 () (@var "BOUND_VARIABLE_8788" tptp.tree1)) % 4.34/4.53 (define @t175 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t167 @t162 @t161 @t174) @t173 @t172 (tptp.node1 tptp.black1 @t171 @t28 @t27 @t38)))) % 4.34/4.53 (define @t176 () (@var "BOUND_VARIABLE_8796" tptp.color1)) % 4.34/4.53 (define @t177 () (@var "BOUND_VARIABLE_8804" tptp.tree1)) % 4.34/4.53 (define @t178 () (@var "BOUND_VARIABLE_8802" Int)) % 4.34/4.53 (define @t179 () (@var "BOUND_VARIABLE_8800" Int)) % 4.34/4.53 (define @t180 () (@var "BOUND_VARIABLE_8798" tptp.tree1)) % 4.34/4.53 (define @t181 () (@var "BOUND_VARIABLE_8784" tptp.tree1)) % 4.34/4.53 (define @t182 () (@var "BOUND_VARIABLE_8782" Int)) % 4.34/4.53 (define @t183 () (@var "BOUND_VARIABLE_8780" Int)) % 4.34/4.53 (define @t184 () (@var "BOUND_VARIABLE_8778" tptp.tree1)) % 4.34/4.53 (define @t185 () (and (or (not (= tptp.leaf1 @t159)) @t169 (not (= @t167 (tptp.node1 tptp.red1 @t184 @t183 @t182 @t181))) (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t184 @t183 @t182 @t181) @t162 @t161 @t160))) (or (not (= @t159 (tptp.node1 @t170 @t174 @t173 @t172 @t171))) (and (or (not (= tptp.red1 @t170)) (and (or (not (= tptp.leaf1 @t167)) @t169 @t175) (or (not (= @t167 (tptp.node1 @t176 @t180 @t179 @t178 @t177))) (and (or (not (= tptp.red1 @t176)) @t169 (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t180 @t179 @t178 @t177) @t162 @t161 @t160))) (or (not (= tptp.black1 @t176)) @t169 @t175))))) (or (not (= tptp.black1 @t170)) @t169 (not (= @t167 (tptp.node1 tptp.red1 @t166 @t165 @t164 @t163))) (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t166 @t165 @t164 @t163) @t162 @t161 @t160))))))) % 4.34/4.53 (define @t186 () (not @t71)) % 4.34/4.53 (define @t187 () (tptp.node1 @t168 @t167 @t162 @t161 @t159)) % 4.34/4.53 (define @t188 () (not (tptp.bst1 @t187))) % 4.34/4.53 (define @t189 () (not @t152)) % 4.34/4.53 (define @t190 () (not (tptp.lt_tree1 @t28 @t187))) % 4.34/4.53 (define @t191 () (or @t190 @t189 @t188 @t186 @t185)) % 4.34/4.53 (define @t192 () (@list @t28 @t27 @t38 @t168 @t167 @t162 @t161 @t159 @t184 @t183 @t182 @t181 @t170 @t174 @t173 @t172 @t171 @t176 @t180 @t179 @t178 @t177 @t166 @t165 @t164 @t163)) % 4.34/4.53 (define @t193 () (forall @t192 @t191)) % 4.34/4.53 (define @t194 () (@quantifiers_skolemize @t193 2)) % 4.34/4.53 (define @t195 () (@quantifiers_skolemize @t193 1)) % 4.34/4.53 (define @t196 () (@quantifiers_skolemize @t193 0)) % 4.34/4.53 (define @t197 () (@quantifiers_skolemize @t193 7)) % 4.34/4.53 (define @t198 () (tptp.node1 tptp.black1 @t197 @t196 @t195 @t194)) % 4.34/4.53 (define @t199 () (@quantifiers_skolemize @t193 6)) % 4.34/4.53 (define @t200 () (@quantifiers_skolemize @t193 5)) % 4.34/4.53 (define @t201 () (@quantifiers_skolemize @t193 4)) % 4.34/4.53 (define @t202 () (@quantifiers_skolemize @t193 3)) % 4.34/4.53 (define @t203 () (tptp.node1 @t202 @t201 @t200 @t199 @t197)) % 4.34/4.53 (define @t204 () (not (= @t187 @t187))) % 4.34/4.53 (define @t205 () (or @t190 @t189 @t188 @t186 @t204 @t185)) % 4.34/4.53 (define @t206 () (not (= @t39 @t187))) % 4.34/4.53 (define @t207 () (not @t68)) % 4.34/4.53 (define @t208 () (not @t153)) % 4.34/4.53 (define @t209 () (or @t206 @t208 @t189 @t207 @t186 @t206 @t185)) % 4.34/4.53 (define @t210 () (@list @t39)) % 4.34/4.53 (define @t211 () (or @t208 @t189 @t207 @t186 @t206 @t185)) % 4.34/4.53 (define @t212 () (forall @t210 @t211)) % 4.34/4.53 (define @t213 () (forall @t192 @t212)) % 4.34/4.53 (define @t214 () (forall (@list @t28 @t27 @t38 @t168 @t167 @t162 @t161 @t159 @t184 @t183 @t182 @t181 @t170 @t174 @t173 @t172 @t171 @t176 @t180 @t179 @t178 @t177 @t166 @t165 @t164 @t163 @t39) @t211)) % 4.34/4.53 (define @t215 () (@list @t39 @t28 @t27 @t38 @t168 @t167 @t162 @t161 @t159 @t184 @t183 @t182 @t181 @t170 @t174 @t173 @t172 @t171 @t176 @t180 @t179 @t178 @t177 @t166 @t165 @t164 @t163)) % 4.34/4.53 (define @t216 () (not (= @t187 @t39))) % 4.34/4.53 (define @t217 () (or @t208 @t189 @t207 @t186 @t216 @t185)) % 4.34/4.53 (define @t218 () (or @t216 @t185)) % 4.34/4.53 (define @t219 () (or @t208 @t189 @t207 @t186 @t218)) % 4.34/4.53 (define @t220 () (forall @t215 @t219)) % 4.34/4.53 (define @t221 () (@list @t168 @t167 @t162 @t161 @t159 @t184 @t183 @t182 @t181 @t170 @t174 @t173 @t172 @t171 @t176 @t180 @t179 @t178 @t177 @t166 @t165 @t164 @t163)) % 4.34/4.53 (define @t222 () (forall @t221 @t219)) % 4.34/4.53 (define @t223 () (forall @t221 @t218)) % 4.34/4.53 (define @t224 () (@var "BOUND_VARIABLE_8711" tptp.tree1)) % 4.34/4.53 (define @t225 () (@var "BOUND_VARIABLE_8709" Int)) % 4.34/4.53 (define @t226 () (@var "BOUND_VARIABLE_8707" Int)) % 4.34/4.53 (define @t227 () (@var "BOUND_VARIABLE_8705" tptp.tree1)) % 4.34/4.53 (define @t228 () (@var "BOUND_VARIABLE_8703" tptp.tree1)) % 4.34/4.53 (define @t229 () (@var "BOUND_VARIABLE_8701" Int)) % 4.34/4.53 (define @t230 () (@var "BOUND_VARIABLE_8699" Int)) % 4.34/4.53 (define @t231 () (@var "BOUND_VARIABLE_8697" tptp.tree1)) % 4.34/4.53 (define @t232 () (@var "BOUND_VARIABLE_8695" tptp.color1)) % 4.34/4.53 (define @t233 () (@var "BOUND_VARIABLE_8693" tptp.tree1)) % 4.34/4.53 (define @t234 () (@var "BOUND_VARIABLE_8691" Int)) % 4.34/4.53 (define @t235 () (@var "BOUND_VARIABLE_8689" Int)) % 4.34/4.53 (define @t236 () (@var "BOUND_VARIABLE_8687" tptp.tree1)) % 4.34/4.53 (define @t237 () (@var "BOUND_VARIABLE_8685" tptp.color1)) % 4.34/4.53 (define @t238 () (@var "BOUND_VARIABLE_8675" tptp.tree1)) % 4.34/4.53 (define @t239 () (@var "BOUND_VARIABLE_8673" Int)) % 4.34/4.53 (define @t240 () (@var "BOUND_VARIABLE_8671" Int)) % 4.34/4.53 (define @t241 () (@var "BOUND_VARIABLE_8669" tptp.tree1)) % 4.34/4.53 (define @t242 () (or @t208 @t189 @t207 @t186 @t223)) % 4.34/4.53 (define @t243 () (= tptp.red1 @t12)) % 4.34/4.53 (define @t244 () (not @t243)) % 4.34/4.53 (define @t245 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t30 @t32 @t31 @t236) @t235 @t234 (tptp.node1 tptp.black1 @t233 @t28 @t27 @t38)))) % 4.34/4.53 (define @t246 () (= tptp.leaf1 @t30)) % 4.34/4.53 (define @t247 () (not @t246)) % 4.34/4.53 (define @t248 () (or (not (= @t29 (tptp.node1 @t237 @t236 @t235 @t234 @t233))) (and (or (not (= tptp.red1 @t237)) (and (or @t247 @t244 @t245) (or (not (= @t30 (tptp.node1 @t232 @t231 @t230 @t229 @t228))) (and (or (not (= tptp.red1 @t232)) @t244 (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t231 @t230 @t229 @t228) @t32 @t31 @t106))) (or (not (= tptp.black1 @t232)) @t244 @t245))))) (or (not (= tptp.black1 @t237)) @t244 (not (= @t30 (tptp.node1 tptp.red1 @t227 @t226 @t225 @t224))) (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t227 @t226 @t225 @t224) @t32 @t31 @t106)))))) % 4.34/4.53 (define @t249 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t241 @t240 @t239 @t238) @t32 @t31 @t106))) % 4.34/4.53 (define @t250 () (not (= @t30 (tptp.node1 tptp.red1 @t241 @t240 @t239 @t238)))) % 4.34/4.53 (define @t251 () (= tptp.leaf1 @t29)) % 4.34/4.53 (define @t252 () (not @t251)) % 4.34/4.53 (define @t253 () (or @t252 @t244 @t250 @t249)) % 4.34/4.53 (define @t254 () (= @t33 @t39)) % 4.34/4.53 (define @t255 () (not @t254)) % 4.34/4.53 (define @t256 () (@list @t12 @t30 @t32 @t31 @t29 @t241 @t240 @t239 @t238 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224)) % 4.34/4.53 (define @t257 () (forall @t256 (or @t255 (and @t253 @t248)))) % 4.34/4.53 (define @t258 () (or @t208 @t189 @t207 @t186 @t257)) % 4.34/4.53 (define @t259 () (or @t208 @t189 @t207 @t186)) % 4.34/4.53 (define @t260 () (or @t250 @t249)) % 4.34/4.53 (define @t261 () (or @t252 @t244 @t260)) % 4.34/4.53 (define @t262 () (and @t261 @t248)) % 4.34/4.53 (define @t263 () (or @t255 @t262)) % 4.34/4.53 (define @t264 () (forall @t256 @t263)) % 4.34/4.53 (define @t265 () (@list @t241 @t240 @t239 @t238 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224)) % 4.34/4.53 (define @t266 () (forall @t265 @t263)) % 4.34/4.53 (define @t267 () (forall (@list @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224) @t248)) % 4.34/4.53 (define @t268 () (@var "BOUND_VARIABLE_8642" tptp.tree1)) % 4.34/4.53 (define @t269 () (@var "BOUND_VARIABLE_8640" Int)) % 4.34/4.53 (define @t270 () (@var "BOUND_VARIABLE_8638" Int)) % 4.34/4.53 (define @t271 () (@var "BOUND_VARIABLE_8636" tptp.tree1)) % 4.34/4.53 (define @t272 () (@var "BOUND_VARIABLE_8618" tptp.tree1)) % 4.34/4.53 (define @t273 () (@var "BOUND_VARIABLE_8616" Int)) % 4.34/4.53 (define @t274 () (@var "BOUND_VARIABLE_8614" Int)) % 4.34/4.53 (define @t275 () (@var "BOUND_VARIABLE_8612" tptp.tree1)) % 4.34/4.53 (define @t276 () (@var "BOUND_VARIABLE_8610" tptp.color1)) % 4.34/4.53 (define @t277 () (forall @t265 @t248)) % 4.34/4.53 (define @t278 () (@list @t241 @t240 @t239 @t238)) % 4.34/4.53 (define @t279 () (forall @t278 @t260)) % 4.34/4.53 (define @t280 () (or @t252 @t244 @t279)) % 4.34/4.53 (define @t281 () (forall @t278 @t261)) % 4.34/4.53 (define @t282 () (forall @t265 @t261)) % 4.34/4.53 (define @t283 () (and @t282 @t277)) % 4.34/4.53 (define @t284 () (forall @t265 @t262)) % 4.34/4.53 (define @t285 () (or @t255 @t284)) % 4.34/4.53 (define @t286 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t271 @t270 @t269 @t268) @t32 @t31 @t106))) % 4.34/4.53 (define @t287 () (not (= @t30 (tptp.node1 tptp.red1 @t271 @t270 @t269 @t268)))) % 4.34/4.53 (define @t288 () (= tptp.black1 @t120)) % 4.34/4.53 (define @t289 () (not @t288)) % 4.34/4.53 (define @t290 () (or @t289 @t244 @t287 @t286)) % 4.34/4.53 (define @t291 () (or (not (= @t30 (tptp.node1 @t276 @t275 @t274 @t273 @t272))) (and (or (not (= tptp.red1 @t276)) @t244 (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t275 @t274 @t273 @t272) @t32 @t31 @t106))) (or (not (= tptp.black1 @t276)) @t244 @t126)))) % 4.34/4.53 (define @t292 () (or @t247 @t244 @t126)) % 4.34/4.53 (define @t293 () (and @t292 @t291)) % 4.34/4.53 (define @t294 () (= tptp.red1 @t120)) % 4.34/4.53 (define @t295 () (not @t294)) % 4.34/4.53 (define @t296 () (or @t295 @t293)) % 4.34/4.53 (define @t297 () (not @t138)) % 4.34/4.53 (define @t298 () (@list @t120 @t125 @t124 @t123 @t122 @t276 @t275 @t274 @t273 @t272 @t271 @t270 @t269 @t268)) % 4.34/4.53 (define @t299 () (forall @t298 (or @t297 (and @t296 @t290)))) % 4.34/4.53 (define @t300 () (not (= @t30 (tptp.node1 tptp.red1 @t125 @t124 @t123 @t122)))) % 4.34/4.53 (define @t301 () (or @t300 @t142)) % 4.34/4.53 (define @t302 () (@list @t125 @t124 @t123 @t122)) % 4.34/4.53 (define @t303 () (forall @t302 @t301)) % 4.34/4.53 (define @t304 () (or @t252 @t244 @t303)) % 4.34/4.53 (define @t305 () (or @t244 @t303)) % 4.34/4.53 (define @t306 () (and (=> @t251 @t305) @t299)) % 4.34/4.53 (define @t307 () (or @t287 @t286)) % 4.34/4.53 (define @t308 () (or @t289 @t244 @t307)) % 4.34/4.53 (define @t309 () (and @t296 @t308)) % 4.34/4.53 (define @t310 () (or @t297 @t309)) % 4.34/4.53 (define @t311 () (forall @t298 @t310)) % 4.34/4.53 (define @t312 () (@list @t276 @t275 @t274 @t273 @t272 @t271 @t270 @t269 @t268)) % 4.34/4.53 (define @t313 () (forall @t312 @t310)) % 4.34/4.53 (define @t314 () (@list @t271 @t270 @t269 @t268)) % 4.34/4.53 (define @t315 () (forall @t314 @t307)) % 4.34/4.53 (define @t316 () (or @t289 @t244 @t315)) % 4.34/4.53 (define @t317 () (forall @t314 @t308)) % 4.34/4.53 (define @t318 () (forall @t312 @t308)) % 4.34/4.53 (define @t319 () (@list @t276 @t275 @t274 @t273 @t272)) % 4.34/4.53 (define @t320 () (forall @t319 @t291)) % 4.34/4.53 (define @t321 () (forall @t319 @t292)) % 4.34/4.53 (define @t322 () (and @t321 @t320)) % 4.34/4.53 (define @t323 () (forall @t319 @t293)) % 4.34/4.53 (define @t324 () (or @t295 @t323)) % 4.34/4.53 (define @t325 () (forall @t319 @t296)) % 4.34/4.53 (define @t326 () (forall @t312 @t296)) % 4.34/4.53 (define @t327 () (and @t326 @t318)) % 4.34/4.53 (define @t328 () (forall @t312 @t309)) % 4.34/4.53 (define @t329 () (or @t297 @t328)) % 4.34/4.53 (define @t330 () (not (= @t30 (tptp.node1 tptp.red1 @t110 @t109 @t108 @t107)))) % 4.34/4.53 (define @t331 () (or @t330 @t111)) % 4.34/4.53 (define @t332 () (@list @t110 @t109 @t108 @t107)) % 4.34/4.53 (define @t333 () (forall @t332 @t331)) % 4.34/4.53 (define @t334 () (or @t289 @t244 @t333)) % 4.34/4.53 (define @t335 () (= tptp.black1 @t113)) % 4.34/4.53 (define @t336 () (not @t335)) % 4.34/4.53 (define @t337 () (or @t336 @t244 @t126)) % 4.34/4.53 (define @t338 () (= tptp.red1 @t113)) % 4.34/4.53 (define @t339 () (not @t338)) % 4.34/4.53 (define @t340 () (or @t339 @t244 @t111)) % 4.34/4.53 (define @t341 () (not @t116)) % 4.34/4.53 (define @t342 () (forall @t118 (or @t341 (and @t340 @t337)))) % 4.34/4.53 (define @t343 () (or @t244 @t333)) % 4.34/4.53 (define @t344 () (or @t244 @t126)) % 4.34/4.53 (define @t345 () (=> @t243 @t126)) % 4.34/4.53 (define @t346 () (and (=> @t246 @t345) @t342)) % 4.34/4.53 (define @t347 () (and (=> @t294 @t346) (=> @t288 @t343))) % 4.34/4.53 (define @t348 () (not (= tptp.red1 tptp.red1))) % 4.34/4.53 (define @t349 () (or @t330 @t348 @t111)) % 4.34/4.53 (define @t350 () (@list @t113)) % 4.34/4.53 (define @t351 () (or @t339 @t341 @t339 @t111)) % 4.34/4.53 (define @t352 () (or @t341 @t339 @t111)) % 4.34/4.53 (define @t353 () (forall @t350 @t352)) % 4.34/4.53 (define @t354 () (forall @t332 @t353)) % 4.34/4.53 (define @t355 () (forall (@list @t110 @t109 @t108 @t107 @t113) @t352)) % 4.34/4.53 (define @t356 () (forall @t118 @t352)) % 4.34/4.53 (define @t357 () (or @t244 @t356)) % 4.34/4.53 (define @t358 () (or @t244 @t352)) % 4.34/4.53 (define @t359 () (or @t341 @t339 @t244 @t111)) % 4.34/4.53 (define @t360 () (=> @t243 @t111)) % 4.34/4.53 (define @t361 () (=> @t338 @t360)) % 4.34/4.53 (define @t362 () (and @t361 (=> @t335 @t345))) % 4.34/4.53 (define @t363 () (or @t300 @t348 @t142)) % 4.34/4.53 (define @t364 () (not @t145)) % 4.34/4.53 (define @t365 () (@list @t120)) % 4.34/4.53 (define @t366 () (or @t295 @t364 @t295 @t142)) % 4.34/4.53 (define @t367 () (or @t364 @t295 @t142)) % 4.34/4.53 (define @t368 () (forall @t365 @t367)) % 4.34/4.53 (define @t369 () (forall @t302 @t368)) % 4.34/4.53 (define @t370 () (forall (@list @t125 @t124 @t123 @t122 @t120) @t367)) % 4.34/4.53 (define @t371 () (forall @t140 @t367)) % 4.34/4.53 (define @t372 () (or @t244 @t371)) % 4.34/4.53 (define @t373 () (or @t244 @t367)) % 4.34/4.53 (define @t374 () (or @t364 @t295 @t244 @t142)) % 4.34/4.53 (define @t375 () (or @t295 @t244 @t142)) % 4.34/4.53 (define @t376 () (=> @t243 @t142)) % 4.34/4.53 (define @t377 () (=> @t294 @t376)) % 4.34/4.53 (define @t378 () (tptp.bst1 @t194)) % 4.34/4.53 (define @t379 () (@quantifiers_skolemize @t193 25)) % 4.34/4.53 (define @t380 () (@quantifiers_skolemize @t193 24)) % 4.34/4.53 (define @t381 () (@quantifiers_skolemize @t193 23)) % 4.34/4.53 (define @t382 () (@quantifiers_skolemize @t193 22)) % 4.34/4.53 (define @t383 () (tptp.node1 tptp.black1 @t382 @t381 @t380 @t379)) % 4.34/4.53 (define @t384 () (tptp.bst1 (tptp.node1 tptp.red1 @t383 @t200 @t199 @t198))) % 4.34/4.53 (define @t385 () (tptp.node1 tptp.red1 @t382 @t381 @t380 @t379)) % 4.34/4.53 (define @t386 () (= @t201 @t385)) % 4.34/4.53 (define @t387 () (not @t386)) % 4.34/4.53 (define @t388 () (= tptp.red1 @t202)) % 4.34/4.53 (define @t389 () (not @t388)) % 4.34/4.53 (define @t390 () (@quantifiers_skolemize @t193 12)) % 4.34/4.53 (define @t391 () (or (not (= tptp.black1 @t390)) @t389 @t387 @t384)) % 4.34/4.53 (define @t392 () (@quantifiers_skolemize @t193 16)) % 4.34/4.53 (define @t393 () (tptp.node1 tptp.black1 @t392 @t196 @t195 @t194)) % 4.34/4.53 (define @t394 () (@quantifiers_skolemize @t193 15)) % 4.34/4.53 (define @t395 () (@quantifiers_skolemize @t193 14)) % 4.34/4.53 (define @t396 () (@quantifiers_skolemize @t193 13)) % 4.34/4.53 (define @t397 () (tptp.node1 tptp.black1 @t201 @t200 @t199 @t396)) % 4.34/4.53 (define @t398 () (tptp.bst1 (tptp.node1 tptp.red1 @t397 @t395 @t394 @t393))) % 4.34/4.53 (define @t399 () (@quantifiers_skolemize @t193 17)) % 4.34/4.53 (define @t400 () (or (not (= tptp.black1 @t399)) @t389 @t398)) % 4.34/4.53 (define @t401 () (@quantifiers_skolemize @t193 21)) % 4.34/4.53 (define @t402 () (@quantifiers_skolemize @t193 20)) % 4.34/4.53 (define @t403 () (@quantifiers_skolemize @t193 19)) % 4.34/4.53 (define @t404 () (@quantifiers_skolemize @t193 18)) % 4.34/4.53 (define @t405 () (tptp.node1 tptp.black1 @t404 @t403 @t402 @t401)) % 4.34/4.53 (define @t406 () (tptp.bst1 (tptp.node1 tptp.red1 @t405 @t200 @t199 @t198))) % 4.34/4.53 (define @t407 () (or (not (= tptp.red1 @t399)) @t389 @t406)) % 4.34/4.53 (define @t408 () (and @t407 @t400)) % 4.34/4.53 (define @t409 () (tptp.node1 @t399 @t404 @t403 @t402 @t401)) % 4.34/4.53 (define @t410 () (= @t201 @t409)) % 4.34/4.53 (define @t411 () (not @t410)) % 4.34/4.53 (define @t412 () (or @t411 @t408)) % 4.34/4.53 (define @t413 () (or (not (= tptp.leaf1 @t201)) @t389 @t398)) % 4.34/4.53 (define @t414 () (and @t413 @t412)) % 4.34/4.53 (define @t415 () (or (not (= tptp.red1 @t390)) @t414)) % 4.34/4.53 (define @t416 () (and @t415 @t391)) % 4.34/4.53 (define @t417 () (tptp.node1 @t390 @t396 @t395 @t394 @t392)) % 4.34/4.53 (define @t418 () (= @t197 @t417)) % 4.34/4.53 (define @t419 () (not @t418)) % 4.34/4.53 (define @t420 () (or @t419 @t416)) % 4.34/4.53 (define @t421 () (@quantifiers_skolemize @t193 11)) % 4.34/4.53 (define @t422 () (@quantifiers_skolemize @t193 10)) % 4.34/4.53 (define @t423 () (@quantifiers_skolemize @t193 9)) % 4.34/4.53 (define @t424 () (@quantifiers_skolemize @t193 8)) % 4.34/4.53 (define @t425 () (tptp.bst1 (tptp.node1 tptp.red1 (tptp.node1 tptp.black1 @t424 @t423 @t422 @t421) @t200 @t199 @t198))) % 4.34/4.53 (define @t426 () (tptp.node1 tptp.red1 @t424 @t423 @t422 @t421)) % 4.34/4.53 (define @t427 () (= @t201 @t426)) % 4.34/4.53 (define @t428 () (not @t427)) % 4.34/4.53 (define @t429 () (or (not (= tptp.leaf1 @t197)) @t389 @t428 @t425)) % 4.34/4.53 (define @t430 () (and @t429 @t420)) % 4.34/4.53 (define @t431 () (not @t378)) % 4.34/4.53 (define @t432 () (tptp.bst1 @t203)) % 4.34/4.53 (define @t433 () (not @t432)) % 4.34/4.53 (define @t434 () (tptp.gt_tree1 @t196 @t194)) % 4.34/4.53 (define @t435 () (not @t434)) % 4.34/4.53 (define @t436 () (tptp.lt_tree1 @t196 @t203)) % 4.34/4.53 (define @t437 () (not @t436)) % 4.34/4.53 (define @t438 () (or @t437 @t435 @t433 @t431 @t430)) % 4.34/4.53 (define @t439 () (@list true)) % 4.34/4.53 (define @t440 () (@list @t438)) % 4.34/4.53 (define @t441 () (and @t432 @t378 @t436 @t434)) % 4.34/4.53 (define @t442 () (@list false false false false)) % 4.34/4.53 (define @t443 () (tptp.bst1 (tptp.node1 tptp.black1 @t203 @t196 @t195 @t194))) % 4.34/4.53 (define @t444 () (= @t443 @t441)) % 4.34/4.53 (define @t445 () (@list false false)) % 4.34/4.53 (define @t446 () (tptp.bst1 (tptp.node1 tptp.red1 @t201 @t200 @t199 @t198))) % 4.34/4.53 (define @t447 () (not @t443)) % 4.34/4.53 (define @t448 () (or @t447 @t446)) % 4.34/4.53 (define @t449 () (tptp.gt_tree1 @t200 @t198)) % 4.34/4.53 (define @t450 () (tptp.lt_tree1 @t200 @t201)) % 4.34/4.53 (define @t451 () (tptp.bst1 @t198)) % 4.34/4.53 (define @t452 () (tptp.bst1 @t201)) % 4.34/4.53 (define @t453 () (and @t452 @t451 @t450 @t449)) % 4.34/4.53 (define @t454 () (= @t446 @t453)) % 4.34/4.53 (define @t455 () (not @t446)) % 4.34/4.53 (define @t456 () (not @t453)) % 4.34/4.53 (define @t457 () (@list false)) % 4.34/4.53 (define @t458 () (@list @t453)) % 4.34/4.53 (define @t459 () (tptp.bst1 (tptp.node1 tptp.red1 @t424 @t423 @t422 (tptp.node1 @t202 @t421 @t200 @t199 @t198)))) % 4.34/4.53 (define @t460 () (not @t459)) % 4.34/4.53 (define @t461 () (or @t460 @t425)) % 4.34/4.53 (define @t462 () (tptp.node1 tptp.red1 @t426 @t200 @t199 @t198)) % 4.34/4.53 (define @t463 () (tptp.bst1 @t462)) % 4.34/4.53 (define @t464 () (not @t463)) % 4.34/4.53 (define @t465 () (or @t464 @t459)) % 4.34/4.53 (define @t466 () (and @t427 @t446)) % 4.34/4.53 (define @t467 () (not @t438)) % 4.34/4.53 (define @t468 () (not @t193)) % 4.34/4.53 (define @t469 () (not @t451)) % 4.34/4.53 (define @t470 () (tptp.bst1 (tptp.node1 tptp.black1 @t417 @t196 @t195 @t194))) % 4.34/4.53 (define @t471 () (not @t470)) % 4.34/4.53 (define @t472 () (and @t418 @t471)) % 4.34/4.53 (define @t473 () (forall @t87 (or (not @t83) @t86))) % 4.34/4.53 (define @t474 () (@list @t395 @t196 @t394 @t195 @t396 @t392 @t194 tptp.red1 tptp.black1 tptp.black1 @t390)) % 4.34/4.53 (define @t475 () (tptp.bst1 (tptp.node1 tptp.red1 @t396 @t395 @t394 @t393))) % 4.34/4.53 (define @t476 () (or @t471 @t475)) % 4.34/4.53 (define @t477 () (@list tptp.red1 @t396 @t395 @t394 @t393)) % 4.34/4.53 (define @t478 () (tptp.gt_tree1 @t395 @t393)) % 4.34/4.53 (define @t479 () (tptp.bst1 @t393)) % 4.34/4.53 (define @t480 () (tptp.bst1 @t396)) % 4.34/4.53 (define @t481 () (and @t480 @t479 (tptp.lt_tree1 @t395 @t396) @t478)) % 4.34/4.53 (define @t482 () (= @t475 @t481)) % 4.34/4.53 (define @t483 () (not @t481)) % 4.34/4.53 (define @t484 () (@list true false)) % 4.34/4.53 (define @t485 () (@list @t420)) % 4.34/4.53 (define @t486 () (tptp.node1 @t202 @t201 @t200 @t199 @t417)) % 4.34/4.53 (define @t487 () (tptp.bst1 @t486)) % 4.34/4.53 (define @t488 () (and @t432 @t418)) % 4.34/4.53 (define @t489 () (tptp.bst1 (tptp.node1 tptp.red1 @t397 @t395 @t394 @t392))) % 4.34/4.53 (define @t490 () (not @t487)) % 4.34/4.53 (define @t491 () (or @t490 @t489)) % 4.34/4.53 (define @t492 () (tptp.lt_tree1 @t395 @t397)) % 4.34/4.53 (define @t493 () (tptp.bst1 @t397)) % 4.34/4.53 (define @t494 () (and @t493 (tptp.bst1 @t392) @t492 (tptp.gt_tree1 @t395 @t392))) % 4.34/4.53 (define @t495 () (= @t489 @t494)) % 4.34/4.53 (define @t496 () (not @t494)) % 4.34/4.53 (define @t497 () (@list @t494)) % 4.34/4.53 (define @t498 () (and @t493 @t479 @t492 @t478)) % 4.34/4.53 (define @t499 () (@list tptp.red1 @t397 @t395 @t394 @t393)) % 4.34/4.53 (define @t500 () (= @t398 @t498)) % 4.34/4.53 (define @t501 () (tptp.gt_tree1 @t200 @t197)) % 4.34/4.53 (define @t502 () (tptp.bst1 @t197)) % 4.34/4.53 (define @t503 () (and @t452 @t502 @t450 @t501)) % 4.34/4.53 (define @t504 () (= @t432 @t503)) % 4.34/4.53 (define @t505 () (tptp.bst1 @t409)) % 4.34/4.53 (define @t506 () (and @t410 @t452)) % 4.34/4.53 (define @t507 () (tptp.bst1 @t405)) % 4.34/4.53 (define @t508 () (not @t505)) % 4.34/4.53 (define @t509 () (or @t508 @t507)) % 4.34/4.53 (define @t510 () (tptp.lt_tree1 @t200 @t405)) % 4.34/4.53 (define @t511 () (and @t507 @t451 @t510 @t449)) % 4.34/4.53 (define @t512 () (= @t406 @t511)) % 4.34/4.53 (define @t513 () (not @t449)) % 4.34/4.53 (define @t514 () (and @t507 @t480 @t510 (tptp.gt_tree1 @t200 @t396))) % 4.34/4.53 (define @t515 () (tptp.bst1 (tptp.node1 tptp.red1 @t405 @t200 @t199 @t396))) % 4.34/4.53 (define @t516 () (= @t515 @t514)) % 4.34/4.53 (define @t517 () (tptp.bst1 (tptp.node1 tptp.red1 @t404 @t403 @t402 (tptp.node1 tptp.black1 @t401 @t200 @t199 @t396)))) % 4.34/4.53 (define @t518 () (not @t517)) % 4.34/4.53 (define @t519 () (or @t518 @t515)) % 4.34/4.53 (define @t520 () (tptp.node1 tptp.black1 @t409 @t200 @t199 @t396)) % 4.34/4.53 (define @t521 () (tptp.bst1 @t520)) % 4.34/4.53 (define @t522 () (not @t521)) % 4.34/4.53 (define @t523 () (or @t522 @t517)) % 4.34/4.53 (define @t524 () (and @t410 @t493)) % 4.34/4.53 (define @t525 () (tptp.bst1 @t385)) % 4.34/4.53 (define @t526 () (and @t386 @t452)) % 4.34/4.53 (define @t527 () (tptp.node1 @t202 @t385 @t200 @t199 @t197)) % 4.34/4.53 (define @t528 () (tptp.bst1 @t527)) % 4.34/4.53 (define @t529 () (and @t432 @t386)) % 4.34/4.53 (define @t530 () (tptp.lt_tree1 @t200 @t383)) % 4.34/4.53 (define @t531 () (tptp.bst1 @t383)) % 4.34/4.53 (define @t532 () (and @t531 @t451 @t530 @t449)) % 4.34/4.53 (define @t533 () (= @t384 @t532)) % 4.34/4.53 (define @t534 () (not @t525)) % 4.34/4.53 (define @t535 () (or @t534 @t531)) % 4.34/4.53 (define @t536 () (tptp.bst1 (tptp.node1 tptp.red1 @t382 @t381 @t380 (tptp.node1 @t202 @t379 @t200 @t199 @t197)))) % 4.34/4.53 (define @t537 () (not @t528)) % 4.34/4.53 (define @t538 () (or @t537 @t536)) % 4.34/4.53 (define @t539 () (tptp.bst1 (tptp.node1 tptp.red1 @t383 @t200 @t199 @t197))) % 4.34/4.53 (define @t540 () (not @t536)) % 4.34/4.53 (define @t541 () (or @t540 @t539)) % 4.34/4.53 (define @t542 () (and @t531 @t502 @t530 @t501)) % 4.34/4.53 (define @t543 () (tptp.node1 @t202 @t383 @t200 @t199 @t197)) % 4.34/4.53 (define @t544 () (tptp.bst1 @t543)) % 4.34/4.53 (define @t545 () (= @t544 @t542)) % 4.34/4.53 (define @t546 () (and @t388 @t539)) % 4.34/4.53 (assume @p1 (forall (@list @t1) (tptp.sort1 @t1 (tptp.witness1 @t1)))) % 4.34/4.53 (assume @p2 (forall (@list @t1 @t4 @t3 @t2) (tptp.sort1 @t1 (tptp.match_bool1 @t1 @t4 @t3 @t2)))) % 4.34/4.53 (assume @p3 (forall @t8 (=> @t7 (= (tptp.match_bool1 @t1 tptp.true1 @t5 @t6) @t5)))) % 4.34/4.53 (assume @p4 (forall @t8 (=> @t9 (= (tptp.match_bool1 @t1 tptp.false1 @t5 @t6) @t6)))) % 4.34/4.53 (assume @p5 (not (= tptp.true1 tptp.false1))) % 4.34/4.53 (assume @p6 (forall (@list @t10) (or (= @t10 tptp.true1) (= @t10 tptp.false1)))) % 4.34/4.53 (assume @p7 (forall (@list @t11) (= @t11 tptp.tuple03))) % 4.34/4.53 (assume @p8 (forall (@list @t1 @t12 @t3 @t2) (tptp.sort1 @t1 (tptp.match_color1 @t1 @t12 @t3 @t2)))) % 4.34/4.53 (assume @p9 (forall @t8 (=> @t7 (= (tptp.match_color1 @t1 tptp.red1 @t5 @t6) @t5)))) % 4.34/4.53 (assume @p10 (forall @t8 (=> @t9 (= (tptp.match_color1 @t1 tptp.black1 @t5 @t6) @t6)))) % 4.34/4.53 (assume @p11 (not (= tptp.red1 tptp.black1))) % 4.34/4.53 (assume @p12 (forall (@list @t13) (or (= @t13 tptp.red1) (= @t13 tptp.black1)))) % 4.34/4.53 (assume @p13 (forall (@list @t1 @t14 @t3 @t2) (tptp.sort1 @t1 (tptp.match_tree1 @t1 @t14 @t3 @t2)))) % 4.34/4.53 (assume @p14 (forall @t8 (=> @t7 (= (tptp.match_tree1 @t1 tptp.leaf1 @t5 @t6) @t5)))) % 4.34/4.53 (assume @p15 (forall (@list @t1 @t5 @t6 @t13 @t18 @t17 @t16 @t15) (=> @t9 (= (tptp.match_tree1 @t1 @t19 @t5 @t6) @t6)))) % 4.34/4.53 (assume @p16 (forall (@list @t24 @t23 @t22 @t21 @t20) (not (= tptp.leaf1 (tptp.node1 @t24 @t23 @t22 @t21 @t20))))) % 4.34/4.53 (assume @p17 (forall @t25 (= (tptp.node_proj_11 @t19) @t13))) % 4.34/4.53 (assume @p18 (forall @t25 (= (tptp.node_proj_21 @t19) @t18))) % 4.34/4.53 (assume @p19 (forall @t25 (= (tptp.node_proj_31 @t19) @t17))) % 4.34/4.53 (assume @p20 (forall @t25 (= (tptp.node_proj_41 @t19) @t16))) % 4.34/4.53 (assume @p21 (forall @t25 (= (tptp.node_proj_51 @t19) @t15))) % 4.34/4.53 (assume @p22 (forall (@list @t26) (or (= @t26 tptp.leaf1) (= @t26 (tptp.node1 (tptp.node_proj_11 @t26) (tptp.node_proj_21 @t26) (tptp.node_proj_31 @t26) (tptp.node_proj_41 @t26) (tptp.node_proj_51 @t26)))))) % 4.34/4.53 (assume @p23 (forall @t35 (and (not (tptp.memt1 tptp.leaf1 @t28 @t27)) (forall @t34 (= (tptp.memt1 @t33 @t28 @t27) (or (and (= @t28 @t32) (= @t27 @t31)) (tptp.memt1 @t30 @t28 @t27) (tptp.memt1 @t29 @t28 @t27))))))) % 4.34/4.53 (assume @p24 (forall (@list @t39 @t38 @t28 @t37 @t27 @t36 @t42 @t40) (=> (tptp.memt1 @t43 @t37 @t36) (tptp.memt1 @t41 @t37 @t36)))) % 4.34/4.53 (assume @p25 (forall (@list @t46 @t45 @t44) (=> (<= @t46 @t45) (=> (<= 0 @t44) (<= (* @t46 @t44) (* @t45 @t44)))))) % 4.34/4.53 (assume @p26 (forall @t50 (= @t49 (forall @t35 (=> @t48 (< @t28 @t46)))))) % 4.34/4.53 (assume @p27 (forall @t50 (= @t51 (forall @t35 (=> @t48 (< @t46 @t28)))))) % 4.34/4.53 (assume @p28 (forall @t52 (tptp.lt_tree1 @t46 tptp.leaf1))) % 4.34/4.53 (assume @p29 (forall @t52 (tptp.gt_tree1 @t46 tptp.leaf1))) % 4.34/4.53 (assume @p30 (forall @t58 (=> @t57 (=> @t56 (=> @t55 @t54))))) % 4.34/4.53 (assume @p31 (forall @t58 (=> @t62 (=> @t61 (=> @t60 @t59))))) % 4.34/4.53 (assume @p32 (forall @t58 (=> @t54 @t55))) % 4.34/4.53 (assume @p33 (forall @t58 (=> @t59 @t60))) % 4.34/4.53 (assume @p34 (forall @t58 (=> @t54 @t57))) % 4.34/4.53 (assume @p35 (forall @t58 (=> @t54 @t56))) % 4.34/4.53 (assume @p36 (forall @t58 (=> @t59 @t62))) % 4.34/4.53 (assume @p37 (forall @t58 (=> @t59 @t61))) % 4.34/4.53 (assume @p38 (forall @t50 (=> @t49 @t63))) % 4.34/4.53 (assume @p39 (forall @t65 (=> @t60 (forall @t64 (=> @t49 (tptp.lt_tree1 @t45 @t47)))))) % 4.34/4.53 (assume @p40 (forall @t50 (=> @t51 @t63))) % 4.34/4.53 (assume @p41 (forall @t65 (=> @t55 (forall @t64 (=> @t51 (tptp.gt_tree1 @t45 @t47)))))) % 4.34/4.53 (assume @p42 (and @t67 @t66)) % 4.34/4.53 (assume @p43 @t67) % 4.34/4.53 (assume @p44 (forall @t70 (=> @t69 @t68))) % 4.34/4.53 (assume @p45 (forall @t70 (=> @t69 @t71))) % 4.34/4.53 (assume @p46 @t73) % 4.34/4.53 (assume @p47 @t88) % 4.34/4.53 (assume @p48 @t89) % 4.34/4.53 (assume @p49 (and (tptp.is_not_red1 tptp.leaf1) (forall @t34 (and (=> @t92 (not @t90)) (=> @t91 @t90))))) % 4.34/4.53 (assume @p50 (forall @t100 (and (= (tptp.rbtree1 @t93 tptp.leaf1) @t99) (forall @t34 (and (=> @t92 (= @t96 (and @t98 @t97 (tptp.is_not_red1 @t30) (tptp.is_not_red1 @t29)))) (=> @t91 (= @t96 @t95))))))) % 4.34/4.53 (assume @p51 (tptp.rbtree1 0 tptp.leaf1)) % 4.34/4.53 (assume @p52 (forall @t35 (tptp.rbtree1 0 (tptp.node1 tptp.red1 tptp.leaf1 @t28 @t27 tptp.leaf1)))) % 4.34/4.53 (assume @p53 (forall @t102 (=> @t101 (exists @t100 (tptp.rbtree1 @t93 @t39))))) % 4.34/4.53 (assume @p54 (forall @t102 (=> @t101 (exists @t100 (tptp.rbtree1 @t93 @t38))))) % 4.34/4.53 (assume @p55 (forall @t100 (and (= (tptp.almost_rbtree1 @t93 tptp.leaf1) @t99) (forall @t34 (and (=> @t92 (= @t103 (and @t98 @t97))) (=> @t91 (= @t103 @t95))))))) % 4.34/4.53 (assume @p56 (forall (@list @t93 @t47) (=> (tptp.rbtree1 @t93 @t47) (tptp.almost_rbtree1 @t93 @t47)))) % 4.34/4.53 (assume @p57 (forall (@list @t104) (=> (exists @t100 (tptp.rbtree1 @t93 @t104)) (exists @t100 (tptp.almost_rbtree1 @t93 @t104))))) % 4.34/4.53 (assume @p58 (forall (@list @t46 @t27 @t39 @t38 @t93) (=> (tptp.almost_rbtree1 @t93 @t105) (tptp.rbtree1 @t93 @t105)))) % 4.34/4.53 (assume @p59 @t158) % 4.34/4.53 (assume @p60 true) % 4.34/4.53 (step @p61 :rule and_elim :premises (@p42) :args (1)) % 4.34/4.53 (step @p62 :rule instantiate :premises (@p61) :args ((@list tptp.red1 @t201 @t200 @t199 @t198))) % 4.34/4.53 (step @p63 :rule bool-impl-elim :args (@t83 @t86)) % 4.34/4.53 (step @p64 :rule cong :premises (@p63) :args (@t89)) % 4.34/4.53 (step @p65 :rule eq_resolve :premises (@p48 @p64)) % 4.34/4.53 (step @p66 :rule instantiate :premises (@p65) :args ((@list @t200 @t196 @t199 @t195 @t201 @t197 @t194 tptp.red1 tptp.black1 tptp.black1 @t202))) % 4.34/4.53 (step @p67 :rule instantiate :premises (@p61) :args ((@list tptp.black1 @t203 @t196 @t195 @t194))) % 4.34/4.53 (step @p68 :rule aci_norm :args ((= (or @t190 @t189 @t188 @t186 false @t185) @t191))) % 4.34/4.53 (step @p69 :rule refl :args (@t185)) % 4.34/4.53 (step @p70 :rule evaluate :args ((not true))) % 4.34/4.53 (step @p71 :rule eq-refl :args (@t187)) % 4.34/4.53 (step @p72 :rule cong :premises (@p71) :args (@t204)) % 4.34/4.53 (step @p73 :rule trans :premises (@p72 @p70)) % 4.34/4.53 (step @p74 :rule refl :args (@t186)) % 4.34/4.53 (step @p75 :rule refl :args (@t188)) % 4.34/4.53 (step @p76 :rule refl :args (@t189)) % 4.34/4.53 (step @p77 :rule refl :args (@t190)) % 4.34/4.53 (step @p78 :rule nary_cong :premises (@p77 @p76 @p75 @p74 @p73 @p69) :args (@t205)) % 4.34/4.53 (step @p79 :rule trans :premises (@p78 @p68)) % 4.34/4.53 (step @p80 :rule cong :premises (@p79) :args ((forall @t192 @t205))) % 4.34/4.53 (step @p81 :rule quant-var-elim-eq :args ((= (forall @t210 @t209) @t205))) % 4.34/4.53 (step @p82 :rule aci_norm :args ((= @t211 @t209))) % 4.34/4.53 (step @p83 :rule cong :premises (@p82) :args (@t212)) % 4.34/4.53 (step @p84 :rule trans :premises (@p83 @p81)) % 4.34/4.53 (step @p85 :rule cong :premises (@p84) :args (@t213)) % 4.34/4.53 (step @p86 :rule quant-merge-prenex :args ((= @t213 @t214))) % 4.34/4.53 (step @p87 :rule symm :premises (@p86)) % 4.34/4.53 (step @p88 :rule quant_var_reordering :args ((= (forall @t215 @t211) @t214))) % 4.34/4.53 (step @p89 :rule trans :premises (@p88 @p87 @p85)) % 4.34/4.53 (step @p90 :rule trans :premises (@p89 @p80)) % 4.34/4.53 (step @p91 :rule eq-symm :args (@t187 @t39)) % 4.34/4.53 (step @p92 :rule cong :premises (@p91) :args (@t216)) % 4.34/4.53 (step @p93 :rule refl :args (@t207)) % 4.34/4.53 (step @p94 :rule refl :args (@t208)) % 4.34/4.53 (step @p95 :rule nary_cong :premises (@p94 @p76 @p93 @p74 @p92 @p69) :args (@t217)) % 4.34/4.53 (step @p96 :rule aci_norm :args ((= @t219 @t217))) % 4.34/4.53 (step @p97 :rule trans :premises (@p96 @p95)) % 4.34/4.53 (step @p98 :rule cong :premises (@p97) :args (@t220)) % 4.34/4.53 (step @p99 :rule trans :premises (@p98 @p90)) % 4.34/4.53 (step @p100 :rule quant-merge-prenex :args ((= (forall @t156 @t222) @t220))) % 4.34/4.53 (step @p101 :rule alpha_equiv :args (@t223 (@list @t168 @t167 @t162 @t161 @t159 @t184 @t183 @t182 @t181 @t170 @t174 @t173 @t172 @t171 @t176 @t180 @t179 @t178 @t177 @t166 @t165 @t164 @t163) (@list @t12 @t30 @t32 @t31 @t29 @t241 @t240 @t239 @t238 @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224))) % 4.34/4.53 (step @p102 :rule refl :args (@t186)) % 4.34/4.53 (step @p103 :rule refl :args (@t207)) % 4.34/4.53 (step @p104 :rule refl :args (@t189)) % 4.34/4.53 (step @p105 :rule refl :args (@t208)) % 4.34/4.53 (step @p106 :rule nary_cong :premises (@p105 @p104 @p103 @p102 @p101) :args (@t242)) % 4.34/4.53 (step @p107 :rule quant-miniscope-or :args ((= @t222 @t242))) % 4.34/4.53 (step @p108 :rule trans :premises (@p107 @p106)) % 4.34/4.53 (step @p109 :rule symm :premises (@p108)) % 4.34/4.53 (step @p110 :rule cong :premises (@p109) :args ((forall @t156 @t258))) % 4.34/4.53 (step @p111 :rule trans :premises (@p110 @p100)) % 4.34/4.53 (step @p112 :rule trans :premises (@p111 @p99)) % 4.34/4.53 (step @p113 :rule aci_norm :args ((= (or @t259 @t257) @t258))) % 4.34/4.53 (step @p114 :rule refl :args (@t257)) % 4.34/4.53 (step @p115 :rule aci_norm :args ((= (or @t208 (or @t189 (or @t207 @t186))) @t259))) % 4.34/4.53 (step @p116 :rule bool-and-de-morgan :args (@t68 @t71 true)) % 4.34/4.53 (step @p117 :rule nary_cong :premises (@p104 @p116) :args ((or @t189 (not (and @t68 @t71))))) % 4.34/4.53 (step @p118 :rule bool-and-de-morgan :args (@t152 @t68 (and @t71))) % 4.34/4.53 (step @p119 :rule trans :premises (@p118 @p117)) % 4.34/4.53 (step @p120 :rule nary_cong :premises (@p105 @p119) :args ((or @t208 (not (and @t152 @t68 @t71))))) % 4.34/4.53 (step @p121 :rule bool-and-de-morgan :args (@t153 @t152 (and @t68 @t71))) % 4.34/4.53 (step @p122 :rule trans :premises (@p121 @p120)) % 4.34/4.53 (step @p123 :rule trans :premises (@p122 @p115)) % 4.34/4.53 (step @p124 :rule nary_cong :premises (@p123 @p114) :args ((or (not @t154) @t257))) % 4.34/4.53 (step @p125 :rule trans :premises (@p124 @p113)) % 4.34/4.53 (step @p126 :rule bool-impl-elim :args (@t154 @t257)) % 4.34/4.53 (step @p127 :rule trans :premises (@p126 @p125)) % 4.34/4.53 (step @p128 :rule cong :premises (@p127) :args ((forall @t156 (=> @t154 @t257)))) % 4.34/4.53 (step @p129 :rule trans :premises (@p128 @p112)) % 4.34/4.53 (step @p130 :rule refl :args (@t248)) % 4.34/4.53 (step @p131 :rule aci_norm :args ((= @t261 @t253))) % 4.34/4.53 (step @p132 :rule nary_cong :premises (@p131 @p130) :args (@t262)) % 4.34/4.53 (step @p133 :rule refl :args (@t255)) % 4.34/4.53 (step @p134 :rule nary_cong :premises (@p133 @p132) :args (@t263)) % 4.34/4.53 (step @p135 :rule cong :premises (@p134) :args (@t264)) % 4.34/4.53 (step @p136 :rule quant-merge-prenex :args ((= (forall @t34 @t266) @t264))) % 4.34/4.53 (step @p137 :rule alpha_equiv :args (@t267 (@list @t237 @t236 @t235 @t234 @t233 @t232 @t231 @t230 @t229 @t228 @t227 @t226 @t225 @t224) (@list @t120 @t125 @t124 @t123 @t122 @t276 @t275 @t274 @t273 @t272 @t271 @t270 @t269 @t268))) % 4.34/4.53 (step @p138 :rule quant-unused-vars :args ((= @t277 @t267))) % 4.34/4.53 (step @p139 :rule trans :premises (@p138 @p137)) % 4.34/4.53 (step @p140 :rule alpha_equiv :args (@t279 (@list @t241 @t240 @t239 @t238) (@list @t125 @t124 @t123 @t122))) % 4.34/4.53 (step @p141 :rule refl :args (@t244)) % 4.34/4.53 (step @p142 :rule refl :args (@t252)) % 4.34/4.53 (step @p143 :rule nary_cong :premises (@p142 @p141 @p140) :args (@t280)) % 4.34/4.53 (step @p144 :rule quant-miniscope-or :args ((= @t281 @t280))) % 4.34/4.53 (step @p145 :rule quant-unused-vars :args ((= @t282 @t281))) % 4.34/4.53 (step @p146 :rule trans :premises (@p145 @p144)) % 4.34/4.53 (step @p147 :rule trans :premises (@p146 @p143)) % 4.34/4.53 (step @p148 :rule nary_cong :premises (@p147 @p139) :args (@t283)) % 4.34/4.53 (step @p149 :rule quant-miniscope-and :args ((= @t284 @t283))) % 4.34/4.53 (step @p150 :rule trans :premises (@p149 @p148)) % 4.34/4.53 (step @p151 :rule refl :args (@t255)) % 4.34/4.53 (step @p152 :rule nary_cong :premises (@p151 @p150) :args (@t285)) % 4.34/4.53 (step @p153 :rule quant-miniscope-or :args ((= @t266 @t285))) % 4.34/4.53 (step @p154 :rule trans :premises (@p153 @p152)) % 4.34/4.53 (step @p155 :rule symm :premises (@p154)) % 4.34/4.53 (step @p156 :rule cong :premises (@p155) :args ((forall @t34 (or @t255 (and @t304 @t299))))) % 4.34/4.53 (step @p157 :rule trans :premises (@p156 @p136)) % 4.34/4.53 (step @p158 :rule trans :premises (@p157 @p135)) % 4.34/4.53 (step @p159 :rule refl :args (@t299)) % 4.34/4.53 (step @p160 :rule aci_norm :args ((= (or @t252 @t305) @t304))) % 4.34/4.53 (step @p161 :rule bool-impl-elim :args (@t251 @t305)) % 4.34/4.53 (step @p162 :rule trans :premises (@p161 @p160)) % 4.34/4.53 (step @p163 :rule nary_cong :premises (@p162 @p159) :args (@t306)) % 4.34/4.53 (step @p164 :rule nary_cong :premises (@p151 @p163) :args ((or @t255 @t306))) % 4.34/4.53 (step @p165 :rule bool-impl-elim :args (@t254 @t306)) % 4.34/4.53 (step @p166 :rule trans :premises (@p165 @p164)) % 4.34/4.53 (step @p167 :rule cong :premises (@p166) :args ((forall @t34 (=> @t254 @t306)))) % 4.34/4.53 (step @p168 :rule trans :premises (@p167 @p158)) % 4.34/4.53 (step @p169 :rule aci_norm :args ((= @t308 @t290))) % 4.34/4.53 (step @p170 :rule refl :args (@t296)) % 4.34/4.53 (step @p171 :rule nary_cong :premises (@p170 @p169) :args (@t309)) % 4.34/4.53 (step @p172 :rule refl :args (@t297)) % 4.34/4.53 (step @p173 :rule nary_cong :premises (@p172 @p171) :args (@t310)) % 4.34/4.53 (step @p174 :rule cong :premises (@p173) :args (@t311)) % 4.34/4.53 (step @p175 :rule quant-merge-prenex :args ((= (forall @t140 @t313) @t311))) % 4.34/4.53 (step @p176 :rule alpha_equiv :args (@t315 (@list @t271 @t270 @t269 @t268) (@list @t110 @t109 @t108 @t107))) % 4.34/4.53 (step @p177 :rule refl :args (@t289)) % 4.34/4.53 (step @p178 :rule nary_cong :premises (@p177 @p141 @p176) :args (@t316)) % 4.34/4.53 (step @p179 :rule quant-miniscope-or :args ((= @t317 @t316))) % 4.34/4.53 (step @p180 :rule quant-unused-vars :args ((= @t318 @t317))) % 4.34/4.53 (step @p181 :rule trans :premises (@p180 @p179)) % 4.34/4.53 (step @p182 :rule trans :premises (@p181 @p178)) % 4.34/4.53 (step @p183 :rule alpha_equiv :args (@t320 (@list @t276 @t275 @t274 @t273 @t272) (@list @t113 @t110 @t109 @t108 @t107))) % 4.34/4.53 (step @p184 :rule quant-unused-vars :args ((= @t321 @t292))) % 4.34/4.53 (step @p185 :rule nary_cong :premises (@p184 @p183) :args (@t322)) % 4.34/4.53 (step @p186 :rule quant-miniscope-and :args ((= @t323 @t322))) % 4.34/4.53 (step @p187 :rule trans :premises (@p186 @p185)) % 4.34/4.53 (step @p188 :rule refl :args (@t295)) % 4.34/4.53 (step @p189 :rule nary_cong :premises (@p188 @p187) :args (@t324)) % 4.34/4.53 (step @p190 :rule quant-miniscope-or :args ((= @t325 @t324))) % 4.34/4.54 (step @p191 :rule quant-unused-vars :args ((= @t326 @t325))) % 4.34/4.54 (step @p192 :rule trans :premises (@p191 @p190)) % 4.34/4.54 (step @p193 :rule trans :premises (@p192 @p189)) % 4.34/4.54 (step @p194 :rule nary_cong :premises (@p193 @p182) :args (@t327)) % 4.34/4.54 (step @p195 :rule quant-miniscope-and :args ((= @t328 @t327))) % 4.34/4.54 (step @p196 :rule trans :premises (@p195 @p194)) % 4.34/4.54 (step @p197 :rule refl :args (@t297)) % 4.34/4.54 (step @p198 :rule nary_cong :premises (@p197 @p196) :args (@t329)) % 4.34/4.54 (step @p199 :rule quant-miniscope-or :args ((= @t313 @t329))) % 4.34/4.54 (step @p200 :rule trans :premises (@p199 @p198)) % 4.34/4.54 (step @p201 :rule symm :premises (@p200)) % 4.34/4.54 (step @p202 :rule cong :premises (@p201) :args ((forall @t140 (or @t297 (and (or @t295 (and @t292 @t342)) @t334))))) % 4.34/4.54 (step @p203 :rule trans :premises (@p202 @p175)) % 4.34/4.54 (step @p204 :rule trans :premises (@p203 @p174)) % 4.34/4.54 (step @p205 :rule aci_norm :args ((= (or @t289 @t343) @t334))) % 4.34/4.54 (step @p206 :rule bool-impl-elim :args (@t288 @t343)) % 4.34/4.54 (step @p207 :rule trans :premises (@p206 @p205)) % 4.34/4.54 (step @p208 :rule refl :args (@t342)) % 4.34/4.54 (step @p209 :rule aci_norm :args ((= (or @t247 @t344) @t292))) % 4.34/4.54 (step @p210 :rule bool-impl-elim :args (@t243 @t126)) % 4.34/4.54 (step @p211 :rule refl :args (@t247)) % 4.34/4.54 (step @p212 :rule nary_cong :premises (@p211 @p210) :args ((or @t247 @t345))) % 4.34/4.54 (step @p213 :rule trans :premises (@p212 @p209)) % 4.34/4.54 (step @p214 :rule bool-impl-elim :args (@t246 @t345)) % 4.34/4.54 (step @p215 :rule trans :premises (@p214 @p213)) % 4.34/4.54 (step @p216 :rule nary_cong :premises (@p215 @p208) :args (@t346)) % 4.34/4.54 (step @p217 :rule nary_cong :premises (@p188 @p216) :args ((or @t295 @t346))) % 4.34/4.54 (step @p218 :rule bool-impl-elim :args (@t294 @t346)) % 4.34/4.54 (step @p219 :rule trans :premises (@p218 @p217)) % 4.34/4.54 (step @p220 :rule nary_cong :premises (@p219 @p207) :args (@t347)) % 4.34/4.54 (step @p221 :rule nary_cong :premises (@p197 @p220) :args ((or @t297 @t347))) % 4.34/4.54 (step @p222 :rule bool-impl-elim :args (@t138 @t347)) % 4.34/4.54 (step @p223 :rule trans :premises (@p222 @p221)) % 4.34/4.54 (step @p224 :rule cong :premises (@p223) :args ((forall @t140 (=> @t138 @t347)))) % 4.34/4.54 (step @p225 :rule trans :premises (@p224 @p204)) % 4.34/4.54 (step @p226 :rule aci_norm :args ((= (or @t330 false @t111) @t331))) % 4.34/4.54 (step @p227 :rule refl :args (@t111)) % 4.34/4.54 (step @p228 :rule eq-refl :args (tptp.red1)) % 4.34/4.54 (step @p229 :rule cong :premises (@p228) :args (@t348)) % 4.34/4.54 (step @p230 :rule trans :premises (@p229 @p70)) % 4.34/4.54 (step @p231 :rule refl :args (@t330)) % 4.34/4.54 (step @p232 :rule nary_cong :premises (@p231 @p230 @p227) :args (@t349)) % 4.34/4.54 (step @p233 :rule trans :premises (@p232 @p226)) % 4.34/4.54 (step @p234 :rule cong :premises (@p233) :args ((forall @t332 @t349))) % 4.34/4.54 (step @p235 :rule quant-var-elim-eq :args ((= (forall @t350 (or (not @t114) @t341 @t339 @t111)) @t349))) % 4.34/4.54 (step @p236 :rule refl :args (@t111)) % 4.34/4.54 (step @p237 :rule refl :args (@t339)) % 4.34/4.54 (step @p238 :rule refl :args (@t341)) % 4.34/4.54 (step @p239 :rule eq-symm :args (tptp.red1 @t113)) % 4.34/4.54 (step @p240 :rule cong :premises (@p239) :args (@t339)) % 4.34/4.54 (step @p241 :rule nary_cong :premises (@p240 @p238 @p237 @p236) :args (@t351)) % 4.34/4.54 (step @p242 :rule aci_norm :args ((= @t352 @t351))) % 4.34/4.54 (step @p243 :rule trans :premises (@p242 @p241)) % 4.34/4.54 (step @p244 :rule cong :premises (@p243) :args (@t353)) % 4.34/4.54 (step @p245 :rule trans :premises (@p244 @p235)) % 4.34/4.54 (step @p246 :rule cong :premises (@p245) :args (@t354)) % 4.34/4.54 (step @p247 :rule quant-merge-prenex :args ((= @t354 @t355))) % 4.34/4.54 (step @p248 :rule symm :premises (@p247)) % 4.34/4.54 (step @p249 :rule quant_var_reordering :args ((= @t356 @t355))) % 4.34/4.54 (step @p250 :rule trans :premises (@p249 @p248 @p246)) % 4.34/4.54 (step @p251 :rule trans :premises (@p250 @p234)) % 4.34/4.54 (step @p252 :rule refl :args (@t244)) % 4.34/4.54 (step @p253 :rule nary_cong :premises (@p252 @p251) :args (@t357)) % 4.34/4.54 (step @p254 :rule quant-miniscope-or :args ((= (forall @t118 @t358) @t357))) % 4.34/4.54 (step @p255 :rule aci_norm :args ((= @t359 @t358))) % 4.34/4.54 (step @p256 :rule cong :premises (@p255) :args ((forall @t118 @t359))) % 4.34/4.54 (step @p257 :rule trans :premises (@p256 @p254)) % 4.34/4.54 (step @p258 :rule trans :premises (@p257 @p253)) % 4.34/4.54 (step @p259 :rule aci_norm :args ((= (or @t341 @t340) @t359))) % 4.34/4.54 (step @p260 :rule aci_norm :args ((= (or @t339 (or @t244 @t111)) @t340))) % 4.34/4.54 (step @p261 :rule bool-impl-elim :args (@t243 @t111)) % 4.34/4.54 (step @p262 :rule nary_cong :premises (@p237 @p261) :args ((or @t339 @t360))) % 4.34/4.54 (step @p263 :rule trans :premises (@p262 @p260)) % 4.34/4.54 (step @p264 :rule bool-impl-elim :args (@t338 @t360)) % 4.34/4.54 (step @p265 :rule trans :premises (@p264 @p263)) % 4.34/4.54 (step @p266 :rule nary_cong :premises (@p238 @p265) :args ((or @t341 @t361))) % 4.34/4.54 (step @p267 :rule trans :premises (@p266 @p259)) % 4.34/4.54 (step @p268 :rule bool-impl-elim :args (@t116 @t361)) % 4.34/4.54 (step @p269 :rule trans :premises (@p268 @p267)) % 4.34/4.54 (step @p270 :rule cong :premises (@p269) :args ((forall @t118 (=> @t116 @t361)))) % 4.34/4.54 (step @p271 :rule trans :premises (@p270 @p258)) % 4.34/4.54 (step @p272 :rule eq-symm :args (@t12 tptp.red1)) % 4.34/4.54 (step @p273 :rule cong :premises (@p272 @p227) :args (@t112)) % 4.34/4.54 (step @p274 :rule eq-symm :args (@t113 tptp.red1)) % 4.34/4.54 (step @p275 :rule cong :premises (@p274 @p273) :args (@t115)) % 4.34/4.54 (step @p276 :rule refl :args (@t116)) % 4.34/4.54 (step @p277 :rule cong :premises (@p276 @p275) :args (@t117)) % 4.34/4.54 (step @p278 :rule cong :premises (@p277) :args (@t119)) % 4.34/4.54 (step @p279 :rule trans :premises (@p278 @p271)) % 4.34/4.54 (step @p280 :rule eq-symm :args (@t120 tptp.black1)) % 4.34/4.54 (step @p281 :rule cong :premises (@p280 @p279) :args (@t121)) % 4.34/4.54 (step @p282 :rule aci_norm :args ((= (or @t336 @t344) @t337))) % 4.34/4.54 (step @p283 :rule refl :args (@t336)) % 4.34/4.54 (step @p284 :rule nary_cong :premises (@p283 @p210) :args ((or @t336 @t345))) % 4.34/4.54 (step @p285 :rule trans :premises (@p284 @p282)) % 4.34/4.54 (step @p286 :rule bool-impl-elim :args (@t335 @t345)) % 4.34/4.54 (step @p287 :rule trans :premises (@p286 @p285)) % 4.34/4.54 (step @p288 :rule nary_cong :premises (@p265 @p287) :args (@t362)) % 4.34/4.54 (step @p289 :rule nary_cong :premises (@p238 @p288) :args ((or @t341 @t362))) % 4.34/4.54 (step @p290 :rule bool-impl-elim :args (@t116 @t362)) % 4.34/4.54 (step @p291 :rule trans :premises (@p290 @p289)) % 4.34/4.54 (step @p292 :rule cong :premises (@p291) :args ((forall @t118 (=> @t116 @t362)))) % 4.34/4.54 (step @p293 :rule refl :args (@t126)) % 4.34/4.54 (step @p294 :rule cong :premises (@p272 @p293) :args (@t127)) % 4.34/4.54 (step @p295 :rule eq-symm :args (@t113 tptp.black1)) % 4.34/4.54 (step @p296 :rule cong :premises (@p295 @p294) :args (@t128)) % 4.34/4.54 (step @p297 :rule nary_cong :premises (@p275 @p296) :args (@t129)) % 4.34/4.54 (step @p298 :rule cong :premises (@p276 @p297) :args (@t130)) % 4.34/4.54 (step @p299 :rule cong :premises (@p298) :args (@t131)) % 4.34/4.54 (step @p300 :rule trans :premises (@p299 @p292)) % 4.34/4.54 (step @p301 :rule eq-symm :args (@t30 tptp.leaf1)) % 4.34/4.54 (step @p302 :rule cong :premises (@p301 @p294) :args (@t132)) % 4.34/4.54 (step @p303 :rule nary_cong :premises (@p302 @p300) :args (@t133)) % 4.34/4.54 (step @p304 :rule eq-symm :args (@t120 tptp.red1)) % 4.34/4.54 (step @p305 :rule cong :premises (@p304 @p303) :args (@t135)) % 4.34/4.54 (step @p306 :rule nary_cong :premises (@p305 @p281) :args (@t136)) % 4.34/4.54 (step @p307 :rule refl :args (@t138)) % 4.34/4.54 (step @p308 :rule cong :premises (@p307 @p306) :args (@t139)) % 4.34/4.54 (step @p309 :rule cong :premises (@p308) :args (@t141)) % 4.34/4.54 (step @p310 :rule trans :premises (@p309 @p225)) % 4.34/4.54 (step @p311 :rule aci_norm :args ((= (or @t300 false @t142) @t301))) % 4.34/4.54 (step @p312 :rule refl :args (@t142)) % 4.34/4.54 (step @p313 :rule refl :args (@t300)) % 4.34/4.54 (step @p314 :rule nary_cong :premises (@p313 @p230 @p312) :args (@t363)) % 4.34/4.54 (step @p315 :rule trans :premises (@p314 @p311)) % 4.34/4.54 (step @p316 :rule cong :premises (@p315) :args ((forall @t302 @t363))) % 4.34/4.54 (step @p317 :rule quant-var-elim-eq :args ((= (forall @t365 (or (not @t134) @t364 @t295 @t142)) @t363))) % 4.34/4.54 (step @p318 :rule refl :args (@t142)) % 4.34/4.54 (step @p319 :rule refl :args (@t364)) % 4.34/4.54 (step @p320 :rule eq-symm :args (tptp.red1 @t120)) % 4.34/4.54 (step @p321 :rule cong :premises (@p320) :args (@t295)) % 4.34/4.54 (step @p322 :rule nary_cong :premises (@p321 @p319 @p188 @p318) :args (@t366)) % 4.34/4.54 (step @p323 :rule aci_norm :args ((= @t367 @t366))) % 4.34/4.54 (step @p324 :rule trans :premises (@p323 @p322)) % 4.34/4.54 (step @p325 :rule cong :premises (@p324) :args (@t368)) % 4.34/4.54 (step @p326 :rule trans :premises (@p325 @p317)) % 4.34/4.54 (step @p327 :rule cong :premises (@p326) :args (@t369)) % 4.34/4.54 (step @p328 :rule quant-merge-prenex :args ((= @t369 @t370))) % 4.34/4.54 (step @p329 :rule symm :premises (@p328)) % 4.34/4.54 (step @p330 :rule quant_var_reordering :args ((= @t371 @t370))) % 4.34/4.54 (step @p331 :rule trans :premises (@p330 @p329 @p327)) % 4.34/4.54 (step @p332 :rule trans :premises (@p331 @p316)) % 4.34/4.54 (step @p333 :rule nary_cong :premises (@p252 @p332) :args (@t372)) % 4.34/4.54 (step @p334 :rule quant-miniscope-or :args ((= (forall @t140 @t373) @t372))) % 4.34/4.54 (step @p335 :rule aci_norm :args ((= @t374 @t373))) % 4.34/4.54 (step @p336 :rule cong :premises (@p335) :args ((forall @t140 @t374))) % 4.34/4.54 (step @p337 :rule trans :premises (@p336 @p334)) % 4.34/4.54 (step @p338 :rule trans :premises (@p337 @p333)) % 4.34/4.54 (step @p339 :rule aci_norm :args ((= (or @t364 @t375) @t374))) % 4.34/4.54 (step @p340 :rule aci_norm :args ((= (or @t295 (or @t244 @t142)) @t375))) % 4.34/4.54 (step @p341 :rule bool-impl-elim :args (@t243 @t142)) % 4.34/4.54 (step @p342 :rule nary_cong :premises (@p188 @p341) :args ((or @t295 @t376))) % 4.34/4.54 (step @p343 :rule trans :premises (@p342 @p340)) % 4.34/4.54 (step @p344 :rule bool-impl-elim :args (@t294 @t376)) % 4.34/4.54 (step @p345 :rule trans :premises (@p344 @p343)) % 4.34/4.54 (step @p346 :rule nary_cong :premises (@p319 @p345) :args ((or @t364 @t377))) % 4.34/4.54 (step @p347 :rule trans :premises (@p346 @p339)) % 4.34/4.54 (step @p348 :rule bool-impl-elim :args (@t145 @t377)) % 4.34/4.54 (step @p349 :rule trans :premises (@p348 @p347)) % 4.34/4.54 (step @p350 :rule cong :premises (@p349) :args ((forall @t140 (=> @t145 @t377)))) % 4.34/4.54 (step @p351 :rule trans :premises (@p350 @p338)) % 4.34/4.54 (step @p352 :rule cong :premises (@p272 @p312) :args (@t143)) % 4.34/4.54 (step @p353 :rule cong :premises (@p304 @p352) :args (@t144)) % 4.34/4.54 (step @p354 :rule refl :args (@t145)) % 4.34/4.54 (step @p355 :rule cong :premises (@p354 @p353) :args (@t146)) % 4.34/4.54 (step @p356 :rule cong :premises (@p355) :args (@t147)) % 4.34/4.54 (step @p357 :rule trans :premises (@p356 @p351)) % 4.34/4.54 (step @p358 :rule eq-symm :args (@t29 tptp.leaf1)) % 4.34/4.54 (step @p359 :rule cong :premises (@p358 @p357) :args (@t148)) % 4.34/4.54 (step @p360 :rule nary_cong :premises (@p359 @p310) :args (@t149)) % 4.34/4.54 (step @p361 :rule eq-symm :args (@t39 @t33)) % 4.34/4.54 (step @p362 :rule cong :premises (@p361 @p360) :args (@t150)) % 4.34/4.54 (step @p363 :rule cong :premises (@p362) :args (@t151)) % 4.34/4.54 (step @p364 :rule trans :premises (@p363 @p168)) % 4.34/4.54 (step @p365 :rule refl :args (@t154)) % 4.34/4.54 (step @p366 :rule cong :premises (@p365 @p364) :args (@t155)) % 4.34/4.54 (step @p367 :rule cong :premises (@p366) :args (@t157)) % 4.34/4.54 (step @p368 :rule trans :premises (@p367 @p129)) % 4.34/4.54 (step @p369 :rule cong :premises (@p368) :args (@t158)) % 4.34/4.54 (step @p370 :rule eq_resolve :premises (@p59 @p369)) % 4.34/4.54 (step @p371 :rule skolemize :premises (@p370)) % 4.34/4.54 (step @p372 :rule bool-double-not-elim :args (@t378)) % 4.34/4.54 (step @p373 :rule refl :args (@t438)) % 4.34/4.54 (step @p374 :rule nary_cong :premises (@p373 @p372) :args ((or @t438 (not @t431)))) % 4.34/4.54 (step @p375 :rule cnf_or_neg :args (@t438 3)) % 4.34/4.54 (step @p376 :rule eq_resolve :premises (@p375 @p374)) % 4.34/4.54 (step @p377 :rule reordering :premises (@p376) :args ((or @t378 @t438))) % 4.34/4.54 (step @p378 :rule chain_m_resolution :premises (@p377 @p371) :args (@t378 @t439 @t440)) % 4.34/4.54 (step @p379 :rule bool-double-not-elim :args (@t432)) % 4.34/4.54 (step @p380 :rule nary_cong :premises (@p373 @p379) :args ((or @t438 (not @t433)))) % 4.34/4.54 (step @p381 :rule cnf_or_neg :args (@t438 2)) % 4.34/4.54 (step @p382 :rule eq_resolve :premises (@p381 @p380)) % 4.34/4.54 (step @p383 :rule reordering :premises (@p382) :args ((or @t432 @t438))) % 4.34/4.54 (step @p384 :rule chain_m_resolution :premises (@p383 @p371) :args (@t432 @t439 @t440)) % 4.34/4.54 (step @p385 :rule bool-double-not-elim :args (@t434)) % 4.34/4.54 (step @p386 :rule nary_cong :premises (@p373 @p385) :args ((or @t438 (not @t435)))) % 4.34/4.54 (step @p387 :rule cnf_or_neg :args (@t438 1)) % 4.34/4.54 (step @p388 :rule eq_resolve :premises (@p387 @p386)) % 4.34/4.54 (step @p389 :rule reordering :premises (@p388) :args ((or @t434 @t438))) % 4.34/4.54 (step @p390 :rule chain_m_resolution :premises (@p389 @p371) :args (@t434 @t439 @t440)) % 4.34/4.54 (step @p391 :rule bool-double-not-elim :args (@t436)) % 4.34/4.54 (step @p392 :rule nary_cong :premises (@p373 @p391) :args ((or @t438 (not @t437)))) % 4.34/4.54 (step @p393 :rule cnf_or_neg :args (@t438 0)) % 4.34/4.54 (step @p394 :rule eq_resolve :premises (@p393 @p392)) % 4.34/4.54 (step @p395 :rule reordering :premises (@p394) :args ((or @t436 @t438))) % 4.34/4.54 (step @p396 :rule chain_m_resolution :premises (@p395 @p371) :args (@t436 @t439 @t440)) % 4.34/4.54 (step @p397 :rule cnf_and_neg :args (@t441)) % 4.34/4.54 (step @p398 :rule reordering :premises (@p397) :args ((or @t437 @t435 @t433 @t431 @t441))) % 4.34/4.54 (step @p399 :rule chain_m_resolution :premises (@p398 @p396 @p390 @p384 @p378) :args (@t441 @t442 (@list @t436 @t434 @t432 @t378))) % 4.34/4.54 (step @p400 :rule cnf_equiv_pos2 :args (@t444)) % 4.34/4.54 (step @p401 :rule reordering :premises (@p400) :args ((or @t443 (not @t441) (not @t444)))) % 4.34/4.54 (step @p402 :rule chain_m_resolution :premises (@p401 @p399 @p67) :args (@t443 @t445 (@list @t441 @t444))) % 4.34/4.54 (step @p403 :rule cnf_or_pos :args (@t448)) % 4.34/4.54 (step @p404 :rule reordering :premises (@p403) :args ((or @t447 @t446 (not @t448)))) % 4.34/4.54 (step @p405 :rule chain_m_resolution :premises (@p404 @p402 @p66) :args (@t446 @t445 (@list @t443 @t448))) % 4.34/4.54 (step @p406 :rule cnf_equiv_pos1 :args (@t454)) % 4.34/4.54 (step @p407 :rule reordering :premises (@p406) :args ((or @t455 @t453 (not @t454)))) % 4.34/4.54 (step @p408 :rule chain_m_resolution :premises (@p407 @p405 @p62) :args (@t453 @t445 (@list @t446 @t454))) % 4.34/4.54 (step @p409 :rule cnf_and_pos :args (@t453 3)) % 4.34/4.54 (step @p410 :rule reordering :premises (@p409) :args ((or @t449 @t456))) % 4.34/4.54 (step @p411 :rule chain_m_resolution :premises (@p410 @p408) :args (@t449 @t457 @t458)) % 4.34/4.54 (step @p412 :rule cnf_and_pos :args (@t453 1)) % 4.34/4.54 (step @p413 :rule reordering :premises (@p412) :args ((or @t451 @t456))) % 4.34/4.54 (step @p414 :rule chain_m_resolution :premises (@p413 @p408) :args (@t451 @t457 @t458)) % 4.34/4.54 (step @p415 :rule bool-double-not-elim :args (@t427)) % 4.34/4.54 (step @p416 :rule refl :args (@t429)) % 4.34/4.54 (step @p417 :rule nary_cong :premises (@p416 @p415) :args ((or @t429 (not @t428)))) % 4.34/4.54 (step @p418 :rule cnf_or_neg :args (@t429 2)) % 4.34/4.54 (step @p419 :rule eq_resolve :premises (@p418 @p417)) % 4.34/4.54 (step @p420 :rule reordering :premises (@p419) :args ((or @t427 @t429))) % 4.34/4.54 (step @p421 :rule cnf_or_neg :args (@t429 3)) % 4.34/4.54 (step @p422 :rule bool-impl-elim :args (@t86 @t83)) % 4.34/4.54 (step @p423 :rule cong :premises (@p422) :args (@t88)) % 4.34/4.54 (step @p424 :rule eq_resolve :premises (@p47 @p423)) % 4.34/4.54 (step @p425 :rule instantiate :premises (@p424) :args ((@list @t423 @t200 @t422 @t199 @t424 @t421 @t198 tptp.red1 @t202 tptp.red1 tptp.black1))) % 4.34/4.54 (step @p426 :rule cnf_or_pos :args (@t461)) % 4.34/4.54 (step @p427 :rule reordering :premises (@p426) :args ((or @t425 @t460 (not @t461)))) % 4.34/4.54 (step @p428 :rule instantiate :premises (@p65) :args ((@list @t423 @t200 @t422 @t199 @t424 @t421 @t198 tptp.red1 @t202 tptp.red1 tptp.red1))) % 4.34/4.54 (step @p429 :rule cnf_or_pos :args (@t465)) % 4.34/4.54 (step @p430 :rule reordering :premises (@p429) :args ((or @t464 @t459 (not @t465)))) % 4.34/4.54 (assume-push @p767 @t427) % 4.34/4.54 (assume-push @p768 @t446) % 4.34/4.54 (assume-push @p769 @t446) % 4.34/4.54 (assume-push @p770 @t427) % 4.34/4.54 (step @p435 :rule true_intro :premises (@p405)) % 4.34/4.54 (step @p436 :rule refl :args (@t198)) % 4.34/4.54 (step @p437 :rule refl :args (@t199)) % 4.34/4.54 (step @p438 :rule refl :args (@t200)) % 4.34/4.54 (step @p439 :rule symm :premises (@p767)) % 4.34/4.54 (step @p440 :rule refl :args (tptp.red1)) % 4.34/4.54 (step @p441 :rule cong :premises (@p440 @p439 @p438 @p437 @p436) :args (@t462)) % 4.34/4.54 (step @p442 :rule cong :premises (@p441) :args (@t463)) % 4.34/4.54 (step @p443 :rule trans :premises (@p442 @p435)) % 4.34/4.54 (step @p444 :rule true_elim :premises (@p443)) % 4.34/4.54 (step-pop @p771 :rule scope :premises (@p444)) % 4.34/4.54 (step-pop @p772 :rule scope :premises (@p771)) % 4.34/4.54 (step @p445 :rule process_scope :premises (@p772) :args (@t463)) % 4.34/4.54 (step @p448 :rule and_intro :premises (@p405 @p767)) % 4.34/4.54 (step @p449 :rule modus_ponens :premises (@p448 @p445)) % 4.34/4.54 (step-pop @p773 :rule scope :premises (@p449)) % 4.34/4.54 (step-pop @p774 :rule scope :premises (@p773)) % 4.34/4.54 (step @p450 :rule process_scope :premises (@p774) :args (@t463)) % 4.34/4.54 (step @p453 :rule implies_elim :premises (@p450)) % 4.34/4.54 (step @p454 :rule cnf_and_neg :args (@t466)) % 4.34/4.54 (step @p455 :rule resolution :premises (@p454 @p453) :args (true @t466)) % 4.34/4.54 (step @p456 :rule reordering :premises (@p455) :args ((or @t428 @t463 @t455))) % 4.34/4.54 (step @p457 :rule chain_m_resolution :premises (@p456 @p405 @p430 @p428 @p427 @p425 @p421 @p420) :args (@t429 (@list false true false true false true false) (@list @t446 @t463 @t465 @t459 @t461 @t425 @t427))) % 4.34/4.54 (step @p458 :rule refl :args (@t467)) % 4.34/4.54 (step @p459 :rule bool-double-not-elim :args (@t193)) % 4.34/4.54 (step @p460 :rule nary_cong :premises (@p459 @p458) :args ((or (not @t468) @t467))) % 4.34/4.54 (assume-push @p775 @t468) % 4.34/4.54 (step-pop @p776 :rule scope :premises (@p371)) % 4.34/4.54 (step @p462 :rule process_scope :premises (@p776) :args (@t467)) % 4.34/4.54 (step @p464 :rule implies_elim :premises (@p462)) % 4.34/4.54 (step @p465 :rule eq_resolve :premises (@p464 @p460)) % 4.34/4.54 (step @p466 :rule cnf_or_neg :args (@t438 4)) % 4.34/4.54 (step @p467 :rule cnf_and_neg :args (@t430)) % 4.34/4.54 (step @p468 :rule bool-double-not-elim :args (@t418)) % 4.34/4.54 (step @p469 :rule refl :args (@t420)) % 4.34/4.54 (step @p470 :rule nary_cong :premises (@p469 @p468) :args ((or @t420 (not @t419)))) % 4.34/4.54 (step @p471 :rule cnf_or_neg :args (@t420 0)) % 4.34/4.54 (step @p472 :rule eq_resolve :premises (@p471 @p470)) % 4.34/4.54 (step @p473 :rule reordering :premises (@p472) :args ((or @t418 @t420))) % 4.34/4.54 (step @p474 :rule refl :args (@t469)) % 4.34/4.54 (step @p475 :rule bool-double-not-elim :args (@t470)) % 4.34/4.54 (step @p476 :rule refl :args (@t419)) % 4.34/4.54 (step @p477 :rule nary_cong :premises (@p476 @p475 @p474) :args ((or @t419 (not @t471) @t469))) % 4.34/4.54 (assume-push @p777 @t418) % 4.34/4.54 (assume-push @p778 @t471) % 4.34/4.54 (assume-push @p779 @t471) % 4.34/4.54 (assume-push @p780 @t418) % 4.34/4.54 (step @p482 :rule false_intro :premises (@p778)) % 4.34/4.54 (step @p483 :rule refl :args (@t194)) % 4.34/4.54 (step @p484 :rule refl :args (@t195)) % 4.34/4.54 (step @p485 :rule refl :args (@t196)) % 4.34/4.54 (step @p486 :rule refl :args (tptp.black1)) % 4.34/4.54 (step @p487 :rule cong :premises (@p486 @p777 @p485 @p484 @p483) :args (@t198)) % 4.34/4.54 (step @p488 :rule cong :premises (@p487) :args (@t451)) % 4.34/4.54 (step @p489 :rule trans :premises (@p488 @p482)) % 4.34/4.54 (step @p490 :rule false_elim :premises (@p489)) % 4.34/4.54 (step-pop @p781 :rule scope :premises (@p490)) % 4.34/4.54 (step-pop @p782 :rule scope :premises (@p781)) % 4.34/4.54 (step @p491 :rule process_scope :premises (@p782) :args (@t469)) % 4.34/4.54 (step @p494 :rule and_intro :premises (@p778 @p777)) % 4.34/4.54 (step @p495 :rule modus_ponens :premises (@p494 @p491)) % 4.34/4.54 (step-pop @p783 :rule scope :premises (@p495)) % 4.34/4.54 (step-pop @p784 :rule scope :premises (@p783)) % 4.34/4.54 (step @p496 :rule process_scope :premises (@p784) :args (@t469)) % 4.34/4.54 (step @p499 :rule implies_elim :premises (@p496)) % 4.34/4.54 (step @p500 :rule cnf_and_neg :args (@t472)) % 4.34/4.54 (step @p501 :rule resolution :premises (@p500 @p499) :args (true @t472)) % 4.34/4.54 (step @p502 :rule eq_resolve :premises (@p501 @p477)) % 4.34/4.54 (assume-push @p785 @t473) % 4.34/4.54 (step @p504 :rule instantiate :premises (@p65) :args (@t474)) % 4.34/4.54 (step-pop @p786 :rule scope :premises (@p504)) % 4.34/4.54 (step @p505 :rule process_scope :premises (@p786) :args (@t476)) % 4.34/4.54 (step @p507 :rule implies_elim :premises (@p505)) % 4.34/4.54 (step @p508 :rule cnf_or_pos :args (@t476)) % 4.34/4.54 (step @p509 :rule reordering :premises (@p508) :args ((or @t471 @t475 (not @t476)))) % 4.34/4.54 (assume-push @p787 @t66) % 4.34/4.54 (step @p511 :rule instantiate :premises (@p61) :args (@t477)) % 4.34/4.54 (step-pop @p788 :rule scope :premises (@p511)) % 4.34/4.54 (step @p512 :rule process_scope :premises (@p788) :args (@t482)) % 4.34/4.54 (step @p514 :rule implies_elim :premises (@p512)) % 4.34/4.54 (step @p515 :rule cnf_equiv_pos1 :args (@t482)) % 4.34/4.54 (step @p516 :rule reordering :premises (@p515) :args ((or (not @t475) @t481 (not @t482)))) % 4.34/4.54 (step @p517 :rule cnf_and_pos :args (@t481 1)) % 4.34/4.54 (step @p518 :rule reordering :premises (@p517) :args ((or @t479 @t483))) % 4.34/4.54 (step @p519 :rule cnf_and_pos :args (@t481 3)) % 4.34/4.54 (step @p520 :rule reordering :premises (@p519) :args ((or @t478 @t483))) % 4.34/4.54 (step @p521 :rule instantiate :premises (@p61) :args ((@list tptp.red1 @t397 @t395 @t394 @t392))) % 4.34/4.54 (step @p522 :rule instantiate :premises (@p424) :args ((@list @t200 @t395 @t199 @t394 @t201 @t396 @t392 @t202 @t390 tptp.red1 tptp.black1))) % 4.34/4.54 (step @p523 :rule chain_m_resolution :premises (@p466 @p371) :args ((not @t430) @t439 @t440)) % 4.34/4.54 (step @p524 :rule chain_m_resolution :premises (@p467 @p523 @p457) :args ((not @t420) @t484 (@list @t430 @t429))) % 4.34/4.54 (step @p525 :rule chain_m_resolution :premises (@p473 @p524) :args (@t418 @t439 @t485)) % 4.34/4.54 (assume-push @p789 @t432) % 4.34/4.54 (assume-push @p790 @t418) % 4.34/4.54 (assume-push @p791 @t432) % 4.34/4.54 (assume-push @p792 @t418) % 4.34/4.54 (step @p530 :rule true_intro :premises (@p384)) % 4.34/4.54 (step @p531 :rule symm :premises (@p790)) % 4.34/4.54 (step @p437 :rule refl :args (@t199)) % 4.34/4.54 (step @p438 :rule refl :args (@t200)) % 4.34/4.54 (step @p532 :rule refl :args (@t201)) % 4.34/4.54 (step @p533 :rule refl :args (@t202)) % 4.34/4.54 (step @p534 :rule cong :premises (@p533 @p532 @p438 @p437 @p531) :args (@t486)) % 4.34/4.54 (step @p535 :rule cong :premises (@p534) :args (@t487)) % 4.34/4.54 (step @p536 :rule trans :premises (@p535 @p530)) % 4.34/4.54 (step @p537 :rule true_elim :premises (@p536)) % 4.34/4.54 (step-pop @p793 :rule scope :premises (@p537)) % 4.34/4.54 (step-pop @p794 :rule scope :premises (@p793)) % 4.34/4.54 (step @p538 :rule process_scope :premises (@p794) :args (@t487)) % 4.34/4.54 (step @p541 :rule and_intro :premises (@p384 @p790)) % 4.34/4.54 (step @p542 :rule modus_ponens :premises (@p541 @p538)) % 4.34/4.54 (step-pop @p795 :rule scope :premises (@p542)) % 4.34/4.54 (step-pop @p796 :rule scope :premises (@p795)) % 4.34/4.54 (step @p543 :rule process_scope :premises (@p796) :args (@t487)) % 4.34/4.54 (step @p546 :rule implies_elim :premises (@p543)) % 4.34/4.54 (step @p547 :rule cnf_and_neg :args (@t488)) % 4.34/4.54 (step @p548 :rule resolution :premises (@p547 @p546) :args (true @t488)) % 4.34/4.54 (step @p549 :rule chain_m_resolution :premises (@p548 @p525 @p384) :args (@t487 @t445 (@list @t418 @t432))) % 4.34/4.54 (step @p550 :rule cnf_or_pos :args (@t491)) % 4.34/4.54 (step @p551 :rule reordering :premises (@p550) :args ((or @t490 @t489 (not @t491)))) % 4.34/4.54 (step @p552 :rule chain_m_resolution :premises (@p551 @p549 @p522) :args (@t489 @t445 (@list @t487 @t491))) % 4.34/4.54 (step @p553 :rule cnf_equiv_pos1 :args (@t495)) % 4.34/4.54 (step @p554 :rule reordering :premises (@p553) :args ((or (not @t489) @t494 (not @t495)))) % 4.34/4.54 (step @p555 :rule chain_m_resolution :premises (@p554 @p552 @p521) :args (@t494 @t445 (@list @t489 @t495))) % 4.34/4.54 (step @p556 :rule cnf_and_pos :args (@t494 2)) % 4.34/4.54 (step @p557 :rule reordering :premises (@p556) :args ((or @t492 @t496))) % 4.34/4.54 (step @p558 :rule chain_m_resolution :premises (@p557 @p555) :args (@t492 @t457 @t497)) % 4.34/4.54 (step @p559 :rule cnf_and_pos :args (@t494 0)) % 4.34/4.54 (step @p560 :rule reordering :premises (@p559) :args ((or @t493 @t496))) % 4.34/4.54 (step @p561 :rule chain_m_resolution :premises (@p560 @p555) :args (@t493 @t457 @t497)) % 4.34/4.54 (step @p562 :rule cnf_and_neg :args (@t498)) % 4.34/4.54 (step @p563 :rule reordering :premises (@p562) :args ((or (not @t479) (not @t478) (not @t493) (not @t492) @t498))) % 4.34/4.54 (step @p564 :rule chain_m_resolution :premises (@p563 @p561 @p558 @p520 @p518) :args ((or @t483 @t498) @t442 (@list @t493 @t492 @t478 @t479))) % 4.34/4.54 (assume-push @p797 @t66) % 4.34/4.54 (step @p566 :rule instantiate :premises (@p61) :args (@t499)) % 4.34/4.54 (step-pop @p798 :rule scope :premises (@p566)) % 4.34/4.54 (step @p567 :rule process_scope :premises (@p798) :args (@t500)) % 4.34/4.54 (step @p569 :rule implies_elim :premises (@p567)) % 4.34/4.54 (step @p570 :rule cnf_equiv_pos2 :args (@t500)) % 4.34/4.54 (step @p571 :rule reordering :premises (@p570) :args ((or @t398 (not @t498) (not @t500)))) % 4.34/4.54 (step @p572 :rule cnf_or_neg :args (@t400 2)) % 4.34/4.54 (step @p573 :rule bool-double-not-elim :args (@t410)) % 4.34/4.54 (step @p574 :rule refl :args (@t412)) % 4.34/4.54 (step @p575 :rule nary_cong :premises (@p574 @p573) :args ((or @t412 (not @t411)))) % 4.34/4.54 (step @p576 :rule cnf_or_neg :args (@t412 0)) % 4.34/4.54 (step @p577 :rule eq_resolve :premises (@p576 @p575)) % 4.34/4.54 (step @p578 :rule reordering :premises (@p577) :args ((or @t410 @t412))) % 4.34/4.54 (step @p579 :rule cnf_or_neg :args (@t412 1)) % 4.34/4.54 (step @p580 :rule instantiate :premises (@p61) :args ((@list @t202 @t201 @t200 @t199 @t197))) % 4.34/4.54 (step @p581 :rule cnf_equiv_pos1 :args (@t504)) % 4.34/4.54 (step @p582 :rule reordering :premises (@p581) :args ((or @t433 @t503 (not @t504)))) % 4.34/4.54 (step @p583 :rule chain_m_resolution :premises (@p582 @p384 @p580) :args (@t503 @t445 (@list @t432 @t504))) % 4.34/4.54 (step @p584 :rule cnf_and_pos :args (@t503 0)) % 4.34/4.54 (step @p585 :rule reordering :premises (@p584) :args ((or @t452 (not @t503)))) % 4.34/4.54 (step @p586 :rule chain_m_resolution :premises (@p585 @p583) :args (@t452 @t457 (@list @t503))) % 4.34/4.54 (assume-push @p799 @t410) % 4.34/4.54 (assume-push @p800 @t452) % 4.34/4.54 (assume-push @p801 @t452) % 4.34/4.54 (assume-push @p802 @t410) % 4.34/4.54 (step @p591 :rule true_intro :premises (@p586)) % 4.34/4.54 (step @p592 :rule symm :premises (@p799)) % 4.34/4.54 (step @p593 :rule cong :premises (@p592) :args (@t505)) % 4.34/4.54 (step @p594 :rule trans :premises (@p593 @p591)) % 4.34/4.54 (step @p595 :rule true_elim :premises (@p594)) % 4.34/4.54 (step-pop @p803 :rule scope :premises (@p595)) % 4.34/4.54 (step-pop @p804 :rule scope :premises (@p803)) % 4.34/4.54 (step @p596 :rule process_scope :premises (@p804) :args (@t505)) % 4.34/4.54 (step @p599 :rule and_intro :premises (@p586 @p799)) % 4.34/4.54 (step @p600 :rule modus_ponens :premises (@p599 @p596)) % 4.34/4.54 (step-pop @p805 :rule scope :premises (@p600)) % 4.34/4.54 (step-pop @p806 :rule scope :premises (@p805)) % 4.34/4.54 (step @p601 :rule process_scope :premises (@p806) :args (@t505)) % 4.34/4.54 (step @p604 :rule implies_elim :premises (@p601)) % 4.34/4.54 (step @p605 :rule cnf_and_neg :args (@t506)) % 4.34/4.54 (step @p606 :rule resolution :premises (@p605 @p604) :args (true @t506)) % 4.34/4.54 (step @p607 :rule cnf_and_neg :args (@t408)) % 4.34/4.54 (step @p608 :rule bool-impl-elim :args (@t69 @t72)) % 4.34/4.54 (step @p609 :rule cong :premises (@p608) :args (@t73)) % 4.34/4.54 (step @p610 :rule eq_resolve :premises (@p46 @p609)) % 4.34/4.54 (step @p611 :rule instantiate :premises (@p610) :args ((@list @t399 tptp.black1 @t403 @t402 @t404 @t401))) % 4.34/4.54 (step @p612 :rule cnf_or_pos :args (@t509)) % 4.34/4.54 (step @p613 :rule reordering :premises (@p612) :args ((or @t507 @t508 (not @t509)))) % 4.34/4.54 (step @p614 :rule cnf_or_neg :args (@t407 2)) % 4.34/4.54 (step @p615 :rule instantiate :premises (@p61) :args ((@list tptp.red1 @t405 @t200 @t199 @t198))) % 4.34/4.54 (step @p616 :rule cnf_equiv_pos2 :args (@t512)) % 4.34/4.54 (step @p617 :rule reordering :premises (@p616) :args ((or @t406 (not @t511) (not @t512)))) % 4.34/4.54 (step @p618 :rule cnf_and_neg :args (@t511)) % 4.34/4.54 (step @p619 :rule reordering :premises (@p618) :args ((or @t469 @t511 (not @t507) (not @t510) @t513))) % 4.34/4.54 (step @p620 :rule cnf_and_pos :args (@t514 2)) % 4.34/4.54 (step @p621 :rule reordering :premises (@p620) :args ((or @t510 (not @t514)))) % 4.34/4.54 (step @p622 :rule instantiate :premises (@p61) :args ((@list tptp.red1 @t405 @t200 @t199 @t396))) % 4.34/4.54 (step @p623 :rule cnf_equiv_pos1 :args (@t516)) % 4.34/4.54 (step @p624 :rule reordering :premises (@p623) :args ((or (not @t515) @t514 (not @t516)))) % 4.34/4.54 (step @p625 :rule instantiate :premises (@p424) :args ((@list @t403 @t200 @t402 @t199 @t404 @t401 @t396 tptp.red1 tptp.black1 tptp.red1 tptp.black1))) % 4.34/4.54 (step @p626 :rule cnf_or_pos :args (@t519)) % 4.34/4.54 (step @p627 :rule reordering :premises (@p626) :args ((or @t518 @t515 (not @t519)))) % 4.34/4.54 (step @p628 :rule instantiate :premises (@p65) :args ((@list @t403 @t200 @t402 @t199 @t404 @t401 @t396 tptp.red1 tptp.black1 tptp.black1 @t399))) % 4.34/4.54 (step @p629 :rule cnf_or_pos :args (@t523)) % 4.34/4.54 (step @p630 :rule reordering :premises (@p629) :args ((or @t522 @t517 (not @t523)))) % 4.34/4.54 (assume-push @p807 @t410) % 4.34/4.54 (assume-push @p808 @t493) % 4.34/4.54 (assume-push @p809 @t493) % 4.34/4.54 (assume-push @p810 @t410) % 4.34/4.54 (step @p635 :rule true_intro :premises (@p808)) % 4.34/4.54 (step @p636 :rule refl :args (@t396)) % 4.34/4.54 (step @p437 :rule refl :args (@t199)) % 4.34/4.54 (step @p438 :rule refl :args (@t200)) % 4.34/4.54 (step @p637 :rule symm :premises (@p807)) % 4.34/4.54 (step @p486 :rule refl :args (tptp.black1)) % 4.34/4.54 (step @p638 :rule cong :premises (@p486 @p637 @p438 @p437 @p636) :args (@t520)) % 4.34/4.54 (step @p639 :rule cong :premises (@p638) :args (@t521)) % 4.34/4.54 (step @p640 :rule trans :premises (@p639 @p635)) % 4.34/4.54 (step @p641 :rule true_elim :premises (@p640)) % 4.34/4.54 (step-pop @p811 :rule scope :premises (@p641)) % 4.34/4.54 (step-pop @p812 :rule scope :premises (@p811)) % 4.34/4.54 (step @p642 :rule process_scope :premises (@p812) :args (@t521)) % 4.34/4.54 (step @p645 :rule and_intro :premises (@p808 @p807)) % 4.34/4.54 (step @p646 :rule modus_ponens :premises (@p645 @p642)) % 4.34/4.54 (step-pop @p813 :rule scope :premises (@p646)) % 4.34/4.54 (step-pop @p814 :rule scope :premises (@p813)) % 4.34/4.54 (step @p647 :rule process_scope :premises (@p814) :args (@t521)) % 4.34/4.54 (step @p650 :rule implies_elim :premises (@p647)) % 4.34/4.54 (step @p651 :rule cnf_and_neg :args (@t524)) % 4.34/4.54 (step @p652 :rule resolution :premises (@p651 @p650) :args (true @t524)) % 4.34/4.54 (step @p653 :rule chain_m_resolution :premises (@p652 @p561 @p630 @p628 @p627 @p625 @p624 @p622 @p621 @p619 @p617 @p615 @p614 @p613 @p611 @p607 @p606 @p586 @p579 @p578 @p572 @p571 @p569 @p564 @p516 @p514 @p61 @p509 @p507 @p65 @p502 @p473 @p467 @p466 @p465 @p370 @p457) :args ((or @t412 @t469 @t513) (@list false true false true false true false true true true false true false false true false false true false false false false false false false false false false false false false true true true true false) (@list @t493 @t521 @t523 @t517 @t519 @t515 @t516 @t514 @t510 @t511 @t512 @t406 @t507 @t509 @t407 @t505 @t452 @t408 @t410 @t400 @t398 @t500 @t498 @t481 @t482 @t66 @t475 @t476 @t473 @t470 @t418 @t420 @t430 @t438 @t193 @t429))) % 4.34/4.54 (step @p654 :rule chain_m_resolution :premises (@p653 @p414 @p411) :args (@t412 @t445 (@list @t451 @t449))) % 4.34/4.54 (step @p566 :rule instantiate :premises (@p61) :args (@t499)) % 4.34/4.54 (step @p511 :rule instantiate :premises (@p61) :args (@t477)) % 4.34/4.54 (step @p504 :rule instantiate :premises (@p65) :args (@t474)) % 4.34/4.54 (step @p655 :rule chain_m_resolution :premises (@p502 @p525 @p414) :args (@t470 @t445 (@list @t418 @t451))) % 4.34/4.54 (step @p656 :rule chain_m_resolution :premises (@p509 @p655 @p504) :args (@t475 @t445 (@list @t470 @t476))) % 4.34/4.54 (step @p657 :rule chain_m_resolution :premises (@p516 @p656 @p511) :args (@t481 @t445 (@list @t475 @t482))) % 4.34/4.54 (step @p658 :rule chain_m_resolution :premises (@p564 @p657) :args (@t498 @t457 (@list @t481))) % 4.34/4.54 (step @p659 :rule chain_m_resolution :premises (@p571 @p658 @p566) :args (@t398 @t445 (@list @t498 @t500))) % 4.34/4.54 (step @p660 :rule cnf_or_neg :args (@t413 2)) % 4.34/4.54 (step @p661 :rule chain_m_resolution :premises (@p660 @p659) :args (@t413 @t457 (@list @t398))) % 4.34/4.54 (step @p662 :rule cnf_and_neg :args (@t414)) % 4.34/4.54 (step @p663 :rule chain_m_resolution :premises (@p662 @p661 @p654) :args (@t414 @t445 (@list @t413 @t412))) % 4.34/4.54 (step @p664 :rule cnf_or_neg :args (@t415 1)) % 4.34/4.54 (step @p665 :rule chain_m_resolution :premises (@p664 @p663) :args (@t415 @t457 (@list @t414))) % 4.34/4.54 (step @p666 :rule cnf_or_neg :args (@t420 1)) % 4.34/4.54 (step @p667 :rule chain_m_resolution :premises (@p666 @p524) :args ((not @t416) @t439 @t485)) % 4.34/4.54 (step @p668 :rule cnf_and_neg :args (@t416)) % 4.34/4.54 (step @p669 :rule chain_m_resolution :premises (@p668 @p667 @p665) :args ((not @t391) @t484 (@list @t416 @t415))) % 4.34/4.54 (step @p670 :rule bool-double-not-elim :args (@t388)) % 4.34/4.54 (step @p671 :rule refl :args (@t391)) % 4.34/4.54 (step @p672 :rule nary_cong :premises (@p671 @p670) :args ((or @t391 (not @t389)))) % 4.34/4.54 (step @p673 :rule cnf_or_neg :args (@t391 1)) % 4.34/4.54 (step @p674 :rule eq_resolve :premises (@p673 @p672)) % 4.34/4.54 (step @p675 :rule reordering :premises (@p674) :args ((or @t388 @t391))) % 4.34/4.54 (step @p676 :rule chain_m_resolution :premises (@p675 @p669) :args (@t388 @t439 (@list @t391))) % 4.34/4.54 (step @p677 :rule bool-double-not-elim :args (@t386)) % 4.34/4.54 (step @p678 :rule nary_cong :premises (@p671 @p677) :args ((or @t391 (not @t387)))) % 4.34/4.54 (step @p679 :rule cnf_or_neg :args (@t391 2)) % 4.34/4.54 (step @p680 :rule eq_resolve :premises (@p679 @p678)) % 4.34/4.54 (step @p681 :rule reordering :premises (@p680) :args ((or @t386 @t391))) % 4.34/4.54 (step @p682 :rule cnf_or_neg :args (@t391 3)) % 4.34/4.54 (assume-push @p815 @t386) % 4.34/4.54 (assume-push @p816 @t452) % 4.34/4.54 (assume-push @p817 @t452) % 4.34/4.54 (assume-push @p818 @t386) % 4.34/4.54 (step @p591 :rule true_intro :premises (@p586)) % 4.34/4.54 (step @p687 :rule symm :premises (@p815)) % 4.34/4.54 (step @p688 :rule cong :premises (@p687) :args (@t525)) % 4.34/4.54 (step @p689 :rule trans :premises (@p688 @p591)) % 4.34/4.54 (step @p690 :rule true_elim :premises (@p689)) % 4.34/4.54 (step-pop @p819 :rule scope :premises (@p690)) % 4.34/4.54 (step-pop @p820 :rule scope :premises (@p819)) % 4.34/4.54 (step @p691 :rule process_scope :premises (@p820) :args (@t525)) % 4.34/4.54 (step @p694 :rule and_intro :premises (@p586 @p815)) % 4.34/4.54 (step @p695 :rule modus_ponens :premises (@p694 @p691)) % 4.34/4.54 (step-pop @p821 :rule scope :premises (@p695)) % 4.34/4.54 (step-pop @p822 :rule scope :premises (@p821)) % 4.34/4.54 (step @p696 :rule process_scope :premises (@p822) :args (@t525)) % 4.34/4.54 (step @p699 :rule implies_elim :premises (@p696)) % 4.34/4.54 (step @p700 :rule cnf_and_neg :args (@t526)) % 4.34/4.54 (step @p701 :rule resolution :premises (@p700 @p699) :args (true @t526)) % 4.34/4.54 (assume-push @p823 @t432) % 4.34/4.54 (assume-push @p824 @t386) % 4.34/4.54 (assume-push @p825 @t386) % 4.34/4.54 (assume-push @p826 @t432) % 4.34/4.54 (step @p530 :rule true_intro :premises (@p384)) % 4.34/4.54 (step @p706 :rule refl :args (@t197)) % 4.34/4.54 (step @p437 :rule refl :args (@t199)) % 4.34/4.54 (step @p438 :rule refl :args (@t200)) % 4.34/4.54 (step @p707 :rule symm :premises (@p824)) % 4.34/4.54 (step @p533 :rule refl :args (@t202)) % 4.34/4.54 (step @p708 :rule cong :premises (@p533 @p707 @p438 @p437 @p706) :args (@t527)) % 4.34/4.54 (step @p709 :rule cong :premises (@p708) :args (@t528)) % 4.34/4.54 (step @p710 :rule trans :premises (@p709 @p530)) % 4.34/4.54 (step @p711 :rule true_elim :premises (@p710)) % 4.34/4.54 (step-pop @p827 :rule scope :premises (@p711)) % 4.34/4.54 (step-pop @p828 :rule scope :premises (@p827)) % 4.34/4.54 (step @p712 :rule process_scope :premises (@p828) :args (@t528)) % 4.34/4.54 (step @p715 :rule and_intro :premises (@p824 @p384)) % 4.34/4.54 (step @p716 :rule modus_ponens :premises (@p715 @p712)) % 4.34/4.54 (step-pop @p829 :rule scope :premises (@p716)) % 4.34/4.54 (step-pop @p830 :rule scope :premises (@p829)) % 4.34/4.54 (step @p717 :rule process_scope :premises (@p830) :args (@t528)) % 4.34/4.54 (step @p720 :rule implies_elim :premises (@p717)) % 4.34/4.54 (step @p721 :rule cnf_and_neg :args (@t529)) % 4.34/4.54 (step @p722 :rule resolution :premises (@p721 @p720) :args (true @t529)) % 4.34/4.54 (step @p723 :rule instantiate :premises (@p61) :args ((@list tptp.red1 @t383 @t200 @t199 @t198))) % 4.34/4.54 (step @p724 :rule cnf_equiv_pos2 :args (@t533)) % 4.34/4.54 (step @p725 :rule reordering :premises (@p724) :args ((or @t384 (not @t532) (not @t533)))) % 4.34/4.54 (step @p726 :rule instantiate :premises (@p610) :args ((@list tptp.red1 tptp.black1 @t381 @t380 @t382 @t379))) % 4.34/4.54 (step @p727 :rule cnf_or_pos :args (@t535)) % 4.34/4.54 (step @p728 :rule reordering :premises (@p727) :args ((or @t534 @t531 (not @t535)))) % 4.34/4.54 (step @p729 :rule instantiate :premises (@p65) :args ((@list @t381 @t200 @t380 @t199 @t382 @t379 @t197 tptp.red1 @t202 @t202 tptp.red1))) % 4.34/4.54 (step @p730 :rule cnf_or_pos :args (@t538)) % 4.34/4.54 (step @p731 :rule reordering :premises (@p730) :args ((or @t537 @t536 (not @t538)))) % 4.34/4.54 (step @p732 :rule cnf_and_neg :args (@t532)) % 4.34/4.54 (step @p733 :rule reordering :premises (@p732) :args ((or @t469 @t513 (not @t531) @t532 (not @t530)))) % 4.34/4.54 (step @p734 :rule instantiate :premises (@p424) :args ((@list @t381 @t200 @t380 @t199 @t382 @t379 @t197 tptp.red1 @t202 tptp.red1 tptp.black1))) % 4.34/4.54 (step @p735 :rule cnf_or_pos :args (@t541)) % 4.34/4.54 (step @p736 :rule reordering :premises (@p735) :args ((or @t540 @t539 (not @t541)))) % 4.34/4.54 (step @p737 :rule cnf_and_pos :args (@t542 2)) % 4.34/4.54 (step @p738 :rule reordering :premises (@p737) :args ((or @t530 (not @t542)))) % 4.34/4.54 (step @p739 :rule instantiate :premises (@p61) :args ((@list @t202 @t383 @t200 @t199 @t197))) % 4.34/4.54 (step @p740 :rule cnf_equiv_pos1 :args (@t545)) % 4.34/4.54 (step @p741 :rule reordering :premises (@p740) :args ((or (not @t544) @t542 (not @t545)))) % 4.34/4.54 (assume-push @p831 @t388) % 4.34/4.54 (assume-push @p832 @t539) % 4.34/4.54 (assume-push @p833 @t539) % 4.34/4.54 (assume-push @p834 @t388) % 4.34/4.54 (step @p746 :rule true_intro :premises (@p832)) % 4.34/4.54 (step @p706 :rule refl :args (@t197)) % 4.34/4.54 (step @p437 :rule refl :args (@t199)) % 4.34/4.54 (step @p438 :rule refl :args (@t200)) % 4.34/4.54 (step @p747 :rule refl :args (@t383)) % 4.34/4.54 (step @p748 :rule symm :premises (@p831)) % 4.34/4.54 (step @p749 :rule cong :premises (@p748 @p747 @p438 @p437 @p706) :args (@t543)) % 4.34/4.54 (step @p750 :rule cong :premises (@p749) :args (@t544)) % 4.34/4.54 (step @p751 :rule trans :premises (@p750 @p746)) % 4.34/4.54 (step @p752 :rule true_elim :premises (@p751)) % 4.34/4.54 (step-pop @p835 :rule scope :premises (@p752)) % 4.34/4.54 (step-pop @p836 :rule scope :premises (@p835)) % 4.34/4.54 (step @p753 :rule process_scope :premises (@p836) :args (@t544)) % 4.34/4.54 (step @p756 :rule and_intro :premises (@p832 @p831)) % 4.34/4.54 (step @p757 :rule modus_ponens :premises (@p756 @p753)) % 4.34/4.54 (step-pop @p837 :rule scope :premises (@p757)) % 4.34/4.54 (step-pop @p838 :rule scope :premises (@p837)) % 4.34/4.54 (step @p758 :rule process_scope :premises (@p838) :args (@t544)) % 4.34/4.54 (step @p761 :rule implies_elim :premises (@p758)) % 4.34/4.54 (step @p762 :rule cnf_and_neg :args (@t546)) % 4.34/4.54 (step @p763 :rule resolution :premises (@p762 @p761) :args (true @t546)) % 4.34/4.54 (step @p764 :rule reordering :premises (@p763) :args ((or @t389 @t544 (not @t539)))) % 4.34/4.54 (step @p765 :rule chain_m_resolution :premises (@p764 @p741 @p739 @p738 @p736 @p734 @p733 @p731 @p729 @p728 @p726 @p725 @p723 @p722 @p384 @p701 @p586 @p682 @p681) :args ((or @t389 @t391 @t469 @t513) (@list true false true false false true false false false false true false false false false false true false) (@list @t544 @t545 @t542 @t539 @t541 @t530 @t536 @t538 @t531 @t535 @t532 @t533 @t528 @t432 @t525 @t452 @t384 @t386))) % 4.34/4.54 (step @p766 false :rule chain_m_resolution :premises (@p765 @p676 @p669 @p414 @p411) :args (false (@list false true false false) (@list @t388 @t391 @t451 @t449))) % 4.34/4.54 ) % 4.34/4.54 % SZS output end Proof % 4.34/4.54 % cvc5 exiting %------------------------------------------------------------------------------