%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SWV419-1.030 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n023.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 : Wed Jul 20 21:38:26 EDT 2022 % Result : Timeout 300.06s 300.31s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWV419-1.030 : TPTP v8.1.0. Released v3.5.0. % 0.06/0.13 % Command : sos-script %s % 0.13/0.34 % Computer : n023.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 : Wed Jun 15 16:36:35 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.37 ----- Otter 3.2, August 2001 ----- % 0.13/0.37 The process was started by sandbox on n023.cluster.edu, % 0.13/0.37 Wed Jun 15 16:36:35 2022 % 0.13/0.37 The command was "./sos". The process ID is 2930. % 0.13/0.37 % 0.13/0.37 set(prolog_style_variables). % 0.13/0.37 set(auto). % 0.13/0.37 dependent: set(auto1). % 0.13/0.37 dependent: set(process_input). % 0.13/0.37 dependent: clear(print_kept). % 0.13/0.37 dependent: clear(print_new_demod). % 0.13/0.37 dependent: clear(print_back_demod). % 0.13/0.37 dependent: clear(print_back_sub). % 0.13/0.37 dependent: set(control_memory). % 0.13/0.37 dependent: assign(max_mem, 12000). % 0.13/0.37 dependent: assign(pick_given_ratio, 4). % 0.13/0.37 dependent: assign(stats_level, 1). % 0.13/0.37 dependent: assign(pick_semantic_ratio, 3). % 0.13/0.37 dependent: assign(sos_limit, 5000). % 0.13/0.37 dependent: assign(max_weight, 60). % 0.13/0.37 clear(print_given). % 0.13/0.37 % 0.13/0.37 list(usable). % 0.13/0.37 % 0.13/0.37 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=31. % 0.13/0.37 % 0.13/0.37 This is a non-Horn set without equality. The strategy % 0.13/0.37 will be ordered hyper_res, ur_res, unit deletion, and % 0.13/0.37 factoring, with satellites in sos and nuclei in usable. % 0.13/0.37 % 0.13/0.37 dependent: set(hyper_res). % 0.13/0.37 dependent: set(factor). % 0.13/0.37 dependent: set(unit_deletion). % 0.13/0.37 % 0.13/0.37 ------------> process usable: % 0.13/0.37 % 0.13/0.37 ------------> process sos: % 0.13/0.37 % 0.13/0.37 ======= end of input processing ======= % 1.18/1.38 % 1.18/1.38 Stopped by limit on insertions % 1.18/1.38 % 1.18/1.38 % 1.18/1.38 Failed to model usable list: disabling FINDER % 1.18/1.38 % 1.18/1.38 % 1.18/1.38 % 1.18/1.38 -------------- Softie stats -------------- % 1.18/1.38 % 1.18/1.38 UPDATE_STOP: 300 % 1.18/1.38 SFINDER_TIME_LIMIT: 2 % 1.18/1.38 SHORT_CLAUSE_CUTOFF: 4 % 1.18/1.38 number of clauses in intial UL: 143 % 1.18/1.38 number of clauses initially in problem: 189 % 1.18/1.38 percentage of clauses intially in UL: 75 % 1.18/1.38 percentage of distinct symbols occuring in initial UL: 99 % 1.18/1.38 percent of all initial clauses that are short: 100 % 1.18/1.38 absolute distinct symbol count: 108 % 1.18/1.38 distinct predicate count: 56 % 1.18/1.38 distinct function count: 0 % 1.18/1.38 distinct constant count: 52 % 1.18/1.38 % 1.18/1.38 ---------- no more Softie stats ---------- % 1.18/1.38 % 1.18/1.38 % 1.18/1.38 % 1.18/1.38 =========== start of search =========== % 3.01/3.30 % 3.01/3.30 % 3.01/3.30 Changing weight limit from 60 to 58. % 3.01/3.30 % 3.01/3.30 Modelling stopped after 300 given clauses and 0.00 seconds % 3.01/3.30 % 3.01/3.30 % 3.01/3.30 Resetting weight limit to 58 after 6305 givens. % 3.01/3.30 % 3.11/3.34 % 3.11/3.34 % 3.11/3.34 Changing weight limit from 58 to 53. % 3.11/3.34 % 3.11/3.34 Resetting weight limit to 53 after 6315 givens. % 3.11/3.34 % 3.49/3.74 % 3.49/3.74 % 3.49/3.74 Changing weight limit from 53 to 49. % 3.49/3.74 % 3.49/3.74 Resetting weight limit to 49 after 6405 givens. % 3.49/3.74 % 3.59/3.78 % 3.59/3.78 % 3.59/3.78 Changing weight limit from 49 to 48. % 3.59/3.78 % 3.59/3.78 Resetting weight limit to 48 after 6410 givens. % 3.59/3.78 % 4.51/4.70 % 4.51/4.70 % 4.51/4.70 Changing weight limit from 48 to 44. % 4.51/4.70 % 4.51/4.70 Resetting weight limit to 44 after 6540 givens. % 4.51/4.70 % 4.69/4.93 % 4.69/4.93 % 4.69/4.93 Changing weight limit from 44 to 43. % 4.69/4.93 % 4.69/4.93 Resetting weight limit to 43 after 6595 givens. % 4.69/4.93 % 10.11/10.31 % 10.11/10.31 % 10.11/10.31 Changing weight limit from 43 to 39. % 10.11/10.31 % 10.11/10.31 Resetting weight limit to 39 after 8915 givens. % 10.11/10.31 % 11.01/11.29 % 11.01/11.29 % 11.01/11.29 Changing weight limit from 39 to 38. % 11.01/11.29 % 11.01/11.29 Resetting weight limit to 38 after 8990 givens. % 11.01/11.29 % 15.94/16.19 % 15.94/16.19 % 15.94/16.19 Changing weight limit from 38 to 34. % 15.94/16.19 % 15.94/16.19 Resetting weight limit to 34 after 9370 givens. % 15.94/16.19 % 16.52/16.71 % 16.52/16.71 % 16.52/16.71 Changing weight limit from 34 to 33. % 16.52/16.71 % 16.52/16.71 Resetting weight limit to 33 after 9410 givens. % 16.52/16.71 % 61.48/61.74 % 61.48/61.74 % 61.48/61.74 Changing weight limit from 33 to 34. % 61.48/61.74 % 61.48/61.74 Resetting weight limit to 34 after 36350 givens. % 61.48/61.74 % 61.48/61.74 % 61.48/61.74 % 61.48/61.74 Changing weight limit from 34 to 35. % 61.48/61.74 % 61.48/61.74 Resetting weight limit to 35 after 36355 givens. % 61.48/61.74 % 61.48/61.74 % 61.48/61.74 % 61.48/61.74 Changing weight limit from 35 to 36. % 61.48/61.74 % 61.48/61.74 Resetting weight limit to 36 after 36360 givens. % 61.48/61.74 % 61.48/61.75 % 61.48/61.75 % 61.48/61.75 Changing weight limit from 36 to 37. % 61.48/61.75 % 61.48/61.75 Resetting weight limit to 37 after 36365 givens. % 61.48/61.75 % 61.48/61.76 % 61.48/61.76 % 61.48/61.76 Changing weight limit from 37 to 38. % 61.48/61.76 % 61.48/61.76 Resetting weight limit to 38 after 36370 givens. % 61.48/61.76 % 61.48/61.76 % 61.48/61.76 % 61.48/61.76 Changing weight limit from 38 to 39. % 61.48/61.76 % 61.48/61.76 Resetting weight limit to 39 after 36375 givens. % 61.48/61.76 % 61.48/61.77 % 61.48/61.77 % 61.48/61.77 Changing weight limit from 39 to 40. % 61.48/61.77 % 61.48/61.77 Resetting weight limit to 40 after 36380 givens. % 61.48/61.77 % 61.48/61.77 % 61.48/61.77 % 61.48/61.77 Changing weight limit from 40 to 41. % 61.48/61.77 % 61.48/61.77 Resetting weight limit to 41 after 36385 givens. % 61.48/61.77 % 61.48/61.77 % 61.48/61.77 % 61.48/61.77 Changing weight limit from 41 to 42. % 61.48/61.77 % 61.48/61.77 Resetting weight limit to 42 after 36390 givens. % 61.48/61.77 % 61.48/61.78 % 61.48/61.78 % 61.48/61.78 Changing weight limit from 42 to 43. % 61.48/61.78 % 61.48/61.78 Resetting weight limit to 43 after 36395 givens. % 61.48/61.78 % 61.48/61.79 % 61.48/61.79 % 61.48/61.79 Changing weight limit from 43 to 44. % 61.48/61.79 % 61.48/61.79 Resetting weight limit to 44 after 36400 givens. % 61.48/61.79 % 61.58/61.80 % 61.58/61.80 % 61.58/61.80 Changing weight limit from 44 to 45. % 61.58/61.80 % 61.58/61.80 Resetting weight limit to 45 after 36405 givens. % 61.58/61.80 % 61.58/61.81 % 61.58/61.81 % 61.58/61.81 Changing weight limit from 45 to 46. % 61.58/61.81 % 61.58/61.81 Resetting weight limit to 46 after 36410 givens. % 61.58/61.81 % 61.58/61.82 % 61.58/61.82 % 61.58/61.82 Changing weight limit from 46 to 47. % 61.58/61.82 % 61.58/61.82 Resetting weight limit to 47 after 36415 givens. % 61.58/61.82 % 61.58/61.82 % 61.58/61.82 % 61.58/61.82 Changing weight limit from 47 to 48. % 61.58/61.82 % 61.58/61.82 Resetting weight limit to 48 after 36420 givens. % 61.58/61.82 % 61.58/61.83 % 61.58/61.83 % 61.58/61.83 Changing weight limit from 48 to 49. % 61.58/61.83 % 61.58/61.83 Resetting weight limit to 49 after 36425 givens. % 61.58/61.83 % 61.58/61.85 % 61.58/61.85 % 61.58/61.85 Changing weight limit from 49 to 50. % 61.58/61.85 % 61.58/61.85 Resetting weight limit to 50 after 36430 givens. % 61.58/61.85 % 61.58/61.86 % 61.58/61.86 % 61.58/61.86 Changing weight limit from 50 to 51. % 61.58/61.86 % 61.58/61.86 Resetting weight limit to 51 after 36435 givens. % 61.58/61.86 % 61.58/61.89 % 61.58/61.89 % 61.58/61.89 Changing weight limit from 51 to 52. % 61.58/61.89 % 61.58/61.89 Resetting weight limit to 52 after 36440 givens. % 61.58/61.89 % 61.67/61.90 % 61.67/61.90 % 61.67/61.90 Changing weight limit from 52 to 53. % 61.67/61.90 % 61.67/61.90 Resetting weight limit to 53 after 36445 givens. % 61.67/61.90 % 61.67/61.91 % 61.67/61.91 % 61.67/61.91 Changing weight limit from 53 to 54. % 61.67/61.91 % 61.67/61.91 Resetting weight limit to 54 after 36450 givens. % 61.67/61.91 % 65.57/65.84 % 65.57/65.84 % 65.57/65.84 Changing weight limit from 54 to 53. % 65.57/65.84 % 65.57/65.84 Resetting weight limit to 53 after 37010 givens. % 65.57/65.84 % 78.83/79.09 % 78.83/79.09 % 78.83/79.09 Changing weight limit from 53 to 52. % 78.83/79.09 % 78.83/79.09 Resetting weight limit to 52 after 37655 givens. % 78.83/79.09 % 79.26/79.52 % 79.26/79.52 % 79.26/79.52 Changing weight limit from 52 to 49. % 79.26/79.52 % 79.26/79.52 Resetting weight limit to 49 after 37710 givens. % 79.26/79.52 % 79.68/79.95 % 79.68/79.95 % 79.68/79.95 Changing weight limit from 49 to 48. % 79.68/79.95 % 79.68/79.95 Resetting weight limit to 48 after 37745 givens. % 79.68/79.95 % 94.19/94.50 % 94.19/94.50 % 94.19/94.50 Changing weight limit from 48 to 47. % 94.19/94.50 % 94.19/94.50 Resetting weight limit to 47 after 39280 givens. % 94.19/94.50 % 95.26/95.58 % 95.26/95.58 % 95.26/95.58 Changing weight limit from 47 to 44. % 95.26/95.58 % 95.26/95.58 Resetting weight limit to 44 after 39390 givens. % 95.26/95.58 % 95.45/95.70 % 95.45/95.70 % 95.45/95.70 Changing weight limit from 44 to 43. % 95.45/95.70 % 95.45/95.70 Resetting weight limit to 43 after 39400 givens. % 95.45/95.70 % 123.93/124.23 % 123.93/124.23 % 123.93/124.23 Changing weight limit from 43 to 42. % 123.93/124.23 % 123.93/124.23 Resetting weight limit to 42 after 43085 givens. % 123.93/124.23 % 126.45/126.69 % 126.45/126.69 % 126.45/126.69 Changing weight limit from 42 to 40. % 126.45/126.69 % 126.45/126.69 Resetting weight limit to 40 after 43440 givens. % 126.45/126.69 % 126.45/126.74 % 126.45/126.74 % 126.45/126.74 Changing weight limit from 40 to 39. % 126.45/126.74 % 126.45/126.74 Resetting weight limit to 39 after 43445 givens. % 126.45/126.74 % 132.24/132.54 % 132.24/132.54 % 132.24/132.54 Changing weight limit from 39 to 38. % 132.24/132.54 % 132.24/132.54 Resetting weight limit to 38 after 43995 givens. % 132.24/132.54 % 140.74/141.00 % 140.74/141.00 % 140.74/141.00 Changing weight limit from 38 to 39. % 140.74/141.00 % 140.74/141.00 Resetting weight limit to 39 after 47910 givens. % 140.74/141.00 % 140.74/141.01 % 140.74/141.01 % 140.74/141.01 Changing weight limit from 39 to 40. % 140.74/141.01 % 140.74/141.01 Resetting weight limit to 40 after 47915 givens. % 140.74/141.01 % 140.74/141.01 % 140.74/141.01 % 140.74/141.01 Changing weight limit from 40 to 41. % 140.74/141.01 % 140.74/141.01 Resetting weight limit to 41 after 47920 givens. % 140.74/141.01 % 140.74/141.02 % 140.74/141.02 % 140.74/141.02 Changing weight limit from 41 to 42. % 140.74/141.02 % 140.74/141.02 Resetting weight limit to 42 after 47925 givens. % 140.74/141.02 % 140.79/141.03 % 140.79/141.03 % 140.79/141.03 Changing weight limit from 42 to 43. % 140.79/141.03 % 140.79/141.03 Resetting weight limit to 43 after 47930 givens. % 140.79/141.03 % 140.79/141.03 % 140.79/141.03 % 140.79/141.03 Changing weight limit from 43 to 44. % 140.79/141.03 % 140.79/141.03 Resetting weight limit to 44 after 47935 givens. % 140.79/141.03 % 140.79/141.04 % 140.79/141.04 % 140.79/141.04 Changing weight limit from 44 to 45. % 140.79/141.04 % 140.79/141.04 Resetting weight limit to 45 after 47940 givens. % 140.79/141.04 % 140.81/141.05 % 140.81/141.05 % 140.81/141.05 Changing weight limit from 45 to 46. % 140.81/141.05 % 140.81/141.05 Resetting weight limit to 46 after 47945 givens. % 140.81/141.05 % 140.81/141.06 % 140.81/141.06 % 140.81/141.06 Changing weight limit from 46 to 47. % 140.81/141.06 % 140.81/141.06 Resetting weight limit to 47 after 47950 givens. % 140.81/141.06 % 140.81/141.07 % 140.81/141.07 % 140.81/141.07 Changing weight limit from 47 to 48. % 140.81/141.07 % 140.81/141.07 Resetting weight limit to 48 after 47955 givens. % 140.81/141.07 % 140.81/141.09 % 140.81/141.09 % 140.81/141.09 Changing weight limit from 48 to 49. % 140.81/141.09 % 140.81/141.09 Resetting weight limit to 49 after 47960 givens. % 140.81/141.09 % 140.88/141.12 % 140.88/141.12 % 140.88/141.12 Changing weight limit from 49 to 50. % 140.88/141.12 % 140.88/141.12 Resetting weight limit to 50 after 47965 givens. % 140.88/141.12 % 140.88/141.14 % 140.88/141.14 % 140.88/141.14 Changing weight limit from 50 to 51. % 140.88/141.14 % 140.88/141.14 Resetting weight limit to 51 after 47970 givens. % 140.88/141.14 % 140.88/141.16 % 140.88/141.16 % 140.88/141.16 Changing weight limit from 51 to 52. % 140.88/141.16 % 140.88/141.16 Resetting weight limit to 52 after 47975 givens. % 140.88/141.16 % 140.93/141.17 % 140.93/141.17 % 140.93/141.17 Changing weight limit from 52 to 53. % 140.93/141.17 % 140.93/141.17 Resetting weight limit to 53 after 47980 givens. % 140.93/141.17 % 140.93/141.19 % 140.93/141.19 % 140.93/141.19 Changing weight limit from 53 to 54. % 140.93/141.19 % 140.93/141.19 Resetting weight limit to 54 after 47985 givens. % 140.93/141.19 % 140.93/141.21 % 140.93/141.21 % 140.93/141.21 Changing weight limit from 54 to 55. % 140.93/141.21 % 140.93/141.21 Resetting weight limit to 55 after 47990 givens. % 140.93/141.21 % 140.93/141.22 % 140.93/141.22 % 140.93/141.22 Changing weight limit from 55 to 56. % 140.93/141.22 % 140.93/141.22 Resetting weight limit to 56 after 47995 givens. % 140.93/141.22 % 140.93/141.25 % 140.93/141.25 % 140.93/141.25 Changing weight limit from 56 to 57. % 140.93/141.25 % 140.93/141.25 Resetting weight limit to 57 after 48000 givens. % 140.93/141.25 % 141.02/141.27 % 141.02/141.27 % 141.02/141.27 Changing weight limit from 57 to 58. % 141.02/141.27 % 141.02/141.27 Resetting weight limit to 58 after 48005 givens. % 141.02/141.27 % 141.06/141.31 % 141.06/141.31 % 141.06/141.31 Changing weight limit from 58 to 59. % 141.06/141.31 % 141.06/141.31 Resetting weight limit to 59 after 48010 givens. % 141.06/141.31 % 141.10/141.36 % 141.10/141.36 % 141.10/141.36 Changing weight limit from 59 to 60. % 141.10/141.36 % 141.10/141.36 Resetting weight limit to 60 after 48015 givens. % 141.10/141.36 % 151.11/151.36 % 151.11/151.36 % 151.11/151.36 Changing weight limit from 60 to 59. % 151.11/151.36 % 151.11/151.36 Resetting weight limit to 59 after 48650 givens. % 151.11/151.36 % 151.62/151.87 % 151.62/151.87 % 151.62/151.87 Changing weight limit from 59 to 58. % 151.62/151.87 % 151.62/151.87 Resetting weight limit to 58 after 48670 givens. % 151.62/151.87 % 178.16/178.44 % 178.16/178.44 % 178.16/178.44 Changing weight limit from 58 to 57. % 178.16/178.44 % 178.16/178.44 Resetting weight limit to 57 after 50275 givens. % 178.16/178.44 % 178.46/178.71 % 178.46/178.71 % 178.46/178.71 Changing weight limit from 57 to 54. % 178.46/178.71 % 178.46/178.71 Resetting weight limit to 54 after 50290 givens. % 178.46/178.71 % 179.21/179.49 % 179.21/179.49 % 179.21/179.49 Changing weight limit from 54 to 53. % 179.21/179.49 % 179.21/179.49 Resetting weight limit to 53 after 50375 givens. % 179.21/179.49 % 207.53/207.78 % 207.53/207.78 % 207.53/207.78 Changing weight limit from 53 to 52. % 207.53/207.78 % 207.53/207.78 Resetting weight limit to 52 after 52145 givens. % 207.53/207.78 % 212.16/212.42 % 212.16/212.42 % 212.16/212.42 Changing weight limit from 52 to 49. % 212.16/212.42 % 212.16/212.42 Resetting weight limit to 49 after 52250 givens. % 212.16/212.42 % 213.34/213.58 % 213.34/213.58 % 213.34/213.58 Changing weight limit from 49 to 48. % 213.34/213.58 % 213.34/213.58 Resetting weight limit to 48 after 52280 givens. % 213.34/213.58 % 279.87/280.11 % 279.87/280.11 % 279.87/280.11 Changing weight limit from 48 to 47. % 279.87/280.11 % 279.87/280.11 Resetting weight limit to 47 after 57750 givens. % 279.87/280.11 % 284.78/285.06 % 284.78/285.06 % 284.78/285.06 Changing weight limit from 47 to 44. % 284.78/285.06 % 284.78/285.06 Resetting weight limit to 44 after 58165 givens. % 284.78/285.06 % 300.06/300.31 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------