%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL220-1 : TPTP v8.1.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n015.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:28:48 EDT 2022 % Result : Timeout 299.36s 299.67s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : LCL220-1 : TPTP v8.1.0. Released v1.1.0. % 0.11/0.13 % Command : sos-script %s % 0.13/0.34 % Computer : n015.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 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 4 15:08:31 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.36 ----- Otter 3.2, August 2001 ----- % 0.13/0.36 The process was started by sandbox2 on n015.cluster.edu, % 0.13/0.36 Mon Jul 4 15:08:31 2022 % 0.13/0.36 The command was "./sos". The process ID is 9626. % 0.13/0.36 % 0.13/0.36 set(prolog_style_variables). % 0.13/0.36 set(auto). % 0.13/0.36 dependent: set(auto1). % 0.13/0.36 dependent: set(process_input). % 0.13/0.36 dependent: clear(print_kept). % 0.13/0.36 dependent: clear(print_new_demod). % 0.13/0.36 dependent: clear(print_back_demod). % 0.13/0.36 dependent: clear(print_back_sub). % 0.13/0.36 dependent: set(control_memory). % 0.13/0.36 dependent: assign(max_mem, 12000). % 0.13/0.36 dependent: assign(pick_given_ratio, 4). % 0.13/0.36 dependent: assign(stats_level, 1). % 0.13/0.36 dependent: assign(pick_semantic_ratio, 3). % 0.13/0.36 dependent: assign(sos_limit, 5000). % 0.13/0.36 dependent: assign(max_weight, 60). % 0.13/0.36 clear(print_given). % 0.13/0.36 % 0.13/0.36 list(usable). % 0.13/0.36 % 0.13/0.36 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. % 0.13/0.36 % 0.13/0.36 This is a Horn set without equality. The strategy will % 0.13/0.36 be hyperresolution, with satellites in sos and nuclei % 0.13/0.36 in usable. % 0.13/0.36 % 0.13/0.36 dependent: set(hyper_res). % 0.13/0.36 dependent: clear(order_hyper). % 0.13/0.36 % 0.13/0.36 ------------> process usable: % 0.13/0.36 % 0.13/0.36 ------------> process sos: % 0.13/0.36 % 0.13/0.36 ======= end of input processing ======= % 0.13/0.39 % 0.13/0.39 Model 1 (0.00 seconds, 0 Inserts) % 0.13/0.39 % 0.13/0.39 Stopped by limit on number of solutions % 0.13/0.39 % 0.13/0.39 % 0.13/0.39 -------------- Softie stats -------------- % 0.13/0.39 % 0.13/0.39 UPDATE_STOP: 300 % 0.13/0.39 SFINDER_TIME_LIMIT: 2 % 0.13/0.39 SHORT_CLAUSE_CUTOFF: 4 % 0.13/0.39 number of clauses in intial UL: 4 % 0.13/0.39 number of clauses initially in problem: 9 % 0.13/0.39 percentage of clauses intially in UL: 44 % 0.13/0.39 percentage of distinct symbols occuring in initial UL: 100 % 0.13/0.39 percent of all initial clauses that are short: 100 % 0.13/0.39 absolute distinct symbol count: 6 % 0.13/0.39 distinct predicate count: 2 % 0.13/0.39 distinct function count: 2 % 0.13/0.39 distinct constant count: 2 % 0.13/0.39 % 0.13/0.39 ---------- no more Softie stats ---------- % 0.13/0.39 % 0.13/0.39 % 0.13/0.39 % 0.13/0.39 Model 2 (0.00 seconds, 0 Inserts) % 0.13/0.39 % 0.13/0.39 Stopped by limit on number of solutions % 0.13/0.39 % 0.13/0.39 =========== start of search =========== % 5.65/5.88 % 5.65/5.88 % 5.65/5.88 Changing weight limit from 60 to 47. % 5.65/5.88 % 5.65/5.88 Model 3 (0.00 seconds, 0 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on number of solutions % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 4 [ 1 0 146 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 5 [ 1 1 525 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 6 [ 1 6 43439 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 7 [ 2 3 27441 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 8 [ 3 0 1655 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Stopped by limit on insertions % 5.65/5.88 % 5.65/5.88 Model 9 [ 4 2 13319 ] (0.00 seconds, 250000 Inserts) % 5.65/5.88 % 5.65/5.88 Modelling stopped after 300 given clauses and 0.00 seconds % 5.65/5.88 % 5.65/5.88 % 5.65/5.88 Resetting weight limit to 47 after 1670 givens. % 5.65/5.88 % 5.73/5.96 % 5.73/5.96 % 5.73/5.96 Changing weight limit from 47 to 33. % 5.73/5.96 % 5.73/5.96 Resetting weight limit to 33 after 1815 givens. % 5.73/5.96 % 5.73/5.97 % 5.73/5.97 % 5.73/5.97 Changing weight limit from 33 to 31. % 5.73/5.97 % 5.73/5.97 Resetting weight limit to 31 after 1820 givens. % 5.73/5.97 % 5.73/5.98 % 5.73/5.98 % 5.73/5.98 Changing weight limit from 31 to 29. % 5.73/5.98 % 5.73/5.98 Resetting weight limit to 29 after 1835 givens. % 5.73/5.98 % 5.84/6.01 % 5.84/6.01 % 5.84/6.01 Changing weight limit from 29 to 28. % 5.84/6.01 % 5.84/6.01 Resetting weight limit to 28 after 1860 givens. % 5.84/6.01 % 5.85/6.02 % 5.85/6.02 % 5.85/6.02 Changing weight limit from 28 to 27. % 5.85/6.02 % 5.85/6.02 Resetting weight limit to 27 after 1880 givens. % 5.85/6.02 % 5.85/6.08 % 5.85/6.08 % 5.85/6.08 Changing weight limit from 27 to 26. % 5.85/6.08 % 5.85/6.08 Resetting weight limit to 26 after 1945 givens. % 5.85/6.08 % 5.85/6.09 % 5.85/6.09 % 5.85/6.09 Changing weight limit from 26 to 25. % 5.85/6.09 % 5.85/6.09 Resetting weight limit to 25 after 1970 givens. % 5.85/6.09 % 6.03/6.22 % 6.03/6.22 % 6.03/6.22 Changing weight limit from 25 to 24. % 6.03/6.22 % 6.03/6.22 Resetting weight limit to 24 after 2110 givens. % 6.03/6.22 % 6.03/6.24 % 6.03/6.24 % 6.03/6.24 Changing weight limit from 24 to 23. % 6.03/6.24 % 6.03/6.24 Resetting weight limit to 23 after 2135 givens. % 6.03/6.24 % 6.15/6.38 % 6.15/6.38 % 6.15/6.38 Changing weight limit from 23 to 22. % 6.15/6.38 % 6.15/6.38 Resetting weight limit to 22 after 2285 givens. % 6.15/6.38 % 6.24/6.41 % 6.24/6.41 % 6.24/6.41 Changing weight limit from 22 to 21. % 6.24/6.41 % 6.24/6.41 Resetting weight limit to 21 after 2320 givens. % 6.24/6.41 % 6.44/6.65 % 6.44/6.65 % 6.44/6.65 Changing weight limit from 21 to 20. % 6.44/6.65 % 6.44/6.65 Resetting weight limit to 20 after 2580 givens. % 6.44/6.65 % 6.63/6.80 % 6.63/6.80 % 6.63/6.80 Changing weight limit from 20 to 19. % 6.63/6.80 % 6.63/6.80 Resetting weight limit to 19 after 2870 givens. % 6.63/6.80 % 36.94/37.15 % 36.94/37.15 % 36.94/37.15 Changing weight limit from 19 to 20. % 36.94/37.15 % 36.94/37.15 Resetting weight limit to 20 after 62725 givens. % 36.94/37.15 % 36.94/37.16 % 36.94/37.16 % 36.94/37.16 Changing weight limit from 20 to 19. % 36.94/37.16 % 36.94/37.16 Resetting weight limit to 19 after 62730 givens. % 36.94/37.16 % 36.94/37.17 % 36.94/37.17 % 36.94/37.17 Changing weight limit from 19 to 20. % 36.94/37.17 % 36.94/37.17 Resetting weight limit to 20 after 62745 givens. % 36.94/37.17 % 36.94/37.17 % 36.94/37.17 % 36.94/37.17 Changing weight limit from 20 to 19. % 36.94/37.17 % 36.94/37.17 Resetting weight limit to 19 after 62750 givens. % 36.94/37.17 % 36.94/37.18 % 36.94/37.18 % 36.94/37.18 Changing weight limit from 19 to 20. % 36.94/37.18 % 36.94/37.18 Resetting weight limit to 20 after 62765 givens. % 36.94/37.18 % 36.94/37.19 % 36.94/37.19 % 36.94/37.19 Changing weight limit from 20 to 19. % 36.94/37.19 % 36.94/37.19 Resetting weight limit to 19 after 62770 givens. % 36.94/37.19 % 36.94/37.19 % 36.94/37.19 % 36.94/37.19 Changing weight limit from 19 to 20. % 36.94/37.19 % 36.94/37.19 Resetting weight limit to 20 after 62785 givens. % 36.94/37.19 % 36.94/37.19 % 36.94/37.19 % 36.94/37.19 Changing weight limit from 20 to 19. % 36.94/37.19 % 36.94/37.19 Resetting weight limit to 19 after 62790 givens. % 36.94/37.19 % 36.94/37.20 % 36.94/37.20 % 36.94/37.20 Changing weight limit from 19 to 20. % 36.94/37.20 % 36.94/37.20 Resetting weight limit to 20 after 62805 givens. % 36.94/37.20 % 36.94/37.20 % 36.94/37.20 % 36.94/37.20 Changing weight limit from 20 to 19. % 36.94/37.20 % 36.94/37.20 Resetting weight limit to 19 after 62810 givens. % 36.94/37.20 % 37.04/37.22 % 37.04/37.22 % 37.04/37.22 Changing weight limit from 19 to 20. % 37.04/37.22 % 37.04/37.22 Resetting weight limit to 20 after 62825 givens. % 37.04/37.22 % 37.04/37.22 % 37.04/37.22 % 37.04/37.22 Changing weight limit from 20 to 19. % 37.04/37.22 % 37.04/37.22 Resetting weight limit to 19 after 62830 givens. % 37.04/37.22 % 37.04/37.24 % 37.04/37.24 % 37.04/37.24 Changing weight limit from 19 to 20. % 37.04/37.24 % 37.04/37.24 Resetting weight limit to 20 after 62845 givens. % 37.04/37.24 % 37.04/37.24 % 37.04/37.24 % 37.04/37.24 Changing weight limit from 20 to 19. % 37.04/37.24 % 37.04/37.24 Resetting weight limit to 19 after 62850 givens. % 37.04/37.24 % 37.04/37.25 % 37.04/37.25 % 37.04/37.25 Changing weight limit from 19 to 20. % 37.04/37.25 % 37.04/37.25 Resetting weight limit to 20 after 62865 givens. % 37.04/37.25 % 37.04/37.26 % 37.04/37.26 % 37.04/37.26 Changing weight limit from 20 to 19. % 37.04/37.26 % 37.04/37.26 Resetting weight limit to 19 after 62870 givens. % 37.04/37.26 % 37.04/37.26 % 37.04/37.26 % 37.04/37.26 Changing weight limit from 19 to 20. % 37.04/37.26 % 37.04/37.26 Resetting weight limit to 20 after 62885 givens. % 37.04/37.26 % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 Changing weight limit from 20 to 19. % 37.04/37.27 % 37.04/37.27 Resetting weight limit to 19 after 62890 givens. % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 Changing weight limit from 19 to 20. % 37.04/37.27 % 37.04/37.27 Resetting weight limit to 20 after 62895 givens. % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 Changing weight limit from 20 to 19. % 37.04/37.27 % 37.04/37.27 Resetting weight limit to 19 after 62900 givens. % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 Changing weight limit from 19 to 20. % 37.04/37.27 % 37.04/37.27 Resetting weight limit to 20 after 62905 givens. % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 % 37.04/37.27 Changing weight limit from 20 to 19. % 37.04/37.27 % 37.04/37.27 Resetting weight limit to 19 after 62910 givens. % 37.04/37.27 % 37.04/37.28 % 37.04/37.28 % 37.04/37.28 Changing weight limit from 19 to 20. % 37.04/37.28 % 37.04/37.28 Resetting weight limit to 20 after 62925 givens. % 37.04/37.28 % 37.04/37.28 % 37.04/37.28 % 37.04/37.28 Changing weight limit from 20 to 19. % 37.04/37.28 % 37.04/37.28 Resetting weight limit to 19 after 62930 givens. % 37.04/37.28 % 37.11/37.30 % 37.11/37.30 % 37.11/37.30 Changing weight limit from 19 to 20. % 37.11/37.30 % 37.11/37.30 Resetting weight limit to 20 after 62965 givens. % 37.11/37.30 % 37.11/37.30 % 37.11/37.30 % 37.11/37.30 Changing weight limit from 20 to 19. % 37.11/37.30 % 37.11/37.30 Resetting weight limit to 19 after 62970 givens. % 37.11/37.30 % 37.11/37.31 % 37.11/37.31 % 37.11/37.31 Changing weight limit from 19 to 20. % 37.11/37.31 % 37.11/37.31 Resetting weight limit to 20 after 62985 givens. % 37.11/37.31 % 37.11/37.32 % 37.11/37.32 % 37.11/37.32 Changing weight limit from 20 to 19. % 37.11/37.32 % 37.11/37.32 Resetting weight limit to 19 after 62990 givens. % 37.11/37.32 % 37.11/37.33 % 37.11/37.33 % 37.11/37.33 Changing weight limit from 19 to 20. % 37.11/37.33 % 37.11/37.33 Resetting weight limit to 20 after 63005 givens. % 37.11/37.33 % 37.11/37.33 % 37.11/37.33 % 37.11/37.33 Changing weight limit from 20 to 19. % 37.11/37.33 % 37.11/37.33 Resetting weight limit to 19 after 63010 givens. % 37.11/37.33 % 37.11/37.35 % 37.11/37.35 % 37.11/37.35 Changing weight limit from 19 to 20. % 37.11/37.35 % 37.11/37.35 Resetting weight limit to 20 after 63040 givens. % 37.11/37.35 % 37.11/37.35 % 37.11/37.35 % 37.11/37.35 Changing weight limit from 20 to 21. % 37.11/37.35 % 37.11/37.35 Resetting weight limit to 21 after 63045 givens. % 37.11/37.35 % 231.23/231.55 % 231.23/231.55 % 231.23/231.55 Changing weight limit from 21 to 22. % 231.23/231.55 % 231.23/231.55 Resetting weight limit to 22 after 192385 givens. % 231.23/231.55 % 231.23/231.57 % 231.23/231.57 % 231.23/231.57 Changing weight limit from 22 to 21. % 231.23/231.57 % 231.23/231.57 Resetting weight limit to 21 after 192390 givens. % 231.23/231.57 % 231.37/231.65 % 231.37/231.65 % 231.37/231.65 Changing weight limit from 21 to 22. % 231.37/231.65 % 231.37/231.65 Resetting weight limit to 22 after 192425 givens. % 231.37/231.65 % 231.37/231.66 % 231.37/231.66 % 231.37/231.66 Changing weight limit from 22 to 21. % 231.37/231.66 % 231.37/231.66 Resetting weight limit to 21 after 192430 givens. % 231.37/231.66 % 231.37/231.68 % 231.37/231.68 % 231.37/231.68 Changing weight limit from 21 to 22. % 231.37/231.68 % 231.37/231.68 Resetting weight limit to 22 after 192435 givens. % 231.37/231.68 % 231.37/231.69 % 231.37/231.69 % 231.37/231.69 Changing weight limit from 22 to 21. % 231.37/231.69 % 231.37/231.69 Resetting weight limit to 21 after 192440 givens. % 231.37/231.69 % 231.46/231.76 % 231.46/231.76 % 231.46/231.76 Changing weight limit from 21 to 22. % 231.46/231.76 % 231.46/231.76 Resetting weight limit to 22 after 192485 givens. % 231.46/231.76 % 231.46/231.78 % 231.46/231.78 % 231.46/231.78 Changing weight limit from 22 to 21. % 231.46/231.78 % 231.46/231.78 Resetting weight limit to 21 after 192490 givens. % 231.46/231.78 % 231.53/231.87 % 231.53/231.87 % 231.53/231.87 Changing weight limit from 21 to 22. % 231.53/231.87 % 231.53/231.87 Resetting weight limit to 22 after 192525 givens. % 231.53/231.87 % 231.62/231.88 % 231.62/231.88 % 231.62/231.88 Changing weight limit from 22 to 21. % 231.62/231.88 % 231.62/231.88 Resetting weight limit to 21 after 192530 givens. % 231.62/231.88 % 231.64/231.90 % 231.64/231.90 % 231.64/231.90 Changing weight limit from 21 to 22. % 231.64/231.90 % 231.64/231.90 Resetting weight limit to 22 after 192545 givens. % 231.64/231.90 % 231.64/231.91 % 231.64/231.91 % 231.64/231.91 Changing weight limit from 22 to 21. % 231.64/231.91 % 231.64/231.91 Resetting weight limit to 21 after 192550 givens. % 231.64/231.91 % 231.82/232.13 % 231.82/232.13 % 231.82/232.13 Changing weight limit from 21 to 22. % 231.82/232.13 % 231.82/232.13 Resetting weight limit to 22 after 192645 givens. % 231.82/232.13 % 232.89/233.21 % 232.89/233.21 % 232.89/233.21 Changing weight limit from 22 to 23. % 232.89/233.21 % 232.89/233.21 Resetting weight limit to 23 after 193085 givens. % 232.89/233.21 % 299.36/299.67 % 299.36/299.67 % 299.36/299.67 Changing weight limit from 23 to 22. % 299.36/299.67 % 299.36/299.67 Resetting weight limit to 22 after 211630 givens. % 299.36/299.67 % 300.05/300.32 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------