%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : SYN428+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n022.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.29s 1.45s % Output : Model 1.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN428+1 : TPTP v8.1.0. Released v2.1.0. % 0.07/0.12 % Command : darwin -pl 0 -pmc true -to %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % DateTime : Tue Jul 12 07:08:55 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 Defaulting to tptp format. % 1.29/1.45 SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.29/1.45 % 1.29/1.45 MODEL (CONTEXT): % 1.29/1.45 SZS output start Model for /export/starexec/sandbox/benchmark/theBenchmark.p % 1.29/1.45 -__-v__(=0) % 1.29/1.45 +__con256 % 1.29/1.45 +__con257 % 1.29/1.45 +__con258 % 1.29/1.45 +__con262 % 1.29/1.45 +__con263 % 1.29/1.45 -__con264 % 1.29/1.45 -__con265 % 1.29/1.45 +__con266 % 1.29/1.45 +__con275 % 1.29/1.45 +__con276 % 1.29/1.45 +__con277 % 1.29/1.45 -__con278 % 1.29/1.45 +__con279 % 1.29/1.45 +__con281 % 1.29/1.45 +__con283 % 1.29/1.45 +__con284 % 1.29/1.45 -__con285 % 1.29/1.45 +__con286 % 1.29/1.45 +__con287 % 1.29/1.45 +__con288 % 1.29/1.45 +__con289 % 1.29/1.45 +__con290 % 1.29/1.45 +__con291 % 1.29/1.45 +__con292 % 1.29/1.45 +__con294 % 1.29/1.45 +__con295 % 1.29/1.45 +__con296 % 1.29/1.45 -__con302 % 1.29/1.45 -__con309 % 1.29/1.45 -__con314 % 1.29/1.45 +__con317 % 1.29/1.45 +__con318 % 1.29/1.45 +__con319 % 1.29/1.45 +__con320 % 1.29/1.45 -__con324 % 1.29/1.45 -__con325 % 1.29/1.45 +__con330 % 1.29/1.45 +__con331 % 1.29/1.45 +__con333 % 1.29/1.45 +__con334 % 1.29/1.45 +__con335 % 1.29/1.45 +__con336 % 1.29/1.45 +__con337 % 1.29/1.45 +__con338 % 1.29/1.45 +__con339 % 1.29/1.45 +__con340 % 1.29/1.45 +__con341 % 1.29/1.45 +__con342 % 1.29/1.45 +__con343 % 1.29/1.45 +__con348 % 1.29/1.45 +__con349 % 1.29/1.45 +__con350 % 1.29/1.45 +__con351 % 1.29/1.45 +__con353 % 1.29/1.45 +__con354 % 1.29/1.45 -__con362 % 1.29/1.45 -__con363 % 1.29/1.45 +__con364 % 1.29/1.45 +__con365 % 1.29/1.45 +__con366 % 1.29/1.45 +__con367 % 1.29/1.45 -__con372 % 1.29/1.45 -__con373 % 1.29/1.45 -__con378 % 1.29/1.45 -__con379 % 1.29/1.45 +__con380 % 1.29/1.45 +__con381 % 1.29/1.45 +__con382 % 1.29/1.45 +__con383 % 1.29/1.45 -__con393 % 1.29/1.45 -__con394 % 1.29/1.45 -__con395 % 1.29/1.45 -__con396 % 1.29/1.45 +__con399 % 1.29/1.45 +__con400 % 1.29/1.45 +__con401 % 1.29/1.45 +__con402 % 1.29/1.45 +__con403 % 1.29/1.45 +__con404 % 1.29/1.45 +__con405 % 1.29/1.45 +__con408 % 1.29/1.45 +__con409 % 1.29/1.45 +__con410 % 1.29/1.45 +__con411 % 1.29/1.45 +__con421 % 1.29/1.45 +__con422 % 1.29/1.45 -__con423 % 1.29/1.45 +__con424 % 1.29/1.45 +__con431 % 1.29/1.45 +__con432 % 1.29/1.45 +__con433 % 1.29/1.45 +__con434 % 1.29/1.45 +__con440 % 1.29/1.45 +__con441 % 1.29/1.45 +__con442 % 1.29/1.45 +__con443 % 1.29/1.45 -__con449 % 1.29/1.45 -__con450 % 1.29/1.45 -__con454 % 1.29/1.45 +__con455 % 1.29/1.45 -__con458 % 1.29/1.45 +__con459 % 1.29/1.45 +__con460 % 1.29/1.45 +__con461 % 1.29/1.45 +__con463 % 1.29/1.45 -__con464 % 1.29/1.45 +__con476 % 1.29/1.45 +__con477 % 1.29/1.45 +__con479 % 1.29/1.45 +__con480 % 1.29/1.45 +__con481 % 1.29/1.45 -__con482 % 1.29/1.45 +__con483 % 1.29/1.45 +__con484 % 1.29/1.45 +__con485 % 1.29/1.45 +__con486 % 1.29/1.45 +__con487 % 1.29/1.45 +__con493 % 1.29/1.45 +__con494 % 1.29/1.45 +__con495 % 1.29/1.45 -__con497 % 1.29/1.45 +__con498 % 1.29/1.45 -__con501 % 1.29/1.45 +__con502 % 1.29/1.45 -__con503 % 1.29/1.45 +__con508 % 1.29/1.45 +__con510 % 1.29/1.45 +__con511 % 1.29/1.45 +__con514 % 1.29/1.45 +__con515 % 1.29/1.45 +__con516 % 1.29/1.45 -__con520 % 1.29/1.45 +__con521 % 1.29/1.45 +__con522 % 1.29/1.45 +__con523 % 1.29/1.45 +__con524 % 1.29/1.45 +__con525 % 1.29/1.45 +__con539 % 1.29/1.45 +__con540 % 1.29/1.45 +__con541 % 1.29/1.45 +__con542 % 1.29/1.45 +__con543 % 1.29/1.45 -__con544 % 1.29/1.45 -__con545 % 1.29/1.45 +__con546 % 1.29/1.45 +__con547 % 1.29/1.45 +__con548 % 1.29/1.45 +__con549 % 1.29/1.45 +__con553 % 1.29/1.45 +__con554 % 1.29/1.45 +__con555 % 1.29/1.45 +__con562 % 1.29/1.45 +__con563 % 1.29/1.45 +__con564 % 1.29/1.45 +__con565 % 1.29/1.45 -__con589 % 1.29/1.45 +__con590 % 1.29/1.45 -__con591 % 1.29/1.45 +__con592 % 1.29/1.45 +__con603 % 1.29/1.45 -__con605 % 1.29/1.45 +__con606 % 1.29/1.45 +__con609 % 1.29/1.45 -__con610 % 1.29/1.45 +__con612 % 1.29/1.45 -__con613 % 1.29/1.45 +__con614 % 1.29/1.45 +__con615 % 1.29/1.45 -__con618 % 1.29/1.45 -__con619 % 1.29/1.45 +__con626 % 1.29/1.45 +__con627 % 1.29/1.45 +__con630 % 1.29/1.45 +__con631 % 1.29/1.45 +__con632 % 1.29/1.45 +__con633 % 1.29/1.45 +__con634 % 1.29/1.45 +__con635 % 1.29/1.45 +__con636 % 1.29/1.45 +__con642 % 1.29/1.45 +__con645 % 1.29/1.45 -__con648 % 1.29/1.45 +__con649 % 1.29/1.45 +__con650 % 1.29/1.45 +__con651 % 1.29/1.45 +__con652 % 1.29/1.45 -__con653 % 1.29/1.45 -__con654 % 1.29/1.45 +__con655 % 1.29/1.45 -c10_0 % 1.29/1.45 +c10_1(a1839) % 1.29/1.45 +c10_1(a1841) % 1.29/1.45 +c10_1(a1865) % 1.29/1.45 +c10_1(a1877) % 1.29/1.45 +c10_1(a1879) % 1.29/1.45 +c10_1(a1881) % 1.29/1.45 +c10_1(a1921) % 1.29/1.45 +c10_1(a1931) % 1.29/1.45 +c10_1(a1933) % 1.29/1.45 +c10_1(a1946) % 1.29/1.45 +c10_1(a1950) % 1.29/1.45 +c10_1(a1951) % 1.29/1.45 +c10_1(a1963) % 1.29/1.45 +c10_1(a1997) % 1.29/1.45 +c10_1(a1998) % 1.29/1.45 +c10_1(a2001) % 1.29/1.45 +c10_1(a2017) % 1.29/1.45 -c10_1(a1907) % 1.29/1.45 -c10_1(a1970) % 1.29/1.45 -c10_1(a2023) % 1.29/1.45 +c10_2(a1877, a1878) % 1.29/1.45 +c10_2(a1881, a1982) % 1.29/1.45 +c10_2(a1933, a1982) % 1.29/1.45 +c10_2(a1951, a1982) % 1.29/1.45 +c10_2(a1997, a1982) % 1.29/1.45 +c10_2(a1998, a1999) % 1.29/1.45 +c10_2(a2021, a1982) % 1.29/1.45 -c10_2(a1933, a1948) % 1.29/1.45 +c1_0 % 1.29/1.45 +c1_1(a1839) % 1.29/1.45 +c1_1(a1841) % 1.29/1.45 +c1_1(a1845) % 1.29/1.45 +c1_1(a1865) % 1.29/1.45 +c1_1(a1877) % 1.29/1.45 +c1_1(a1879) % 1.29/1.45 +c1_1(a1881) % 1.29/1.45 +c1_1(a1907) % 1.29/1.45 +c1_1(a1921) % 1.29/1.45 +c1_1(a1931) % 1.29/1.45 +c1_1(a1933) % 1.29/1.45 +c1_1(a1946) % 1.29/1.45 +c1_1(a1950) % 1.29/1.45 +c1_1(a1951) % 1.29/1.45 +c1_1(a1963) % 1.29/1.45 +c1_1(a1997) % 1.29/1.45 +c1_1(a1998) % 1.29/1.45 +c1_1(a2001) % 1.29/1.45 +c1_1(a2017) % 1.29/1.45 -c1_1(a1926) % 1.29/1.45 -c1_1(a2021) % 1.29/1.45 +c1_2(a1881, a1882) % 1.29/1.45 +c1_2(a1881, a1983) % 1.29/1.45 +c1_2(a1907, a1983) % 1.29/1.45 +c1_2(a1921, a1983) % 1.29/1.45 +c1_2(a1931, a1932) % 1.29/1.45 +c1_2(a1933, a1983) % 1.29/1.45 +c1_2(a1950, a1983) % 1.29/1.45 +c1_2(a1951, a1983) % 1.29/1.45 +c1_2(a1963, a1983) % 1.29/1.45 +c1_2(a1997, a1983) % 1.29/1.45 +c1_2(a1998, a2000) % 1.29/1.45 -c1_2(a1877, a1878) % 1.29/1.45 -c1_2(a1933, a1934) % 1.29/1.45 -c2_0 % 1.29/1.45 +c2_1(a1839) % 1.29/1.45 +c2_1(a1841) % 1.29/1.45 +c2_1(a1845) % 1.29/1.45 +c2_1(a1865) % 1.29/1.45 +c2_1(a1877) % 1.29/1.45 +c2_1(a1879) % 1.29/1.45 +c2_1(a1881) % 1.29/1.45 +c2_1(a1907) % 1.29/1.45 +c2_1(a1921) % 1.29/1.45 +c2_1(a1931) % 1.29/1.45 +c2_1(a1933) % 1.29/1.45 +c2_1(a1946) % 1.29/1.45 +c2_1(a1950) % 1.29/1.45 +c2_1(a1951) % 1.29/1.45 +c2_1(a1963) % 1.29/1.45 +c2_1(a1997) % 1.29/1.45 +c2_1(a1998) % 1.29/1.45 +c2_1(a2001) % 1.29/1.45 +c2_1(a2014) % 1.29/1.45 +c2_1(a2017) % 1.29/1.45 +c2_2(a1841, a1842) % 1.29/1.45 +c2_2(a1907, a1863) % 1.29/1.45 +c2_2(a1907, a1983) % 1.29/1.45 +c2_2(a2017, =0) % 1.29/1.45 -c2_2(a1841, a1864) % 1.29/1.45 -c2_2(a1841, a1948) % 1.29/1.45 -c2_2(a1877, a1878) % 1.29/1.45 -c2_2(a1933, _0) % 1.29/1.45 +c3_0 % 1.29/1.45 +c3_1(=0) % 1.29/1.45 +c3_1(a1903) % 1.29/1.45 +c3_1(a1912) % 1.29/1.45 +c3_1(a1970) % 1.29/1.45 +c3_1(a2017) % 1.29/1.45 -c3_1(a1881) % 1.29/1.45 -c3_1(a1933) % 1.29/1.45 -c3_1(a1951) % 1.29/1.45 -c3_1(a1997) % 1.29/1.45 -c3_1(a2021) % 1.29/1.45 +c3_2(a1839, a1840) % 1.29/1.45 +c3_2(a1865, a1867) % 1.29/1.45 +c3_2(a1998, a1999) % 1.29/1.45 +c4_0 % 1.29/1.45 +c4_1(a1839) % 1.29/1.45 +c4_1(a1841) % 1.29/1.45 +c4_1(a1865) % 1.29/1.45 +c4_1(a1877) % 1.29/1.45 +c4_1(a1879) % 1.29/1.45 +c4_1(a1881) % 1.29/1.45 +c4_1(a1907) % 1.29/1.45 +c4_1(a1921) % 1.29/1.45 +c4_1(a1926) % 1.29/1.45 +c4_1(a1931) % 1.29/1.45 +c4_1(a1933) % 1.29/1.45 +c4_1(a1946) % 1.29/1.45 +c4_1(a1950) % 1.29/1.45 +c4_1(a1951) % 1.29/1.45 +c4_1(a1963) % 1.29/1.45 +c4_1(a1997) % 1.29/1.45 +c4_1(a1998) % 1.29/1.45 +c4_1(a2001) % 1.29/1.45 +c4_1(a2017) % 1.29/1.45 +c4_1(a2021) % 1.29/1.45 -c4_1(a1857) % 1.29/1.45 +c4_2(a1841, a1842) % 1.29/1.45 +c4_2(a1926, a1883) % 1.29/1.45 +c4_2(a2021, a1883) % 1.29/1.45 +c5_0 % 1.29/1.45 +c5_1(a1881) % 1.29/1.45 +c5_1(a1907) % 1.29/1.45 +c5_1(a1921) % 1.29/1.45 +c5_1(a1926) % 1.29/1.45 +c5_1(a1933) % 1.29/1.45 +c5_1(a1950) % 1.29/1.45 +c5_1(a1951) % 1.29/1.45 +c5_1(a1963) % 1.29/1.45 +c5_1(a1997) % 1.29/1.45 +c5_1(a2021) % 1.29/1.45 -c5_1(a1970) % 1.29/1.45 +c5_2(a1881, a1982) % 1.29/1.45 +c5_2(a1933, a1934) % 1.29/1.45 +c5_2(a1933, a1982) % 1.29/1.45 +c5_2(a1951, a1982) % 1.29/1.45 +c5_2(a1997, a1982) % 1.29/1.45 +c5_2(a2021, a1982) % 1.29/1.45 -c5_2(a1881, a1983) % 1.29/1.45 -c5_2(a1907, a1983) % 1.29/1.45 -c5_2(a1921, a1983) % 1.29/1.45 -c5_2(a1933, a1983) % 1.29/1.45 -c5_2(a1950, a1983) % 1.29/1.45 -c5_2(a1951, a1983) % 1.29/1.45 -c5_2(a1963, a1983) % 1.29/1.45 -c5_2(a1997, a1983) % 1.29/1.45 -c6_0 % 1.29/1.45 -c6_1(a1926) % 1.29/1.45 -c6_1(a1931) % 1.29/1.45 +c6_2(a1926, a1883) % 1.29/1.45 +c6_2(a1998, a2000) % 1.29/1.45 +c6_2(a2021, a1883) % 1.29/1.45 -c6_2(a1933, a1948) % 1.29/1.45 +c7_0 % 1.29/1.45 +c7_1(a1970) % 1.29/1.45 -c7_1(a1975) % 1.29/1.45 +c7_2(a1839, a1948) % 1.29/1.45 +c7_2(a1841, a1864) % 1.29/1.45 +c7_2(a1841, a1948) % 1.29/1.45 +c7_2(a1865, a1948) % 1.29/1.45 +c7_2(a1877, a1948) % 1.29/1.45 +c7_2(a1879, a1948) % 1.29/1.45 +c7_2(a1881, a1948) % 1.29/1.45 +c7_2(a1907, a1864) % 1.29/1.45 +c7_2(a1921, a1864) % 1.29/1.45 +c7_2(a1921, a1948) % 1.29/1.45 +c7_2(a1931, a1932) % 1.29/1.45 +c7_2(a1931, a1948) % 1.29/1.45 +c7_2(a1933, a1948) % 1.29/1.45 +c7_2(a1946, a1864) % 1.29/1.45 +c7_2(a1946, a1948) % 1.29/1.45 +c7_2(a1950, a1948) % 1.29/1.45 +c7_2(a1951, a1948) % 1.29/1.45 +c7_2(a1963, a1948) % 1.29/1.45 +c7_2(a1997, a1864) % 1.29/1.45 +c7_2(a1997, a1948) % 1.29/1.45 +c7_2(a1998, a1948) % 1.29/1.45 +c7_2(a2001, a1948) % 1.29/1.45 +c7_2(a2017, a1864) % 1.29/1.45 +c7_2(a2017, a1948) % 1.29/1.45 -c7_2(a1841, a1842) % 1.29/1.45 -c8_0 % 1.29/1.45 +c8_1(a1841) % 1.29/1.45 +c8_1(a1907) % 1.29/1.45 +c8_1(a1921) % 1.29/1.45 +c8_1(a1946) % 1.29/1.45 +c8_1(a1997) % 1.29/1.45 +c8_1(a2017) % 1.29/1.45 -c8_1(a1933) % 1.29/1.45 -c8_1(a2021) % 1.29/1.45 -c8_1(a2023) % 1.29/1.45 +c8_2(a1841, a1863) % 1.29/1.45 +c8_2(a1881, a1983) % 1.29/1.45 +c8_2(a1907, a1863) % 1.29/1.45 +c8_2(a1907, a1983) % 1.29/1.45 +c8_2(a1921, a1863) % 1.29/1.45 +c8_2(a1921, a1983) % 1.29/1.45 +c8_2(a1933, a1934) % 1.29/1.45 +c8_2(a1933, a1983) % 1.29/1.45 +c8_2(a1946, a1863) % 1.29/1.45 +c8_2(a1950, a1983) % 1.29/1.45 +c8_2(a1951, a1983) % 1.29/1.45 +c8_2(a1963, a1983) % 1.29/1.45 +c8_2(a1997, a1863) % 1.29/1.45 +c8_2(a1997, a1983) % 1.29/1.45 +c8_2(a2017, a1863) % 1.29/1.45 -c9_0 % 1.29/1.45 +c9_2(a1926, a1883) % 1.29/1.45 +c9_2(a1998, a2000) % 1.29/1.45 +c9_2(a2021, a1883) % 1.29/1.45 -c9_2(a1881, a1982) % 1.29/1.45 -c9_2(a1933, a1982) % 1.29/1.45 -c9_2(a1951, a1982) % 1.29/1.45 -c9_2(a1997, a1982) % 1.29/1.45 -c9_2(a2021, a1982) % 1.29/1.45 +epred11_0 % 1.29/1.45 +epred2_0 % 1.29/1.45 +epred3_0 % 1.29/1.45 +epred5_0 % 1.29/1.45 +epred6_0 % 1.29/1.45 +epred9_0 % 1.29/1.45 +ndr1_0 % 1.29/1.45 +ndr1_1(a1839) % 1.29/1.45 +ndr1_1(a1841) % 1.29/1.45 +ndr1_1(a1865) % 1.29/1.45 +ndr1_1(a1877) % 1.29/1.45 +ndr1_1(a1879) % 1.29/1.45 +ndr1_1(a1881) % 1.29/1.45 +ndr1_1(a1907) % 1.29/1.45 +ndr1_1(a1921) % 1.29/1.45 +ndr1_1(a1926) % 1.29/1.45 +ndr1_1(a1931) % 1.29/1.45 +ndr1_1(a1933) % 1.29/1.45 +ndr1_1(a1946) % 1.29/1.45 +ndr1_1(a1950) % 1.29/1.45 +ndr1_1(a1951) % 1.29/1.45 +ndr1_1(a1963) % 1.29/1.45 +ndr1_1(a1997) % 1.29/1.45 +ndr1_1(a1998) % 1.29/1.45 +ndr1_1(a2001) % 1.29/1.45 +ndr1_1(a2017) % 1.29/1.45 +ndr1_1(a2021) % 1.29/1.45 SZS output end Model for /export/starexec/sandbox/benchmark/theBenchmark.p %------------------------------------------------------------------------------