%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN425+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % 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 : 0s % DateTime : Thu Jul 21 03:49:52 EDT 2022 % Result : CounterSatisfiable 1.01s 1.18s % Output : Model 1.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN425+1 : TPTP v8.1.0. Released v2.1.0. % 0.11/0.13 % Command : darwin -pl 0 -pmc true -to %d %s % 0.13/0.34 % Computer : n020.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 04:38:42 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.34 Defaulting to tptp format. % 1.01/1.18 SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.01/1.18 % 1.01/1.18 MODEL (CONTEXT): % 1.01/1.18 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.01/1.18 -__-v__(=0) % 1.01/1.18 -__con234 % 1.01/1.18 +__con235 % 1.01/1.18 -__con236 % 1.01/1.18 +__con237 % 1.01/1.18 +__con240 % 1.01/1.18 +__con241 % 1.01/1.18 +__con242 % 1.01/1.18 +__con243 % 1.01/1.18 +__con244 % 1.01/1.18 +__con245 % 1.01/1.18 -__con246 % 1.01/1.18 +__con247 % 1.01/1.18 -__con248 % 1.01/1.18 +__con250 % 1.01/1.18 -__con255 % 1.01/1.18 -__con257 % 1.01/1.18 -__con258 % 1.01/1.18 -__con259 % 1.01/1.18 +__con260 % 1.01/1.18 +__con261 % 1.01/1.18 +__con262 % 1.01/1.18 +__con263 % 1.01/1.18 +__con264 % 1.01/1.18 +__con265 % 1.01/1.18 +__con266 % 1.01/1.18 +__con267 % 1.01/1.18 +__con268 % 1.01/1.18 +__con269 % 1.01/1.18 +__con270 % 1.01/1.18 +__con271 % 1.01/1.18 +__con273 % 1.01/1.18 +__con274 % 1.01/1.18 +__con275 % 1.01/1.18 +__con276 % 1.01/1.18 -__con283 % 1.01/1.18 +__con284 % 1.01/1.18 -__con292 % 1.01/1.18 +__con293 % 1.01/1.18 +__con302 % 1.01/1.18 +__con303 % 1.01/1.18 +__con304 % 1.01/1.18 +__con305 % 1.01/1.18 +__con306 % 1.01/1.18 +__con307 % 1.01/1.18 +__con308 % 1.01/1.18 +__con309 % 1.01/1.18 +__con310 % 1.01/1.18 +__con311 % 1.01/1.18 +__con312 % 1.01/1.18 +__con316 % 1.01/1.18 +__con317 % 1.01/1.18 +__con318 % 1.01/1.18 -__con319 % 1.01/1.18 -__con320 % 1.01/1.18 -__con325 % 1.01/1.18 -__con326 % 1.01/1.18 +__con327 % 1.01/1.18 +__con361 % 1.01/1.18 +__con363 % 1.01/1.18 +__con364 % 1.01/1.18 +__con365 % 1.01/1.18 +__con366 % 1.01/1.18 +__con367 % 1.01/1.18 +__con368 % 1.01/1.18 -__con419 % 1.01/1.18 +__con420 % 1.01/1.18 -__con421 % 1.01/1.18 +__con422 % 1.01/1.18 +__con423 % 1.01/1.18 +__con424 % 1.01/1.18 -__con437 % 1.01/1.18 +__con438 % 1.01/1.18 +__con439 % 1.01/1.18 -__con440 % 1.01/1.18 -__con463 % 1.01/1.18 +__con464 % 1.01/1.18 -__con465 % 1.01/1.18 -__con468 % 1.01/1.18 +__con473 % 1.01/1.18 -__con479 % 1.01/1.18 +__con480 % 1.01/1.18 +c10_0 % 1.01/1.18 +c10_1(a1208) % 1.01/1.18 +c10_1(a1220) % 1.01/1.18 +c10_1(a1305) % 1.01/1.18 +c10_1(a1327) % 1.01/1.18 +c10_1(a1357) % 1.01/1.18 -c10_1(a1211) % 1.01/1.18 +c10_2(a1208, a1352) % 1.01/1.18 +c10_2(a1211, a1212) % 1.01/1.18 +c10_2(a1211, a1352) % 1.01/1.18 +c10_2(a1242, a1352) % 1.01/1.18 +c10_2(a1244, a1245) % 1.01/1.18 +c10_2(a1298, a1352) % 1.01/1.18 +c10_2(a1305, a1352) % 1.01/1.18 +c10_2(a1307, a1352) % 1.01/1.18 +c10_2(a1327, a1352) % 1.01/1.18 +c10_2(a1331, a1352) % 1.01/1.18 +c10_2(a1333, a1352) % 1.01/1.18 +c10_2(a1335, a1352) % 1.01/1.18 +c10_2(a1346, a1352) % 1.01/1.18 +c10_2(a1357, a1352) % 1.01/1.18 +c10_2(a1361, a1352) % 1.01/1.18 -c10_2(a1331, a1332) % 1.01/1.18 +c1_0 % 1.01/1.18 +c1_1(a1214) % 1.01/1.18 +c1_1(a1215) % 1.01/1.18 +c1_1(a1305) % 1.01/1.18 +c1_2(a1220, a1300) % 1.01/1.18 +c1_2(a1305, a1306) % 1.01/1.18 +c1_2(a1357, a1358) % 1.01/1.18 +c2_0 % 1.01/1.18 +c2_1(=0) % 1.01/1.18 +c2_1(a1220) % 1.01/1.18 +c2_1(a1244) % 1.01/1.18 -c2_1(a1208) % 1.01/1.18 -c2_1(a1211) % 1.01/1.18 -c2_1(a1242) % 1.01/1.18 -c2_1(a1298) % 1.01/1.18 -c2_1(a1305) % 1.01/1.18 -c2_1(a1307) % 1.01/1.18 -c2_1(a1327) % 1.01/1.18 -c2_1(a1331) % 1.01/1.18 -c2_1(a1333) % 1.01/1.18 -c2_1(a1335) % 1.01/1.18 -c2_1(a1346) % 1.01/1.18 -c2_1(a1357) % 1.01/1.18 -c2_1(a1361) % 1.01/1.18 +c2_2(a1215, a1216) % 1.01/1.18 +c2_2(a1242, a1243) % 1.01/1.18 -c2_2(a1211, a1212) % 1.01/1.18 -c2_2(a1220, a1317) % 1.01/1.18 -c2_2(a1346, a1347) % 1.01/1.18 -c3_0 % 1.01/1.18 +c3_1(a1214) % 1.01/1.18 +c3_1(a1331) % 1.01/1.18 +c3_1(a1333) % 1.01/1.18 +c3_1(a1343) % 1.01/1.18 -c3_2(a1327, a1328) % 1.01/1.18 +c4_0 % 1.01/1.18 +c4_1(a1220) % 1.01/1.18 +c4_1(a1244) % 1.01/1.18 +c4_2(a1244, a1245) % 1.01/1.18 +c4_2(a1298, a1299) % 1.01/1.18 -c4_2(a1208, a1352) % 1.01/1.18 -c4_2(a1346, a1347) % 1.01/1.18 -c5_0 % 1.01/1.18 +c5_2(a1220, a1300) % 1.01/1.18 -c5_2(a1226, a1227) % 1.01/1.18 +c6_0 % 1.01/1.18 +c6_1(=0) % 1.01/1.18 +c6_1(a1215) % 1.01/1.18 +c6_1(a1247) % 1.01/1.18 -c6_1(a1200) % 1.01/1.18 -c6_1(a1220) % 1.01/1.18 -c6_1(a1357) % 1.01/1.18 +c6_2(a1244, a1245) % 1.01/1.18 +c6_2(a1333, a1334) % 1.01/1.18 +c6_2(a1346, a1347) % 1.01/1.18 +c6_2(a1357, a1358) % 1.01/1.18 -c6_2(a1220, a1317) % 1.01/1.18 -c6_2(a1226, a1227) % 1.01/1.18 -c7_0 % 1.01/1.18 +c7_1(a1200) % 1.01/1.18 +c7_1(a1214) % 1.01/1.18 +c7_1(a1215) % 1.01/1.18 +c7_1(a1220) % 1.01/1.18 +c7_1(a1226) % 1.01/1.18 +c7_1(a1244) % 1.01/1.18 +c7_1(a1269) % 1.01/1.18 +c7_1(a1278) % 1.01/1.18 +c7_1(a1305) % 1.01/1.18 +c7_1(a1357) % 1.01/1.18 +c7_2(a1244, a1245) % 1.01/1.18 +c7_2(a1331, a1332) % 1.01/1.18 -c8_0 % 1.01/1.18 +c8_1(a1207) % 1.01/1.18 +c8_1(a1208) % 1.01/1.18 +c8_1(a1214) % 1.01/1.18 +c8_1(a1242) % 1.01/1.18 +c8_1(a1247) % 1.01/1.18 +c8_1(a1331) % 1.01/1.18 +c8_1(a1333) % 1.01/1.18 +c8_1(a1343) % 1.01/1.18 +c8_1(a1361) % 1.01/1.18 +c8_2(a1327, a1328) % 1.01/1.18 -c8_2(a1211, a1212) % 1.01/1.18 -c8_2(a1226, a1227) % 1.01/1.18 +c9_0 % 1.01/1.18 +c9_1(a1207) % 1.01/1.18 +c9_1(a1208) % 1.01/1.18 +c9_1(a1242) % 1.01/1.18 +c9_1(a1247) % 1.01/1.18 -c9_1(a1226) % 1.01/1.18 +c9_2(a1357, a1358) % 1.01/1.18 -c9_2(a1331, a1332) % 1.01/1.18 -epred1_0 % 1.01/1.18 +epred2_0 % 1.01/1.18 +epred5_0 % 1.01/1.18 +epred6_0 % 1.01/1.18 +epred7_0 % 1.01/1.18 +epred8_0 % 1.01/1.18 +ndr1_0 % 1.01/1.18 +ndr1_1(a1208) % 1.01/1.18 +ndr1_1(a1211) % 1.01/1.18 +ndr1_1(a1215) % 1.01/1.18 +ndr1_1(a1220) % 1.01/1.18 +ndr1_1(a1226) % 1.01/1.18 +ndr1_1(a1242) % 1.01/1.18 +ndr1_1(a1244) % 1.01/1.18 +ndr1_1(a1298) % 1.01/1.18 +ndr1_1(a1305) % 1.01/1.18 +ndr1_1(a1307) % 1.01/1.18 +ndr1_1(a1327) % 1.01/1.18 +ndr1_1(a1331) % 1.01/1.18 +ndr1_1(a1333) % 1.01/1.18 +ndr1_1(a1335) % 1.01/1.18 +ndr1_1(a1346) % 1.01/1.18 +ndr1_1(a1357) % 1.01/1.18 +ndr1_1(a1361) % 1.01/1.18 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------