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