%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL657+1.005 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n008.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 : 600s % DateTime : Sun Jul 17 14:31:38 EDT 2022 % Result : Unknown 5.90s 6.11s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : LCL657+1.005 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : sos-script %s % 0.12/0.33 % Computer : n008.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 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jul 4 11:58:38 EDT 2022 % 0.12/0.33 % CPUTime : % 4.45/4.64 ----- Otter 3.2, August 2001 ----- % 4.45/4.64 The process was started by sandbox on n008.cluster.edu, % 4.45/4.64 Mon Jul 4 11:58:38 2022 % 4.45/4.64 The command was "./sos". The process ID is 31309. % 4.45/4.64 % 4.45/4.64 set(prolog_style_variables). % 4.45/4.64 set(auto). % 4.45/4.64 dependent: set(auto1). % 4.45/4.64 dependent: set(process_input). % 4.45/4.64 dependent: clear(print_kept). % 4.45/4.64 dependent: clear(print_new_demod). % 4.45/4.64 dependent: clear(print_back_demod). % 4.45/4.64 dependent: clear(print_back_sub). % 4.45/4.64 dependent: set(control_memory). % 4.45/4.64 dependent: assign(max_mem, 12000). % 4.45/4.64 dependent: assign(pick_given_ratio, 4). % 4.45/4.64 dependent: assign(stats_level, 1). % 4.45/4.64 dependent: assign(pick_semantic_ratio, 3). % 4.45/4.64 dependent: assign(sos_limit, 5000). % 4.45/4.64 dependent: assign(max_weight, 60). % 4.45/4.64 clear(print_given). % 4.45/4.64 % 4.45/4.64 formula_list(usable). % 4.45/4.64 % 4.45/4.64 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=10. % 4.45/4.64 % 4.45/4.64 This is a non-Horn set without equality. The strategy % 4.45/4.64 will be ordered hyper_res, ur_res, unit deletion, and % 4.45/4.64 factoring, with satellites in sos and nuclei in usable. % 4.45/4.64 % 4.45/4.64 dependent: set(hyper_res). % 4.45/4.64 dependent: set(factor). % 4.45/4.64 dependent: set(unit_deletion). % 4.45/4.64 % 4.45/4.64 ------------> process usable: % 4.45/4.64 1391 back subsumes 1383. % 4.45/4.64 1391 back subsumes 1380. % 4.45/4.64 1396 back subsumes 1390. % 4.45/4.64 1397 back subsumes 1395. % 4.45/4.64 1398 back subsumes 1388. % 4.45/4.64 1402 back subsumes 1378. % 4.45/4.64 1414 back subsumes 1407. % 4.45/4.64 1414 back subsumes 1404. % 4.45/4.64 1418 back subsumes 1413. % 4.45/4.64 1438 back subsumes 1430. % 4.45/4.64 1438 back subsumes 1427. % 4.45/4.64 1443 back subsumes 1437. % 4.45/4.64 1444 back subsumes 1442. % 4.45/4.64 1445 back subsumes 1435. % 4.45/4.64 1449 back subsumes 1425. % 4.45/4.64 1461 back subsumes 1454. % 4.45/4.64 1461 back subsumes 1451. % 4.45/4.64 1465 back subsumes 1460. % 4.45/4.64 1485 back subsumes 1477. % 4.45/4.64 1485 back subsumes 1474. % 4.45/4.64 1490 back subsumes 1484. % 4.45/4.64 1491 back subsumes 1489. % 4.45/4.64 1492 back subsumes 1482. % 4.45/4.64 1496 back subsumes 1472. % 4.45/4.64 1508 back subsumes 1501. % 4.45/4.64 1508 back subsumes 1498. % 4.45/4.64 1512 back subsumes 1507. % 4.45/4.64 1532 back subsumes 1524. % 4.45/4.64 1532 back subsumes 1521. % 4.45/4.64 1537 back subsumes 1531. % 4.45/4.64 1538 back subsumes 1536. % 4.45/4.64 1539 back subsumes 1529. % 4.45/4.64 1543 back subsumes 1519. % 4.45/4.64 1555 back subsumes 1548. % 4.45/4.64 1555 back subsumes 1545. % 4.45/4.64 1559 back subsumes 1554. % 4.45/4.64 1569 back subsumes 1567. % 4.45/4.64 1575 back subsumes 1573. % 4.45/4.64 1584 back subsumes 1582. % 4.45/4.64 1608 back subsumes 1600. % 4.45/4.64 1608 back subsumes 1597. % 4.45/4.64 1613 back subsumes 1607. % 4.45/4.64 1614 back subsumes 1612. % 4.45/4.64 1615 back subsumes 1605. % 4.45/4.64 1619 back subsumes 1595. % 4.45/4.64 1631 back subsumes 1624. % 4.45/4.64 1631 back subsumes 1621. % 4.45/4.64 1635 back subsumes 1630. % 4.45/4.64 1645 back subsumes 1643. % 4.45/4.64 1656 back subsumes 1654. % 4.45/4.64 1667 back subsumes 1665. % 4.45/4.64 1678 back subsumes 1676. % 4.45/4.64 1684 back subsumes 1542. % 4.45/4.64 1684 back subsumes 1517. % 4.45/4.64 1684 back subsumes 1109. % 4.45/4.64 1684 back subsumes 1102. % 4.45/4.64 1684 back subsumes 1091. % 4.45/4.64 1684 back subsumes 1084. % 4.45/4.64 1684 back subsumes 1073. % 4.45/4.64 1684 back subsumes 1066. % 4.45/4.64 1684 back subsumes 1055. % 4.45/4.64 1684 back subsumes 1048. % 4.45/4.64 1684 back subsumes 1037. % 4.45/4.64 1684 back subsumes 1030. % 4.45/4.64 1684 back subsumes 1019. % 4.45/4.64 1684 back subsumes 1012. % 4.45/4.64 1684 back subsumes 1001. % 4.45/4.64 1684 back subsumes 994. % 4.45/4.64 1684 back subsumes 983. % 4.45/4.64 1684 back subsumes 976. % 4.45/4.64 1687 back subsumes 1111. % 4.45/4.64 1687 back subsumes 1107. % 4.45/4.64 1687 back subsumes 1093. % 4.45/4.64 1687 back subsumes 1089. % 4.45/4.64 1687 back subsumes 1075. % 4.45/4.64 1687 back subsumes 1071. % 4.45/4.64 1687 back subsumes 1057. % 4.45/4.64 1687 back subsumes 1053. % 4.45/4.64 1687 back subsumes 1039. % 4.45/4.64 1687 back subsumes 1035. % 4.45/4.64 1687 back subsumes 1021. % 4.45/4.64 1687 back subsumes 1017. % 4.45/4.64 1687 back subsumes 1003. % 4.45/4.64 1687 back subsumes 999. % 4.45/4.64 1687 back subsumes 985. % 4.45/4.64 1687 back subsumes 981. % 4.45/4.64 % 4.45/4.64 ------------> process sos: % 4.45/4.64 % 4.45/4.64 ======= end of input processing ======= % 5.90/6.11 % 5.90/6.11 Stopped by limit on insertions % 5.90/6.11 % 5.90/6.11 % 5.90/6.11 % 5.90/6.11 Aborting on detection of an error: % 5.90/6.11 % 5.90/6.11 Too many clauses (whew!). % 5.90/6.11 %------------------------------------------------------------------------------