%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN424+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n010.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:51 EDT 2022 % Result : CounterSatisfiable 1.74s 1.94s % Output : Model 1.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SYN424+1 : TPTP v8.1.0. Released v2.1.0. % 0.04/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % DateTime : Tue Jul 12 06:45:00 EDT 2022 % 0.13/0.35 % CPUTime : % 0.13/0.35 Defaulting to tptp format. % 1.74/1.94 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.74/1.94 % 1.74/1.94 MODEL (CONTEXT): % 1.74/1.94 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.74/1.94 -__-v__(=0) % 1.74/1.94 +__con288 % 1.74/1.94 +__con289 % 1.74/1.94 -__con292 % 1.74/1.94 +__con293 % 1.74/1.94 -__con296 % 1.74/1.94 -__con297 % 1.74/1.94 -__con298 % 1.74/1.94 -__con299 % 1.74/1.94 +__con300 % 1.74/1.94 +__con301 % 1.74/1.94 +__con302 % 1.74/1.94 +__con303 % 1.74/1.94 -__con305 % 1.74/1.94 -__con306 % 1.74/1.94 -__con307 % 1.74/1.94 +__con311 % 1.74/1.94 +__con313 % 1.74/1.94 +__con314 % 1.74/1.94 -__con315 % 1.74/1.94 -__con316 % 1.74/1.94 -__con317 % 1.74/1.94 -__con318 % 1.74/1.94 +__con321 % 1.74/1.94 +__con322 % 1.74/1.94 +__con323 % 1.74/1.94 +__con324 % 1.74/1.94 +__con325 % 1.74/1.94 +__con329 % 1.74/1.94 +__con330 % 1.74/1.94 +__con331 % 1.74/1.94 +__con332 % 1.74/1.94 +__con333 % 1.74/1.94 -__con342 % 1.74/1.94 -__con345 % 1.74/1.94 +__con346 % 1.74/1.94 -__con348 % 1.74/1.94 +__con349 % 1.74/1.94 -__con353 % 1.74/1.94 +__con354 % 1.74/1.94 +__con355 % 1.74/1.94 +__con358 % 1.74/1.94 +__con359 % 1.74/1.94 +__con360 % 1.74/1.94 +__con361 % 1.74/1.94 -__con363 % 1.74/1.94 +__con381 % 1.74/1.94 +__con383 % 1.74/1.94 +__con384 % 1.74/1.94 +__con385 % 1.74/1.94 +__con386 % 1.74/1.94 +__con387 % 1.74/1.94 +__con388 % 1.74/1.94 +__con389 % 1.74/1.94 +__con390 % 1.74/1.94 +__con391 % 1.74/1.94 +__con396 % 1.74/1.94 -__con397 % 1.74/1.94 -__con398 % 1.74/1.94 +__con399 % 1.74/1.94 -__con407 % 1.74/1.94 +__con408 % 1.74/1.94 -__con409 % 1.74/1.94 -__con410 % 1.74/1.94 -__con411 % 1.74/1.94 -__con412 % 1.74/1.94 -__con413 % 1.74/1.94 +__con414 % 1.74/1.94 +__con415 % 1.74/1.94 +__con416 % 1.74/1.94 -__con417 % 1.74/1.94 -__con425 % 1.74/1.94 +__con426 % 1.74/1.94 +__con427 % 1.74/1.94 -__con432 % 1.74/1.94 +__con433 % 1.74/1.94 -__con434 % 1.74/1.94 -__con435 % 1.74/1.94 +__con436 % 1.74/1.94 -__con437 % 1.74/1.94 -__con438 % 1.74/1.94 -__con439 % 1.74/1.94 +__con443 % 1.74/1.94 +__con444 % 1.74/1.94 -__con446 % 1.74/1.94 -__con447 % 1.74/1.94 +__con448 % 1.74/1.94 +__con449 % 1.74/1.94 +__con450 % 1.74/1.94 +__con454 % 1.74/1.94 +__con456 % 1.74/1.94 +__con457 % 1.74/1.94 +__con458 % 1.74/1.94 +__con459 % 1.74/1.94 +__con460 % 1.74/1.94 +__con462 % 1.74/1.94 +__con464 % 1.74/1.94 -__con483 % 1.74/1.94 +__con484 % 1.74/1.94 -__con485 % 1.74/1.94 -__con486 % 1.74/1.94 -__con487 % 1.74/1.94 -__con499 % 1.74/1.94 +__con500 % 1.74/1.94 -__con505 % 1.74/1.94 +__con506 % 1.74/1.94 -__con507 % 1.74/1.94 -__con508 % 1.74/1.94 +__con509 % 1.74/1.94 +__con510 % 1.74/1.94 +__con515 % 1.74/1.94 +__con516 % 1.74/1.94 +__con517 % 1.74/1.94 +__con518 % 1.74/1.94 -__con530 % 1.74/1.94 +__con531 % 1.74/1.94 +__con537 % 1.74/1.94 +__con538 % 1.74/1.94 +__con539 % 1.74/1.94 +__con540 % 1.74/1.94 -c10_0 % 1.74/1.94 +c10_1(a963) % 1.74/1.94 +c10_1(a972) % 1.74/1.94 +c10_1(a980) % 1.74/1.94 +c10_1(a1003) % 1.74/1.94 +c10_1(a1062) % 1.74/1.94 +c10_1(a1066) % 1.74/1.94 +c10_1(a1106) % 1.74/1.94 +c10_1(a1118) % 1.74/1.94 +c10_1(a1125) % 1.74/1.94 +c10_1(a1133) % 1.74/1.94 +c10_2(a963, =0) % 1.74/1.94 +c10_2(a1005, a1111) % 1.74/1.94 +c10_2(a1008, a1009) % 1.74/1.94 +c10_2(a1013, a1014) % 1.74/1.94 +c10_2(a1013, a1111) % 1.74/1.94 +c10_2(a1068, a1111) % 1.74/1.94 +c10_2(a1118, a1111) % 1.74/1.94 +c10_2(a1183, a1185) % 1.74/1.94 -c10_2(a1087, a1088) % 1.74/1.94 -c10_2(a1106, a1108) % 1.74/1.94 -c10_2(a1125, a1126) % 1.74/1.94 +c1_0 % 1.74/1.94 -c1_1(a1068) % 1.74/1.94 +c1_2(a963, a964) % 1.74/1.94 +c1_2(a980, =0) % 1.74/1.94 +c1_2(a1003, a1004) % 1.74/1.94 +c1_2(a1066, a1067) % 1.74/1.94 +c1_2(a1068, a1070) % 1.74/1.94 +c1_2(a1120, a1121) % 1.74/1.94 +c1_2(a1125, a1126) % 1.74/1.94 -c1_2(a1008, a1010) % 1.74/1.94 -c1_2(a1125, a1127) % 1.74/1.94 +c2_0 % 1.74/1.94 +c2_1(a963) % 1.74/1.94 +c2_1(a980) % 1.74/1.94 +c2_1(a1003) % 1.74/1.94 +c2_1(a1106) % 1.74/1.94 +c2_1(a1118) % 1.74/1.94 +c2_2(a963, =0) % 1.74/1.94 +c2_2(a980, =0) % 1.74/1.94 +c2_2(a1003, =0) % 1.74/1.94 +c2_2(a1106, =0) % 1.74/1.94 +c2_2(a1106, a1108) % 1.74/1.94 +c2_2(a1118, =0) % 1.74/1.94 +c2_2(a1131, a1132) % 1.74/1.94 -c2_2(a963, a1084) % 1.74/1.94 -c2_2(a980, a1084) % 1.74/1.94 -c2_2(a1003, a1084) % 1.74/1.94 -c2_2(a1008, a1010) % 1.74/1.94 -c2_2(a1068, a1069) % 1.74/1.94 -c2_2(a1068, a1070) % 1.74/1.94 -c2_2(a1118, a1119) % 1.74/1.94 +c3_0 % 1.74/1.94 +c3_1(=0) % 1.74/1.94 +c3_1(a963) % 1.74/1.94 +c3_1(a980) % 1.74/1.94 +c3_1(a1003) % 1.74/1.94 +c3_1(a1020) % 1.74/1.94 +c3_1(a1106) % 1.74/1.94 +c3_1(a1118) % 1.74/1.94 -c3_1(a1068) % 1.74/1.94 +c3_2(a963, a1084) % 1.74/1.94 +c3_2(a980, a1084) % 1.74/1.94 +c3_2(a1003, a1084) % 1.74/1.94 +c3_2(a1008, a1009) % 1.74/1.94 +c3_2(a1118, a1119) % 1.74/1.94 -c3_2(a1106, a1108) % 1.74/1.94 -c3_2(a1125, a1126) % 1.74/1.94 +c4_0 % 1.74/1.94 +c4_1(a972) % 1.74/1.94 +c4_1(a1066) % 1.74/1.94 +c4_1(a1118) % 1.74/1.94 +c4_1(a1120) % 1.74/1.94 +c4_1(a1133) % 1.74/1.94 -c4_1(a1125) % 1.74/1.94 +c4_2(a963, a964) % 1.74/1.94 +c4_2(a1106, a1107) % 1.74/1.94 +c4_2(a1118, a1119) % 1.74/1.94 +c4_2(a1125, a1127) % 1.74/1.94 -c4_2(a980, a981) % 1.74/1.94 -c4_2(a1087, a1088) % 1.74/1.94 +c5_0 % 1.74/1.94 +c5_1(a1106) % 1.74/1.94 +c5_1(a1123) % 1.74/1.94 +c5_1(a1125) % 1.74/1.94 +c5_2(a980, a981) % 1.74/1.94 +c5_2(a1005, a1112) % 1.74/1.94 +c5_2(a1013, a1112) % 1.74/1.94 +c5_2(a1068, a1112) % 1.74/1.94 +c5_2(a1087, =0) % 1.74/1.94 +c5_2(a1118, a1112) % 1.74/1.94 +c5_2(a1125, a1127) % 1.74/1.94 +c5_2(a1133, a1134) % 1.74/1.94 -c5_2(a963, a964) % 1.74/1.94 -c5_2(a1068, a1069) % 1.74/1.94 -c5_2(a1087, a1088) % 1.74/1.94 +c6_0 % 1.74/1.94 +c6_1(a1005) % 1.74/1.94 +c6_1(a1013) % 1.74/1.94 +c6_1(a1068) % 1.74/1.94 +c6_1(a1118) % 1.74/1.94 -c6_1(a963) % 1.74/1.94 +c6_2(a980, a981) % 1.74/1.94 +c6_2(a1066, a1067) % 1.74/1.94 +c6_2(a1087, a1088) % 1.74/1.94 -c6_2(a1008, a1010) % 1.74/1.94 -c6_2(a1106, a1107) % 1.74/1.94 +c7_0 % 1.74/1.94 +c7_1(a972) % 1.74/1.94 +c7_1(a1066) % 1.74/1.94 +c7_1(a1118) % 1.74/1.94 +c7_1(a1133) % 1.74/1.94 -c7_1(a980) % 1.74/1.94 +c7_2(a1005, a1112) % 1.74/1.94 +c7_2(a1013, a1112) % 1.74/1.94 +c7_2(a1068, a1112) % 1.74/1.94 +c7_2(a1118, a1112) % 1.74/1.94 -c8_0 % 1.74/1.94 +c8_1(a963) % 1.74/1.94 +c8_1(a972) % 1.74/1.94 +c8_1(a980) % 1.74/1.94 +c8_1(a1003) % 1.74/1.94 +c8_1(a1005) % 1.74/1.94 +c8_1(a1013) % 1.74/1.94 +c8_1(a1062) % 1.74/1.94 +c8_1(a1066) % 1.74/1.94 +c8_1(a1068) % 1.74/1.94 +c8_1(a1106) % 1.74/1.94 +c8_1(a1118) % 1.74/1.94 +c8_1(a1125) % 1.74/1.94 +c8_1(a1133) % 1.74/1.94 +c8_2(a1008, a1009) % 1.74/1.94 +c8_2(a1013, a1014) % 1.74/1.94 +c8_2(a1068, a1070) % 1.74/1.94 +c8_2(a1125, a1126) % 1.74/1.94 -c8_2(a1106, a1108) % 1.74/1.94 +c9_0 % 1.74/1.94 +c9_1(a977) % 1.74/1.94 +c9_1(a1020) % 1.74/1.94 +c9_2(a1106, a1107) % 1.74/1.94 +c9_2(a1106, a1149) % 1.74/1.94 +c9_2(a1125, a1149) % 1.74/1.94 +epred10_0 % 1.74/1.94 +epred12_0 % 1.74/1.94 +epred13_0 % 1.74/1.94 +epred14_0 % 1.74/1.94 +epred2_0 % 1.74/1.94 +epred3_0 % 1.74/1.94 +epred4_0 % 1.74/1.94 +epred5_0 % 1.74/1.94 +epred6_0 % 1.74/1.94 +epred7_0 % 1.74/1.94 +epred8_0 % 1.74/1.94 +epred9_0 % 1.74/1.94 +ndr1_0 % 1.74/1.94 +ndr1_1(a963) % 1.74/1.94 +ndr1_1(a980) % 1.74/1.94 +ndr1_1(a1003) % 1.74/1.94 +ndr1_1(a1005) % 1.74/1.94 +ndr1_1(a1008) % 1.74/1.94 +ndr1_1(a1013) % 1.74/1.94 +ndr1_1(a1066) % 1.74/1.94 +ndr1_1(a1068) % 1.74/1.94 +ndr1_1(a1087) % 1.74/1.94 +ndr1_1(a1106) % 1.74/1.94 +ndr1_1(a1118) % 1.74/1.94 +ndr1_1(a1120) % 1.74/1.94 +ndr1_1(a1125) % 1.74/1.94 +ndr1_1(a1131) % 1.74/1.94 +ndr1_1(a1133) % 1.74/1.94 +ndr1_1(a1183) % 1.74/1.94 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------