%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : KRS153+1 : TPTP v9.2.1. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:29:01 AM UTC 2026 % Result : Theorem 0.38s 0.75s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS153+1 : TPTP v9.2.1. Released v3.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.35 % Computer : n003.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 05:28:14 EDT 2026 % 0.18/0.35 % CPUTime : % 0.28/0.52 %----Proving TF0_NAR, FOF, or CNF % 0.38/0.75 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.38/0.75 % SZS status Theorem % 0.38/0.75 % SZS output start Proof % 0.38/0.75 ( % 0.38/0.75 (declare-sort $$unsorted 0) % 0.38/0.75 (declare-const tptp.iV16465 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16464 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16462 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16459 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16460 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16455 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16449 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16463 $$unsorted) % 0.38/0.75 (declare-const tptp.iV16441 $$unsorted) % 0.38/0.75 (declare-const tptp.cTEST (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC96 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC90 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC88 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC86 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC84 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC82 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC80 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC78 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC76 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC74 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC14 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC126 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC130 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC122 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC40 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC120 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC98 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC38 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC72 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC128 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC46 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC118 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cTOP (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC116 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC36 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC114 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC70 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC110 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC12 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC64 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC34 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC4 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16461 $$unsorted) % 0.38/0.75 (declare-const tptp.cC48 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC28 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC112 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cowlNothing (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16439 $$unsorted) % 0.38/0.75 (declare-const tptp.cC102 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC24 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16448 $$unsorted) % 0.38/0.75 (declare-const tptp.cowlThing (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC104 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC6 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC92 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC18 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.xsd_string (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16440 $$unsorted) % 0.38/0.75 (declare-const tptp.cC106 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC60 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC8 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC52 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC124 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16453 $$unsorted) % 0.38/0.75 (declare-const tptp.cC42 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.rR1 (-> $$unsorted $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC68 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC108 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC100 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC94 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC10 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC20 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC54 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC50 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.xsd_integer (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC16 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC22 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC2 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16442 $$unsorted) % 0.38/0.75 (declare-const tptp.cC30 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC32 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC44 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.iV16457 $$unsorted) % 0.38/0.75 (declare-const tptp.cC56 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC58 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC26 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC62 (-> $$unsorted Bool)) % 0.38/0.75 (declare-const tptp.cC66 (-> $$unsorted Bool)) % 0.38/0.75 (define @t1 () (@var "X" $$unsorted)) % 0.38/0.75 (define @t2 () (not (tptp.cowlNothing @t1))) % 0.38/0.75 (define @t3 () (tptp.cowlThing @t1)) % 0.38/0.75 (define @t4 () (@list @t1)) % 0.38/0.75 (define @t5 () (forall @t4 (and @t3 @t2))) % 0.38/0.75 (define @t6 () (forall @t4 (= (tptp.xsd_string @t1) (not (tptp.xsd_integer @t1))))) % 0.38/0.75 (define @t7 () (tptp.cC6 @t1)) % 0.38/0.75 (define @t8 () (tptp.cC8 @t1)) % 0.38/0.75 (define @t9 () (tptp.cC10 @t1)) % 0.38/0.75 (define @t10 () (@var "Y" $$unsorted)) % 0.38/0.75 (define @t11 () (tptp.rR1 @t1 @t10)) % 0.38/0.75 (define @t12 () (@list @t10)) % 0.38/0.75 (define @t13 () (tptp.cC100 @t1)) % 0.38/0.75 (define @t14 () (tptp.cC104 @t1)) % 0.38/0.75 (define @t15 () (tptp.cC106 @t1)) % 0.38/0.75 (define @t16 () (tptp.cC28 @t1)) % 0.38/0.75 (define @t17 () (tptp.cC108 @t1)) % 0.38/0.75 (define @t18 () (tptp.cC4 @t1)) % 0.38/0.75 (define @t19 () (not @t18)) % 0.38/0.75 (define @t20 () (tptp.cC12 @t1)) % 0.38/0.75 (define @t21 () (not @t20)) % 0.38/0.75 (define @t22 () (tptp.cC110 @t1)) % 0.38/0.75 (define @t23 () (tptp.cC112 @t1)) % 0.38/0.75 (define @t24 () (tptp.cC116 @t1)) % 0.38/0.75 (define @t25 () (tptp.cC130 @t1)) % 0.38/0.75 (define @t26 () (tptp.cC14 @t1)) % 0.38/0.75 (define @t27 () (tptp.cC2 @t1)) % 0.38/0.75 (define @t28 () (and @t18 @t27)) % 0.38/0.75 (define @t29 () (tptp.cC30 @t1)) % 0.38/0.75 (define @t30 () (not @t27)) % 0.38/0.75 (define @t31 () (tptp.cC32 @t1)) % 0.38/0.75 (define @t32 () (tptp.cC34 @t1)) % 0.38/0.75 (define @t33 () (tptp.cC36 @t1)) % 0.38/0.75 (define @t34 () (tptp.cC38 @t1)) % 0.38/0.75 (define @t35 () (tptp.cC40 @t1)) % 0.38/0.75 (define @t36 () (tptp.cC8 @t10)) % 0.38/0.75 (define @t37 () (not @t36)) % 0.38/0.75 (define @t38 () (and @t11 @t37)) % 0.38/0.75 (define @t39 () (exists @t12 @t38)) % 0.38/0.75 (define @t40 () (tptp.cC42 @t1)) % 0.38/0.75 (define @t41 () (= @t40 @t39)) % 0.38/0.75 (define @t42 () (forall @t4 @t41)) % 0.38/0.75 (define @t43 () (tptp.cC44 @t1)) % 0.38/0.75 (define @t44 () (tptp.cC46 @t1)) % 0.38/0.75 (define @t45 () (not @t8)) % 0.38/0.75 (define @t46 () (tptp.cC48 @t1)) % 0.38/0.75 (define @t47 () (tptp.cC50 @t1)) % 0.38/0.75 (define @t48 () (tptp.cC52 @t1)) % 0.38/0.75 (define @t49 () (tptp.cC54 @t1)) % 0.38/0.75 (define @t50 () (tptp.cC56 @t1)) % 0.38/0.75 (define @t51 () (tptp.cC58 @t1)) % 0.38/0.75 (define @t52 () (tptp.cC12 @t10)) % 0.38/0.75 (define @t53 () (not @t52)) % 0.38/0.75 (define @t54 () (and @t11 @t53)) % 0.38/0.75 (define @t55 () (exists @t12 @t54)) % 0.38/0.75 (define @t56 () (tptp.cC60 @t1)) % 0.38/0.75 (define @t57 () (= @t56 @t55)) % 0.38/0.75 (define @t58 () (forall @t4 @t57)) % 0.38/0.75 (define @t59 () (tptp.cC62 @t1)) % 0.38/0.75 (define @t60 () (forall @t4 (= @t59 (and @t56 (not @t51))))) % 0.38/0.75 (define @t61 () (tptp.cC64 @t1)) % 0.38/0.75 (define @t62 () (tptp.cC66 @t1)) % 0.38/0.75 (define @t63 () (tptp.cC68 @t1)) % 0.38/0.75 (define @t64 () (tptp.cC70 @t1)) % 0.38/0.75 (define @t65 () (tptp.cC72 @t1)) % 0.38/0.75 (define @t66 () (tptp.cC74 @t1)) % 0.38/0.75 (define @t67 () (tptp.cC76 @t1)) % 0.38/0.75 (define @t68 () (forall @t4 (= @t67 (and (not @t66) @t59)))) % 0.38/0.75 (define @t69 () (tptp.cC78 @t1)) % 0.38/0.75 (define @t70 () (tptp.cC80 @t1)) % 0.38/0.75 (define @t71 () (tptp.cC82 @t1)) % 0.38/0.75 (define @t72 () (tptp.cC84 @t1)) % 0.38/0.75 (define @t73 () (tptp.cC86 @t1)) % 0.38/0.75 (define @t74 () (tptp.cC88 @t1)) % 0.38/0.75 (define @t75 () (tptp.cC90 @t1)) % 0.38/0.75 (define @t76 () (tptp.cC92 @t1)) % 0.38/0.75 (define @t77 () (tptp.cC94 @t1)) % 0.38/0.75 (define @t78 () (tptp.cC96 @t1)) % 0.38/0.75 (define @t79 () (tptp.cC98 @t1)) % 0.38/0.75 (define @t80 () (tptp.rR1 tptp.iV16439 @t1)) % 0.38/0.75 (define @t81 () (forall @t4 (=> @t80 @t79))) % 0.38/0.75 (define @t82 () (tptp.cTEST tptp.iV16439)) % 0.38/0.75 (define @t83 () (not (tptp.cC100 tptp.iV16439))) % 0.38/0.75 (define @t84 () (tptp.cowlThing tptp.iV16439)) % 0.38/0.75 (define @t85 () (tptp.rR1 tptp.iV16439 tptp.iV16440)) % 0.38/0.75 (define @t86 () (tptp.rR1 tptp.iV16440 @t1)) % 0.38/0.75 (define @t87 () (forall @t4 (=> @t86 @t67))) % 0.38/0.75 (define @t88 () (not (tptp.cC78 tptp.iV16440))) % 0.38/0.75 (define @t89 () (not (tptp.cC96 tptp.iV16440))) % 0.38/0.75 (define @t90 () (tptp.cowlThing tptp.iV16440)) % 0.38/0.75 (define @t91 () (tptp.rR1 tptp.iV16440 tptp.iV16463)) % 0.38/0.75 (define @t92 () (tptp.cC36 tptp.iV16448)) % 0.38/0.75 (define @t93 () (not @t92)) % 0.38/0.75 (define @t94 () (tptp.rR1 tptp.iV16448 @t1)) % 0.38/0.75 (define @t95 () (tptp.cTOP tptp.iV16448)) % 0.38/0.75 (define @t96 () (tptp.cowlThing tptp.iV16448)) % 0.38/0.75 (define @t97 () (not @t76)) % 0.38/0.75 (define @t98 () (tptp.rR1 tptp.iV16453 @t1)) % 0.38/0.75 (define @t99 () (not @t65)) % 0.38/0.75 (define @t100 () (tptp.cC58 tptp.iV16453)) % 0.38/0.75 (define @t101 () (not @t100)) % 0.38/0.75 (define @t102 () (tptp.cC74 tptp.iV16453)) % 0.38/0.75 (define @t103 () (not @t102)) % 0.38/0.75 (define @t104 () (forall @t4 (=> @t98 @t50))) % 0.38/0.75 (define @t105 () (tptp.cowlThing tptp.iV16453)) % 0.38/0.75 (define @t106 () (tptp.rR1 tptp.iV16453 tptp.iV16461)) % 0.38/0.75 (define @t107 () (tptp.cC40 tptp.iV16455)) % 0.38/0.75 (define @t108 () (not @t107)) % 0.38/0.75 (define @t109 () (not @t75)) % 0.38/0.75 (define @t110 () (tptp.rR1 tptp.iV16455 @t1)) % 0.38/0.75 (define @t111 () (not @t64)) % 0.38/0.75 (define @t112 () (not @t48)) % 0.38/0.75 (define @t113 () (tptp.cC54 tptp.iV16455)) % 0.38/0.75 (define @t114 () (not @t113)) % 0.38/0.75 (define @t115 () (tptp.cowlThing tptp.iV16455)) % 0.38/0.75 (define @t116 () (tptp.rR1 tptp.iV16455 tptp.iV16460)) % 0.38/0.75 (define @t117 () (tptp.cC36 tptp.iV16457)) % 0.38/0.75 (define @t118 () (not @t117)) % 0.38/0.75 (define @t119 () (tptp.rR1 tptp.iV16457 @t1)) % 0.38/0.75 (define @t120 () (tptp.cTOP tptp.iV16457)) % 0.38/0.75 (define @t121 () (tptp.cowlThing tptp.iV16457)) % 0.38/0.75 (define @t122 () (tptp.cC48 tptp.iV16459)) % 0.38/0.75 (define @t123 () (not @t122)) % 0.38/0.75 (define @t124 () (tptp.cC30 tptp.iV16459)) % 0.38/0.75 (define @t125 () (not @t124)) % 0.38/0.75 (define @t126 () (tptp.cC86 tptp.iV16459)) % 0.38/0.75 (define @t127 () (not @t126)) % 0.38/0.75 (define @t128 () (tptp.cC46 tptp.iV16459)) % 0.38/0.75 (define @t129 () (not @t128)) % 0.38/0.75 (define @t130 () (tptp.cC66 tptp.iV16459)) % 0.38/0.75 (define @t131 () (not @t130)) % 0.38/0.75 (define @t132 () (tptp.cC84 tptp.iV16459)) % 0.38/0.75 (define @t133 () (not @t132)) % 0.38/0.75 (define @t134 () (tptp.cC64 tptp.iV16459)) % 0.38/0.75 (define @t135 () (not @t134)) % 0.38/0.75 (define @t136 () (tptp.cowlThing tptp.iV16459)) % 0.38/0.75 (define @t137 () (tptp.cC32 tptp.iV16459)) % 0.38/0.75 (define @t138 () (not @t137)) % 0.38/0.75 (define @t139 () (tptp.cC36 tptp.iV16460)) % 0.38/0.75 (define @t140 () (not @t139)) % 0.38/0.75 (define @t141 () (tptp.rR1 tptp.iV16460 @t1)) % 0.38/0.75 (define @t142 () (tptp.cTOP tptp.iV16460)) % 0.38/0.75 (define @t143 () (tptp.cC8 tptp.iV16460)) % 0.38/0.75 (define @t144 () (tptp.cowlThing tptp.iV16460)) % 0.38/0.75 (define @t145 () (not (tptp.cC40 tptp.iV16461))) % 0.38/0.75 (define @t146 () (tptp.rR1 tptp.iV16461 @t1)) % 0.38/0.75 (define @t147 () (tptp.cC12 tptp.iV16461)) % 0.38/0.75 (define @t148 () (not (tptp.cC54 tptp.iV16461))) % 0.38/0.75 (define @t149 () (tptp.cowlThing tptp.iV16461)) % 0.38/0.75 (define @t150 () (tptp.rR1 tptp.iV16462 @t1)) % 0.38/0.75 (define @t151 () (tptp.cC36 tptp.iV16462)) % 0.38/0.75 (define @t152 () (not @t151)) % 0.38/0.75 (define @t153 () (tptp.cTOP tptp.iV16462)) % 0.38/0.75 (define @t154 () (tptp.cowlThing tptp.iV16462)) % 0.38/0.75 (define @t155 () (tptp.rR1 tptp.iV16463 @t1)) % 0.38/0.75 (define @t156 () (forall @t4 (=> @t155 @t50))) % 0.38/0.75 (define @t157 () (not (tptp.cC74 tptp.iV16463))) % 0.38/0.75 (define @t158 () (not (tptp.cC58 tptp.iV16463))) % 0.38/0.75 (define @t159 () (tptp.cowlThing tptp.iV16463)) % 0.38/0.75 (define @t160 () (tptp.rR1 tptp.iV16463 tptp.iV16464)) % 0.38/0.75 (define @t161 () (not (tptp.cC40 tptp.iV16464))) % 0.38/0.75 (define @t162 () (tptp.rR1 tptp.iV16464 @t1)) % 0.38/0.75 (define @t163 () (not (tptp.cC54 tptp.iV16464))) % 0.38/0.75 (define @t164 () (tptp.cowlThing tptp.iV16464)) % 0.38/0.75 (define @t165 () (tptp.rR1 tptp.iV16465 @t1)) % 0.38/0.75 (define @t166 () (tptp.cC36 tptp.iV16465)) % 0.38/0.75 (define @t167 () (not @t166)) % 0.38/0.75 (define @t168 () (tptp.cTOP tptp.iV16465)) % 0.38/0.75 (define @t169 () (tptp.cowlThing tptp.iV16465)) % 0.38/0.75 (define @t170 () (tptp.cC38 tptp.iV16465)) % 0.38/0.75 (define @t171 () (tptp.cC42 tptp.iV16464)) % 0.38/0.75 (define @t172 () (tptp.cC56 tptp.iV16464)) % 0.38/0.75 (define @t173 () (tptp.cC44 tptp.iV16464)) % 0.38/0.75 (define @t174 () (tptp.cC60 tptp.iV16463)) % 0.38/0.75 (define @t175 () (tptp.cC76 tptp.iV16463)) % 0.38/0.75 (define @t176 () (tptp.cC62 tptp.iV16463)) % 0.38/0.75 (define @t177 () (tptp.cC38 tptp.iV16462)) % 0.38/0.75 (define @t178 () (tptp.cC42 tptp.iV16461)) % 0.38/0.75 (define @t179 () (tptp.cC56 tptp.iV16461)) % 0.38/0.75 (define @t180 () (tptp.cC44 tptp.iV16461)) % 0.38/0.75 (define @t181 () (tptp.cC38 tptp.iV16460)) % 0.38/0.75 (define @t182 () (tptp.cC34 tptp.iV16459)) % 0.38/0.75 (define @t183 () (tptp.cC50 tptp.iV16459)) % 0.38/0.75 (define @t184 () (tptp.cC88 tptp.iV16459)) % 0.38/0.75 (define @t185 () (tptp.cC68 tptp.iV16459)) % 0.38/0.75 (define @t186 () (tptp.cC38 tptp.iV16457)) % 0.38/0.75 (define @t187 () (tptp.cC42 tptp.iV16455)) % 0.38/0.75 (define @t188 () (tptp.cC56 tptp.iV16455)) % 0.38/0.75 (define @t189 () (tptp.cC44 tptp.iV16455)) % 0.38/0.75 (define @t190 () (tptp.cC60 tptp.iV16453)) % 0.38/0.75 (define @t191 () (tptp.cC76 tptp.iV16453)) % 0.38/0.75 (define @t192 () (tptp.cC62 tptp.iV16453)) % 0.38/0.75 (define @t193 () (tptp.cC38 tptp.iV16448)) % 0.38/0.75 (define @t194 () (tptp.cC98 tptp.iV16440)) % 0.38/0.75 (define @t195 () (tptp.cC82 tptp.iV16440)) % 0.38/0.75 (define @t196 () (tptp.cC80 tptp.iV16440)) % 0.38/0.75 (define @t197 () (tptp.cC104 tptp.iV16439)) % 0.38/0.75 (define @t198 () (tptp.cC108 tptp.iV16439)) % 0.38/0.75 (define @t199 () (tptp.cC130 tptp.iV16439)) % 0.38/0.75 (define @t200 () (tptp.cC28 tptp.iV16439)) % 0.38/0.75 (define @t201 () (tptp.cC106 tptp.iV16439)) % 0.38/0.75 (define @t202 () (and @t5 @t6 @t201 @t200 @t199 @t84 @t198 @t197 @t196 @t90 @t195 @t194 @t96 @t193 @t192 @t105 @t191 @t190 @t189 @t115 @t188 @t187 @t121 @t186 @t185 @t136 @t184 @t183 @t182 @t144 @t181 @t180 @t149 @t179 @t178 @t154 @t177 @t176 @t159 @t175 @t174 @t173 @t164 @t172 @t171 @t169 @t170)) % 0.38/0.75 (define @t203 () (not @t202)) % 0.38/0.75 (define @t204 () (not @t11)) % 0.38/0.75 (define @t205 () (forall @t12 (not @t54))) % 0.38/0.75 (define @t206 () (not @t205)) % 0.38/0.75 (define @t207 () (@list tptp.iV16453)) % 0.38/0.75 (define @t208 () (forall @t12 (not @t38))) % 0.38/0.75 (define @t209 () (not @t208)) % 0.38/0.75 (define @t210 () (@list tptp.iV16455)) % 0.38/0.75 (define @t211 () (not @t116)) % 0.38/0.75 (define @t212 () (or @t211 @t143)) % 0.38/0.75 (define @t213 () (not @t212)) % 0.38/0.75 (define @t214 () (@list true false)) % 0.38/0.75 (define @t215 () (forall @t12 (or (not (tptp.rR1 tptp.iV16455 @t10)) @t36))) % 0.38/0.75 (define @t216 () (@list tptp.iV16460)) % 0.38/0.75 (define @t217 () (not @t215)) % 0.38/0.75 (define @t218 () (= @t187 @t217)) % 0.38/0.75 (define @t219 () (not @t218)) % 0.38/0.75 (define @t220 () (not @t190)) % 0.38/0.75 (define @t221 () (and @t190 @t101)) % 0.38/0.75 (define @t222 () (= @t192 @t221)) % 0.38/0.75 (define @t223 () (not @t192)) % 0.38/0.75 (define @t224 () (and @t103 @t192)) % 0.38/0.75 (define @t225 () (= @t191 @t224)) % 0.38/0.75 (define @t226 () (not @t187)) % 0.38/0.75 (define @t227 () (and @t108 @t187)) % 0.38/0.75 (define @t228 () (= @t189 @t227)) % 0.38/0.75 (define @t229 () (not @t189)) % 0.38/0.75 (define @t230 () (and @t189 @t114)) % 0.38/0.75 (define @t231 () (forall @t4 @t2)) % 0.38/0.75 (define @t232 () (@list @t1)) % 0.38/0.75 (define @t233 () (@var "BOUND_VARIABLE_8148" $$unsorted)) % 0.38/0.75 (define @t234 () (forall @t4 @t3)) % 0.38/0.75 (define @t235 () (@var "BOUND_VARIABLE_8143" $$unsorted)) % 0.38/0.75 (define @t236 () (and @t234 @t231)) % 0.38/0.75 (define @t237 () (not @t168)) % 0.38/0.75 (define @t238 () (and @t167 @t168)) % 0.38/0.75 (define @t239 () (= @t170 @t238)) % 0.38/0.75 (define @t240 () (@list false false)) % 0.38/0.75 (define @t241 () (@list tptp.iV16464)) % 0.38/0.75 (define @t242 () (not @t160)) % 0.38/0.75 (define @t243 () (or @t242 @t172)) % 0.38/0.75 (define @t244 () (and @t173 @t163)) % 0.38/0.75 (define @t245 () (= @t172 @t244)) % 0.38/0.75 (define @t246 () (not @t172)) % 0.38/0.75 (define @t247 () (@list false)) % 0.38/0.75 (define @t248 () (and @t161 @t171)) % 0.38/0.75 (define @t249 () (= @t173 @t248)) % 0.38/0.75 (define @t250 () (not @t173)) % 0.38/0.75 (define @t251 () (@list tptp.iV16463)) % 0.38/0.75 (define @t252 () (not @t91)) % 0.38/0.75 (define @t253 () (or @t252 @t175)) % 0.38/0.75 (define @t254 () (and @t157 @t176)) % 0.38/0.75 (define @t255 () (= @t175 @t254)) % 0.38/0.75 (define @t256 () (not @t175)) % 0.38/0.75 (define @t257 () (and @t174 @t158)) % 0.38/0.75 (define @t258 () (= @t176 @t257)) % 0.38/0.75 (define @t259 () (not @t176)) % 0.38/0.75 (define @t260 () (not @t153)) % 0.38/0.75 (define @t261 () (and @t152 @t153)) % 0.38/0.75 (define @t262 () (= @t177 @t261)) % 0.38/0.75 (define @t263 () (@list tptp.iV16461)) % 0.38/0.75 (define @t264 () (not @t106)) % 0.38/0.75 (define @t265 () (or @t264 @t179)) % 0.38/0.75 (define @t266 () (and @t180 @t148)) % 0.38/0.75 (define @t267 () (= @t179 @t266)) % 0.38/0.75 (define @t268 () (not @t179)) % 0.38/0.75 (define @t269 () (and @t145 @t178)) % 0.38/0.75 (define @t270 () (= @t180 @t269)) % 0.38/0.75 (define @t271 () (not @t180)) % 0.38/0.75 (define @t272 () (not @t142)) % 0.38/0.75 (define @t273 () (and @t140 @t142)) % 0.38/0.75 (define @t274 () (= @t181 @t273)) % 0.38/0.75 (define @t275 () (@list tptp.iV16459)) % 0.38/0.75 (define @t276 () (and @t138 @t125)) % 0.38/0.75 (define @t277 () (@list true true)) % 0.38/0.75 (define @t278 () (= @t182 @t276)) % 0.38/0.75 (define @t279 () (and @t129 @t123)) % 0.38/0.75 (define @t280 () (= @t183 @t279)) % 0.38/0.75 (define @t281 () (and @t133 @t127)) % 0.38/0.75 (define @t282 () (= @t184 @t281)) % 0.38/0.75 (define @t283 () (and @t135 @t131)) % 0.38/0.75 (define @t284 () (= @t185 @t283)) % 0.38/0.75 (define @t285 () (not @t120)) % 0.38/0.75 (define @t286 () (and @t118 @t120)) % 0.38/0.75 (define @t287 () (= @t186 @t286)) % 0.38/0.75 (define @t288 () (@list tptp.iV16440)) % 0.38/0.75 (define @t289 () (not @t85)) % 0.38/0.75 (define @t290 () (or @t289 @t194)) % 0.38/0.75 (define @t291 () (and @t89 @t195)) % 0.38/0.75 (define @t292 () (= @t194 @t291)) % 0.38/0.75 (define @t293 () (not @t194)) % 0.38/0.75 (define @t294 () (and @t88 @t196)) % 0.38/0.75 (define @t295 () (= @t195 @t294)) % 0.38/0.75 (define @t296 () (not @t195)) % 0.38/0.75 (define @t297 () (@list tptp.iV16439)) % 0.38/0.75 (define @t298 () (and @t198 @t199)) % 0.38/0.75 (define @t299 () (= @t82 @t298)) % 0.38/0.75 (define @t300 () (not @t298)) % 0.38/0.75 (define @t301 () (@list @t298)) % 0.38/0.75 (define @t302 () (and @t200 @t201)) % 0.38/0.75 (define @t303 () (= @t198 @t302)) % 0.38/0.75 (define @t304 () (not @t198)) % 0.38/0.75 (define @t305 () (not @t302)) % 0.38/0.75 (define @t306 () (@list @t302)) % 0.38/0.75 (define @t307 () (and @t83 @t197)) % 0.38/0.75 (define @t308 () (= @t201 @t307)) % 0.38/0.75 (define @t309 () (not @t201)) % 0.38/0.75 (define @t310 () (not @t95)) % 0.38/0.75 (define @t311 () (and @t93 @t95)) % 0.38/0.75 (define @t312 () (= @t193 @t311)) % 0.38/0.75 (define @t313 () (forall (@list @t233) (not (tptp.cowlNothing @t233)))) % 0.38/0.75 (define @t314 () (forall (@list @t235) (tptp.cowlThing @t235))) % 0.38/0.75 (define @t315 () (= @t188 @t230)) % 0.38/0.75 (define @t316 () (forall @t12 (or (not (tptp.rR1 tptp.iV16453 @t10)) @t52))) % 0.38/0.75 (define @t317 () (not @t316)) % 0.38/0.75 (define @t318 () (= @t190 @t317)) % 0.38/0.75 (define @t319 () (not @t318)) % 0.38/0.75 (define @t320 () (or @t264 @t147)) % 0.38/0.75 (define @t321 () (not @t320)) % 0.38/0.75 (assume @p1 @t5) % 0.38/0.75 (assume @p2 @t6) % 0.38/0.75 (assume @p3 (forall @t4 (= @t9 (and @t8 @t7)))) % 0.38/0.75 (assume @p4 (forall @t4 (= @t13 (exists @t12 (and @t11 (not (tptp.cC98 @t10))))))) % 0.38/0.75 (assume @p5 (forall @t4 (= @t14 (exists @t12 (and @t11 (not (tptp.cC102 @t10))))))) % 0.38/0.75 (assume @p6 (forall @t4 (= @t15 (and (not @t13) @t14)))) % 0.38/0.75 (assume @p7 (forall @t4 (= @t17 (and @t16 @t15)))) % 0.38/0.75 (assume @p8 (forall @t4 (= @t22 (and @t21 @t19)))) % 0.38/0.75 (assume @p9 (forall @t4 (= @t23 (and (not (tptp.cC102 @t1)) @t22)))) % 0.38/0.75 (assume @p10 (forall @t4 (= @t24 (and @t23 (not (tptp.cC114 @t1)))))) % 0.38/0.75 (assume @p11 (forall @t4 (= (tptp.cC120 @t1) (and @t24 (not (tptp.cC118 @t1)))))) % 0.38/0.75 (assume @p12 (forall @t4 (= (tptp.cC122 @t1) (exists @t12 (and @t11 (not (tptp.cC120 @t10))))))) % 0.38/0.75 (assume @p13 (forall @t4 (= (tptp.cC124 @t1) (exists @t12 (and @t11 (tptp.cC122 @t10)))))) % 0.38/0.75 (assume @p14 (forall @t4 (= (tptp.cC126 @t1) (exists @t12 (and @t11 (tptp.cC124 @t10)))))) % 0.38/0.75 (assume @p15 (forall @t4 (= (tptp.cC128 @t1) (exists @t12 (and @t11 (tptp.cC126 @t10)))))) % 0.38/0.75 (assume @p16 (forall @t4 (= @t25 (exists @t12 (and @t11 (tptp.cC128 @t10)))))) % 0.38/0.75 (assume @p17 (forall @t4 (= @t26 (and @t9 @t20)))) % 0.38/0.75 (assume @p18 (forall @t4 (= (tptp.cC18 @t1) (and @t26 (tptp.cC16 @t1))))) % 0.38/0.75 (assume @p19 (forall @t4 (= (tptp.cC20 @t1) (exists @t12 (and @t11 (not (tptp.cC18 @t10))))))) % 0.38/0.75 (assume @p20 (forall @t4 (= (tptp.cC22 @t1) (exists @t12 (and @t11 (tptp.cC20 @t10)))))) % 0.38/0.75 (assume @p21 (forall @t4 (= (tptp.cC24 @t1) (exists @t12 (and @t11 (tptp.cC22 @t10)))))) % 0.38/0.75 (assume @p22 (forall @t4 (= (tptp.cC26 @t1) (exists @t12 (and @t11 (tptp.cC24 @t10)))))) % 0.38/0.75 (assume @p23 (forall @t4 (= @t16 (exists @t12 (and @t11 (tptp.cC26 @t10)))))) % 0.38/0.75 (assume @p24 (forall @t4 (= @t29 @t28))) % 0.38/0.75 (assume @p25 (forall @t4 (= @t31 (and @t30 @t19)))) % 0.38/0.75 (assume @p26 (forall @t4 (= @t32 (and (not @t31) (not @t29))))) % 0.38/0.75 (assume @p27 (forall @t4 (= @t33 (exists @t12 (and @t11 (not (tptp.cC34 @t10))))))) % 0.38/0.75 (assume @p28 (forall @t4 (= @t34 (and (not @t33) (tptp.cTOP @t1))))) % 0.38/0.75 (assume @p29 (forall @t4 (= @t35 (exists @t12 (and @t11 (not (tptp.cC38 @t10))))))) % 0.38/0.75 (assume @p30 @t42) % 0.38/0.75 (assume @p31 (forall @t4 (= @t43 (and (not @t35) @t40)))) % 0.38/0.75 (assume @p32 (forall @t4 (= @t44 (and @t8 @t18)))) % 0.38/0.75 (assume @p33 (forall @t4 (= @t46 (and @t45 @t19)))) % 0.38/0.75 (assume @p34 (forall @t4 (= @t47 (and (not @t44) (not @t46))))) % 0.38/0.75 (assume @p35 (forall @t4 (= @t48 (exists @t12 (and @t11 (not (tptp.cC50 @t10))))))) % 0.38/0.75 (assume @p36 (forall @t4 (= @t49 (exists @t12 (and @t11 (tptp.cC52 @t10)))))) % 0.38/0.75 (assume @p37 (forall @t4 (= @t50 (and @t43 (not @t49))))) % 0.38/0.75 (assume @p38 (forall @t4 (= @t51 (exists @t12 (and @t11 (not (tptp.cC56 @t10))))))) % 0.38/0.75 (assume @p39 (forall @t4 (= @t7 @t28))) % 0.38/0.75 (assume @p40 @t58) % 0.38/0.75 (assume @p41 @t60) % 0.38/0.75 (assume @p42 (forall @t4 (= @t61 (and @t8 @t20)))) % 0.38/0.75 (assume @p43 (forall @t4 (= @t62 (and @t45 @t21)))) % 0.38/0.75 (assume @p44 (forall @t4 (= @t63 (and (not @t61) (not @t62))))) % 0.38/0.75 (assume @p45 (forall @t4 (= @t64 (exists @t12 (and @t11 (not (tptp.cC68 @t10))))))) % 0.38/0.75 (assume @p46 (forall @t4 (= @t65 (exists @t12 (and @t11 (tptp.cC70 @t10)))))) % 0.38/0.75 (assume @p47 (forall @t4 (= @t66 (exists @t12 (and @t11 (tptp.cC72 @t10)))))) % 0.38/0.75 (assume @p48 @t68) % 0.38/0.75 (assume @p49 (forall @t4 (= @t69 (exists @t12 (and @t11 (not (tptp.cC76 @t10))))))) % 0.38/0.75 (assume @p50 (forall @t4 (= @t70 (exists @t12 (and @t11 (not (tptp.cC16 @t10))))))) % 0.38/0.75 (assume @p51 (forall @t4 (= @t71 (and (not @t69) @t70)))) % 0.38/0.75 (assume @p52 (forall @t4 (= @t72 (and @t27 @t20)))) % 0.38/0.75 (assume @p53 (forall @t4 (= @t73 (and @t21 @t30)))) % 0.38/0.75 (assume @p54 (forall @t4 (= @t74 (and (not @t72) (not @t73))))) % 0.38/0.75 (assume @p55 (forall @t4 (= @t75 (exists @t12 (and @t11 (not (tptp.cC88 @t10))))))) % 0.38/0.75 (assume @p56 (forall @t4 (= @t76 (exists @t12 (and @t11 (tptp.cC90 @t10)))))) % 0.38/0.75 (assume @p57 (forall @t4 (= @t77 (exists @t12 (and @t11 (tptp.cC92 @t10)))))) % 0.38/0.75 (assume @p58 (forall @t4 (= @t78 (exists @t12 (and @t11 (tptp.cC94 @t10)))))) % 0.38/0.75 (assume @p59 (forall @t4 (= @t79 (and (not @t78) @t71)))) % 0.38/0.75 (assume @p60 (forall @t4 (= (tptp.cTEST @t1) (and @t17 @t25)))) % 0.38/0.75 (assume @p61 @t81) % 0.38/0.75 (assume @p62 @t82) % 0.38/0.75 (assume @p63 @t83) % 0.38/0.75 (assume @p64 @t84) % 0.38/0.75 (assume @p65 @t85) % 0.38/0.75 (assume @p66 (tptp.rR1 tptp.iV16439 tptp.iV16442)) % 0.38/0.75 (assume @p67 (tptp.rR1 tptp.iV16439 tptp.iV16441)) % 0.38/0.75 (assume @p68 @t87) % 0.38/0.75 (assume @p69 (forall @t4 (=> @t86 (not @t77)))) % 0.38/0.75 (assume @p70 (not (tptp.cC102 tptp.iV16440))) % 0.38/0.75 (assume @p71 @t88) % 0.38/0.75 (assume @p72 @t89) % 0.38/0.75 (assume @p73 @t90) % 0.38/0.75 (assume @p74 @t91) % 0.38/0.75 (assume @p75 (tptp.cowlThing tptp.iV16441)) % 0.38/0.75 (assume @p76 (tptp.cowlThing tptp.iV16442)) % 0.38/0.75 (assume @p77 @t93) % 0.38/0.75 (assume @p78 (forall @t4 (=> @t94 @t63))) % 0.38/0.75 (assume @p79 (forall @t4 (=> @t94 @t32))) % 0.38/0.75 (assume @p80 @t95) % 0.38/0.75 (assume @p81 (forall @t4 (=> @t94 @t47))) % 0.38/0.75 (assume @p82 (not (tptp.cC52 tptp.iV16448))) % 0.38/0.75 (assume @p83 (not (tptp.cC70 tptp.iV16448))) % 0.38/0.75 (assume @p84 (not (tptp.cC90 tptp.iV16448))) % 0.38/0.75 (assume @p85 @t96) % 0.38/0.75 (assume @p86 (forall @t4 (=> @t94 @t74))) % 0.38/0.75 (assume @p87 (tptp.rR1 tptp.iV16448 tptp.iV16449)) % 0.38/0.75 (assume @p88 (tptp.cowlThing tptp.iV16449)) % 0.38/0.75 (assume @p89 (forall @t4 (=> @t98 @t97))) % 0.38/0.75 (assume @p90 (forall @t4 (=> @t98 @t99))) % 0.38/0.75 (assume @p91 (not (tptp.cC16 tptp.iV16453))) % 0.38/0.75 (assume @p92 @t101) % 0.38/0.75 (assume @p93 @t103) % 0.38/0.75 (assume @p94 @t104) % 0.38/0.75 (assume @p95 @t105) % 0.38/0.75 (assume @p96 (not (tptp.cC94 tptp.iV16453))) % 0.38/0.75 (assume @p97 @t106) % 0.38/0.75 (assume @p98 (not (tptp.cC12 tptp.iV16455))) % 0.38/0.75 (assume @p99 @t108) % 0.38/0.75 (assume @p100 (forall @t4 (=> @t110 @t109))) % 0.38/0.75 (assume @p101 (forall @t4 (=> @t110 @t111))) % 0.38/0.75 (assume @p102 (forall @t4 (=> @t110 @t112))) % 0.38/0.75 (assume @p103 (not (tptp.cC72 tptp.iV16455))) % 0.38/0.75 (assume @p104 @t114) % 0.38/0.75 (assume @p105 (not (tptp.cC92 tptp.iV16455))) % 0.38/0.75 (assume @p106 @t115) % 0.38/0.75 (assume @p107 (forall @t4 (=> @t110 @t34))) % 0.38/0.75 (assume @p108 @t116) % 0.38/0.75 (assume @p109 @t118) % 0.38/0.75 (assume @p110 (forall @t4 (=> @t119 @t74))) % 0.38/0.75 (assume @p111 (not (tptp.cC52 tptp.iV16457))) % 0.38/0.75 (assume @p112 (forall @t4 (=> @t119 @t63))) % 0.38/0.75 (assume @p113 (forall @t4 (=> @t119 @t32))) % 0.38/0.75 (assume @p114 @t120) % 0.38/0.75 (assume @p115 (not (tptp.cC90 tptp.iV16457))) % 0.38/0.75 (assume @p116 (not (tptp.cC70 tptp.iV16457))) % 0.38/0.75 (assume @p117 (forall @t4 (=> @t119 @t47))) % 0.38/0.75 (assume @p118 @t121) % 0.38/0.75 (assume @p119 (not (tptp.cC8 tptp.iV16457))) % 0.38/0.75 (assume @p120 (tptp.cC4 tptp.iV16459)) % 0.38/0.75 (assume @p121 @t123) % 0.38/0.75 (assume @p122 @t125) % 0.38/0.75 (assume @p123 (not (tptp.cC6 tptp.iV16459))) % 0.38/0.75 (assume @p124 @t127) % 0.38/0.75 (assume @p125 @t129) % 0.38/0.75 (assume @p126 (not (tptp.cC14 tptp.iV16459))) % 0.38/0.75 (assume @p127 (not (tptp.cC18 tptp.iV16459))) % 0.38/0.75 (assume @p128 @t131) % 0.38/0.75 (assume @p129 (tptp.cC12 tptp.iV16459)) % 0.38/0.75 (assume @p130 (not (tptp.cC8 tptp.iV16459))) % 0.38/0.75 (assume @p131 (not (tptp.cC2 tptp.iV16459))) % 0.38/0.75 (assume @p132 (not (tptp.cC10 tptp.iV16459))) % 0.38/0.75 (assume @p133 @t133) % 0.38/0.75 (assume @p134 @t135) % 0.38/0.75 (assume @p135 @t136) % 0.38/0.75 (assume @p136 @t138) % 0.38/0.75 (assume @p137 (not (tptp.cC90 tptp.iV16460))) % 0.38/0.75 (assume @p138 @t140) % 0.38/0.75 (assume @p139 (forall @t4 (=> @t141 @t63))) % 0.38/0.75 (assume @p140 (not (tptp.cC52 tptp.iV16460))) % 0.38/0.75 (assume @p141 @t142) % 0.38/0.75 (assume @p142 (not @t143)) % 0.38/0.75 (assume @p143 (not (tptp.cC70 tptp.iV16460))) % 0.38/0.75 (assume @p144 (forall @t4 (=> @t141 @t74))) % 0.38/0.75 (assume @p145 (forall @t4 (=> @t141 @t47))) % 0.38/0.75 (assume @p146 (forall @t4 (=> @t141 @t32))) % 0.38/0.75 (assume @p147 @t144) % 0.38/0.75 (assume @p148 @t145) % 0.38/0.75 (assume @p149 (forall @t4 (=> @t146 @t112))) % 0.38/0.75 (assume @p150 (not (tptp.cC92 tptp.iV16461))) % 0.38/0.75 (assume @p151 (forall @t4 (=> @t146 @t109))) % 0.38/0.75 (assume @p152 (not @t147)) % 0.38/0.75 (assume @p153 @t148) % 0.38/0.75 (assume @p154 (forall @t4 (=> @t146 @t111))) % 0.38/0.75 (assume @p155 (forall @t4 (=> @t146 @t34))) % 0.38/0.75 (assume @p156 @t149) % 0.38/0.75 (assume @p157 (not (tptp.cC72 tptp.iV16461))) % 0.38/0.75 (assume @p158 (tptp.rR1 tptp.iV16461 tptp.iV16462)) % 0.38/0.75 (assume @p159 (not (tptp.cC52 tptp.iV16462))) % 0.38/0.75 (assume @p160 (not (tptp.cC8 tptp.iV16462))) % 0.38/0.75 (assume @p161 (forall @t4 (=> @t150 @t63))) % 0.38/0.75 (assume @p162 @t152) % 0.38/0.75 (assume @p163 @t153) % 0.38/0.75 (assume @p164 (not (tptp.cC90 tptp.iV16462))) % 0.38/0.75 (assume @p165 (forall @t4 (=> @t150 @t32))) % 0.38/0.75 (assume @p166 (forall @t4 (=> @t150 @t47))) % 0.38/0.75 (assume @p167 (forall @t4 (=> @t150 @t74))) % 0.38/0.75 (assume @p168 (not (tptp.cC70 tptp.iV16462))) % 0.38/0.75 (assume @p169 @t154) % 0.38/0.75 (assume @p170 (forall @t4 (=> @t155 @t97))) % 0.38/0.75 (assume @p171 (not (tptp.cC94 tptp.iV16463))) % 0.38/0.75 (assume @p172 @t156) % 0.38/0.75 (assume @p173 (forall @t4 (=> @t155 @t99))) % 0.38/0.75 (assume @p174 @t157) % 0.38/0.75 (assume @p175 @t158) % 0.38/0.75 (assume @p176 (not (tptp.cC16 tptp.iV16463))) % 0.38/0.75 (assume @p177 @t159) % 0.38/0.75 (assume @p178 @t160) % 0.38/0.75 (assume @p179 (not (tptp.cC72 tptp.iV16464))) % 0.38/0.75 (assume @p180 @t161) % 0.38/0.75 (assume @p181 (forall @t4 (=> @t162 @t111))) % 0.38/0.75 (assume @p182 @t163) % 0.38/0.75 (assume @p183 (forall @t4 (=> @t162 @t34))) % 0.38/0.75 (assume @p184 (not (tptp.cC12 tptp.iV16464))) % 0.38/0.75 (assume @p185 (not (tptp.cC92 tptp.iV16464))) % 0.38/0.75 (assume @p186 (forall @t4 (=> @t162 @t109))) % 0.38/0.75 (assume @p187 (forall @t4 (=> @t162 @t112))) % 0.38/0.75 (assume @p188 @t164) % 0.38/0.75 (assume @p189 (tptp.rR1 tptp.iV16464 tptp.iV16465)) % 0.38/0.75 (assume @p190 (forall @t4 (=> @t165 @t63))) % 0.38/0.75 (assume @p191 (not (tptp.cC70 tptp.iV16465))) % 0.38/0.75 (assume @p192 (not (tptp.cC52 tptp.iV16465))) % 0.38/0.75 (assume @p193 (forall @t4 (=> @t165 @t74))) % 0.38/0.75 (assume @p194 (forall @t4 (=> @t165 @t32))) % 0.38/0.75 (assume @p195 (not (tptp.cC8 tptp.iV16465))) % 0.38/0.75 (assume @p196 @t167) % 0.38/0.75 (assume @p197 @t168) % 0.38/0.75 (assume @p198 (forall @t4 (=> @t165 @t47))) % 0.38/0.75 (assume @p199 @t169) % 0.38/0.75 (assume @p200 (not (tptp.cC90 tptp.iV16465))) % 0.38/0.75 (assume @p201 @t203) % 0.38/0.75 (assume @p202 true) % 0.38/0.75 (step @p203 :rule bool-double-not-elim :args (@t52)) % 0.38/0.75 (step @p204 :rule refl :args (@t204)) % 0.38/0.75 (step @p205 :rule nary_cong :premises (@p204 @p203) :args ((or @t204 (not @t53)))) % 0.38/0.75 (step @p206 :rule bool-and-de-morgan :args (@t11 @t53 true)) % 0.38/0.75 (step @p207 :rule trans :premises (@p206 @p205)) % 0.38/0.75 (step @p208 :rule cong :premises (@p207) :args (@t205)) % 0.38/0.75 (step @p209 :rule cong :premises (@p208) :args (@t206)) % 0.38/0.75 (step @p210 :rule exists-elim :args ((= @t55 @t206))) % 0.38/0.75 (step @p211 :rule trans :premises (@p210 @p209)) % 0.38/0.75 (step @p212 :rule refl :args (@t56)) % 0.38/0.75 (step @p213 :rule cong :premises (@p212 @p211) :args (@t57)) % 0.38/0.75 (step @p214 :rule cong :premises (@p213) :args (@t58)) % 0.38/0.75 (step @p215 :rule eq_resolve :premises (@p40 @p214)) % 0.38/0.75 (step @p216 :rule instantiate :premises (@p215) :args (@t207)) % 0.38/0.75 (step @p217 :rule bool-double-not-elim :args (@t36)) % 0.38/0.75 (step @p218 :rule nary_cong :premises (@p204 @p217) :args ((or @t204 (not @t37)))) % 0.38/0.75 (step @p219 :rule bool-and-de-morgan :args (@t11 @t37 true)) % 0.38/0.75 (step @p220 :rule trans :premises (@p219 @p218)) % 0.38/0.75 (step @p221 :rule cong :premises (@p220) :args (@t208)) % 0.38/0.75 (step @p222 :rule cong :premises (@p221) :args (@t209)) % 0.38/0.75 (step @p223 :rule exists-elim :args ((= @t39 @t209))) % 0.38/0.75 (step @p224 :rule trans :premises (@p223 @p222)) % 0.38/0.75 (step @p225 :rule refl :args (@t40)) % 0.38/0.75 (step @p226 :rule cong :premises (@p225 @p224) :args (@t41)) % 0.38/0.75 (step @p227 :rule cong :premises (@p226) :args (@t42)) % 0.38/0.75 (step @p228 :rule eq_resolve :premises (@p30 @p227)) % 0.38/0.75 (step @p229 :rule instantiate :premises (@p228) :args (@t210)) % 0.38/0.75 (step @p230 :rule cnf_or_pos :args (@t212)) % 0.38/0.75 (step @p231 :rule reordering :premises (@p230) :args ((or @t143 @t211 @t213))) % 0.38/0.75 (step @p232 :rule chain_m_resolution :premises (@p231 @p142 @p108) :args (@t213 @t214 (@list @t143 @t116))) % 0.38/0.75 (assume-push @p592 @t215) % 0.38/0.75 (step @p234 :rule instantiate :premises (@p592) :args (@t216)) % 0.38/0.75 (step-pop @p593 :rule scope :premises (@p234)) % 0.38/0.75 (step @p235 :rule process_scope :premises (@p593) :args (@t212)) % 0.38/0.75 (step @p237 :rule implies_elim :premises (@p235)) % 0.38/0.75 (step @p238 :rule chain_m_resolution :premises (@p237 @p232) :args (@t217 (@list true) (@list @t212))) % 0.38/0.75 (step @p239 :rule bool-double-not-elim :args (@t215)) % 0.38/0.75 (step @p240 :rule refl :args (@t187)) % 0.38/0.75 (step @p241 :rule refl :args (@t219)) % 0.38/0.75 (step @p242 :rule nary_cong :premises (@p241 @p240 @p239) :args ((or @t219 @t187 (not @t217)))) % 0.38/0.75 (step @p243 :rule cnf_equiv_pos2 :args (@t218)) % 0.38/0.75 (step @p244 :rule eq_resolve :premises (@p243 @p242)) % 0.38/0.75 (step @p245 :rule reordering :premises (@p244) :args ((or @t187 @t215 @t219))) % 0.38/0.75 (step @p246 :rule chain_m_resolution :premises (@p245 @p238 @p229) :args (@t187 @t214 (@list @t215 @t218))) % 0.38/0.75 (step @p247 :rule bool-double-not-elim :args (@t100)) % 0.38/0.75 (step @p248 :rule refl :args (@t220)) % 0.38/0.75 (step @p249 :rule refl :args (@t221)) % 0.38/0.75 (step @p250 :rule nary_cong :premises (@p249 @p248 @p247) :args ((or @t221 @t220 (not @t101)))) % 0.38/0.75 (step @p251 :rule cnf_and_neg :args (@t221)) % 0.38/0.75 (step @p252 :rule eq_resolve :premises (@p251 @p250)) % 0.38/0.75 (step @p253 :rule reordering :premises (@p252) :args ((or @t100 @t220 @t221))) % 0.38/0.75 (assume-push @p594 @t60) % 0.38/0.75 (step @p255 :rule instantiate :premises (@p41) :args (@t207)) % 0.38/0.75 (step-pop @p595 :rule scope :premises (@p255)) % 0.38/0.75 (step @p256 :rule process_scope :premises (@p595) :args (@t222)) % 0.38/0.75 (step @p258 :rule implies_elim :premises (@p256)) % 0.38/0.75 (step @p259 :rule cnf_equiv_pos2 :args (@t222)) % 0.38/0.75 (step @p260 :rule reordering :premises (@p259) :args ((or @t192 (not @t221) (not @t222)))) % 0.38/0.75 (step @p261 :rule refl :args (@t223)) % 0.38/0.75 (step @p262 :rule bool-double-not-elim :args (@t102)) % 0.38/0.75 (step @p263 :rule refl :args (@t224)) % 0.38/0.75 (step @p264 :rule nary_cong :premises (@p263 @p262 @p261) :args ((or @t224 (not @t103) @t223))) % 0.38/0.75 (step @p265 :rule cnf_and_neg :args (@t224)) % 0.38/0.75 (step @p266 :rule eq_resolve :premises (@p265 @p264)) % 0.38/0.75 (step @p267 :rule reordering :premises (@p266) :args ((or @t102 @t223 @t224))) % 0.38/0.75 (assume-push @p596 @t68) % 0.38/0.75 (step @p269 :rule instantiate :premises (@p48) :args (@t207)) % 0.38/0.75 (step-pop @p597 :rule scope :premises (@p269)) % 0.38/0.75 (step @p270 :rule process_scope :premises (@p597) :args (@t225)) % 0.38/0.75 (step @p272 :rule implies_elim :premises (@p270)) % 0.38/0.75 (step @p273 :rule cnf_equiv_pos2 :args (@t225)) % 0.38/0.75 (step @p274 :rule reordering :premises (@p273) :args ((or @t191 (not @t224) (not @t225)))) % 0.38/0.75 (step @p275 :rule refl :args (@t226)) % 0.38/0.75 (step @p276 :rule bool-double-not-elim :args (@t107)) % 0.38/0.75 (step @p277 :rule refl :args (@t227)) % 0.38/0.75 (step @p278 :rule nary_cong :premises (@p277 @p276 @p275) :args ((or @t227 (not @t108) @t226))) % 0.38/0.75 (step @p279 :rule cnf_and_neg :args (@t227)) % 0.38/0.75 (step @p280 :rule eq_resolve :premises (@p279 @p278)) % 0.38/0.75 (step @p281 :rule reordering :premises (@p280) :args ((or @t107 @t226 @t227))) % 0.38/0.75 (step @p282 :rule instantiate :premises (@p31) :args (@t210)) % 0.38/0.75 (step @p283 :rule cnf_equiv_pos2 :args (@t228)) % 0.38/0.75 (step @p284 :rule reordering :premises (@p283) :args ((or @t189 (not @t227) (not @t228)))) % 0.38/0.75 (step @p285 :rule bool-double-not-elim :args (@t113)) % 0.38/0.75 (step @p286 :rule refl :args (@t229)) % 0.38/0.75 (step @p287 :rule refl :args (@t230)) % 0.38/0.75 (step @p288 :rule nary_cong :premises (@p287 @p286 @p285) :args ((or @t230 @t229 (not @t114)))) % 0.38/0.75 (step @p289 :rule cnf_and_neg :args (@t230)) % 0.38/0.75 (step @p290 :rule eq_resolve :premises (@p289 @p288)) % 0.38/0.75 (step @p291 :rule reordering :premises (@p290) :args ((or @t113 @t229 @t230))) % 0.38/0.75 (step @p292 :rule alpha_equiv :args (@t231 @t232 (@list @t233))) % 0.38/0.75 (step @p293 :rule alpha_equiv :args (@t234 @t232 (@list @t235))) % 0.38/0.75 (step @p294 :rule nary_cong :premises (@p293 @p292) :args (@t236)) % 0.38/0.75 (step @p295 :rule quant-miniscope-and :args ((= @t5 @t236))) % 0.38/0.75 (step @p296 :rule trans :premises (@p295 @p294)) % 0.38/0.75 (step @p297 :rule eq_resolve :premises (@p1 @p296)) % 0.38/0.75 (step @p298 :rule and_elim :premises (@p297) :args (0)) % 0.38/0.75 (step @p299 :rule and_elim :premises (@p297) :args (1)) % 0.38/0.75 (step @p300 :rule instantiate :premises (@p28) :args ((@list tptp.iV16465))) % 0.38/0.75 (step @p301 :rule refl :args (@t237)) % 0.38/0.75 (step @p302 :rule bool-double-not-elim :args (@t166)) % 0.38/0.75 (step @p303 :rule refl :args (@t238)) % 0.38/0.75 (step @p304 :rule nary_cong :premises (@p303 @p302 @p301) :args ((or @t238 (not @t167) @t237))) % 0.38/0.75 (step @p305 :rule cnf_and_neg :args (@t238)) % 0.38/0.75 (step @p306 :rule eq_resolve :premises (@p305 @p304)) % 0.38/0.75 (step @p307 :rule reordering :premises (@p306) :args ((or @t166 @t237 @t238))) % 0.38/0.75 (step @p308 :rule chain_m_resolution :premises (@p307 @p196 @p197) :args (@t238 @t214 (@list @t166 @t168))) % 0.38/0.75 (step @p309 :rule cnf_equiv_pos2 :args (@t239)) % 0.38/0.75 (step @p310 :rule reordering :premises (@p309) :args ((or @t170 (not @t238) (not @t239)))) % 0.38/0.75 (step @p311 :rule chain_m_resolution :premises (@p310 @p308 @p300) :args (@t170 @t240 (@list @t238 @t239))) % 0.38/0.75 (step @p312 :rule instantiate :premises (@p31) :args (@t241)) % 0.38/0.75 (step @p313 :rule instantiate :premises (@p37) :args (@t241)) % 0.38/0.75 (step @p314 :rule bool-impl-elim :args (@t155 @t50)) % 0.38/0.75 (step @p315 :rule cong :premises (@p314) :args (@t156)) % 0.38/0.75 (step @p316 :rule eq_resolve :premises (@p172 @p315)) % 0.38/0.75 (step @p317 :rule instantiate :premises (@p316) :args (@t241)) % 0.38/0.75 (step @p318 :rule cnf_or_pos :args (@t243)) % 0.38/0.75 (step @p319 :rule reordering :premises (@p318) :args ((or @t172 @t242 (not @t243)))) % 0.38/0.75 (step @p320 :rule chain_m_resolution :premises (@p319 @p178 @p317) :args (@t172 @t240 (@list @t160 @t243))) % 0.38/0.75 (step @p321 :rule cnf_equiv_pos1 :args (@t245)) % 0.38/0.75 (step @p322 :rule reordering :premises (@p321) :args ((or @t246 @t244 (not @t245)))) % 0.38/0.75 (step @p323 :rule chain_m_resolution :premises (@p322 @p320 @p313) :args (@t244 @t240 (@list @t172 @t245))) % 0.38/0.75 (step @p324 :rule cnf_and_pos :args (@t244 0)) % 0.38/0.75 (step @p325 :rule reordering :premises (@p324) :args ((or @t173 (not @t244)))) % 0.38/0.75 (step @p326 :rule chain_m_resolution :premises (@p325 @p323) :args (@t173 @t247 (@list @t244))) % 0.38/0.75 (step @p327 :rule cnf_equiv_pos1 :args (@t249)) % 0.38/0.75 (step @p328 :rule reordering :premises (@p327) :args ((or @t250 @t248 (not @t249)))) % 0.38/0.75 (step @p329 :rule chain_m_resolution :premises (@p328 @p326 @p312) :args (@t248 @t240 (@list @t173 @t249))) % 0.38/0.75 (step @p330 :rule cnf_and_pos :args (@t248 1)) % 0.38/0.75 (step @p331 :rule reordering :premises (@p330) :args ((or @t171 (not @t248)))) % 0.38/0.75 (step @p332 :rule chain_m_resolution :premises (@p331 @p329) :args (@t171 @t247 (@list @t248))) % 0.38/0.75 (step @p333 :rule instantiate :premises (@p41) :args (@t251)) % 0.38/0.75 (step @p334 :rule instantiate :premises (@p48) :args (@t251)) % 0.38/0.75 (step @p335 :rule bool-impl-elim :args (@t86 @t67)) % 0.38/0.75 (step @p336 :rule cong :premises (@p335) :args (@t87)) % 0.38/0.75 (step @p337 :rule eq_resolve :premises (@p68 @p336)) % 0.38/0.75 (step @p338 :rule instantiate :premises (@p337) :args (@t251)) % 0.38/0.75 (step @p339 :rule cnf_or_pos :args (@t253)) % 0.38/0.75 (step @p340 :rule reordering :premises (@p339) :args ((or @t175 @t252 (not @t253)))) % 0.38/0.75 (step @p341 :rule chain_m_resolution :premises (@p340 @p74 @p338) :args (@t175 @t240 (@list @t91 @t253))) % 0.38/0.75 (step @p342 :rule cnf_equiv_pos1 :args (@t255)) % 0.38/0.75 (step @p343 :rule reordering :premises (@p342) :args ((or @t256 @t254 (not @t255)))) % 0.38/0.75 (step @p344 :rule chain_m_resolution :premises (@p343 @p341 @p334) :args (@t254 @t240 (@list @t175 @t255))) % 0.38/0.75 (step @p345 :rule cnf_and_pos :args (@t254 1)) % 0.38/0.75 (step @p346 :rule reordering :premises (@p345) :args ((or @t176 (not @t254)))) % 0.38/0.75 (step @p347 :rule chain_m_resolution :premises (@p346 @p344) :args (@t176 @t247 (@list @t254))) % 0.38/0.75 (step @p348 :rule cnf_equiv_pos1 :args (@t258)) % 0.38/0.75 (step @p349 :rule reordering :premises (@p348) :args ((or @t259 @t257 (not @t258)))) % 0.38/0.75 (step @p350 :rule chain_m_resolution :premises (@p349 @p347 @p333) :args (@t257 @t240 (@list @t176 @t258))) % 0.38/0.75 (step @p351 :rule cnf_and_pos :args (@t257 0)) % 0.38/0.75 (step @p352 :rule reordering :premises (@p351) :args ((or @t174 (not @t257)))) % 0.38/0.75 (step @p353 :rule chain_m_resolution :premises (@p352 @p350) :args (@t174 @t247 (@list @t257))) % 0.38/0.75 (step @p354 :rule instantiate :premises (@p28) :args ((@list tptp.iV16462))) % 0.38/0.75 (step @p355 :rule refl :args (@t260)) % 0.38/0.75 (step @p356 :rule bool-double-not-elim :args (@t151)) % 0.38/0.75 (step @p357 :rule refl :args (@t261)) % 0.38/0.75 (step @p358 :rule nary_cong :premises (@p357 @p356 @p355) :args ((or @t261 (not @t152) @t260))) % 0.38/0.75 (step @p359 :rule cnf_and_neg :args (@t261)) % 0.38/0.75 (step @p360 :rule eq_resolve :premises (@p359 @p358)) % 0.38/0.75 (step @p361 :rule reordering :premises (@p360) :args ((or @t151 @t260 @t261))) % 0.38/0.75 (step @p362 :rule chain_m_resolution :premises (@p361 @p162 @p163) :args (@t261 @t214 (@list @t151 @t153))) % 0.38/0.75 (step @p363 :rule cnf_equiv_pos2 :args (@t262)) % 0.38/0.75 (step @p364 :rule reordering :premises (@p363) :args ((or @t177 (not @t261) (not @t262)))) % 0.38/0.75 (step @p365 :rule chain_m_resolution :premises (@p364 @p362 @p354) :args (@t177 @t240 (@list @t261 @t262))) % 0.38/0.75 (step @p366 :rule instantiate :premises (@p31) :args (@t263)) % 0.38/0.75 (step @p367 :rule instantiate :premises (@p37) :args (@t263)) % 0.38/0.75 (step @p368 :rule bool-impl-elim :args (@t98 @t50)) % 0.38/0.75 (step @p369 :rule cong :premises (@p368) :args (@t104)) % 0.38/0.75 (step @p370 :rule eq_resolve :premises (@p94 @p369)) % 0.38/0.75 (step @p371 :rule instantiate :premises (@p370) :args (@t263)) % 0.38/0.75 (step @p372 :rule cnf_or_pos :args (@t265)) % 0.38/0.75 (step @p373 :rule reordering :premises (@p372) :args ((or @t179 @t264 (not @t265)))) % 0.38/0.75 (step @p374 :rule chain_m_resolution :premises (@p373 @p97 @p371) :args (@t179 @t240 (@list @t106 @t265))) % 0.38/0.75 (step @p375 :rule cnf_equiv_pos1 :args (@t267)) % 0.38/0.75 (step @p376 :rule reordering :premises (@p375) :args ((or @t268 @t266 (not @t267)))) % 0.38/0.75 (step @p377 :rule chain_m_resolution :premises (@p376 @p374 @p367) :args (@t266 @t240 (@list @t179 @t267))) % 0.38/0.75 (step @p378 :rule cnf_and_pos :args (@t266 0)) % 0.38/0.75 (step @p379 :rule reordering :premises (@p378) :args ((or @t180 (not @t266)))) % 0.38/0.76 (step @p380 :rule chain_m_resolution :premises (@p379 @p377) :args (@t180 @t247 (@list @t266))) % 0.38/0.76 (step @p381 :rule cnf_equiv_pos1 :args (@t270)) % 0.38/0.76 (step @p382 :rule reordering :premises (@p381) :args ((or @t271 @t269 (not @t270)))) % 0.38/0.76 (step @p383 :rule chain_m_resolution :premises (@p382 @p380 @p366) :args (@t269 @t240 (@list @t180 @t270))) % 0.38/0.76 (step @p384 :rule cnf_and_pos :args (@t269 1)) % 0.38/0.76 (step @p385 :rule reordering :premises (@p384) :args ((or @t178 (not @t269)))) % 0.38/0.76 (step @p386 :rule chain_m_resolution :premises (@p385 @p383) :args (@t178 @t247 (@list @t269))) % 0.38/0.76 (step @p387 :rule instantiate :premises (@p28) :args (@t216)) % 0.38/0.76 (step @p388 :rule refl :args (@t272)) % 0.38/0.76 (step @p389 :rule bool-double-not-elim :args (@t139)) % 0.38/0.76 (step @p390 :rule refl :args (@t273)) % 0.38/0.76 (step @p391 :rule nary_cong :premises (@p390 @p389 @p388) :args ((or @t273 (not @t140) @t272))) % 0.38/0.76 (step @p392 :rule cnf_and_neg :args (@t273)) % 0.38/0.76 (step @p393 :rule eq_resolve :premises (@p392 @p391)) % 0.38/0.76 (step @p394 :rule reordering :premises (@p393) :args ((or @t139 @t272 @t273))) % 0.38/0.76 (step @p395 :rule chain_m_resolution :premises (@p394 @p138 @p141) :args (@t273 @t214 (@list @t139 @t142))) % 0.38/0.76 (step @p396 :rule cnf_equiv_pos2 :args (@t274)) % 0.38/0.76 (step @p397 :rule reordering :premises (@p396) :args ((or @t181 (not @t273) (not @t274)))) % 0.38/0.76 (step @p398 :rule chain_m_resolution :premises (@p397 @p395 @p387) :args (@t181 @t240 (@list @t273 @t274))) % 0.38/0.76 (step @p399 :rule instantiate :premises (@p26) :args (@t275)) % 0.38/0.76 (step @p400 :rule bool-double-not-elim :args (@t124)) % 0.38/0.76 (step @p401 :rule bool-double-not-elim :args (@t137)) % 0.38/0.76 (step @p402 :rule refl :args (@t276)) % 0.38/0.76 (step @p403 :rule nary_cong :premises (@p402 @p401 @p400) :args ((or @t276 (not @t138) (not @t125)))) % 0.38/0.76 (step @p404 :rule cnf_and_neg :args (@t276)) % 0.38/0.76 (step @p405 :rule eq_resolve :premises (@p404 @p403)) % 0.38/0.76 (step @p406 :rule reordering :premises (@p405) :args ((or @t124 @t137 @t276))) % 0.38/0.76 (step @p407 :rule chain_m_resolution :premises (@p406 @p122 @p136) :args (@t276 @t277 (@list @t124 @t137))) % 0.38/0.76 (step @p408 :rule cnf_equiv_pos2 :args (@t278)) % 0.38/0.76 (step @p409 :rule reordering :premises (@p408) :args ((or @t182 (not @t276) (not @t278)))) % 0.38/0.76 (step @p410 :rule chain_m_resolution :premises (@p409 @p407 @p399) :args (@t182 @t240 (@list @t276 @t278))) % 0.38/0.76 (step @p411 :rule instantiate :premises (@p34) :args (@t275)) % 0.38/0.76 (step @p412 :rule bool-double-not-elim :args (@t122)) % 0.38/0.76 (step @p413 :rule bool-double-not-elim :args (@t128)) % 0.38/0.76 (step @p414 :rule refl :args (@t279)) % 0.38/0.76 (step @p415 :rule nary_cong :premises (@p414 @p413 @p412) :args ((or @t279 (not @t129) (not @t123)))) % 0.38/0.76 (step @p416 :rule cnf_and_neg :args (@t279)) % 0.38/0.76 (step @p417 :rule eq_resolve :premises (@p416 @p415)) % 0.38/0.76 (step @p418 :rule reordering :premises (@p417) :args ((or @t122 @t128 @t279))) % 0.38/0.76 (step @p419 :rule chain_m_resolution :premises (@p418 @p121 @p125) :args (@t279 @t277 (@list @t122 @t128))) % 0.38/0.76 (step @p420 :rule cnf_equiv_pos2 :args (@t280)) % 0.38/0.76 (step @p421 :rule reordering :premises (@p420) :args ((or @t183 (not @t279) (not @t280)))) % 0.38/0.76 (step @p422 :rule chain_m_resolution :premises (@p421 @p419 @p411) :args (@t183 @t240 (@list @t279 @t280))) % 0.38/0.76 (step @p423 :rule instantiate :premises (@p54) :args (@t275)) % 0.38/0.76 (step @p424 :rule bool-double-not-elim :args (@t126)) % 0.38/0.76 (step @p425 :rule bool-double-not-elim :args (@t132)) % 0.38/0.76 (step @p426 :rule refl :args (@t281)) % 0.38/0.76 (step @p427 :rule nary_cong :premises (@p426 @p425 @p424) :args ((or @t281 (not @t133) (not @t127)))) % 0.38/0.76 (step @p428 :rule cnf_and_neg :args (@t281)) % 0.38/0.76 (step @p429 :rule eq_resolve :premises (@p428 @p427)) % 0.38/0.76 (step @p430 :rule reordering :premises (@p429) :args ((or @t126 @t132 @t281))) % 0.38/0.76 (step @p431 :rule chain_m_resolution :premises (@p430 @p124 @p133) :args (@t281 @t277 (@list @t126 @t132))) % 0.38/0.76 (step @p432 :rule cnf_equiv_pos2 :args (@t282)) % 0.38/0.76 (step @p433 :rule reordering :premises (@p432) :args ((or @t184 (not @t281) (not @t282)))) % 0.38/0.76 (step @p434 :rule chain_m_resolution :premises (@p433 @p431 @p423) :args (@t184 @t240 (@list @t281 @t282))) % 0.38/0.76 (step @p435 :rule instantiate :premises (@p44) :args (@t275)) % 0.38/0.76 (step @p436 :rule bool-double-not-elim :args (@t130)) % 0.38/0.76 (step @p437 :rule bool-double-not-elim :args (@t134)) % 0.38/0.76 (step @p438 :rule refl :args (@t283)) % 0.38/0.76 (step @p439 :rule nary_cong :premises (@p438 @p437 @p436) :args ((or @t283 (not @t135) (not @t131)))) % 0.38/0.76 (step @p440 :rule cnf_and_neg :args (@t283)) % 0.38/0.76 (step @p441 :rule eq_resolve :premises (@p440 @p439)) % 0.38/0.76 (step @p442 :rule reordering :premises (@p441) :args ((or @t130 @t134 @t283))) % 0.38/0.76 (step @p443 :rule chain_m_resolution :premises (@p442 @p128 @p134) :args (@t283 @t277 (@list @t130 @t134))) % 0.38/0.76 (step @p444 :rule cnf_equiv_pos2 :args (@t284)) % 0.38/0.76 (step @p445 :rule reordering :premises (@p444) :args ((or @t185 (not @t283) (not @t284)))) % 0.38/0.76 (step @p446 :rule chain_m_resolution :premises (@p445 @p443 @p435) :args (@t185 @t240 (@list @t283 @t284))) % 0.38/0.76 (step @p447 :rule instantiate :premises (@p28) :args ((@list tptp.iV16457))) % 0.38/0.76 (step @p448 :rule refl :args (@t285)) % 0.38/0.76 (step @p449 :rule bool-double-not-elim :args (@t117)) % 0.38/0.76 (step @p450 :rule refl :args (@t286)) % 0.38/0.76 (step @p451 :rule nary_cong :premises (@p450 @p449 @p448) :args ((or @t286 (not @t118) @t285))) % 0.38/0.76 (step @p452 :rule cnf_and_neg :args (@t286)) % 0.38/0.76 (step @p453 :rule eq_resolve :premises (@p452 @p451)) % 0.38/0.76 (step @p454 :rule reordering :premises (@p453) :args ((or @t117 @t285 @t286))) % 0.38/0.76 (step @p455 :rule chain_m_resolution :premises (@p454 @p109 @p114) :args (@t286 @t214 (@list @t117 @t120))) % 0.38/0.76 (step @p456 :rule cnf_equiv_pos2 :args (@t287)) % 0.38/0.76 (step @p457 :rule reordering :premises (@p456) :args ((or @t186 (not @t286) (not @t287)))) % 0.38/0.76 (step @p458 :rule chain_m_resolution :premises (@p457 @p455 @p447) :args (@t186 @t240 (@list @t286 @t287))) % 0.38/0.76 (step @p459 :rule instantiate :premises (@p51) :args (@t288)) % 0.38/0.76 (step @p460 :rule instantiate :premises (@p59) :args (@t288)) % 0.38/0.76 (step @p461 :rule bool-impl-elim :args (@t80 @t79)) % 0.38/0.76 (step @p462 :rule cong :premises (@p461) :args (@t81)) % 0.38/0.76 (step @p463 :rule eq_resolve :premises (@p61 @p462)) % 0.38/0.76 (step @p464 :rule instantiate :premises (@p463) :args (@t288)) % 0.38/0.76 (step @p465 :rule cnf_or_pos :args (@t290)) % 0.38/0.76 (step @p466 :rule reordering :premises (@p465) :args ((or @t194 @t289 (not @t290)))) % 0.38/0.76 (step @p467 :rule chain_m_resolution :premises (@p466 @p65 @p464) :args (@t194 @t240 (@list @t85 @t290))) % 0.38/0.76 (step @p468 :rule cnf_equiv_pos1 :args (@t292)) % 0.38/0.76 (step @p469 :rule reordering :premises (@p468) :args ((or @t293 @t291 (not @t292)))) % 0.38/0.76 (step @p470 :rule chain_m_resolution :premises (@p469 @p467 @p460) :args (@t291 @t240 (@list @t194 @t292))) % 0.38/0.76 (step @p471 :rule cnf_and_pos :args (@t291 1)) % 0.38/0.76 (step @p472 :rule reordering :premises (@p471) :args ((or @t195 (not @t291)))) % 0.38/0.76 (step @p473 :rule chain_m_resolution :premises (@p472 @p470) :args (@t195 @t247 (@list @t291))) % 0.38/0.76 (step @p474 :rule cnf_equiv_pos1 :args (@t295)) % 0.38/0.76 (step @p475 :rule reordering :premises (@p474) :args ((or @t296 @t294 (not @t295)))) % 0.38/0.76 (step @p476 :rule chain_m_resolution :premises (@p475 @p473 @p459) :args (@t294 @t240 (@list @t195 @t295))) % 0.38/0.76 (step @p477 :rule cnf_and_pos :args (@t294 1)) % 0.38/0.76 (step @p478 :rule reordering :premises (@p477) :args ((or @t196 (not @t294)))) % 0.38/0.76 (step @p479 :rule chain_m_resolution :premises (@p478 @p476) :args (@t196 @t247 (@list @t294))) % 0.38/0.76 (step @p480 :rule instantiate :premises (@p6) :args (@t297)) % 0.38/0.76 (step @p481 :rule instantiate :premises (@p7) :args (@t297)) % 0.38/0.76 (step @p482 :rule instantiate :premises (@p60) :args (@t297)) % 0.38/0.76 (step @p483 :rule cnf_equiv_pos1 :args (@t299)) % 0.38/0.76 (step @p484 :rule reordering :premises (@p483) :args ((or (not @t82) @t298 (not @t299)))) % 0.38/0.76 (step @p485 :rule chain_m_resolution :premises (@p484 @p62 @p482) :args (@t298 @t240 (@list @t82 @t299))) % 0.38/0.76 (step @p486 :rule cnf_and_pos :args (@t298 0)) % 0.38/0.76 (step @p487 :rule reordering :premises (@p486) :args ((or @t198 @t300))) % 0.38/0.76 (step @p488 :rule chain_m_resolution :premises (@p487 @p485) :args (@t198 @t247 @t301)) % 0.38/0.76 (step @p489 :rule cnf_equiv_pos1 :args (@t303)) % 0.38/0.76 (step @p490 :rule reordering :premises (@p489) :args ((or @t304 @t302 (not @t303)))) % 0.38/0.76 (step @p491 :rule chain_m_resolution :premises (@p490 @p488 @p481) :args (@t302 @t240 (@list @t198 @t303))) % 0.38/0.76 (step @p492 :rule cnf_and_pos :args (@t302 1)) % 0.38/0.76 (step @p493 :rule reordering :premises (@p492) :args ((or @t201 @t305))) % 0.38/0.76 (step @p494 :rule chain_m_resolution :premises (@p493 @p491) :args (@t201 @t247 @t306)) % 0.38/0.76 (step @p495 :rule cnf_equiv_pos1 :args (@t308)) % 0.38/0.76 (step @p496 :rule reordering :premises (@p495) :args ((or @t309 @t307 (not @t308)))) % 0.38/0.76 (step @p497 :rule chain_m_resolution :premises (@p496 @p494 @p480) :args (@t307 @t240 (@list @t201 @t308))) % 0.38/0.76 (step @p498 :rule cnf_and_pos :args (@t307 1)) % 0.38/0.76 (step @p499 :rule reordering :premises (@p498) :args ((or @t197 (not @t307)))) % 0.38/0.76 (step @p500 :rule chain_m_resolution :premises (@p499 @p497) :args (@t197 @t247 (@list @t307))) % 0.38/0.76 (step @p501 :rule instantiate :premises (@p28) :args ((@list tptp.iV16448))) % 0.38/0.76 (step @p502 :rule refl :args (@t310)) % 0.38/0.76 (step @p503 :rule bool-double-not-elim :args (@t92)) % 0.38/0.76 (step @p504 :rule refl :args (@t311)) % 0.38/0.76 (step @p505 :rule nary_cong :premises (@p504 @p503 @p502) :args ((or @t311 (not @t93) @t310))) % 0.38/0.76 (step @p506 :rule cnf_and_neg :args (@t311)) % 0.38/0.76 (step @p507 :rule eq_resolve :premises (@p506 @p505)) % 0.38/0.76 (step @p508 :rule reordering :premises (@p507) :args ((or @t92 @t310 @t311))) % 0.38/0.76 (step @p509 :rule chain_m_resolution :premises (@p508 @p77 @p80) :args (@t311 @t214 (@list @t92 @t95))) % 0.38/0.76 (step @p510 :rule cnf_equiv_pos2 :args (@t312)) % 0.38/0.76 (step @p511 :rule reordering :premises (@p510) :args ((or @t193 (not @t311) (not @t312)))) % 0.38/0.76 (step @p512 :rule chain_m_resolution :premises (@p511 @p509 @p501) :args (@t193 @t240 (@list @t311 @t312))) % 0.38/0.76 (step @p513 :rule cnf_and_pos :args (@t302 0)) % 0.38/0.76 (step @p514 :rule reordering :premises (@p513) :args ((or @t200 @t305))) % 0.38/0.76 (step @p515 :rule chain_m_resolution :premises (@p514 @p491) :args (@t200 @t247 @t306)) % 0.38/0.76 (step @p516 :rule cnf_and_pos :args (@t298 1)) % 0.38/0.76 (step @p517 :rule reordering :premises (@p516) :args ((or @t199 @t300))) % 0.38/0.76 (step @p518 :rule chain_m_resolution :premises (@p517 @p485) :args (@t199 @t247 @t301)) % 0.38/0.76 (step @p519 :rule aci_norm :args ((= (and (and @t314 @t313) @t6 @t201 @t200 @t199 @t84 @t198 @t197 @t196 @t90 @t195 @t194 @t96 @t193 @t192 @t105 @t191 @t190 @t189 @t115 @t188 @t187 @t121 @t186 @t185 @t136 @t184 @t183 @t182 @t144 @t181 @t180 @t149 @t179 @t178 @t154 @t177 @t176 @t159 @t175 @t174 @t173 @t164 @t172 @t171 @t169 @t170) (and @t6 @t201 @t200 @t199 @t84 @t198 @t197 @t196 @t90 @t195 @t194 @t96 @t193 @t192 @t105 @t191 @t190 @t189 @t115 @t188 @t187 @t121 @t186 @t185 @t136 @t184 @t183 @t182 @t144 @t181 @t180 @t149 @t179 @t178 @t154 @t177 @t176 @t159 @t175 @t174 @t173 @t164 @t172 @t171 @t169 @t170 @t314 @t313)))) % 0.38/0.76 (step @p520 :rule refl :args (@t170)) % 0.38/0.76 (step @p521 :rule refl :args (@t169)) % 0.38/0.76 (step @p522 :rule refl :args (@t171)) % 0.38/0.76 (step @p523 :rule refl :args (@t172)) % 0.38/0.76 (step @p524 :rule refl :args (@t164)) % 0.38/0.76 (step @p525 :rule refl :args (@t173)) % 0.38/0.76 (step @p526 :rule refl :args (@t174)) % 0.38/0.76 (step @p527 :rule refl :args (@t175)) % 0.38/0.76 (step @p528 :rule refl :args (@t159)) % 0.38/0.76 (step @p529 :rule refl :args (@t176)) % 0.38/0.76 (step @p530 :rule refl :args (@t177)) % 0.38/0.76 (step @p531 :rule refl :args (@t154)) % 0.38/0.76 (step @p532 :rule refl :args (@t178)) % 0.38/0.76 (step @p533 :rule refl :args (@t179)) % 0.38/0.76 (step @p534 :rule refl :args (@t149)) % 0.38/0.76 (step @p535 :rule refl :args (@t180)) % 0.38/0.76 (step @p536 :rule refl :args (@t181)) % 0.38/0.76 (step @p537 :rule refl :args (@t144)) % 0.38/0.76 (step @p538 :rule refl :args (@t182)) % 0.38/0.76 (step @p539 :rule refl :args (@t183)) % 0.38/0.76 (step @p540 :rule refl :args (@t184)) % 0.38/0.76 (step @p541 :rule refl :args (@t136)) % 0.38/0.76 (step @p542 :rule refl :args (@t185)) % 0.38/0.76 (step @p543 :rule refl :args (@t186)) % 0.38/0.76 (step @p544 :rule refl :args (@t121)) % 0.38/0.76 (step @p545 :rule refl :args (@t188)) % 0.38/0.76 (step @p546 :rule refl :args (@t115)) % 0.38/0.76 (step @p547 :rule refl :args (@t189)) % 0.38/0.76 (step @p548 :rule refl :args (@t190)) % 0.38/0.76 (step @p549 :rule refl :args (@t191)) % 0.38/0.76 (step @p550 :rule refl :args (@t105)) % 0.38/0.76 (step @p551 :rule refl :args (@t192)) % 0.38/0.76 (step @p552 :rule refl :args (@t193)) % 0.38/0.76 (step @p553 :rule refl :args (@t96)) % 0.38/0.76 (step @p554 :rule refl :args (@t194)) % 0.38/0.76 (step @p555 :rule refl :args (@t195)) % 0.38/0.76 (step @p556 :rule refl :args (@t90)) % 0.38/0.76 (step @p557 :rule refl :args (@t196)) % 0.38/0.76 (step @p558 :rule refl :args (@t197)) % 0.38/0.76 (step @p559 :rule refl :args (@t198)) % 0.38/0.76 (step @p560 :rule refl :args (@t84)) % 0.38/0.76 (step @p561 :rule refl :args (@t199)) % 0.38/0.76 (step @p562 :rule refl :args (@t200)) % 0.38/0.76 (step @p563 :rule refl :args (@t201)) % 0.38/0.76 (step @p564 :rule refl :args (@t6)) % 0.38/0.76 (step @p565 :rule nary_cong :premises (@p296 @p564 @p563 @p562 @p561 @p560 @p559 @p558 @p557 @p556 @p555 @p554 @p553 @p552 @p551 @p550 @p549 @p548 @p547 @p546 @p545 @p240 @p544 @p543 @p542 @p541 @p540 @p539 @p538 @p537 @p536 @p535 @p534 @p533 @p532 @p531 @p530 @p529 @p528 @p527 @p526 @p525 @p524 @p523 @p522 @p521 @p520) :args (@t202)) % 0.38/0.76 (step @p566 :rule trans :premises (@p565 @p519)) % 0.38/0.76 (step @p567 :rule cong :premises (@p566) :args (@t203)) % 0.38/0.76 (step @p568 :rule eq_resolve :premises (@p201 @p567)) % 0.38/0.76 (step @p569 :rule not_and :premises (@p568)) % 0.38/0.76 (step @p570 :rule reordering :premises (@p569) :args ((or (not @t314) (not @t313) (not @t6) (not @t84) (not @t90) (not @t96) (not @t105) (not @t115) (not @t121) (not @t136) (not @t144) (not @t149) (not @t154) (not @t159) (not @t164) (not @t169) @t309 (not @t200) (not @t199) @t304 (not @t197) (not @t196) @t296 @t293 (not @t193) @t223 (not @t191) @t220 @t229 (not @t188) @t226 (not @t186) (not @t185) (not @t184) (not @t183) (not @t182) (not @t181) @t271 @t268 (not @t178) (not @t177) @t259 @t256 (not @t174) @t250 @t246 (not @t171) (not @t170)))) % 0.38/0.76 (step @p571 :rule instantiate :premises (@p37) :args (@t210)) % 0.38/0.76 (step @p572 :rule cnf_equiv_pos2 :args (@t315)) % 0.38/0.76 (step @p573 :rule reordering :premises (@p572) :args ((or @t188 (not @t230) (not @t315)))) % 0.38/0.76 (step @p574 :rule chain_m_resolution :premises (@p573 @p571 @p570 @p518 @p488 @p515 @p494 @p473 @p467 @p512 @p500 @p479 @p458 @p446 @p434 @p422 @p410 @p398 @p380 @p374 @p386 @p365 @p347 @p341 @p353 @p326 @p320 @p332 @p311 @p199 @p188 @p177 @p169 @p156 @p147 @p135 @p118 @p106 @p95 @p85 @p73 @p64 @p2 @p299 @p298 @p291 @p104 @p284 @p282 @p281 @p99 @p274 @p272 @p48 @p267 @p93 @p260 @p258 @p41 @p253 @p92) :args ((or @t220 @t226) (@list false true false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false true false false false true false false false false true false false false false true) (@list @t315 @t188 @t199 @t198 @t200 @t201 @t195 @t194 @t193 @t197 @t196 @t186 @t185 @t184 @t183 @t182 @t181 @t180 @t179 @t178 @t177 @t176 @t175 @t174 @t173 @t172 @t171 @t170 @t169 @t164 @t159 @t154 @t149 @t144 @t136 @t121 @t115 @t105 @t96 @t90 @t84 @t6 @t313 @t314 @t230 @t113 @t189 @t228 @t227 @t107 @t191 @t225 @t68 @t224 @t102 @t192 @t222 @t60 @t221 @t100))) % 0.38/0.76 (step @p575 :rule chain_m_resolution :premises (@p574 @p246) :args (@t220 @t247 (@list @t187))) % 0.38/0.76 (step @p576 :rule bool-double-not-elim :args (@t316)) % 0.38/0.76 (step @p577 :rule refl :args (@t319)) % 0.38/0.76 (step @p578 :rule nary_cong :premises (@p577 @p548 @p576) :args ((or @t319 @t190 (not @t317)))) % 0.38/0.76 (step @p579 :rule cnf_equiv_pos2 :args (@t318)) % 0.38/0.76 (step @p580 :rule eq_resolve :premises (@p579 @p578)) % 0.38/0.76 (step @p581 :rule reordering :premises (@p580) :args ((or @t190 @t316 @t319))) % 0.38/0.76 (step @p582 :rule chain_m_resolution :premises (@p581 @p575 @p216) :args (@t316 @t214 (@list @t190 @t318))) % 0.38/0.76 (step @p583 :rule cnf_or_pos :args (@t320)) % 0.38/0.76 (step @p584 :rule reordering :premises (@p583) :args ((or @t147 @t264 @t321))) % 0.38/0.76 (step @p585 :rule chain_m_resolution :premises (@p584 @p152 @p97) :args (@t321 @t214 (@list @t147 @t106))) % 0.38/0.76 (assume-push @p598 @t316) % 0.38/0.76 (step @p587 :rule instantiate :premises (@p598) :args (@t263)) % 0.38/0.76 (step-pop @p599 :rule scope :premises (@p587)) % 0.38/0.76 (step @p588 :rule process_scope :premises (@p599) :args (@t320)) % 0.38/0.76 (step @p590 :rule implies_elim :premises (@p588)) % 0.38/0.76 (step @p591 false :rule chain_m_resolution :premises (@p590 @p585 @p582) :args (false @t214 (@list @t320 @t316))) % 0.38/0.76 ) % 0.38/0.76 % SZS output end Proof % 0.38/0.76 % cvc5 exiting %------------------------------------------------------------------------------