%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL247-1 : TPTP v8.1.0. Bugfixed v2.3.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n027.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:29:05 EDT 2022 % Result : Timeout 300.10s 300.35s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : LCL247-1 : TPTP v8.1.0. Bugfixed v2.3.0. % 0.06/0.12 % Command : sos-script %s % 0.12/0.33 % Computer : n027.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 18:00:26 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.35 ----- Otter 3.2, August 2001 ----- % 0.12/0.35 The process was started by sandbox on n027.cluster.edu, % 0.12/0.35 Mon Jul 4 18:00:26 2022 % 0.12/0.35 The command was "./sos". The process ID is 8768. % 0.12/0.35 % 0.12/0.35 set(prolog_style_variables). % 0.12/0.35 set(auto). % 0.12/0.35 dependent: set(auto1). % 0.12/0.35 dependent: set(process_input). % 0.12/0.35 dependent: clear(print_kept). % 0.12/0.35 dependent: clear(print_new_demod). % 0.12/0.35 dependent: clear(print_back_demod). % 0.12/0.35 dependent: clear(print_back_sub). % 0.12/0.35 dependent: set(control_memory). % 0.12/0.35 dependent: assign(max_mem, 12000). % 0.12/0.35 dependent: assign(pick_given_ratio, 4). % 0.12/0.35 dependent: assign(stats_level, 1). % 0.12/0.35 dependent: assign(pick_semantic_ratio, 3). % 0.12/0.35 dependent: assign(sos_limit, 5000). % 0.12/0.35 dependent: assign(max_weight, 60). % 0.12/0.35 clear(print_given). % 0.12/0.35 % 0.12/0.35 list(usable). % 0.12/0.35 % 0.12/0.35 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. % 0.12/0.35 % 0.12/0.35 This is a Horn set without equality. The strategy will % 0.12/0.35 be hyperresolution, with satellites in sos and nuclei % 0.12/0.35 in usable. % 0.12/0.35 % 0.12/0.35 dependent: set(hyper_res). % 0.12/0.35 dependent: clear(order_hyper). % 0.12/0.35 % 0.12/0.35 ------------> process usable: % 0.12/0.35 % 0.12/0.35 ------------> process sos: % 0.12/0.35 % 0.12/0.35 ======= end of input processing ======= % 0.12/0.38 % 0.12/0.38 Model 1 (0.00 seconds, 0 Inserts) % 0.12/0.38 % 0.12/0.38 Stopped by limit on number of solutions % 0.12/0.38 % 0.12/0.38 % 0.12/0.38 -------------- Softie stats -------------- % 0.12/0.38 % 0.12/0.38 UPDATE_STOP: 300 % 0.12/0.38 SFINDER_TIME_LIMIT: 2 % 0.12/0.38 SHORT_CLAUSE_CUTOFF: 4 % 0.12/0.38 number of clauses in intial UL: 4 % 0.12/0.38 number of clauses initially in problem: 9 % 0.12/0.38 percentage of clauses intially in UL: 44 % 0.12/0.38 percentage of distinct symbols occuring in initial UL: 100 % 0.12/0.38 percent of all initial clauses that are short: 100 % 0.12/0.38 absolute distinct symbol count: 7 % 0.12/0.38 distinct predicate count: 2 % 0.12/0.38 distinct function count: 2 % 0.12/0.38 distinct constant count: 3 % 0.12/0.38 % 0.12/0.38 ---------- no more Softie stats ---------- % 0.12/0.38 % 0.12/0.38 % 0.12/0.38 % 0.12/0.38 Model 2 (0.00 seconds, 0 Inserts) % 0.12/0.38 % 0.12/0.38 Stopped by limit on number of solutions % 0.12/0.38 % 0.12/0.38 =========== start of search =========== % 4.23/4.42 % 4.23/4.42 % 4.23/4.42 Changing weight limit from 60 to 57. % 4.23/4.42 % 4.23/4.42 Model 3 (0.00 seconds, 0 Inserts) % 4.23/4.42 % 4.23/4.42 Stopped by limit on number of solutions % 4.23/4.42 % 4.23/4.42 Stopped by limit on insertions % 4.23/4.42 % 4.23/4.42 Stopped by limit on insertions % 4.23/4.42 % 4.23/4.42 Model 4 [ 1 5 60917 ] (0.00 seconds, 250000 Inserts) % 4.23/4.42 % 4.23/4.42 Stopped by limit on insertions % 4.23/4.42 % 4.23/4.42 Model 5 [ 1 6 55529 ] (0.00 seconds, 250000 Inserts) % 4.23/4.42 % 4.23/4.42 Modelling stopped after 300 given clauses and 0.00 seconds % 4.23/4.42 % 4.23/4.42 % 4.23/4.42 Resetting weight limit to 57 after 1395 givens. % 4.23/4.42 % 4.71/4.91 % 4.71/4.91 % 4.71/4.91 Changing weight limit from 57 to 47. % 4.71/4.91 % 4.71/4.91 Resetting weight limit to 47 after 2690 givens. % 4.71/4.91 % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 Changing weight limit from 47 to 43. % 4.71/4.92 % 4.71/4.92 Resetting weight limit to 43 after 2695 givens. % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 Changing weight limit from 43 to 42. % 4.71/4.92 % 4.71/4.92 Resetting weight limit to 42 after 2700 givens. % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 Changing weight limit from 42 to 41. % 4.71/4.92 % 4.71/4.92 Resetting weight limit to 41 after 2710 givens. % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 % 4.71/4.92 Changing weight limit from 41 to 39. % 4.71/4.92 % 4.71/4.92 Resetting weight limit to 39 after 2715 givens. % 4.71/4.92 % 4.71/4.93 % 4.71/4.93 % 4.71/4.93 Changing weight limit from 39 to 38. % 4.71/4.93 % 4.71/4.93 Resetting weight limit to 38 after 2730 givens. % 4.71/4.93 % 4.71/4.93 % 4.71/4.93 % 4.71/4.93 Changing weight limit from 38 to 37. % 4.71/4.93 % 4.71/4.93 Resetting weight limit to 37 after 2735 givens. % 4.71/4.93 % 4.71/4.94 % 4.71/4.94 % 4.71/4.94 Changing weight limit from 37 to 36. % 4.71/4.94 % 4.71/4.94 Resetting weight limit to 36 after 2765 givens. % 4.71/4.94 % 4.71/4.95 % 4.71/4.95 % 4.71/4.95 Changing weight limit from 36 to 35. % 4.71/4.95 % 4.71/4.95 Resetting weight limit to 35 after 2770 givens. % 4.71/4.95 % 4.71/4.95 % 4.71/4.95 % 4.71/4.95 Changing weight limit from 35 to 34. % 4.71/4.95 % 4.71/4.95 Resetting weight limit to 34 after 2795 givens. % 4.71/4.95 % 4.78/4.96 % 4.78/4.96 % 4.78/4.96 Changing weight limit from 34 to 33. % 4.78/4.96 % 4.78/4.96 Resetting weight limit to 33 after 2810 givens. % 4.78/4.96 % 4.78/4.97 % 4.78/4.97 % 4.78/4.97 Changing weight limit from 33 to 32. % 4.78/4.97 % 4.78/4.97 Resetting weight limit to 32 after 2830 givens. % 4.78/4.97 % 4.80/4.98 % 4.80/4.98 % 4.80/4.98 Changing weight limit from 32 to 31. % 4.80/4.98 % 4.80/4.98 Resetting weight limit to 31 after 2840 givens. % 4.80/4.98 % 4.80/5.00 % 4.80/5.00 % 4.80/5.00 Changing weight limit from 31 to 30. % 4.80/5.00 % 4.80/5.00 Resetting weight limit to 30 after 2875 givens. % 4.80/5.00 % 4.80/5.01 % 4.80/5.01 % 4.80/5.01 Changing weight limit from 30 to 29. % 4.80/5.01 % 4.80/5.01 Resetting weight limit to 29 after 2885 givens. % 4.80/5.01 % 4.80/5.02 % 4.80/5.02 % 4.80/5.02 Changing weight limit from 29 to 28. % 4.80/5.02 % 4.80/5.02 Resetting weight limit to 28 after 2910 givens. % 4.80/5.02 % 4.85/5.04 % 4.85/5.04 % 4.85/5.04 Changing weight limit from 28 to 27. % 4.85/5.04 % 4.85/5.04 Resetting weight limit to 27 after 2940 givens. % 4.85/5.04 % 4.88/5.05 % 4.88/5.05 % 4.88/5.05 Changing weight limit from 27 to 26. % 4.88/5.05 % 4.88/5.05 Resetting weight limit to 26 after 2970 givens. % 4.88/5.05 % 4.88/5.08 % 4.88/5.08 % 4.88/5.08 Changing weight limit from 26 to 25. % 4.88/5.08 % 4.88/5.08 Resetting weight limit to 25 after 3025 givens. % 4.88/5.08 % 4.95/5.12 % 4.95/5.12 % 4.95/5.12 Changing weight limit from 25 to 24. % 4.95/5.12 % 4.95/5.12 Resetting weight limit to 24 after 3100 givens. % 4.95/5.12 % 4.95/5.14 % 4.95/5.14 % 4.95/5.14 Changing weight limit from 24 to 23. % 4.95/5.14 % 4.95/5.14 Resetting weight limit to 23 after 3140 givens. % 4.95/5.14 % 5.07/5.25 % 5.07/5.25 % 5.07/5.25 Changing weight limit from 23 to 22. % 5.07/5.25 % 5.07/5.25 Resetting weight limit to 22 after 3315 givens. % 5.07/5.25 % 5.10/5.28 % 5.10/5.28 % 5.10/5.28 Changing weight limit from 22 to 21. % 5.10/5.28 % 5.10/5.28 Resetting weight limit to 21 after 3370 givens. % 5.10/5.28 % 5.24/5.45 % 5.24/5.45 % 5.24/5.45 Changing weight limit from 21 to 20. % 5.24/5.45 % 5.24/5.45 Resetting weight limit to 20 after 3670 givens. % 5.24/5.45 % 5.30/5.49 % 5.30/5.49 % 5.30/5.49 Changing weight limit from 20 to 19. % 5.30/5.49 % 5.30/5.49 Resetting weight limit to 19 after 3750 givens. % 5.30/5.49 % 5.59/5.85 % 5.59/5.85 % 5.59/5.85 Changing weight limit from 19 to 18. % 5.59/5.85 % 5.59/5.85 Resetting weight limit to 18 after 4530 givens. % 5.59/5.85 % 5.76/5.99 % 5.76/5.99 % 5.76/5.99 Changing weight limit from 18 to 17. % 5.76/5.99 % 5.76/5.99 Resetting weight limit to 17 after 4995 givens. % 5.76/5.99 % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 Changing weight limit from 17 to 18. % 7.96/8.16 % 7.96/8.16 Resetting weight limit to 18 after 17135 givens. % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 Changing weight limit from 18 to 17. % 7.96/8.16 % 7.96/8.16 Resetting weight limit to 17 after 17140 givens. % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 Changing weight limit from 17 to 18. % 7.96/8.16 % 7.96/8.16 Resetting weight limit to 18 after 17145 givens. % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 % 7.96/8.16 Changing weight limit from 18 to 17. % 7.96/8.16 % 7.96/8.16 Resetting weight limit to 17 after 17150 givens. % 7.96/8.16 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 17 to 18. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 18 after 17165 givens. % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 18 to 17. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 17 after 17170 givens. % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 17 to 18. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 18 after 17185 givens. % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 18 to 17. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 17 after 17190 givens. % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 17 to 18. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 18 after 17205 givens. % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 % 7.96/8.17 Changing weight limit from 18 to 17. % 7.96/8.17 % 7.96/8.17 Resetting weight limit to 17 after 17210 givens. % 7.96/8.17 % 7.96/8.18 % 7.96/8.18 % 7.96/8.18 Changing weight limit from 17 to 18. % 7.96/8.18 % 7.96/8.18 Resetting weight limit to 18 after 17220 givens. % 7.96/8.18 % 8.00/8.18 % 8.00/8.18 % 8.00/8.18 Changing weight limit from 18 to 19. % 8.00/8.18 % 8.00/8.18 Resetting weight limit to 19 after 17240 givens. % 8.00/8.18 % 8.00/8.18 % 8.00/8.18 % 8.00/8.18 Changing weight limit from 19 to 20. % 8.00/8.18 % 8.00/8.18 Resetting weight limit to 20 after 17245 givens. % 8.00/8.18 % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 Changing weight limit from 20 to 21. % 8.00/8.19 % 8.00/8.19 Resetting weight limit to 21 after 17265 givens. % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 Changing weight limit from 21 to 20. % 8.00/8.19 % 8.00/8.19 Resetting weight limit to 20 after 17270 givens. % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 Changing weight limit from 20 to 21. % 8.00/8.19 % 8.00/8.19 Resetting weight limit to 21 after 17280 givens. % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 Changing weight limit from 21 to 22. % 8.00/8.19 % 8.00/8.19 Resetting weight limit to 22 after 17300 givens. % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 % 8.00/8.19 Changing weight limit from 22 to 21. % 8.00/8.19 % 8.00/8.19 Resetting weight limit to 21 after 17305 givens. % 8.00/8.19 % 9.32/9.49 % 9.32/9.49 % 9.32/9.49 Changing weight limit from 21 to 20. % 9.32/9.49 % 9.32/9.49 Resetting weight limit to 20 after 21300 givens. % 9.32/9.49 % 9.35/9.58 % 9.35/9.58 % 9.35/9.58 Changing weight limit from 20 to 19. % 9.35/9.58 % 9.35/9.58 Resetting weight limit to 19 after 21520 givens. % 9.35/9.58 % 18.79/19.00 % 18.79/19.00 % 18.79/19.00 Changing weight limit from 19 to 20. % 18.79/19.00 % 18.79/19.00 Resetting weight limit to 20 after 48245 givens. % 18.79/19.00 % 18.79/19.00 % 18.79/19.00 % 18.79/19.00 Changing weight limit from 20 to 19. % 18.79/19.00 % 18.79/19.00 Resetting weight limit to 19 after 48250 givens. % 18.79/19.00 % 18.79/19.02 % 18.79/19.02 % 18.79/19.02 Changing weight limit from 19 to 20. % 18.79/19.02 % 18.79/19.02 Resetting weight limit to 20 after 48305 givens. % 18.79/19.02 % 18.79/19.02 % 18.79/19.02 % 18.79/19.02 Changing weight limit from 20 to 19. % 18.79/19.02 % 18.79/19.02 Resetting weight limit to 19 after 48310 givens. % 18.79/19.02 % 18.79/19.05 % 18.79/19.05 % 18.79/19.05 Changing weight limit from 19 to 20. % 18.79/19.05 % 18.79/19.05 Resetting weight limit to 20 after 48385 givens. % 18.79/19.05 % 18.79/19.06 % 18.79/19.06 % 18.79/19.06 Changing weight limit from 20 to 19. % 18.79/19.06 % 18.79/19.06 Resetting weight limit to 19 after 48390 givens. % 18.79/19.06 % 18.88/19.07 % 18.88/19.07 % 18.88/19.07 Changing weight limit from 19 to 20. % 18.88/19.07 % 18.88/19.07 Resetting weight limit to 20 after 48425 givens. % 18.88/19.07 % 18.88/19.07 % 18.88/19.07 % 18.88/19.07 Changing weight limit from 20 to 19. % 18.88/19.07 % 18.88/19.07 Resetting weight limit to 19 after 48430 givens. % 18.88/19.07 % 18.88/19.08 % 18.88/19.08 % 18.88/19.08 Changing weight limit from 19 to 20. % 18.88/19.08 % 18.88/19.08 Resetting weight limit to 20 after 48445 givens. % 18.88/19.08 % 18.88/19.08 % 18.88/19.08 % 18.88/19.08 Changing weight limit from 20 to 19. % 18.88/19.08 % 18.88/19.08 Resetting weight limit to 19 after 48450 givens. % 18.88/19.08 % 18.92/19.12 % 18.92/19.12 % 18.92/19.12 Changing weight limit from 19 to 20. % 18.92/19.12 % 18.92/19.12 Resetting weight limit to 20 after 48525 givens. % 18.92/19.12 % 18.92/19.12 % 18.92/19.12 % 18.92/19.12 Changing weight limit from 20 to 19. % 18.92/19.12 % 18.92/19.12 Resetting weight limit to 19 after 48530 givens. % 18.92/19.12 % 18.92/19.13 % 18.92/19.13 % 18.92/19.13 Changing weight limit from 19 to 20. % 18.92/19.13 % 18.92/19.13 Resetting weight limit to 20 after 48545 givens. % 18.92/19.13 % 18.92/19.13 % 18.92/19.13 % 18.92/19.13 Changing weight limit from 20 to 19. % 18.92/19.13 % 18.92/19.13 Resetting weight limit to 19 after 48550 givens. % 18.92/19.13 % 18.96/19.14 % 18.96/19.14 % 18.96/19.14 Changing weight limit from 19 to 20. % 18.96/19.14 % 18.96/19.14 Resetting weight limit to 20 after 48585 givens. % 18.96/19.14 % 18.96/19.15 % 18.96/19.15 % 18.96/19.15 Changing weight limit from 20 to 19. % 18.96/19.15 % 18.96/19.15 Resetting weight limit to 19 after 48590 givens. % 18.96/19.15 % 18.96/19.16 % 18.96/19.16 % 18.96/19.16 Changing weight limit from 19 to 20. % 18.96/19.16 % 18.96/19.16 Resetting weight limit to 20 after 48625 givens. % 18.96/19.16 % 18.96/19.16 % 18.96/19.16 % 18.96/19.16 Changing weight limit from 20 to 19. % 18.96/19.16 % 18.96/19.16 Resetting weight limit to 19 after 48630 givens. % 18.96/19.16 % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 Changing weight limit from 19 to 20. % 18.96/19.18 % 18.96/19.18 Resetting weight limit to 20 after 48655 givens. % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 Changing weight limit from 20 to 19. % 18.96/19.18 % 18.96/19.18 Resetting weight limit to 19 after 48660 givens. % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 Changing weight limit from 19 to 20. % 18.96/19.18 % 18.96/19.18 Resetting weight limit to 20 after 48665 givens. % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 % 18.96/19.18 Changing weight limit from 20 to 19. % 18.96/19.18 % 18.96/19.18 Resetting weight limit to 19 after 48670 givens. % 18.96/19.18 % 18.96/19.19 % 18.96/19.19 % 18.96/19.19 Changing weight limit from 19 to 20. % 18.96/19.19 % 18.96/19.19 Resetting weight limit to 20 after 48685 givens. % 18.96/19.19 % 19.04/19.23 % 19.04/19.23 % 19.04/19.23 Changing weight limit from 20 to 21. % 19.04/19.23 % 19.04/19.23 Resetting weight limit to 21 after 48745 givens. % 19.04/19.23 % 19.04/19.24 % 19.04/19.24 % 19.04/19.24 Changing weight limit from 21 to 22. % 19.04/19.24 % 19.04/19.24 Resetting weight limit to 22 after 48785 givens. % 19.04/19.24 % 19.04/19.25 % 19.04/19.25 % 19.04/19.25 Changing weight limit from 22 to 21. % 19.04/19.25 % 19.04/19.25 Resetting weight limit to 21 after 48790 givens. % 19.04/19.25 % 19.04/19.26 % 19.04/19.26 % 19.04/19.26 Changing weight limit from 21 to 22. % 19.04/19.26 % 19.04/19.26 Resetting weight limit to 22 after 48805 givens. % 19.04/19.26 % 19.04/19.26 % 19.04/19.26 % 19.04/19.26 Changing weight limit from 22 to 21. % 19.04/19.26 % 19.04/19.26 Resetting weight limit to 21 after 48810 givens. % 19.04/19.26 % 170.84/171.15 % 170.84/171.15 % 170.84/171.15 Changing weight limit from 21 to 22. % 170.84/171.15 % 170.84/171.15 Resetting weight limit to 22 after 182985 givens. % 170.84/171.15 % 170.84/171.16 % 170.84/171.16 % 170.84/171.16 Changing weight limit from 22 to 21. % 170.84/171.16 % 170.84/171.16 Resetting weight limit to 21 after 182990 givens. % 170.84/171.16 % 170.84/171.16 % 170.84/171.16 % 170.84/171.16 Changing weight limit from 21 to 22. % 170.84/171.16 % 170.84/171.16 Resetting weight limit to 22 after 182995 givens. % 170.84/171.16 % 170.84/171.17 % 170.84/171.17 % 170.84/171.17 Changing weight limit from 22 to 21. % 170.84/171.17 % 170.84/171.17 Resetting weight limit to 21 after 183000 givens. % 170.84/171.17 % 170.94/171.19 % 170.94/171.19 % 170.94/171.19 Changing weight limit from 21 to 22. % 170.94/171.19 % 170.94/171.19 Resetting weight limit to 22 after 183025 givens. % 170.94/171.19 % 170.94/171.21 % 170.94/171.21 % 170.94/171.21 Changing weight limit from 22 to 21. % 170.94/171.21 % 170.94/171.21 Resetting weight limit to 21 after 183030 givens. % 170.94/171.21 % 170.97/171.24 % 170.97/171.24 % 170.97/171.24 Changing weight limit from 21 to 22. % 170.97/171.24 % 170.97/171.24 Resetting weight limit to 22 after 183045 givens. % 170.97/171.24 % 170.97/171.26 % 170.97/171.26 % 170.97/171.26 Changing weight limit from 22 to 21. % 170.97/171.26 % 170.97/171.26 Resetting weight limit to 21 after 183050 givens. % 170.97/171.26 % 171.34/171.62 % 171.34/171.62 % 171.34/171.62 Changing weight limit from 21 to 22. % 171.34/171.62 % 171.34/171.62 Resetting weight limit to 22 after 183230 givens. % 171.34/171.62 % 171.37/171.62 % 171.37/171.62 % 171.37/171.62 Changing weight limit from 22 to 23. % 171.37/171.62 % 171.37/171.62 Resetting weight limit to 23 after 183235 givens. % 171.37/171.62 % 171.47/171.76 % 171.47/171.76 % 171.47/171.76 Changing weight limit from 23 to 24. % 171.47/171.76 % 171.47/171.76 Resetting weight limit to 24 after 183280 givens. % 171.47/171.76 % 171.47/171.77 % 171.47/171.77 % 171.47/171.77 Changing weight limit from 24 to 23. % 171.47/171.77 % 171.47/171.77 Resetting weight limit to 23 after 183285 givens. % 171.47/171.77 % 193.65/193.95 % 193.65/193.95 % 193.65/193.95 Changing weight limit from 23 to 22. % 193.65/193.95 % 193.65/193.95 Resetting weight limit to 22 after 192440 givens. % 193.65/193.95 % 219.44/219.79 % 219.44/219.79 % 219.44/219.79 Changing weight limit from 22 to 21. % 219.44/219.79 % 219.44/219.79 Resetting weight limit to 21 after 207010 givens. % 219.44/219.79 % 300.10/300.35 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------