%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN429+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n011.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:49:55 EDT 2022 % Result : CounterSatisfiable 1.19s 1.39s % Output : Model 1.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN429+1 : TPTP v8.1.0. Released v2.1.0. % 0.03/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.34 % Computer : n011.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % DateTime : Tue Jul 12 07:15:28 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 Defaulting to tptp format. % 1.19/1.39 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.19/1.39 % 1.19/1.39 MODEL (CONTEXT): % 1.19/1.39 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.19/1.39 -__-v__(=0) % 1.19/1.39 +__con265 % 1.19/1.39 +__con266 % 1.19/1.39 -__con274 % 1.19/1.39 -__con275 % 1.19/1.39 -__con276 % 1.19/1.39 -__con280 % 1.19/1.39 +__con281 % 1.19/1.39 -__con282 % 1.19/1.39 +__con283 % 1.19/1.39 +__con287 % 1.19/1.39 +__con288 % 1.19/1.39 +__con289 % 1.19/1.39 +__con290 % 1.19/1.39 -__con291 % 1.19/1.39 +__con292 % 1.19/1.39 -__con293 % 1.19/1.39 +__con294 % 1.19/1.39 -__con295 % 1.19/1.39 -__con296 % 1.19/1.39 -__con297 % 1.19/1.39 -__con298 % 1.19/1.39 -__con299 % 1.19/1.39 +__con301 % 1.19/1.39 +__con302 % 1.19/1.39 +__con313 % 1.19/1.39 +__con314 % 1.19/1.39 +__con317 % 1.19/1.39 +__con318 % 1.19/1.39 -__con327 % 1.19/1.39 +__con328 % 1.19/1.39 +__con329 % 1.19/1.39 +__con330 % 1.19/1.39 +__con331 % 1.19/1.39 +__con338 % 1.19/1.39 +__con350 % 1.19/1.39 +__con351 % 1.19/1.39 +__con352 % 1.19/1.39 +__con353 % 1.19/1.39 +__con354 % 1.19/1.39 +__con355 % 1.19/1.39 -__con367 % 1.19/1.39 +__con368 % 1.19/1.39 -__con369 % 1.19/1.39 -__con377 % 1.19/1.39 +__con378 % 1.19/1.39 +__con379 % 1.19/1.39 +__con380 % 1.19/1.39 +__con381 % 1.19/1.39 +__con387 % 1.19/1.39 -__con389 % 1.19/1.39 -__con390 % 1.19/1.39 -__con391 % 1.19/1.39 -__con392 % 1.19/1.39 +__con393 % 1.19/1.39 +__con394 % 1.19/1.39 +__con395 % 1.19/1.39 +__con409 % 1.19/1.39 +__con410 % 1.19/1.39 -__con412 % 1.19/1.39 +__con413 % 1.19/1.39 -__con414 % 1.19/1.39 -__con415 % 1.19/1.39 -__con416 % 1.19/1.39 -__con417 % 1.19/1.39 -__con418 % 1.19/1.39 -__con419 % 1.19/1.39 -__con420 % 1.19/1.39 -__con421 % 1.19/1.39 -__con424 % 1.19/1.39 +__con425 % 1.19/1.39 +__con426 % 1.19/1.39 +__con427 % 1.19/1.39 +__con428 % 1.19/1.39 +__con429 % 1.19/1.39 -__con431 % 1.19/1.39 +__con432 % 1.19/1.39 -__con441 % 1.19/1.39 -__con442 % 1.19/1.39 -__con447 % 1.19/1.39 -__con448 % 1.19/1.39 -__con453 % 1.19/1.39 +__con454 % 1.19/1.39 +__con455 % 1.19/1.39 +__con458 % 1.19/1.39 +__con459 % 1.19/1.39 +__con460 % 1.19/1.39 +__con461 % 1.19/1.39 +__con462 % 1.19/1.39 -__con472 % 1.19/1.39 +__con481 % 1.19/1.39 +__con485 % 1.19/1.39 +__con486 % 1.19/1.39 +__con487 % 1.19/1.39 +__con491 % 1.19/1.39 +__con492 % 1.19/1.39 -__con498 % 1.19/1.39 +__con499 % 1.19/1.39 -__con500 % 1.19/1.39 +__con501 % 1.19/1.39 +__con502 % 1.19/1.39 -__con503 % 1.19/1.39 -__con506 % 1.19/1.39 +c10_0 % 1.19/1.39 +c10_1(a182) % 1.19/1.39 +c10_2(a127, a128) % 1.19/1.39 +c10_2(a210, a211) % 1.19/1.39 -c10_2(a111, a113) % 1.19/1.39 -c10_2(a141, a142) % 1.19/1.39 +c1_0 % 1.19/1.39 +c1_1(a104) % 1.19/1.39 +c1_1(a107) % 1.19/1.39 +c1_1(a145) % 1.19/1.39 +c1_1(a182) % 1.19/1.39 -c1_1(a86) % 1.19/1.39 +c1_2(a104, a105) % 1.19/1.39 +c1_2(a119, a120) % 1.19/1.39 +c1_2(a127, a128) % 1.19/1.39 +c2_0 % 1.19/1.39 +c2_1(a182) % 1.19/1.39 +c2_2(a111, a208) % 1.19/1.39 -c2_2(a104, a105) % 1.19/1.39 -c2_2(a104, a106) % 1.19/1.39 +c3_0 % 1.19/1.39 +c3_2(a111, a209) % 1.19/1.39 +c3_2(a119, a100) % 1.19/1.39 -c3_2(a141, a142) % 1.19/1.39 -c4_0 % 1.19/1.39 +c4_1(a182) % 1.19/1.39 +c4_1(a213) % 1.19/1.39 +c4_2(a104, a106) % 1.19/1.39 -c4_2(a111, a112) % 1.19/1.39 +c5_0 % 1.19/1.39 +c5_1(=0) % 1.19/1.39 +c5_1(a119) % 1.19/1.39 -c5_1(a86) % 1.19/1.39 +c5_2(a107, a108) % 1.19/1.39 +c5_2(a111, a209) % 1.19/1.39 -c5_2(a104, a106) % 1.19/1.39 -c6_0 % 1.19/1.39 +c6_1(a51) % 1.19/1.39 +c6_2(a111, a112) % 1.19/1.39 +c6_2(a111, a113) % 1.19/1.39 -c6_2(a107, a108) % 1.19/1.39 +c7_0 % 1.19/1.39 +c7_1(=0) % 1.19/1.39 +c7_1(a86) % 1.19/1.39 +c7_2(a101, a102) % 1.19/1.39 +c7_2(a111, a113) % 1.19/1.39 +c7_2(a127, a128) % 1.19/1.39 -c7_2(a141, a142) % 1.19/1.39 -c8_0 % 1.19/1.39 +c8_1(a182) % 1.19/1.39 +c8_1(a213) % 1.19/1.39 +c8_2(a104, a105) % 1.19/1.39 +c8_2(a107, a108) % 1.19/1.39 +c8_2(a111, a112) % 1.19/1.39 +c9_0 % 1.19/1.39 +c9_1(a104) % 1.19/1.39 +c9_1(a107) % 1.19/1.39 +c9_1(a119) % 1.19/1.39 +c9_1(a145) % 1.19/1.39 +c9_1(a182) % 1.19/1.39 +c9_1(a210) % 1.19/1.39 -c9_1(a141) % 1.19/1.39 +ndr1_0 % 1.19/1.39 +ndr1_1(a51) % 1.19/1.39 +ndr1_1(a86) % 1.19/1.39 +ndr1_1(a101) % 1.19/1.39 +ndr1_1(a104) % 1.19/1.39 +ndr1_1(a107) % 1.19/1.39 +ndr1_1(a111) % 1.19/1.39 +ndr1_1(a119) % 1.19/1.39 +ndr1_1(a121) % 1.19/1.39 +ndr1_1(a127) % 1.19/1.39 +ndr1_1(a141) % 1.19/1.39 +ndr1_1(a145) % 1.19/1.39 +ndr1_1(a182) % 1.19/1.39 +ndr1_1(a210) % 1.19/1.39 +ndr1_1(a213) % 1.19/1.39 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------