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