%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : NLP004-1 : TPTP v9.2.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n021.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:36:15 AM UTC 2026 % Result : Unsatisfiable 0.32s 0.55s % Output : Proof 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NLP004-1 : TPTP v9.2.1. Released v2.4.0. % 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.16/0.33 % Computer : n021.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue Jun 2 09:52:50 EDT 2026 % 0.16/0.34 % CPUTime : % 0.32/0.48 %----Proving TF0_NAR, FOF, or CNF % 0.32/0.50 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.32/0.55 % SZS status Unsatisfiable % 0.32/0.55 % SZS output start Proof % 0.38/0.57 ( % 0.38/0.57 (declare-sort $$unsorted 0) % 0.38/0.57 (declare-const tptp.barrel (-> $$unsorted $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.furniture (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.in (-> $$unsorted $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.city (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.down (-> $$unsorted $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.way (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.dirty (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc26 $$unsorted) % 0.38/0.57 (declare-const tptp.front (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.ssSkC0 Bool) % 0.38/0.57 (declare-const tptp.skc27 $$unsorted) % 0.38/0.57 (declare-const tptp.man (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.old (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc28 $$unsorted) % 0.38/0.57 (declare-const tptp.skc17 $$unsorted) % 0.38/0.57 (declare-const tptp.skc29 $$unsorted) % 0.38/0.57 (declare-const tptp.skc31 $$unsorted) % 0.38/0.57 (declare-const tptp.event (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.seat (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.car (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc30 $$unsorted) % 0.38/0.57 (declare-const tptp.lonely (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.street (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc18 $$unsorted) % 0.38/0.57 (declare-const tptp.hollywood (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc25 $$unsorted) % 0.38/0.57 (declare-const tptp.fellow (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.white (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc24 $$unsorted) % 0.38/0.57 (declare-const tptp.young (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc23 $$unsorted) % 0.38/0.57 (declare-const tptp.skc22 $$unsorted) % 0.38/0.57 (declare-const tptp.skc21 $$unsorted) % 0.38/0.57 (declare-const tptp.chevy (-> $$unsorted Bool)) % 0.38/0.57 (declare-const tptp.skc20 $$unsorted) % 0.38/0.57 (declare-const tptp.skc19 $$unsorted) % 0.38/0.57 (declare-const tptp.skc16 $$unsorted) % 0.38/0.57 (define @t1 () (tptp.hollywood tptp.skc31)) % 0.38/0.57 (define @t2 () (tptp.event tptp.skc30)) % 0.38/0.57 (define @t3 () (tptp.street tptp.skc29)) % 0.38/0.57 (define @t4 () (tptp.old tptp.skc28)) % 0.38/0.57 (define @t5 () (tptp.front tptp.skc27)) % 0.38/0.57 (define @t6 () (tptp.seat tptp.skc26)) % 0.38/0.57 (define @t7 () (tptp.fellow tptp.skc25)) % 0.38/0.57 (define @t8 () (tptp.young tptp.skc24)) % 0.38/0.57 (define @t9 () (tptp.hollywood tptp.skc23)) % 0.38/0.57 (define @t10 () (tptp.event tptp.skc22)) % 0.38/0.57 (define @t11 () (tptp.chevy tptp.skc21)) % 0.38/0.57 (define @t12 () (tptp.lonely tptp.skc20)) % 0.38/0.57 (define @t13 () (tptp.front tptp.skc19)) % 0.38/0.57 (define @t14 () (tptp.seat tptp.skc18)) % 0.38/0.57 (define @t15 () (tptp.fellow tptp.skc17)) % 0.38/0.57 (define @t16 () (tptp.young tptp.skc16)) % 0.38/0.57 (define @t17 () (tptp.chevy tptp.skc28)) % 0.38/0.57 (define @t18 () (tptp.car tptp.skc28)) % 0.38/0.57 (define @t19 () (tptp.white tptp.skc28)) % 0.38/0.57 (define @t20 () (tptp.dirty tptp.skc28)) % 0.38/0.57 (define @t21 () (tptp.lonely tptp.skc29)) % 0.38/0.57 (define @t22 () (tptp.way tptp.skc29)) % 0.38/0.57 (define @t23 () (tptp.city tptp.skc31)) % 0.38/0.57 (define @t24 () (tptp.seat tptp.skc27)) % 0.38/0.57 (define @t25 () (tptp.furniture tptp.skc27)) % 0.38/0.57 (define @t26 () (tptp.fellow tptp.skc24)) % 0.38/0.57 (define @t27 () (tptp.man tptp.skc24)) % 0.38/0.57 (define @t28 () (tptp.front tptp.skc26)) % 0.38/0.57 (define @t29 () (tptp.furniture tptp.skc26)) % 0.38/0.57 (define @t30 () (tptp.young tptp.skc25)) % 0.38/0.57 (define @t31 () (tptp.man tptp.skc25)) % 0.38/0.57 (define @t32 () (tptp.street tptp.skc20)) % 0.38/0.57 (define @t33 () (not tptp.ssSkC0)) % 0.38/0.57 (define @t34 () (tptp.way tptp.skc20)) % 0.38/0.57 (define @t35 () (tptp.old tptp.skc21)) % 0.38/0.57 (define @t36 () (tptp.dirty tptp.skc21)) % 0.38/0.57 (define @t37 () (tptp.white tptp.skc21)) % 0.38/0.57 (define @t38 () (tptp.car tptp.skc21)) % 0.38/0.57 (define @t39 () (tptp.city tptp.skc23)) % 0.38/0.57 (define @t40 () (tptp.seat tptp.skc19)) % 0.38/0.57 (define @t41 () (tptp.furniture tptp.skc19)) % 0.38/0.57 (define @t42 () (tptp.fellow tptp.skc16)) % 0.38/0.57 (define @t43 () (tptp.man tptp.skc16)) % 0.38/0.57 (define @t44 () (tptp.front tptp.skc18)) % 0.38/0.57 (define @t45 () (tptp.furniture tptp.skc18)) % 0.38/0.57 (define @t46 () (tptp.young tptp.skc17)) % 0.38/0.57 (define @t47 () (tptp.man tptp.skc17)) % 0.38/0.57 (define @t48 () (tptp.barrel tptp.skc30 tptp.skc28)) % 0.38/0.57 (define @t49 () (tptp.down tptp.skc30 tptp.skc29)) % 0.38/0.57 (define @t50 () (tptp.in tptp.skc30 tptp.skc31)) % 0.38/0.57 (define @t51 () (tptp.in tptp.skc24 tptp.skc27)) % 0.38/0.57 (define @t52 () (tptp.in tptp.skc25 tptp.skc26)) % 0.38/0.57 (define @t53 () (tptp.barrel tptp.skc22 tptp.skc21)) % 0.38/0.57 (define @t54 () (tptp.down tptp.skc22 tptp.skc20)) % 0.38/0.57 (define @t55 () (tptp.in tptp.skc22 tptp.skc23)) % 0.38/0.57 (define @t56 () (tptp.in tptp.skc16 tptp.skc19)) % 0.38/0.57 (define @t57 () (tptp.in tptp.skc17 tptp.skc18)) % 0.38/0.57 (define @t58 () (= tptp.skc25 tptp.skc24)) % 0.38/0.57 (define @t59 () (not @t58)) % 0.38/0.57 (define @t60 () (= tptp.skc17 tptp.skc16)) % 0.38/0.57 (define @t61 () (not @t60)) % 0.38/0.57 (define @t62 () (@var "Z" $$unsorted)) % 0.38/0.57 (define @t63 () (@var "X1" $$unsorted)) % 0.38/0.57 (define @t64 () (= @t63 @t62)) % 0.38/0.57 (define @t65 () (not (tptp.fellow @t63))) % 0.38/0.57 (define @t66 () (not (tptp.man @t63))) % 0.38/0.57 (define @t67 () (not (tptp.young @t63))) % 0.38/0.57 (define @t68 () (@var "X2" $$unsorted)) % 0.38/0.57 (define @t69 () (not (tptp.seat @t68))) % 0.38/0.57 (define @t70 () (not (tptp.furniture @t68))) % 0.38/0.57 (define @t71 () (not (tptp.front @t68))) % 0.38/0.57 (define @t72 () (not (tptp.in @t63 @t68))) % 0.38/0.57 (define @t73 () (not (tptp.young @t62))) % 0.38/0.57 (define @t74 () (not (tptp.man @t62))) % 0.38/0.57 (define @t75 () (not (tptp.fellow @t62))) % 0.38/0.57 (define @t76 () (@var "Y" $$unsorted)) % 0.38/0.57 (define @t77 () (not (tptp.in @t62 @t76))) % 0.38/0.57 (define @t78 () (not (tptp.front @t76))) % 0.38/0.57 (define @t79 () (not (tptp.furniture @t76))) % 0.38/0.57 (define @t80 () (not (tptp.seat @t76))) % 0.38/0.57 (define @t81 () (@var "X" $$unsorted)) % 0.38/0.57 (define @t82 () (not (tptp.hollywood @t81))) % 0.38/0.57 (define @t83 () (not (tptp.city @t81))) % 0.38/0.57 (define @t84 () (@var "W" $$unsorted)) % 0.38/0.57 (define @t85 () (not (tptp.in @t84 @t81))) % 0.38/0.57 (define @t86 () (@var "U" $$unsorted)) % 0.38/0.57 (define @t87 () (not (tptp.down @t84 @t86))) % 0.38/0.57 (define @t88 () (@var "V" $$unsorted)) % 0.38/0.57 (define @t89 () (not (tptp.barrel @t84 @t88))) % 0.38/0.57 (define @t90 () (not (tptp.event @t84))) % 0.38/0.57 (define @t91 () (not (tptp.chevy @t88))) % 0.38/0.57 (define @t92 () (not (tptp.car @t88))) % 0.38/0.57 (define @t93 () (not (tptp.white @t88))) % 0.38/0.57 (define @t94 () (not (tptp.dirty @t88))) % 0.38/0.57 (define @t95 () (not (tptp.old @t88))) % 0.38/0.57 (define @t96 () (not (tptp.lonely @t86))) % 0.38/0.57 (define @t97 () (not (tptp.way @t86))) % 0.38/0.57 (define @t98 () (not (tptp.street @t86))) % 0.38/0.57 (define @t99 () (or @t98 @t97 @t96 @t95 @t94 @t93 @t92 @t91 @t90 @t89 @t87 @t85 @t83 @t82 @t80 @t79 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t67 @t66 @t65 tptp.ssSkC0 @t64)) % 0.38/0.57 (define @t100 () (@list @t86 @t88 @t84 @t81 @t76 @t62 @t63 @t68)) % 0.38/0.57 (define @t101 () (forall @t100 @t99)) % 0.38/0.57 (define @t102 () (not (tptp.down @t84 @t88))) % 0.38/0.57 (define @t103 () (not (tptp.barrel @t84 @t86))) % 0.38/0.57 (define @t104 () (not (tptp.street @t88))) % 0.38/0.57 (define @t105 () (not (tptp.way @t88))) % 0.38/0.57 (define @t106 () (not (tptp.lonely @t88))) % 0.38/0.57 (define @t107 () (not (tptp.old @t86))) % 0.38/0.57 (define @t108 () (not (tptp.dirty @t86))) % 0.38/0.57 (define @t109 () (not (tptp.white @t86))) % 0.38/0.57 (define @t110 () (not (tptp.car @t86))) % 0.38/0.57 (define @t111 () (not (tptp.chevy @t86))) % 0.38/0.57 (define @t112 () (or @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t90 @t103 @t102 @t85 @t83 @t82 @t80 @t79 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t67 @t66 @t65 @t33 @t64)) % 0.38/0.57 (define @t113 () (forall @t100 @t112)) % 0.38/0.57 (define @t114 () (not @t7)) % 0.38/0.57 (define @t115 () (not @t31)) % 0.38/0.57 (define @t116 () (not @t30)) % 0.38/0.57 (define @t117 () (not @t6)) % 0.38/0.57 (define @t118 () (not @t29)) % 0.38/0.57 (define @t119 () (not @t28)) % 0.38/0.57 (define @t120 () (not @t52)) % 0.38/0.57 (define @t121 () (not @t8)) % 0.38/0.57 (define @t122 () (not @t27)) % 0.38/0.57 (define @t123 () (not @t26)) % 0.38/0.57 (define @t124 () (not @t51)) % 0.38/0.57 (define @t125 () (not @t5)) % 0.38/0.57 (define @t126 () (not @t25)) % 0.38/0.57 (define @t127 () (not @t24)) % 0.38/0.57 (define @t128 () (or @t127 @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t118 @t117 @t116 @t115 @t114 @t58)) % 0.38/0.57 (define @t129 () (or @t127 @t126 @t125 @t124 @t123 @t122 @t121 @t120 @t119 @t118 @t117 @t116 @t115 @t114 (= tptp.skc24 tptp.skc25))) % 0.38/0.57 (define @t130 () (= @t62 @t63)) % 0.38/0.57 (define @t131 () (or @t80 @t79 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t67 @t66 @t65 @t130)) % 0.38/0.57 (define @t132 () (forall (@list @t76 @t62 @t63 @t68) @t131)) % 0.38/0.57 (define @t133 () (or @t98 @t97 @t96 @t95 @t94 @t93 @t92 @t91 @t90 @t89 @t87 @t85 @t83 @t82)) % 0.38/0.57 (define @t134 () (@list @t86 @t88 @t84 @t81)) % 0.38/0.57 (define @t135 () (forall @t134 @t133)) % 0.38/0.57 (define @t136 () (or tptp.ssSkC0 @t133 @t131)) % 0.38/0.57 (define @t137 () (or @t98 @t97 @t96 @t95 @t94 @t93 @t92 @t91 @t90 @t89 @t87 @t85 @t83 @t82 @t80 @t79 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t67 @t66 @t65 tptp.ssSkC0 @t130)) % 0.38/0.57 (define @t138 () (not @t1)) % 0.38/0.57 (define @t139 () (not @t23)) % 0.38/0.57 (define @t140 () (not @t50)) % 0.38/0.57 (define @t141 () (not @t49)) % 0.38/0.57 (define @t142 () (not @t48)) % 0.38/0.57 (define @t143 () (not @t2)) % 0.38/0.57 (define @t144 () (not @t17)) % 0.38/0.57 (define @t145 () (not @t18)) % 0.38/0.57 (define @t146 () (not @t19)) % 0.38/0.57 (define @t147 () (not @t20)) % 0.38/0.57 (define @t148 () (not @t4)) % 0.38/0.57 (define @t149 () (not @t21)) % 0.38/0.57 (define @t150 () (not @t22)) % 0.38/0.57 (define @t151 () (not @t3)) % 0.38/0.57 (define @t152 () (or @t151 @t150 @t149 @t148 @t147 @t146 @t145 @t144 @t143 @t142 @t141 @t140 @t139 @t138)) % 0.38/0.57 (define @t153 () (@list false)) % 0.38/0.57 (define @t154 () (@list tptp.ssSkC0)) % 0.38/0.57 (define @t155 () (not @t15)) % 0.38/0.57 (define @t156 () (not @t47)) % 0.38/0.57 (define @t157 () (not @t46)) % 0.38/0.57 (define @t158 () (not @t14)) % 0.38/0.57 (define @t159 () (not @t45)) % 0.38/0.57 (define @t160 () (not @t44)) % 0.38/0.57 (define @t161 () (not @t57)) % 0.38/0.57 (define @t162 () (not @t16)) % 0.38/0.57 (define @t163 () (not @t43)) % 0.38/0.57 (define @t164 () (not @t42)) % 0.38/0.57 (define @t165 () (not @t56)) % 0.38/0.57 (define @t166 () (not @t13)) % 0.38/0.57 (define @t167 () (not @t41)) % 0.38/0.57 (define @t168 () (not @t40)) % 0.38/0.57 (define @t169 () (or @t168 @t167 @t166 @t165 @t164 @t163 @t162 @t161 @t160 @t159 @t158 @t157 @t156 @t155 @t60)) % 0.38/0.57 (define @t170 () (not @t169)) % 0.38/0.57 (define @t171 () (or @t168 @t167 @t166 @t165 @t164 @t163 @t162 @t161 @t160 @t159 @t158 @t157 @t156 @t155 (= tptp.skc16 tptp.skc17))) % 0.38/0.57 (define @t172 () (or @t106 @t105 @t104 @t111 @t110 @t109 @t108 @t107 @t90 @t103 @t102 @t85 @t83 @t82)) % 0.38/0.57 (define @t173 () (forall @t134 @t172)) % 0.38/0.57 (define @t174 () (or @t33 @t172 @t131)) % 0.38/0.57 (define @t175 () (or @t111 @t110 @t109 @t108 @t107 @t106 @t105 @t104 @t90 @t103 @t102 @t85 @t83 @t82 @t80 @t79 @t78 @t77 @t75 @t74 @t73 @t72 @t71 @t70 @t69 @t67 @t66 @t65 @t33 @t130)) % 0.38/0.57 (define @t176 () (or @t104 @t105 @t106 @t107 @t108 @t109 @t110 @t111 @t90 @t103 @t102 @t85 @t83 @t82)) % 0.38/0.57 (define @t177 () (forall @t134 @t176)) % 0.38/0.57 (define @t178 () (@var "BOUND_VARIABLE_7898" $$unsorted)) % 0.38/0.57 (define @t179 () (@var "BOUND_VARIABLE_7897" $$unsorted)) % 0.38/0.57 (define @t180 () (@var "BOUND_VARIABLE_7895" $$unsorted)) % 0.38/0.57 (define @t181 () (@var "BOUND_VARIABLE_7896" $$unsorted)) % 0.38/0.57 (define @t182 () (@list @t180 @t181 @t179 @t178)) % 0.38/0.57 (define @t183 () (not @t9)) % 0.38/0.57 (define @t184 () (not @t39)) % 0.38/0.57 (define @t185 () (not @t55)) % 0.38/0.57 (define @t186 () (not @t54)) % 0.38/0.57 (define @t187 () (not @t53)) % 0.38/0.57 (define @t188 () (not @t10)) % 0.38/0.57 (define @t189 () (not @t11)) % 0.38/0.57 (define @t190 () (not @t38)) % 0.38/0.57 (define @t191 () (not @t37)) % 0.38/0.57 (define @t192 () (not @t36)) % 0.38/0.57 (define @t193 () (not @t35)) % 0.38/0.57 (define @t194 () (not @t12)) % 0.38/0.57 (define @t195 () (not @t34)) % 0.38/0.57 (define @t196 () (not @t32)) % 0.38/0.57 (define @t197 () (or @t196 @t195 @t194 @t193 @t192 @t191 @t190 @t189 @t188 @t187 @t186 @t185 @t184 @t183)) % 0.38/0.57 (define @t198 () (not @t197)) % 0.38/0.57 (assume @p1 @t1) % 0.38/0.57 (assume @p2 @t2) % 0.38/0.57 (assume @p3 @t3) % 0.38/0.57 (assume @p4 @t4) % 0.38/0.57 (assume @p5 @t5) % 0.38/0.57 (assume @p6 @t6) % 0.38/0.57 (assume @p7 @t7) % 0.38/0.57 (assume @p8 @t8) % 0.38/0.57 (assume @p9 @t9) % 0.38/0.57 (assume @p10 @t10) % 0.38/0.57 (assume @p11 @t11) % 0.38/0.57 (assume @p12 @t12) % 0.38/0.57 (assume @p13 @t13) % 0.38/0.57 (assume @p14 @t14) % 0.38/0.57 (assume @p15 @t15) % 0.38/0.57 (assume @p16 @t16) % 0.38/0.57 (assume @p17 (or tptp.ssSkC0 @t17)) % 0.38/0.57 (assume @p18 (or tptp.ssSkC0 @t18)) % 0.38/0.57 (assume @p19 (or tptp.ssSkC0 @t19)) % 0.38/0.57 (assume @p20 (or tptp.ssSkC0 @t20)) % 0.38/0.57 (assume @p21 (or tptp.ssSkC0 @t21)) % 0.38/0.57 (assume @p22 (or tptp.ssSkC0 @t22)) % 0.38/0.57 (assume @p23 (or tptp.ssSkC0 @t23)) % 0.38/0.57 (assume @p24 (or tptp.ssSkC0 @t24)) % 0.38/0.57 (assume @p25 (or tptp.ssSkC0 @t25)) % 0.38/0.57 (assume @p26 (or tptp.ssSkC0 @t26)) % 0.38/0.57 (assume @p27 (or tptp.ssSkC0 @t27)) % 0.38/0.57 (assume @p28 (or tptp.ssSkC0 @t28)) % 0.38/0.57 (assume @p29 (or tptp.ssSkC0 @t29)) % 0.38/0.57 (assume @p30 (or tptp.ssSkC0 @t30)) % 0.38/0.57 (assume @p31 (or tptp.ssSkC0 @t31)) % 0.38/0.57 (assume @p32 (or @t33 @t32)) % 0.38/0.57 (assume @p33 (or @t33 @t34)) % 0.38/0.57 (assume @p34 (or @t33 @t35)) % 0.38/0.57 (assume @p35 (or @t33 @t36)) % 0.38/0.57 (assume @p36 (or @t33 @t37)) % 0.38/0.57 (assume @p37 (or @t33 @t38)) % 0.38/0.57 (assume @p38 (or @t33 @t39)) % 0.38/0.57 (assume @p39 (or @t33 @t40)) % 0.38/0.57 (assume @p40 (or @t33 @t41)) % 0.38/0.57 (assume @p41 (or @t33 @t42)) % 0.38/0.57 (assume @p42 (or @t33 @t43)) % 0.38/0.57 (assume @p43 (or @t33 @t44)) % 0.38/0.57 (assume @p44 (or @t33 @t45)) % 0.38/0.57 (assume @p45 (or @t33 @t46)) % 0.38/0.57 (assume @p46 (or @t33 @t47)) % 0.38/0.57 (assume @p47 (or tptp.ssSkC0 @t48)) % 0.38/0.57 (assume @p48 (or tptp.ssSkC0 @t49)) % 0.38/0.57 (assume @p49 (or tptp.ssSkC0 @t50)) % 0.38/0.57 (assume @p50 (or tptp.ssSkC0 @t51)) % 0.38/0.57 (assume @p51 (or tptp.ssSkC0 @t52)) % 0.38/0.57 (assume @p52 (or @t33 @t53)) % 0.38/0.57 (assume @p53 (or @t33 @t54)) % 0.38/0.57 (assume @p54 (or @t33 @t55)) % 0.38/0.57 (assume @p55 (or @t33 @t56)) % 0.38/0.57 (assume @p56 (or @t33 @t57)) % 0.38/0.57 (assume @p57 (or @t59 tptp.ssSkC0)) % 0.38/0.57 (assume @p58 (or @t61 @t33)) % 0.38/0.57 (assume @p59 @t101) % 0.38/0.57 (assume @p60 @t113) % 0.38/0.57 (step @p61 :rule reordering :premises (@p57) :args ((or tptp.ssSkC0 @t59))) % 0.38/0.57 (step @p62 :rule cnf_or_pos :args (@t128)) % 0.38/0.57 (step @p63 :rule reordering :premises (@p62) :args ((or @t58 @t125 @t117 @t114 @t121 @t127 @t126 @t123 @t122 @t119 @t118 @t116 @t115 @t124 @t120 (not @t128)))) % 0.38/0.57 (step @p64 :rule eq-symm :args (tptp.skc24 tptp.skc25)) % 0.38/0.57 (step @p65 :rule refl :args (@t114)) % 0.38/0.57 (step @p66 :rule refl :args (@t115)) % 0.38/0.57 (step @p67 :rule refl :args (@t116)) % 0.38/0.57 (step @p68 :rule refl :args (@t117)) % 0.38/0.57 (step @p69 :rule refl :args (@t118)) % 0.38/0.57 (step @p70 :rule refl :args (@t119)) % 0.38/0.57 (step @p71 :rule refl :args (@t120)) % 0.38/0.57 (step @p72 :rule refl :args (@t121)) % 0.38/0.57 (step @p73 :rule refl :args (@t122)) % 0.38/0.57 (step @p74 :rule refl :args (@t123)) % 0.38/0.57 (step @p75 :rule refl :args (@t124)) % 0.38/0.57 (step @p76 :rule refl :args (@t125)) % 0.38/0.57 (step @p77 :rule refl :args (@t126)) % 0.38/0.57 (step @p78 :rule refl :args (@t127)) % 0.38/0.57 (step @p79 :rule nary_cong :premises (@p78 @p77 @p76 @p75 @p74 @p73 @p72 @p71 @p70 @p69 @p68 @p67 @p66 @p65 @p64) :args (@t129)) % 0.38/0.57 (step @p80 :rule refl :args (@t132)) % 0.38/0.57 (step @p81 :rule cong :premises (@p80 @p79) :args ((=> @t132 @t129))) % 0.38/0.57 (assume-push @p224 @t132) % 0.38/0.57 (step @p83 :rule instantiate :premises (@p224) :args ((@list tptp.skc27 tptp.skc24 tptp.skc25 tptp.skc26))) % 0.38/0.57 (step-pop @p225 :rule scope :premises (@p83)) % 0.38/0.57 (step @p84 :rule process_scope :premises (@p225) :args (@t129)) % 0.38/0.57 (step @p86 :rule eq_resolve :premises (@p84 @p81)) % 0.38/0.57 (step @p87 :rule implies_elim :premises (@p86)) % 0.38/0.57 (step @p88 :rule quant-miniscope-or :args ((= (forall @t100 @t136) (or tptp.ssSkC0 @t135 @t132)))) % 0.38/0.57 (step @p89 :rule aci_norm :args ((= @t137 @t136))) % 0.38/0.57 (step @p90 :rule cong :premises (@p89) :args ((forall @t100 @t137))) % 0.38/0.57 (step @p91 :rule trans :premises (@p90 @p88)) % 0.38/0.57 (step @p92 :rule eq-symm :args (@t63 @t62)) % 0.38/0.57 (step @p93 :rule refl :args (tptp.ssSkC0)) % 0.38/0.57 (step @p94 :rule refl :args (@t65)) % 0.38/0.57 (step @p95 :rule refl :args (@t66)) % 0.38/0.57 (step @p96 :rule refl :args (@t67)) % 0.38/0.57 (step @p97 :rule refl :args (@t69)) % 0.38/0.57 (step @p98 :rule refl :args (@t70)) % 0.38/0.57 (step @p99 :rule refl :args (@t71)) % 0.38/0.57 (step @p100 :rule refl :args (@t72)) % 0.38/0.57 (step @p101 :rule refl :args (@t73)) % 0.38/0.57 (step @p102 :rule refl :args (@t74)) % 0.38/0.57 (step @p103 :rule refl :args (@t75)) % 0.38/0.57 (step @p104 :rule refl :args (@t77)) % 0.38/0.57 (step @p105 :rule refl :args (@t78)) % 0.38/0.57 (step @p106 :rule refl :args (@t79)) % 0.38/0.57 (step @p107 :rule refl :args (@t80)) % 0.38/0.57 (step @p108 :rule refl :args (@t82)) % 0.38/0.57 (step @p109 :rule refl :args (@t83)) % 0.38/0.57 (step @p110 :rule refl :args (@t85)) % 0.38/0.57 (step @p111 :rule refl :args (@t87)) % 0.38/0.57 (step @p112 :rule refl :args (@t89)) % 0.38/0.57 (step @p113 :rule refl :args (@t90)) % 0.38/0.57 (step @p114 :rule refl :args (@t91)) % 0.38/0.57 (step @p115 :rule refl :args (@t92)) % 0.38/0.57 (step @p116 :rule refl :args (@t93)) % 0.38/0.57 (step @p117 :rule refl :args (@t94)) % 0.38/0.57 (step @p118 :rule refl :args (@t95)) % 0.38/0.57 (step @p119 :rule refl :args (@t96)) % 0.38/0.57 (step @p120 :rule refl :args (@t97)) % 0.38/0.57 (step @p121 :rule refl :args (@t98)) % 0.38/0.57 (step @p122 :rule nary_cong :premises (@p121 @p120 @p119 @p118 @p117 @p116 @p115 @p114 @p113 @p112 @p111 @p110 @p109 @p108 @p107 @p106 @p105 @p104 @p103 @p102 @p101 @p100 @p99 @p98 @p97 @p96 @p95 @p94 @p93 @p92) :args (@t99)) % 0.38/0.57 (step @p123 :rule cong :premises (@p122) :args (@t101)) % 0.38/0.57 (step @p124 :rule trans :premises (@p123 @p91)) % 0.38/0.57 (step @p125 :rule eq_resolve :premises (@p59 @p124)) % 0.38/0.57 (step @p126 :rule cnf_or_pos :args (@t152)) % 0.38/0.57 (step @p127 :rule reordering :premises (@p126) :args ((or @t138 @t143 @t151 @t148 @t144 @t145 @t146 @t147 @t149 @t150 @t139 @t142 @t141 @t140 (not @t152)))) % 0.38/0.57 (assume-push @p226 @t135) % 0.38/0.57 (step @p129 :rule instantiate :premises (@p226) :args ((@list tptp.skc29 tptp.skc28 tptp.skc30 tptp.skc31))) % 0.38/0.57 (step-pop @p227 :rule scope :premises (@p129)) % 0.38/0.57 (step @p130 :rule process_scope :premises (@p227) :args (@t152)) % 0.38/0.57 (step @p132 :rule implies_elim :premises (@p130)) % 0.38/0.57 (step @p133 :rule chain_m_resolution :premises (@p132 @p127 @p4 @p3 @p2 @p1 @p125 @p87 @p63 @p8 @p7 @p6 @p5 @p61 @p51 @p50 @p49 @p48 @p47 @p31 @p30 @p29 @p28 @p27 @p26 @p25 @p24 @p23 @p22 @p21 @p20 @p19 @p18 @p17) :args (tptp.ssSkC0 (@list true false false false false false true true false false false false true false false false false false false false false false false false false false false false false false false false false) (@list @t152 @t4 @t3 @t2 @t1 @t135 @t132 @t128 @t8 @t7 @t6 @t5 @t58 @t52 @t51 @t50 @t49 @t48 @t31 @t30 @t29 @t28 @t27 @t26 @t25 @t24 @t23 @t22 @t21 @t20 @t19 @t18 @t17))) % 0.38/0.57 (step @p134 :rule chain_m_resolution :premises (@p56 @p133) :args (@t57 @t153 @t154)) % 0.38/0.57 (step @p135 :rule chain_m_resolution :premises (@p55 @p133) :args (@t56 @t153 @t154)) % 0.38/0.57 (step @p136 :rule chain_m_resolution :premises (@p46 @p133) :args (@t47 @t153 @t154)) % 0.38/0.57 (step @p137 :rule chain_m_resolution :premises (@p45 @p133) :args (@t46 @t153 @t154)) % 0.38/0.57 (step @p138 :rule chain_m_resolution :premises (@p44 @p133) :args (@t45 @t153 @t154)) % 0.38/0.57 (step @p139 :rule chain_m_resolution :premises (@p43 @p133) :args (@t44 @t153 @t154)) % 0.38/0.57 (step @p140 :rule chain_m_resolution :premises (@p42 @p133) :args (@t43 @t153 @t154)) % 0.38/0.57 (step @p141 :rule chain_m_resolution :premises (@p41 @p133) :args (@t42 @t153 @t154)) % 0.38/0.57 (step @p142 :rule chain_m_resolution :premises (@p40 @p133) :args (@t41 @t153 @t154)) % 0.38/0.57 (step @p143 :rule chain_m_resolution :premises (@p39 @p133) :args (@t40 @t153 @t154)) % 0.38/0.57 (step @p144 :rule reordering :premises (@p58) :args ((or @t33 @t61))) % 0.38/0.57 (step @p145 :rule chain_m_resolution :premises (@p144 @p133) :args (@t61 @t153 @t154)) % 0.38/0.57 (step @p146 :rule cnf_or_pos :args (@t169)) % 0.38/0.57 (step @p147 :rule reordering :premises (@p146) :args ((or @t60 @t166 @t158 @t155 @t162 @t168 @t167 @t164 @t163 @t160 @t159 @t157 @t156 @t165 @t161 @t170))) % 0.38/0.57 (step @p148 :rule chain_m_resolution :premises (@p147 @p145 @p13 @p14 @p15 @p16 @p143 @p142 @p141 @p140 @p139 @p138 @p137 @p136 @p135 @p134) :args (@t170 (@list true false false false false false false false false false false false false false false) (@list @t60 @t13 @t14 @t15 @t16 @t40 @t41 @t42 @t43 @t44 @t45 @t46 @t47 @t56 @t57))) % 0.38/0.57 (step @p149 :rule eq-symm :args (tptp.skc16 tptp.skc17)) % 0.38/0.57 (step @p150 :rule refl :args (@t155)) % 0.38/0.57 (step @p151 :rule refl :args (@t156)) % 0.38/0.57 (step @p152 :rule refl :args (@t157)) % 0.38/0.57 (step @p153 :rule refl :args (@t158)) % 0.38/0.57 (step @p154 :rule refl :args (@t159)) % 0.38/0.57 (step @p155 :rule refl :args (@t160)) % 0.38/0.57 (step @p156 :rule refl :args (@t161)) % 0.38/0.57 (step @p157 :rule refl :args (@t162)) % 0.38/0.57 (step @p158 :rule refl :args (@t163)) % 0.38/0.57 (step @p159 :rule refl :args (@t164)) % 0.38/0.57 (step @p160 :rule refl :args (@t165)) % 0.38/0.57 (step @p161 :rule refl :args (@t166)) % 0.38/0.57 (step @p162 :rule refl :args (@t167)) % 0.38/0.57 (step @p163 :rule refl :args (@t168)) % 0.38/0.57 (step @p164 :rule nary_cong :premises (@p163 @p162 @p161 @p160 @p159 @p158 @p157 @p156 @p155 @p154 @p153 @p152 @p151 @p150 @p149) :args (@t171)) % 0.38/0.57 (step @p165 :rule cong :premises (@p80 @p164) :args ((=> @t132 @t171))) % 0.38/0.57 (assume-push @p228 @t132) % 0.38/0.57 (step @p167 :rule instantiate :premises (@p228) :args ((@list tptp.skc19 tptp.skc16 tptp.skc17 tptp.skc18))) % 0.38/0.57 (step-pop @p229 :rule scope :premises (@p167)) % 0.38/0.57 (step @p168 :rule process_scope :premises (@p229) :args (@t171)) % 0.38/0.57 (step @p170 :rule eq_resolve :premises (@p168 @p165)) % 0.38/0.57 (step @p171 :rule implies_elim :premises (@p170)) % 0.38/0.57 (step @p172 :rule chain_m_resolution :premises (@p171 @p148) :args ((not @t132) (@list true) (@list @t169))) % 0.38/0.57 (step @p173 :rule quant-miniscope-or :args ((= (forall @t100 @t174) (or @t33 @t173 @t132)))) % 0.38/0.57 (step @p174 :rule aci_norm :args ((= @t175 @t174))) % 0.38/0.57 (step @p175 :rule cong :premises (@p174) :args ((forall @t100 @t175))) % 0.38/0.57 (step @p176 :rule trans :premises (@p175 @p173)) % 0.38/0.57 (step @p177 :rule refl :args (@t33)) % 0.38/0.57 (step @p178 :rule refl :args (@t102)) % 0.38/0.57 (step @p179 :rule refl :args (@t103)) % 0.38/0.57 (step @p180 :rule refl :args (@t104)) % 0.38/0.57 (step @p181 :rule refl :args (@t105)) % 0.38/0.57 (step @p182 :rule refl :args (@t106)) % 0.38/0.57 (step @p183 :rule refl :args (@t107)) % 0.38/0.57 (step @p184 :rule refl :args (@t108)) % 0.38/0.57 (step @p185 :rule refl :args (@t109)) % 0.38/0.57 (step @p186 :rule refl :args (@t110)) % 0.38/0.57 (step @p187 :rule refl :args (@t111)) % 0.38/0.57 (step @p188 :rule nary_cong :premises (@p187 @p186 @p185 @p184 @p183 @p182 @p181 @p180 @p113 @p179 @p178 @p110 @p109 @p108 @p107 @p106 @p105 @p104 @p103 @p102 @p101 @p100 @p99 @p98 @p97 @p96 @p95 @p94 @p177 @p92) :args (@t112)) % 0.38/0.57 (step @p189 :rule cong :premises (@p188) :args (@t113)) % 0.38/0.57 (step @p190 :rule trans :premises (@p189 @p176)) % 0.38/0.57 (step @p191 :rule eq_resolve :premises (@p60 @p190)) % 0.38/0.57 (step @p192 :rule reordering :premises (@p191) :args ((or @t33 @t132 @t173))) % 0.38/0.57 (step @p193 :rule chain_m_resolution :premises (@p192 @p133 @p172) :args (@t173 (@list false true) (@list tptp.ssSkC0 @t132))) % 0.38/0.57 (step @p194 :rule aci_norm :args ((= @t172 @t176))) % 0.38/0.57 (step @p195 :rule cong :premises (@p194) :args (@t173)) % 0.38/0.57 (step @p196 :rule symm :premises (@p195)) % 0.38/0.57 (step @p197 :rule cong :premises (@p196 @p195) :args ((= @t177 @t173))) % 0.38/0.57 (step @p198 :rule true_elim :premises (@p197)) % 0.38/0.57 (step @p199 :rule quant_var_reordering :args ((= (forall (@list @t88 @t86 @t84 @t81) @t176) @t177))) % 0.38/0.57 (step @p200 :rule alpha_equiv :args ((forall (@list @t180 @t181 @t179 @t178) (or (not (tptp.street @t180)) (not (tptp.way @t180)) (not (tptp.lonely @t180)) (not (tptp.old @t181)) (not (tptp.dirty @t181)) (not (tptp.white @t181)) (not (tptp.car @t181)) (not (tptp.chevy @t181)) (not (tptp.event @t179)) (not (tptp.barrel @t179 @t181)) (not (tptp.down @t179 @t180)) (not (tptp.in @t179 @t178)) (not (tptp.city @t178)) (not (tptp.hollywood @t178)))) @t182 (@list @t88 @t86 @t84 @t81))) % 0.38/0.57 (step @p201 :rule alpha_equiv :args (@t135 (@list @t86 @t88 @t84 @t81) @t182)) % 0.38/0.57 (step @p202 :rule trans :premises (@p201 @p200 @p199 @p198)) % 0.38/0.57 (step @p203 :rule equiv_elim2 :premises (@p202)) % 0.38/0.57 (step @p204 :rule chain_m_resolution :premises (@p203 @p193) :args (@t135 @t153 (@list @t173))) % 0.38/0.57 (step @p205 :rule chain_m_resolution :premises (@p54 @p133) :args (@t55 @t153 @t154)) % 0.38/0.57 (step @p206 :rule chain_m_resolution :premises (@p53 @p133) :args (@t54 @t153 @t154)) % 0.38/0.57 (step @p207 :rule chain_m_resolution :premises (@p52 @p133) :args (@t53 @t153 @t154)) % 0.38/0.57 (step @p208 :rule chain_m_resolution :premises (@p38 @p133) :args (@t39 @t153 @t154)) % 0.38/0.57 (step @p209 :rule chain_m_resolution :premises (@p37 @p133) :args (@t38 @t153 @t154)) % 0.38/0.57 (step @p210 :rule chain_m_resolution :premises (@p36 @p133) :args (@t37 @t153 @t154)) % 0.38/0.57 (step @p211 :rule chain_m_resolution :premises (@p35 @p133) :args (@t36 @t153 @t154)) % 0.38/0.57 (step @p212 :rule chain_m_resolution :premises (@p34 @p133) :args (@t35 @t153 @t154)) % 0.38/0.57 (step @p213 :rule chain_m_resolution :premises (@p33 @p133) :args (@t34 @t153 @t154)) % 0.38/0.57 (step @p214 :rule chain_m_resolution :premises (@p32 @p133) :args (@t32 @t153 @t154)) % 0.38/0.57 (step @p215 :rule cnf_or_pos :args (@t197)) % 0.38/0.57 (step @p216 :rule reordering :premises (@p215) :args ((or @t183 @t188 @t189 @t194 @t196 @t195 @t193 @t192 @t191 @t190 @t184 @t187 @t186 @t185 @t198))) % 0.38/0.57 (step @p217 :rule chain_m_resolution :premises (@p216 @p9 @p10 @p11 @p12 @p214 @p213 @p212 @p211 @p210 @p209 @p208 @p207 @p206 @p205) :args (@t198 (@list false false false false false false false false false false false false false false) (@list @t9 @t10 @t11 @t12 @t32 @t34 @t35 @t36 @t37 @t38 @t39 @t53 @t54 @t55))) % 0.38/0.57 (assume-push @p230 @t135) % 0.38/0.57 (step @p219 :rule instantiate :premises (@p230) :args ((@list tptp.skc20 tptp.skc21 tptp.skc22 tptp.skc23))) % 0.38/0.57 (step-pop @p231 :rule scope :premises (@p219)) % 0.38/0.57 (step @p220 :rule process_scope :premises (@p231) :args (@t197)) % 0.38/0.57 (step @p222 :rule implies_elim :premises (@p220)) % 0.38/0.57 (step @p223 false :rule chain_m_resolution :premises (@p222 @p217 @p204) :args (false (@list true false) (@list @t197 @t135))) % 0.38/0.57 ) % 0.38/0.57 % SZS output end Proof % 0.38/0.57 % cvc5 exiting %------------------------------------------------------------------------------