%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN547+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n015.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 : 0s % DateTime : Thu Jul 21 03:51:23 EDT 2022 % Result : CounterSatisfiable 0.71s 0.90s % Output : Model 0.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN547+1 : TPTP v8.1.0. Released v2.1.0. % 0.03/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.33 % Computer : n015.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % DateTime : Tue Jul 12 00:11:39 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 Defaulting to tptp format. % 0.71/0.90 SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.90 % 0.71/0.90 MODEL (CONTEXT): % 0.71/0.90 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.90 -__-v__(=0) % 0.71/0.90 +__con190 % 0.71/0.90 +__con191 % 0.71/0.90 +__con193 % 0.71/0.90 +__con194 % 0.71/0.90 +__con195 % 0.71/0.90 +__con197 % 0.71/0.90 +__con204 % 0.71/0.90 +__con205 % 0.71/0.90 +__con206 % 0.71/0.90 +__con212 % 0.71/0.90 +__con214 % 0.71/0.90 -__con215 % 0.71/0.90 +__con216 % 0.71/0.90 -__con217 % 0.71/0.90 -__con220 % 0.71/0.90 +__con226 % 0.71/0.90 +__con227 % 0.71/0.90 -__con228 % 0.71/0.90 +__con230 % 0.71/0.90 +__con231 % 0.71/0.90 +__con232 % 0.71/0.90 +__con233 % 0.71/0.90 +__con234 % 0.71/0.90 +__con235 % 0.71/0.90 -__con238 % 0.71/0.90 +__con239 % 0.71/0.90 -__con240 % 0.71/0.90 +__con241 % 0.71/0.90 +__con242 % 0.71/0.90 -__con244 % 0.71/0.90 -__con245 % 0.71/0.90 +__con246 % 0.71/0.90 -__con251 % 0.71/0.90 -__con253 % 0.71/0.90 -__con255 % 0.71/0.90 +__con261 % 0.71/0.90 +__con262 % 0.71/0.90 -__con263 % 0.71/0.90 -__con264 % 0.71/0.90 +__con265 % 0.71/0.90 -__con268 % 0.71/0.90 +__con270 % 0.71/0.90 +__con271 % 0.71/0.90 +__con272 % 0.71/0.90 -__con273 % 0.71/0.90 +__con275 % 0.71/0.90 -__con279 % 0.71/0.90 +__con280 % 0.71/0.90 -__con281 % 0.71/0.90 -__con282 % 0.71/0.90 +__con289 % 0.71/0.90 -__con291 % 0.71/0.90 +__con296 % 0.71/0.90 +__con297 % 0.71/0.90 +__con302 % 0.71/0.90 -__con303 % 0.71/0.90 -__con317 % 0.71/0.90 -__con318 % 0.71/0.90 -__con319 % 0.71/0.90 -__con320 % 0.71/0.90 +__con321 % 0.71/0.90 +__con323 % 0.71/0.90 +__con324 % 0.71/0.90 +__con325 % 0.71/0.90 +__con326 % 0.71/0.90 +__con328 % 0.71/0.90 +__con329 % 0.71/0.90 +__con330 % 0.71/0.90 +__con331 % 0.71/0.90 -__con336 % 0.71/0.90 -__con338 % 0.71/0.90 -__con343 % 0.71/0.90 -__con344 % 0.71/0.90 -__con345 % 0.71/0.90 +__con346 % 0.71/0.90 -__con350 % 0.71/0.90 -__con351 % 0.71/0.90 -c1_0 % 0.71/0.90 +c1_1(a466) % 0.71/0.90 +c1_1(a520) % 0.71/0.90 +c1_1(a538) % 0.71/0.90 +c1_1(a558) % 0.71/0.90 +c1_1(a581) % 0.71/0.90 +c1_2(_0, a460) % 0.71/0.90 +c1_2(a570, a571) % 0.71/0.90 -c1_2(a520, a521) % 0.71/0.90 +c2_0 % 0.71/0.90 +c2_1(=0) % 0.71/0.90 +c2_1(a565) % 0.71/0.90 -c2_1(a520) % 0.71/0.90 -c2_1(a581) % 0.71/0.90 +c2_2(a488, a572) % 0.71/0.90 +c2_2(a520, a521) % 0.71/0.90 +c2_2(a537, a572) % 0.71/0.90 +c2_2(a539, a572) % 0.71/0.90 +c2_2(a569, a572) % 0.71/0.90 +c2_2(a570, a571) % 0.71/0.90 +c2_2(a570, a572) % 0.71/0.90 +c2_2(a581, =0) % 0.71/0.90 +c3_0 % 0.71/0.90 +c3_1(a565) % 0.71/0.90 +c3_1(a569) % 0.71/0.90 +c3_1(a600) % 0.71/0.90 +c3_2(a539, a540) % 0.71/0.90 +c3_2(a570, a571) % 0.71/0.90 -c4_0 % 0.71/0.90 +c4_1(a488) % 0.71/0.90 +c4_1(a537) % 0.71/0.90 +c4_1(a539) % 0.71/0.90 +c4_1(a569) % 0.71/0.90 +c4_1(a570) % 0.71/0.90 +c4_2(a530, =0) % 0.71/0.90 -c4_2(a520, a521) % 0.71/0.90 -c5_0 % 0.71/0.90 +c5_1(a539) % 0.71/0.90 +c5_1(a558) % 0.71/0.90 +c5_1(a565) % 0.71/0.90 +c5_1(a570) % 0.71/0.90 +c5_1(a601) % 0.71/0.90 -c5_1(a520) % 0.71/0.90 +c5_2(_0, a460) % 0.71/0.90 +c6_0 % 0.71/0.90 +c6_1(a539) % 0.71/0.90 +c6_1(a558) % 0.71/0.90 +c6_1(a565) % 0.71/0.90 -c6_1(a581) % 0.71/0.90 +c7_0 % 0.71/0.90 +c7_1(a520) % 0.71/0.90 +c7_1(a581) % 0.71/0.90 +c7_1(a601) % 0.71/0.90 +c8_0 % 0.71/0.90 +c8_1(a581) % 0.71/0.90 -c8_1(a466) % 0.71/0.90 +c8_2(a539, a540) % 0.71/0.90 +c8_2(a539, a541) % 0.71/0.90 +epred1_0 % 0.71/0.90 +ndr1_0 % 0.71/0.90 +ndr1_1(_0) % 0.71/0.90 +ndr1_1(a520) % 0.71/0.90 +ndr1_1(a539) % 0.71/0.90 +ndr1_1(a570) % 0.71/0.90 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------