%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL251-1 : TPTP v8.1.0. Bugfixed v2.3.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n029.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:07 EDT 2022 % Result : Timeout 300.02s 300.28s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : LCL251-1 : TPTP v8.1.0. Bugfixed v2.3.0. % 0.04/0.13 % Command : sos-script %s % 0.12/0.34 % Computer : n029.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 600 % 0.12/0.35 % DateTime : Sat Jul 2 18:59:55 EDT 2022 % 0.12/0.35 % CPUTime : % 0.12/0.36 ----- Otter 3.2, August 2001 ----- % 0.12/0.36 The process was started by sandbox on n029.cluster.edu, % 0.12/0.36 Sat Jul 2 18:59:55 2022 % 0.12/0.36 The command was "./sos". The process ID is 451. % 0.12/0.36 % 0.12/0.36 set(prolog_style_variables). % 0.12/0.36 set(auto). % 0.12/0.36 dependent: set(auto1). % 0.12/0.36 dependent: set(process_input). % 0.12/0.36 dependent: clear(print_kept). % 0.12/0.36 dependent: clear(print_new_demod). % 0.12/0.36 dependent: clear(print_back_demod). % 0.12/0.36 dependent: clear(print_back_sub). % 0.12/0.36 dependent: set(control_memory). % 0.12/0.36 dependent: assign(max_mem, 12000). % 0.12/0.36 dependent: assign(pick_given_ratio, 4). % 0.12/0.36 dependent: assign(stats_level, 1). % 0.12/0.36 dependent: assign(pick_semantic_ratio, 3). % 0.12/0.36 dependent: assign(sos_limit, 5000). % 0.12/0.36 dependent: assign(max_weight, 60). % 0.12/0.36 clear(print_given). % 0.12/0.36 % 0.12/0.36 list(usable). % 0.12/0.36 % 0.12/0.36 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=3. % 0.12/0.36 % 0.12/0.36 This is a Horn set without equality. The strategy will % 0.12/0.36 be hyperresolution, with satellites in sos and nuclei % 0.12/0.36 in usable. % 0.12/0.36 % 0.12/0.36 dependent: set(hyper_res). % 0.12/0.36 dependent: clear(order_hyper). % 0.12/0.36 % 0.12/0.36 ------------> process usable: % 0.12/0.36 % 0.12/0.36 ------------> process sos: % 0.12/0.36 % 0.12/0.36 ======= end of input processing ======= % 0.20/0.40 % 0.20/0.40 Model 1 (0.00 seconds, 0 Inserts) % 0.20/0.40 % 0.20/0.40 Stopped by limit on number of solutions % 0.20/0.40 % 0.20/0.40 % 0.20/0.40 -------------- Softie stats -------------- % 0.20/0.40 % 0.20/0.40 UPDATE_STOP: 300 % 0.20/0.40 SFINDER_TIME_LIMIT: 2 % 0.20/0.40 SHORT_CLAUSE_CUTOFF: 4 % 0.20/0.40 number of clauses in intial UL: 4 % 0.20/0.40 number of clauses initially in problem: 9 % 0.20/0.40 percentage of clauses intially in UL: 44 % 0.20/0.40 percentage of distinct symbols occuring in initial UL: 100 % 0.20/0.40 percent of all initial clauses that are short: 100 % 0.20/0.40 absolute distinct symbol count: 7 % 0.20/0.40 distinct predicate count: 2 % 0.20/0.40 distinct function count: 2 % 0.20/0.40 distinct constant count: 3 % 0.20/0.40 % 0.20/0.40 ---------- no more Softie stats ---------- % 0.20/0.40 % 0.20/0.40 % 0.20/0.40 % 0.20/0.40 Model 2 (0.00 seconds, 0 Inserts) % 0.20/0.40 % 0.20/0.40 Stopped by limit on number of solutions % 0.20/0.40 % 0.20/0.40 =========== start of search =========== % 4.47/4.65 % 4.47/4.65 % 4.47/4.65 Changing weight limit from 60 to 40. % 4.47/4.65 % 4.47/4.65 Model 3 (0.00 seconds, 0 Inserts) % 4.47/4.65 % 4.47/4.65 Stopped by limit on number of solutions % 4.47/4.65 % 4.47/4.65 Stopped by limit on insertions % 4.47/4.65 % 4.47/4.65 Model 4 [ 12 0 46 ] (0.00 seconds, 250000 Inserts) % 4.47/4.65 % 4.47/4.65 Stopped by limit on insertions % 4.47/4.65 % 4.47/4.65 Stopped by limit on insertions % 4.47/4.65 % 4.47/4.65 Model 5 [ 12 1 115 ] (0.00 seconds, 250000 Inserts) % 4.47/4.65 % 4.47/4.65 Modelling stopped after 300 given clauses and 0.00 seconds % 4.47/4.65 % 4.47/4.65 % 4.47/4.65 Resetting weight limit to 40 after 1660 givens. % 4.47/4.65 % 4.47/4.65 % 4.47/4.65 % 4.47/4.65 Changing weight limit from 40 to 39. % 4.47/4.65 % 4.47/4.65 Resetting weight limit to 39 after 1665 givens. % 4.47/4.65 % 4.62/4.84 % 4.62/4.84 % 4.62/4.84 Changing weight limit from 39 to 35. % 4.62/4.84 % 4.62/4.84 Resetting weight limit to 35 after 2120 givens. % 4.62/4.84 % 4.68/4.85 % 4.68/4.85 % 4.68/4.85 Changing weight limit from 35 to 31. % 4.68/4.85 % 4.68/4.85 Resetting weight limit to 31 after 2130 givens. % 4.68/4.85 % 4.68/4.86 % 4.68/4.86 % 4.68/4.86 Changing weight limit from 31 to 30. % 4.68/4.86 % 4.68/4.86 Resetting weight limit to 30 after 2140 givens. % 4.68/4.86 % 4.68/4.86 % 4.68/4.86 % 4.68/4.86 Changing weight limit from 30 to 28. % 4.68/4.86 % 4.68/4.86 Resetting weight limit to 28 after 2155 givens. % 4.68/4.86 % 4.68/4.88 % 4.68/4.88 % 4.68/4.88 Changing weight limit from 28 to 27. % 4.68/4.88 % 4.68/4.88 Resetting weight limit to 27 after 2170 givens. % 4.68/4.88 % 4.68/4.89 % 4.68/4.89 % 4.68/4.89 Changing weight limit from 27 to 26. % 4.68/4.89 % 4.68/4.89 Resetting weight limit to 26 after 2180 givens. % 4.68/4.89 % 4.68/4.91 % 4.68/4.91 % 4.68/4.91 Changing weight limit from 26 to 25. % 4.68/4.91 % 4.68/4.91 Resetting weight limit to 25 after 2205 givens. % 4.68/4.91 % 4.74/4.94 % 4.74/4.94 % 4.74/4.94 Changing weight limit from 25 to 24. % 4.74/4.94 % 4.74/4.94 Resetting weight limit to 24 after 2240 givens. % 4.74/4.94 % 4.74/4.96 % 4.74/4.96 % 4.74/4.96 Changing weight limit from 24 to 23. % 4.74/4.96 % 4.74/4.96 Resetting weight limit to 23 after 2270 givens. % 4.74/4.96 % 4.80/5.02 % 4.80/5.02 % 4.80/5.02 Changing weight limit from 23 to 22. % 4.80/5.02 % 4.80/5.02 Resetting weight limit to 22 after 2370 givens. % 4.80/5.02 % 4.80/5.05 % 4.80/5.05 % 4.80/5.05 Changing weight limit from 22 to 21. % 4.80/5.05 % 4.80/5.05 Resetting weight limit to 21 after 2415 givens. % 4.80/5.05 % 5.03/5.26 % 5.03/5.26 % 5.03/5.26 Changing weight limit from 21 to 20. % 5.03/5.26 % 5.03/5.26 Resetting weight limit to 20 after 2860 givens. % 5.03/5.26 % 5.10/5.31 % 5.10/5.31 % 5.10/5.31 Changing weight limit from 20 to 19. % 5.10/5.31 % 5.10/5.31 Resetting weight limit to 19 after 2920 givens. % 5.10/5.31 % 5.72/5.93 % 5.72/5.93 % 5.72/5.93 Changing weight limit from 19 to 18. % 5.72/5.93 % 5.72/5.93 Resetting weight limit to 18 after 4295 givens. % 5.72/5.93 % 5.97/6.15 % 5.97/6.15 % 5.97/6.15 Changing weight limit from 18 to 17. % 5.97/6.15 % 5.97/6.15 Resetting weight limit to 17 after 5100 givens. % 5.97/6.15 % 8.26/8.48 % 8.26/8.48 % 8.26/8.48 Changing weight limit from 17 to 18. % 8.26/8.48 % 8.26/8.48 Resetting weight limit to 18 after 16505 givens. % 8.26/8.48 % 8.26/8.48 % 8.26/8.48 % 8.26/8.48 Changing weight limit from 18 to 17. % 8.26/8.48 % 8.26/8.48 Resetting weight limit to 17 after 16510 givens. % 8.26/8.48 % 8.26/8.49 % 8.26/8.49 % 8.26/8.49 Changing weight limit from 17 to 18. % 8.26/8.49 % 8.26/8.49 Resetting weight limit to 18 after 16585 givens. % 8.26/8.49 % 8.26/8.49 % 8.26/8.49 % 8.26/8.49 Changing weight limit from 18 to 17. % 8.26/8.49 % 8.26/8.49 Resetting weight limit to 17 after 16590 givens. % 8.26/8.49 % 8.26/8.50 % 8.26/8.50 % 8.26/8.50 Changing weight limit from 17 to 18. % 8.26/8.50 % 8.26/8.50 Resetting weight limit to 18 after 16625 givens. % 8.26/8.50 % 8.26/8.50 % 8.26/8.50 % 8.26/8.50 Changing weight limit from 18 to 17. % 8.26/8.50 % 8.26/8.50 Resetting weight limit to 17 after 16630 givens. % 8.26/8.50 % 8.33/8.50 % 8.33/8.50 % 8.33/8.50 Changing weight limit from 17 to 18. % 8.33/8.50 % 8.33/8.50 Resetting weight limit to 18 after 16645 givens. % 8.33/8.50 % 8.33/8.51 % 8.33/8.51 % 8.33/8.51 Changing weight limit from 18 to 17. % 8.33/8.51 % 8.33/8.51 Resetting weight limit to 17 after 16650 givens. % 8.33/8.51 % 8.33/8.51 % 8.33/8.51 % 8.33/8.51 Changing weight limit from 17 to 18. % 8.33/8.51 % 8.33/8.51 Resetting weight limit to 18 after 16685 givens. % 8.33/8.51 % 8.33/8.51 % 8.33/8.51 % 8.33/8.51 Changing weight limit from 18 to 17. % 8.33/8.51 % 8.33/8.51 Resetting weight limit to 17 after 16690 givens. % 8.33/8.51 % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 Changing weight limit from 17 to 18. % 8.33/8.53 % 8.33/8.53 Resetting weight limit to 18 after 16745 givens. % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 Changing weight limit from 18 to 17. % 8.33/8.53 % 8.33/8.53 Resetting weight limit to 17 after 16750 givens. % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 Changing weight limit from 17 to 18. % 8.33/8.53 % 8.33/8.53 Resetting weight limit to 18 after 16765 givens. % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 % 8.33/8.53 Changing weight limit from 18 to 17. % 8.33/8.53 % 8.33/8.53 Resetting weight limit to 17 after 16770 givens. % 8.33/8.53 % 8.33/8.54 % 8.33/8.54 % 8.33/8.54 Changing weight limit from 17 to 18. % 8.33/8.54 % 8.33/8.54 Resetting weight limit to 18 after 16785 givens. % 8.33/8.54 % 8.33/8.54 % 8.33/8.54 % 8.33/8.54 Changing weight limit from 18 to 17. % 8.33/8.54 % 8.33/8.54 Resetting weight limit to 17 after 16790 givens. % 8.33/8.54 % 8.33/8.55 % 8.33/8.55 % 8.33/8.55 Changing weight limit from 17 to 18. % 8.33/8.55 % 8.33/8.55 Resetting weight limit to 18 after 16825 givens. % 8.33/8.55 % 8.33/8.55 % 8.33/8.55 % 8.33/8.55 Changing weight limit from 18 to 17. % 8.33/8.55 % 8.33/8.55 Resetting weight limit to 17 after 16830 givens. % 8.33/8.55 % 8.39/8.57 % 8.39/8.57 % 8.39/8.57 Changing weight limit from 17 to 18. % 8.39/8.57 % 8.39/8.57 Resetting weight limit to 18 after 16945 givens. % 8.39/8.57 % 8.39/8.57 % 8.39/8.57 % 8.39/8.57 Changing weight limit from 18 to 17. % 8.39/8.57 % 8.39/8.57 Resetting weight limit to 17 after 16950 givens. % 8.39/8.57 % 8.39/8.58 % 8.39/8.58 % 8.39/8.58 Changing weight limit from 17 to 18. % 8.39/8.58 % 8.39/8.58 Resetting weight limit to 18 after 16985 givens. % 8.39/8.58 % 8.39/8.58 % 8.39/8.58 % 8.39/8.58 Changing weight limit from 18 to 17. % 8.39/8.58 % 8.39/8.58 Resetting weight limit to 17 after 16990 givens. % 8.39/8.58 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 17 to 18. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 18 after 17025 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 18 to 17. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 17 after 17030 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 17 to 18. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 18 after 17035 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 18 to 17. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 17 after 17040 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 17 to 18. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 18 after 17045 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 18 to 17. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 17 after 17050 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 17 to 18. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 18 after 17065 givens. % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 % 8.39/8.59 Changing weight limit from 18 to 17. % 8.39/8.59 % 8.39/8.59 Resetting weight limit to 17 after 17070 givens. % 8.39/8.59 % 8.39/8.60 % 8.39/8.60 % 8.39/8.60 Changing weight limit from 17 to 18. % 8.39/8.60 % 8.39/8.60 Resetting weight limit to 18 after 17105 givens. % 8.39/8.60 % 8.39/8.60 % 8.39/8.60 % 8.39/8.60 Changing weight limit from 18 to 17. % 8.39/8.60 % 8.39/8.60 Resetting weight limit to 17 after 17110 givens. % 8.39/8.60 % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 Changing weight limit from 17 to 18. % 8.39/8.62 % 8.39/8.62 Resetting weight limit to 18 after 17165 givens. % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 Changing weight limit from 18 to 17. % 8.39/8.62 % 8.39/8.62 Resetting weight limit to 17 after 17170 givens. % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 Changing weight limit from 17 to 18. % 8.39/8.62 % 8.39/8.62 Resetting weight limit to 18 after 17175 givens. % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 % 8.39/8.62 Changing weight limit from 18 to 17. % 8.39/8.62 % 8.39/8.62 Resetting weight limit to 17 after 17180 givens. % 8.39/8.62 % 8.39/8.64 % 8.39/8.64 % 8.39/8.64 Changing weight limit from 17 to 18. % 8.39/8.64 % 8.39/8.64 Resetting weight limit to 18 after 17285 givens. % 8.39/8.64 % 8.39/8.64 % 8.39/8.64 % 8.39/8.64 Changing weight limit from 18 to 17. % 8.39/8.64 % 8.39/8.64 Resetting weight limit to 17 after 17290 givens. % 8.39/8.64 % 8.39/8.66 % 8.39/8.66 % 8.39/8.66 Changing weight limit from 17 to 18. % 8.39/8.66 % 8.39/8.66 Resetting weight limit to 18 after 17365 givens. % 8.39/8.66 % 8.39/8.66 % 8.39/8.66 % 8.39/8.66 Changing weight limit from 18 to 17. % 8.39/8.66 % 8.39/8.66 Resetting weight limit to 17 after 17370 givens. % 8.39/8.66 % 8.49/8.66 % 8.49/8.66 % 8.49/8.66 Changing weight limit from 17 to 18. % 8.49/8.66 % 8.49/8.66 Resetting weight limit to 18 after 17395 givens. % 8.49/8.66 % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 Changing weight limit from 18 to 17. % 8.49/8.67 % 8.49/8.67 Resetting weight limit to 17 after 17400 givens. % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 Changing weight limit from 17 to 18. % 8.49/8.67 % 8.49/8.67 Resetting weight limit to 18 after 17405 givens. % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 Changing weight limit from 18 to 17. % 8.49/8.67 % 8.49/8.67 Resetting weight limit to 17 after 17410 givens. % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 Changing weight limit from 17 to 18. % 8.49/8.67 % 8.49/8.67 Resetting weight limit to 18 after 17420 givens. % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 % 8.49/8.67 Changing weight limit from 18 to 19. % 8.49/8.67 % 8.49/8.67 Resetting weight limit to 19 after 17425 givens. % 8.49/8.67 % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 Changing weight limit from 19 to 20. % 8.49/8.68 % 8.49/8.68 Resetting weight limit to 20 after 17445 givens. % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 Changing weight limit from 20 to 19. % 8.49/8.68 % 8.49/8.68 Resetting weight limit to 19 after 17450 givens. % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 Changing weight limit from 19 to 20. % 8.49/8.68 % 8.49/8.68 Resetting weight limit to 20 after 17455 givens. % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 % 8.49/8.68 Changing weight limit from 20 to 21. % 8.49/8.68 % 8.49/8.68 Resetting weight limit to 21 after 17460 givens. % 8.49/8.68 % 8.52/8.69 % 8.52/8.69 % 8.52/8.69 Changing weight limit from 21 to 22. % 8.52/8.69 % 8.52/8.69 Resetting weight limit to 22 after 17505 givens. % 8.52/8.69 % 8.52/8.69 % 8.52/8.69 % 8.52/8.69 Changing weight limit from 22 to 21. % 8.52/8.69 % 8.52/8.69 Resetting weight limit to 21 after 17510 givens. % 8.52/8.69 % 8.52/8.72 % 8.52/8.72 % 8.52/8.72 Changing weight limit from 21 to 22. % 8.52/8.72 % 8.52/8.72 Resetting weight limit to 22 after 17585 givens. % 8.52/8.72 % 8.52/8.72 % 8.52/8.72 % 8.52/8.72 Changing weight limit from 22 to 21. % 8.52/8.72 % 8.52/8.72 Resetting weight limit to 21 after 17590 givens. % 8.52/8.72 % 8.56/8.74 % 8.56/8.74 % 8.56/8.74 Changing weight limit from 21 to 22. % 8.56/8.74 % 8.56/8.74 Resetting weight limit to 22 after 17645 givens. % 8.56/8.74 % 8.56/8.74 % 8.56/8.74 % 8.56/8.74 Changing weight limit from 22 to 21. % 8.56/8.74 % 8.56/8.74 Resetting weight limit to 21 after 17650 givens. % 8.56/8.74 % 8.56/8.75 % 8.56/8.75 % 8.56/8.75 Changing weight limit from 21 to 22. % 8.56/8.75 % 8.56/8.75 Resetting weight limit to 22 after 17665 givens. % 8.56/8.75 % 8.57/8.75 % 8.57/8.75 % 8.57/8.75 Changing weight limit from 22 to 21. % 8.57/8.75 % 8.57/8.75 Resetting weight limit to 21 after 17670 givens. % 8.57/8.75 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 21 to 22. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 22 after 17685 givens. % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 22 to 21. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 21 after 17690 givens. % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 21 to 22. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 22 after 17695 givens. % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 22 to 21. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 21 after 17700 givens. % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 21 to 22. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 22 after 17705 givens. % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 % 8.57/8.76 Changing weight limit from 22 to 21. % 8.57/8.76 % 8.57/8.76 Resetting weight limit to 21 after 17710 givens. % 8.57/8.76 % 8.57/8.77 % 8.57/8.77 % 8.57/8.77 Changing weight limit from 21 to 22. % 8.57/8.77 % 8.57/8.77 Resetting weight limit to 22 after 17745 givens. % 8.57/8.77 % 9.48/9.67 % 9.48/9.67 % 9.48/9.67 Changing weight limit from 22 to 21. % 9.48/9.67 % 9.48/9.67 Resetting weight limit to 21 after 20680 givens. % 9.48/9.67 % 9.90/10.11 % 9.90/10.11 % 9.90/10.11 Changing weight limit from 21 to 20. % 9.90/10.11 % 9.90/10.11 Resetting weight limit to 20 after 21465 givens. % 9.90/10.11 % 10.05/10.24 % 10.05/10.24 % 10.05/10.24 Changing weight limit from 20 to 19. % 10.05/10.24 % 10.05/10.24 Resetting weight limit to 19 after 21795 givens. % 10.05/10.24 % 22.66/22.84 % 22.66/22.84 % 22.66/22.84 Changing weight limit from 19 to 20. % 22.66/22.84 % 22.66/22.84 Resetting weight limit to 20 after 47645 givens. % 22.66/22.84 % 22.66/22.84 % 22.66/22.84 % 22.66/22.84 Changing weight limit from 20 to 19. % 22.66/22.84 % 22.66/22.84 Resetting weight limit to 19 after 47650 givens. % 22.66/22.84 % 25.27/25.49 % 25.27/25.49 % 25.27/25.49 Changing weight limit from 19 to 20. % 25.27/25.49 % 25.27/25.49 Resetting weight limit to 20 after 51665 givens. % 25.27/25.49 % 25.27/25.49 % 25.27/25.49 % 25.27/25.49 Changing weight limit from 20 to 19. % 25.27/25.49 % 25.27/25.49 Resetting weight limit to 19 after 51670 givens. % 25.27/25.49 % 25.27/25.50 % 25.27/25.50 % 25.27/25.50 Changing weight limit from 19 to 20. % 25.27/25.50 % 25.27/25.50 Resetting weight limit to 20 after 51685 givens. % 25.27/25.50 % 25.27/25.50 % 25.27/25.50 % 25.27/25.50 Changing weight limit from 20 to 19. % 25.27/25.50 % 25.27/25.50 Resetting weight limit to 19 after 51690 givens. % 25.27/25.50 % 25.27/25.51 % 25.27/25.51 % 25.27/25.51 Changing weight limit from 19 to 20. % 25.27/25.51 % 25.27/25.51 Resetting weight limit to 20 after 51705 givens. % 25.27/25.51 % 25.27/25.51 % 25.27/25.51 % 25.27/25.51 Changing weight limit from 20 to 19. % 25.27/25.51 % 25.27/25.51 Resetting weight limit to 19 after 51710 givens. % 25.27/25.51 % 25.27/25.52 % 25.27/25.52 % 25.27/25.52 Changing weight limit from 19 to 20. % 25.27/25.52 % 25.27/25.52 Resetting weight limit to 20 after 51735 givens. % 25.27/25.52 % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 Changing weight limit from 20 to 19. % 25.27/25.53 % 25.27/25.53 Resetting weight limit to 19 after 51740 givens. % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 Changing weight limit from 19 to 20. % 25.27/25.53 % 25.27/25.53 Resetting weight limit to 20 after 51745 givens. % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 Changing weight limit from 20 to 19. % 25.27/25.53 % 25.27/25.53 Resetting weight limit to 19 after 51750 givens. % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 % 25.27/25.53 Changing weight limit from 19 to 20. % 25.27/25.53 % 25.27/25.53 Resetting weight limit to 20 after 51755 givens. % 25.27/25.53 % 25.27/25.54 % 25.27/25.54 % 25.27/25.54 Changing weight limit from 20 to 19. % 25.27/25.54 % 25.27/25.54 Resetting weight limit to 19 after 51760 givens. % 25.27/25.54 % 25.27/25.54 % 25.27/25.54 % 25.27/25.54 Changing weight limit from 19 to 20. % 25.27/25.54 % 25.27/25.54 Resetting weight limit to 20 after 51765 givens. % 25.27/25.54 % 25.27/25.55 % 25.27/25.55 % 25.27/25.55 Changing weight limit from 20 to 19. % 25.27/25.55 % 25.27/25.55 Resetting weight limit to 19 after 51770 givens. % 25.27/25.55 % 25.37/25.55 % 25.37/25.55 % 25.37/25.55 Changing weight limit from 19 to 20. % 25.37/25.55 % 25.37/25.55 Resetting weight limit to 20 after 51780 givens. % 25.37/25.55 % 25.37/25.56 % 25.37/25.56 % 25.37/25.56 Changing weight limit from 20 to 19. % 25.37/25.56 % 25.37/25.56 Resetting weight limit to 19 after 51785 givens. % 25.37/25.56 % 25.37/25.56 % 25.37/25.56 % 25.37/25.56 Changing weight limit from 19 to 20. % 25.37/25.56 % 25.37/25.56 Resetting weight limit to 20 after 51795 givens. % 25.37/25.56 % 25.37/25.57 % 25.37/25.57 % 25.37/25.57 Changing weight limit from 20 to 19. % 25.37/25.57 % 25.37/25.57 Resetting weight limit to 19 after 51800 givens. % 25.37/25.57 % 25.37/25.57 % 25.37/25.57 % 25.37/25.57 Changing weight limit from 19 to 20. % 25.37/25.57 % 25.37/25.57 Resetting weight limit to 20 after 51805 givens. % 25.37/25.57 % 25.37/25.57 % 25.37/25.57 % 25.37/25.57 Changing weight limit from 20 to 19. % 25.37/25.57 % 25.37/25.57 Resetting weight limit to 19 after 51810 givens. % 25.37/25.57 % 25.37/25.58 % 25.37/25.58 % 25.37/25.58 Changing weight limit from 19 to 20. % 25.37/25.58 % 25.37/25.58 Resetting weight limit to 20 after 51825 givens. % 25.37/25.58 % 25.37/25.58 % 25.37/25.58 % 25.37/25.58 Changing weight limit from 20 to 19. % 25.37/25.58 % 25.37/25.58 Resetting weight limit to 19 after 51830 givens. % 25.37/25.58 % 25.37/25.59 % 25.37/25.59 % 25.37/25.59 Changing weight limit from 19 to 20. % 25.37/25.59 % 25.37/25.59 Resetting weight limit to 20 after 51845 givens. % 25.37/25.59 % 25.37/25.59 % 25.37/25.59 % 25.37/25.59 Changing weight limit from 20 to 19. % 25.37/25.59 % 25.37/25.59 Resetting weight limit to 19 after 51850 givens. % 25.37/25.59 % 25.37/25.60 % 25.37/25.60 % 25.37/25.60 Changing weight limit from 19 to 20. % 25.37/25.60 % 25.37/25.60 Resetting weight limit to 20 after 51865 givens. % 25.37/25.60 % 25.37/25.60 % 25.37/25.60 % 25.37/25.60 Changing weight limit from 20 to 19. % 25.37/25.60 % 25.37/25.60 Resetting weight limit to 19 after 51870 givens. % 25.37/25.60 % 25.44/25.61 % 25.44/25.61 % 25.44/25.61 Changing weight limit from 19 to 20. % 25.44/25.61 % 25.44/25.61 Resetting weight limit to 20 after 51885 givens. % 25.44/25.61 % 25.51/25.70 % 25.51/25.70 % 25.51/25.70 Changing weight limit from 20 to 21. % 25.51/25.70 % 25.51/25.70 Resetting weight limit to 21 after 52005 givens. % 25.51/25.70 % 25.51/25.70 % 25.51/25.70 % 25.51/25.70 Changing weight limit from 21 to 20. % 25.51/25.70 % 25.51/25.70 Resetting weight limit to 20 after 52010 givens. % 25.51/25.70 % 25.51/25.71 % 25.51/25.71 % 25.51/25.71 Changing weight limit from 20 to 21. % 25.51/25.71 % 25.51/25.71 Resetting weight limit to 21 after 52025 givens. % 25.51/25.71 % 25.51/25.71 % 25.51/25.71 % 25.51/25.71 Changing weight limit from 21 to 20. % 25.51/25.71 % 25.51/25.71 Resetting weight limit to 20 after 52030 givens. % 25.51/25.71 % 25.51/25.72 % 25.51/25.72 % 25.51/25.72 Changing weight limit from 20 to 21. % 25.51/25.72 % 25.51/25.72 Resetting weight limit to 21 after 52045 givens. % 25.51/25.72 % 25.51/25.73 % 25.51/25.73 % 25.51/25.73 Changing weight limit from 21 to 20. % 25.51/25.73 % 25.51/25.73 Resetting weight limit to 20 after 52050 givens. % 25.51/25.73 % 25.51/25.74 % 25.51/25.74 % 25.51/25.74 Changing weight limit from 20 to 21. % 25.51/25.74 % 25.51/25.74 Resetting weight limit to 21 after 52065 givens. % 25.51/25.74 % 25.51/25.75 % 25.51/25.75 % 25.51/25.75 Changing weight limit from 21 to 22. % 25.51/25.75 % 25.51/25.75 Resetting weight limit to 22 after 52085 givens. % 25.51/25.75 % 25.51/25.76 % 25.51/25.76 % 25.51/25.76 Changing weight limit from 22 to 21. % 25.51/25.76 % 25.51/25.76 Resetting weight limit to 21 after 52090 givens. % 25.51/25.76 % 25.61/25.78 % 25.61/25.78 % 25.61/25.78 Changing weight limit from 21 to 22. % 25.61/25.78 % 25.61/25.78 Resetting weight limit to 22 after 52115 givens. % 25.61/25.78 % 25.63/25.79 % 25.63/25.79 % 25.63/25.79 Changing weight limit from 22 to 23. % 25.63/25.79 % 25.63/25.79 Resetting weight limit to 23 after 52125 givens. % 25.63/25.79 % 25.63/25.80 % 25.63/25.80 % 25.63/25.80 Changing weight limit from 23 to 22. % 25.63/25.80 % 25.63/25.80 Resetting weight limit to 22 after 52130 givens. % 25.63/25.80 % 25.63/25.81 % 25.63/25.81 % 25.63/25.81 Changing weight limit from 22 to 23. % 25.63/25.81 % 25.63/25.81 Resetting weight limit to 23 after 52145 givens. % 25.63/25.81 % 25.63/25.82 % 25.63/25.82 % 25.63/25.82 Changing weight limit from 23 to 22. % 25.63/25.82 % 25.63/25.82 Resetting weight limit to 22 after 52150 givens. % 25.63/25.82 % 25.67/25.84 % 25.67/25.84 % 25.67/25.84 Changing weight limit from 22 to 23. % 25.67/25.84 % 25.67/25.84 Resetting weight limit to 23 after 52165 givens. % 25.67/25.84 % 25.67/25.84 % 25.67/25.84 % 25.67/25.84 Changing weight limit from 23 to 22. % 25.67/25.84 % 25.67/25.84 Resetting weight limit to 22 after 52170 givens. % 25.67/25.84 % 25.67/25.90 % 25.67/25.90 % 25.67/25.90 Changing weight limit from 22 to 23. % 25.67/25.90 % 25.67/25.90 Resetting weight limit to 23 after 52225 givens. % 25.67/25.90 % 29.88/30.05 % 29.88/30.05 % 29.88/30.05 Changing weight limit from 23 to 22. % 29.88/30.05 % 29.88/30.05 Resetting weight limit to 22 after 55910 givens. % 29.88/30.05 % 30.00/30.20 % 30.00/30.20 % 30.00/30.20 Changing weight limit from 22 to 21. % 30.00/30.20 % 30.00/30.20 Resetting weight limit to 21 after 56005 givens. % 30.00/30.20 % 137.52/137.79 % 137.52/137.79 % 137.52/137.79 Changing weight limit from 21 to 22. % 137.52/137.79 % 137.52/137.79 Resetting weight limit to 22 after 140925 givens. % 137.52/137.79 % 137.52/137.79 % 137.52/137.79 % 137.52/137.79 Changing weight limit from 22 to 21. % 137.52/137.79 % 137.52/137.79 Resetting weight limit to 21 after 140930 givens. % 137.52/137.79 % 137.58/137.80 % 137.58/137.80 % 137.58/137.80 Changing weight limit from 21 to 22. % 137.58/137.80 % 137.58/137.80 Resetting weight limit to 22 after 140935 givens. % 137.58/137.80 % 137.58/137.81 % 137.58/137.81 % 137.58/137.81 Changing weight limit from 22 to 21. % 137.58/137.81 % 137.58/137.81 Resetting weight limit to 21 after 140940 givens. % 137.58/137.81 % 137.58/137.85 % 137.58/137.85 % 137.58/137.85 Changing weight limit from 21 to 22. % 137.58/137.85 % 137.58/137.85 Resetting weight limit to 22 after 140965 givens. % 137.58/137.85 % 137.65/137.87 % 137.65/137.87 % 137.65/137.87 Changing weight limit from 22 to 23. % 137.65/137.87 % 137.65/137.87 Resetting weight limit to 23 after 140975 givens. % 137.65/137.87 % 137.65/137.87 % 137.65/137.87 % 137.65/137.87 Changing weight limit from 23 to 24. % 137.65/137.87 % 137.65/137.87 Resetting weight limit to 24 after 140980 givens. % 137.65/137.87 % 137.65/137.88 % 137.65/137.88 % 137.65/137.88 Changing weight limit from 24 to 23. % 137.65/137.88 % 137.65/137.88 Resetting weight limit to 23 after 140985 givens. % 137.65/137.88 % 300.02/300.28 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------