%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : PLA007-1 : TPTP v8.1.0. Released v1.1.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n017.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 : Mon Jul 18 17:32:11 EDT 2022 % Result : Timeout 300.05s 300.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PLA007-1 : TPTP v8.1.0. Released v1.1.0. % 0.00/0.12 % Command : sos-script %s % 0.12/0.33 % Computer : n017.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 : Tue May 31 21:07:11 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.35 ----- Otter 3.2, August 2001 ----- % 0.19/0.35 The process was started by sandbox on n017.cluster.edu, % 0.19/0.35 Tue May 31 21:07:11 2022 % 0.19/0.35 The command was "./sos". The process ID is 14428. % 0.19/0.35 % 0.19/0.35 set(prolog_style_variables). % 0.19/0.35 set(auto). % 0.19/0.35 dependent: set(auto1). % 0.19/0.35 dependent: set(process_input). % 0.19/0.35 dependent: clear(print_kept). % 0.19/0.35 dependent: clear(print_new_demod). % 0.19/0.35 dependent: clear(print_back_demod). % 0.19/0.35 dependent: clear(print_back_sub). % 0.19/0.35 dependent: set(control_memory). % 0.19/0.35 dependent: assign(max_mem, 12000). % 0.19/0.35 dependent: assign(pick_given_ratio, 4). % 0.19/0.35 dependent: assign(stats_level, 1). % 0.19/0.35 dependent: assign(pick_semantic_ratio, 3). % 0.19/0.35 dependent: assign(sos_limit, 5000). % 0.19/0.35 dependent: assign(max_weight, 60). % 0.19/0.35 clear(print_given). % 0.19/0.35 % 0.19/0.35 list(usable). % 0.19/0.35 % 0.19/0.35 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=4. % 0.19/0.35 % 0.19/0.35 This is a Horn set without equality. The strategy will % 0.19/0.35 be hyperresolution, with satellites in sos and nuclei % 0.19/0.35 in usable. % 0.19/0.35 % 0.19/0.35 dependent: set(hyper_res). % 0.19/0.35 dependent: clear(order_hyper). % 0.19/0.35 % 0.19/0.35 ------------> process usable: % 0.19/0.35 % 0.19/0.35 ------------> process sos: % 0.19/0.35 % 0.19/0.35 ======= end of input processing ======= % 0.19/0.39 % 0.19/0.39 Model 1 (0.00 seconds, 0 Inserts) % 0.19/0.39 % 0.19/0.39 Stopped by limit on number of solutions % 0.19/0.39 % 0.19/0.39 % 0.19/0.39 -------------- Softie stats -------------- % 0.19/0.39 % 0.19/0.39 UPDATE_STOP: 300 % 0.19/0.39 SFINDER_TIME_LIMIT: 2 % 0.19/0.39 SHORT_CLAUSE_CUTOFF: 4 % 0.19/0.39 number of clauses in intial UL: 12 % 0.19/0.39 number of clauses initially in problem: 31 % 0.19/0.39 percentage of clauses intially in UL: 38 % 0.19/0.39 percentage of distinct symbols occuring in initial UL: 81 % 0.19/0.39 percent of all initial clauses that are short: 96 % 0.19/0.39 absolute distinct symbol count: 16 % 0.19/0.39 distinct predicate count: 2 % 0.19/0.39 distinct function count: 7 % 0.19/0.39 distinct constant count: 7 % 0.19/0.39 % 0.19/0.39 ---------- no more Softie stats ---------- % 0.19/0.39 % 0.19/0.39 % 0.19/0.39 % 0.19/0.39 Model 2 (0.00 seconds, 0 Inserts) % 0.19/0.39 % 0.19/0.39 Stopped by limit on number of solutions % 0.19/0.39 % 0.19/0.39 =========== start of search =========== % 1.16/1.35 % 1.16/1.35 % 1.16/1.35 Changing weight limit from 60 to 16. % 1.16/1.35 % 1.16/1.35 Model 3 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Model 4 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Model 5 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Model 6 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Model 7 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Model 8 (0.00 seconds, 0 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on number of solutions % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Model 9 [ 3 1 900 ] (0.00 seconds, 250000 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Model 10 [ 6 0 827 ] (0.00 seconds, 250000 Inserts) % 1.16/1.35 % 1.16/1.35 Stopped by limit on insertions % 1.16/1.35 % 1.16/1.35 Model 11 [ 6 1 6726 ] (0.00 seconds, 250000 Inserts) % 1.16/1.35 % 1.16/1.35 Resetting weight limit to 16 after 115 givens. % 1.16/1.35 % 1.16/1.37 % 1.16/1.37 % 1.16/1.37 Changing weight limit from 16 to 15. % 1.16/1.37 % 1.16/1.37 Resetting weight limit to 15 after 120 givens. % 1.16/1.37 % 2.65/2.82 % 2.65/2.82 % 2.65/2.82 Changing weight limit from 15 to 14. % 2.65/2.82 % 2.65/2.82 Modelling stopped after 300 given clauses and 0.00 seconds % 2.65/2.82 % 2.65/2.82 % 2.65/2.82 Resetting weight limit to 14 after 690 givens. % 2.65/2.82 % 44.00/44.23 % 44.00/44.23 % 44.00/44.23 Changing weight limit from 14 to 15. % 44.00/44.23 % 44.00/44.23 Resetting weight limit to 15 after 7965 givens. % 44.00/44.23 % 44.09/44.30 % 44.09/44.30 % 44.09/44.30 Changing weight limit from 15 to 14. % 44.09/44.30 % 44.09/44.30 Resetting weight limit to 14 after 7970 givens. % 44.09/44.30 % 44.36/44.54 % 44.36/44.54 % 44.36/44.54 Changing weight limit from 14 to 15. % 44.36/44.54 % 44.36/44.54 Resetting weight limit to 15 after 7985 givens. % 44.36/44.54 % 44.44/44.62 % 44.44/44.62 % 44.44/44.62 Changing weight limit from 15 to 14. % 44.44/44.62 % 44.44/44.62 Resetting weight limit to 14 after 7990 givens. % 44.44/44.62 % 44.68/44.85 % 44.68/44.85 % 44.68/44.85 Changing weight limit from 14 to 15. % 44.68/44.85 % 44.68/44.85 Resetting weight limit to 15 after 8005 givens. % 44.68/44.85 % 44.76/44.93 % 44.76/44.93 % 44.76/44.93 Changing weight limit from 15 to 14. % 44.76/44.93 % 44.76/44.93 Resetting weight limit to 14 after 8010 givens. % 44.76/44.93 % 44.97/45.17 % 44.97/45.17 % 44.97/45.17 Changing weight limit from 14 to 15. % 44.97/45.17 % 44.97/45.17 Resetting weight limit to 15 after 8025 givens. % 44.97/45.17 % 45.05/45.25 % 45.05/45.25 % 45.05/45.25 Changing weight limit from 15 to 14. % 45.05/45.25 % 45.05/45.25 Resetting weight limit to 14 after 8030 givens. % 45.05/45.25 % 45.28/45.48 % 45.28/45.48 % 45.28/45.48 Changing weight limit from 14 to 15. % 45.28/45.48 % 45.28/45.48 Resetting weight limit to 15 after 8045 givens. % 45.28/45.48 % 45.36/45.56 % 45.36/45.56 % 45.36/45.56 Changing weight limit from 15 to 14. % 45.36/45.56 % 45.36/45.56 Resetting weight limit to 14 after 8050 givens. % 45.36/45.56 % 45.57/45.80 % 45.57/45.80 % 45.57/45.80 Changing weight limit from 14 to 15. % 45.57/45.80 % 45.57/45.80 Resetting weight limit to 15 after 8065 givens. % 45.57/45.80 % 45.66/45.88 % 45.66/45.88 % 45.66/45.88 Changing weight limit from 15 to 14. % 45.66/45.88 % 45.66/45.88 Resetting weight limit to 14 after 8070 givens. % 45.66/45.88 % 45.88/46.12 % 45.88/46.12 % 45.88/46.12 Changing weight limit from 14 to 15. % 45.88/46.12 % 45.88/46.12 Resetting weight limit to 15 after 8085 givens. % 45.88/46.12 % 46.02/46.20 % 46.02/46.20 % 46.02/46.20 Changing weight limit from 15 to 14. % 46.02/46.20 % 46.02/46.20 Resetting weight limit to 14 after 8090 givens. % 46.02/46.20 % 46.27/46.44 % 46.27/46.44 % 46.27/46.44 Changing weight limit from 14 to 15. % 46.27/46.44 % 46.27/46.44 Resetting weight limit to 15 after 8105 givens. % 46.27/46.44 % 46.32/46.52 % 46.32/46.52 % 46.32/46.52 Changing weight limit from 15 to 14. % 46.32/46.52 % 46.32/46.52 Resetting weight limit to 14 after 8110 givens. % 46.32/46.52 % 46.57/46.77 % 46.57/46.77 % 46.57/46.77 Changing weight limit from 14 to 15. % 46.57/46.77 % 46.57/46.77 Resetting weight limit to 15 after 8125 givens. % 46.57/46.77 % 46.66/46.85 % 46.66/46.85 % 46.66/46.85 Changing weight limit from 15 to 14. % 46.66/46.85 % 46.66/46.85 Resetting weight limit to 14 after 8130 givens. % 46.66/46.85 % 46.91/47.09 % 46.91/47.09 % 46.91/47.09 Changing weight limit from 14 to 15. % 46.91/47.09 % 46.91/47.09 Resetting weight limit to 15 after 8145 givens. % 46.91/47.09 % 47.00/47.17 % 47.00/47.17 % 47.00/47.17 Changing weight limit from 15 to 14. % 47.00/47.17 % 47.00/47.17 Resetting weight limit to 14 after 8150 givens. % 47.00/47.17 % 47.19/47.41 % 47.19/47.41 % 47.19/47.41 Changing weight limit from 14 to 15. % 47.19/47.41 % 47.19/47.41 Resetting weight limit to 15 after 8165 givens. % 47.19/47.41 % 47.29/47.49 % 47.29/47.49 % 47.29/47.49 Changing weight limit from 15 to 14. % 47.29/47.49 % 47.29/47.49 Resetting weight limit to 14 after 8170 givens. % 47.29/47.49 % 47.46/47.66 % 47.46/47.66 % 47.46/47.66 Changing weight limit from 14 to 15. % 47.46/47.66 % 47.46/47.66 Resetting weight limit to 15 after 8185 givens. % 47.46/47.66 % 47.51/47.71 % 47.51/47.71 % 47.51/47.71 Changing weight limit from 15 to 14. % 47.51/47.71 % 47.51/47.71 Resetting weight limit to 14 after 8190 givens. % 47.51/47.71 % 47.62/47.79 % 47.62/47.79 % 47.62/47.79 Changing weight limit from 14 to 15. % 47.62/47.79 % 47.62/47.79 Resetting weight limit to 15 after 8205 givens. % 47.62/47.79 % 47.66/47.84 % 47.66/47.84 % 47.66/47.84 Changing weight limit from 15 to 14. % 47.66/47.84 % 47.66/47.84 Resetting weight limit to 14 after 8210 givens. % 47.66/47.84 % 47.75/47.92 % 47.75/47.92 % 47.75/47.92 Changing weight limit from 14 to 15. % 47.75/47.92 % 47.75/47.92 Resetting weight limit to 15 after 8225 givens. % 47.75/47.92 % 47.79/47.97 % 47.79/47.97 % 47.79/47.97 Changing weight limit from 15 to 14. % 47.79/47.97 % 47.79/47.97 Resetting weight limit to 14 after 8230 givens. % 47.79/47.97 % 47.88/48.05 % 47.88/48.05 % 47.88/48.05 Changing weight limit from 14 to 15. % 47.88/48.05 % 47.88/48.05 Resetting weight limit to 15 after 8245 givens. % 47.88/48.05 % 47.91/48.10 % 47.91/48.10 % 47.91/48.10 Changing weight limit from 15 to 14. % 47.91/48.10 % 47.91/48.10 Resetting weight limit to 14 after 8250 givens. % 47.91/48.10 % 48.11/48.31 % 48.11/48.31 % 48.11/48.31 Changing weight limit from 14 to 15. % 48.11/48.31 % 48.11/48.31 Resetting weight limit to 15 after 8265 givens. % 48.11/48.31 % 48.21/48.39 % 48.21/48.39 % 48.21/48.39 Changing weight limit from 15 to 14. % 48.21/48.39 % 48.21/48.39 Resetting weight limit to 14 after 8270 givens. % 48.21/48.39 % 48.41/48.64 % 48.41/48.64 % 48.41/48.64 Changing weight limit from 14 to 15. % 48.41/48.64 % 48.41/48.64 Resetting weight limit to 15 after 8285 givens. % 48.41/48.64 % 48.55/48.72 % 48.55/48.72 % 48.55/48.72 Changing weight limit from 15 to 14. % 48.55/48.72 % 48.55/48.72 Resetting weight limit to 14 after 8290 givens. % 48.55/48.72 % 48.80/48.97 % 48.80/48.97 % 48.80/48.97 Changing weight limit from 14 to 15. % 48.80/48.97 % 48.80/48.97 Resetting weight limit to 15 after 8305 givens. % 48.80/48.97 % 48.86/49.05 % 48.86/49.05 % 48.86/49.05 Changing weight limit from 15 to 14. % 48.86/49.05 % 48.86/49.05 Resetting weight limit to 14 after 8310 givens. % 48.86/49.05 % 49.10/49.30 % 49.10/49.30 % 49.10/49.30 Changing weight limit from 14 to 15. % 49.10/49.30 % 49.10/49.30 Resetting weight limit to 15 after 8325 givens. % 49.10/49.30 % 49.18/49.39 % 49.18/49.39 % 49.18/49.39 Changing weight limit from 15 to 14. % 49.18/49.39 % 49.18/49.39 Resetting weight limit to 14 after 8330 givens. % 49.18/49.39 % 49.43/49.63 % 49.43/49.63 % 49.43/49.63 Changing weight limit from 14 to 15. % 49.43/49.63 % 49.43/49.63 Resetting weight limit to 15 after 8345 givens. % 49.43/49.63 % 49.47/49.72 % 49.47/49.72 % 49.47/49.72 Changing weight limit from 15 to 14. % 49.47/49.72 % 49.47/49.72 Resetting weight limit to 14 after 8350 givens. % 49.47/49.72 % 49.79/49.97 % 49.79/49.97 % 49.79/49.97 Changing weight limit from 14 to 15. % 49.79/49.97 % 49.79/49.97 Resetting weight limit to 15 after 8365 givens. % 49.79/49.97 % 49.87/50.05 % 49.87/50.05 % 49.87/50.05 Changing weight limit from 15 to 14. % 49.87/50.05 % 49.87/50.05 Resetting weight limit to 14 after 8370 givens. % 49.87/50.05 % 50.09/50.30 % 50.09/50.30 % 50.09/50.30 Changing weight limit from 14 to 15. % 50.09/50.30 % 50.09/50.30 Resetting weight limit to 15 after 8385 givens. % 50.09/50.30 % 50.21/50.39 % 50.21/50.39 % 50.21/50.39 Changing weight limit from 15 to 14. % 50.21/50.39 % 50.21/50.39 Resetting weight limit to 14 after 8390 givens. % 50.21/50.39 % 50.46/50.64 % 50.46/50.64 % 50.46/50.64 Changing weight limit from 14 to 15. % 50.46/50.64 % 50.46/50.64 Resetting weight limit to 15 after 8405 givens. % 50.46/50.64 % 50.49/50.72 % 50.49/50.72 % 50.49/50.72 Changing weight limit from 15 to 14. % 50.49/50.72 % 50.49/50.72 Resetting weight limit to 14 after 8410 givens. % 50.49/50.72 % 50.76/50.97 % 50.76/50.97 % 50.76/50.97 Changing weight limit from 14 to 15. % 50.76/50.97 % 50.76/50.97 Resetting weight limit to 15 after 8425 givens. % 50.76/50.97 % 50.89/51.06 % 50.89/51.06 % 50.89/51.06 Changing weight limit from 15 to 14. % 50.89/51.06 % 50.89/51.06 Resetting weight limit to 14 after 8430 givens. % 50.89/51.06 % 51.10/51.31 % 51.10/51.31 % 51.10/51.31 Changing weight limit from 14 to 15. % 51.10/51.31 % 51.10/51.31 Resetting weight limit to 15 after 8445 givens. % 51.10/51.31 % 51.21/51.39 % 51.21/51.39 % 51.21/51.39 Changing weight limit from 15 to 14. % 51.21/51.39 % 51.21/51.39 Resetting weight limit to 14 after 8450 givens. % 51.21/51.39 % 51.41/51.65 % 51.41/51.65 % 51.41/51.65 Changing weight limit from 14 to 15. % 51.41/51.65 % 51.41/51.65 Resetting weight limit to 15 after 8465 givens. % 51.41/51.65 % 51.57/51.73 % 51.57/51.73 % 51.57/51.73 Changing weight limit from 15 to 14. % 51.57/51.73 % 51.57/51.73 Resetting weight limit to 14 after 8470 givens. % 51.57/51.73 % 51.82/51.99 % 51.82/51.99 % 51.82/51.99 Changing weight limit from 14 to 15. % 51.82/51.99 % 51.82/51.99 Resetting weight limit to 15 after 8485 givens. % 51.82/51.99 % 51.88/52.07 % 51.88/52.07 % 51.88/52.07 Changing weight limit from 15 to 14. % 51.88/52.07 % 51.88/52.07 Resetting weight limit to 14 after 8490 givens. % 51.88/52.07 % 52.13/52.33 % 52.13/52.33 % 52.13/52.33 Changing weight limit from 14 to 15. % 52.13/52.33 % 52.13/52.33 Resetting weight limit to 15 after 8505 givens. % 52.13/52.33 % 52.16/52.41 % 52.16/52.41 % 52.16/52.41 Changing weight limit from 15 to 14. % 52.16/52.41 % 52.16/52.41 Resetting weight limit to 14 after 8510 givens. % 52.16/52.41 % 52.48/52.67 % 52.48/52.67 % 52.48/52.67 Changing weight limit from 14 to 15. % 52.48/52.67 % 52.48/52.67 Resetting weight limit to 15 after 8525 givens. % 52.48/52.67 % 52.57/52.75 % 52.57/52.75 % 52.57/52.75 Changing weight limit from 15 to 14. % 52.57/52.75 % 52.57/52.75 Resetting weight limit to 14 after 8530 givens. % 52.57/52.75 % 52.78/53.01 % 52.78/53.01 % 52.78/53.01 Changing weight limit from 14 to 15. % 52.78/53.01 % 52.78/53.01 Resetting weight limit to 15 after 8545 givens. % 52.78/53.01 % 52.93/53.10 % 52.93/53.10 % 52.93/53.10 Changing weight limit from 15 to 14. % 52.93/53.10 % 52.93/53.10 Resetting weight limit to 14 after 8550 givens. % 52.93/53.10 % 53.18/53.36 % 53.18/53.36 % 53.18/53.36 Changing weight limit from 14 to 15. % 53.18/53.36 % 53.18/53.36 Resetting weight limit to 15 after 8565 givens. % 53.18/53.36 % 53.27/53.44 % 53.27/53.44 % 53.27/53.44 Changing weight limit from 15 to 14. % 53.27/53.44 % 53.27/53.44 Resetting weight limit to 14 after 8570 givens. % 53.27/53.44 % 53.51/53.70 % 53.51/53.70 % 53.51/53.70 Changing weight limit from 14 to 15. % 53.51/53.70 % 53.51/53.70 Resetting weight limit to 15 after 8585 givens. % 53.51/53.70 % 53.60/53.79 % 53.60/53.79 % 53.60/53.79 Changing weight limit from 15 to 14. % 53.60/53.79 % 53.60/53.79 Resetting weight limit to 14 after 8590 givens. % 53.60/53.79 % 53.87/54.05 % 53.87/54.05 % 53.87/54.05 Changing weight limit from 14 to 15. % 53.87/54.05 % 53.87/54.05 Resetting weight limit to 15 after 8605 givens. % 53.87/54.05 % 53.96/54.14 % 53.96/54.14 % 53.96/54.14 Changing weight limit from 15 to 14. % 53.96/54.14 % 53.96/54.14 Resetting weight limit to 14 after 8610 givens. % 53.96/54.14 % 54.21/54.40 % 54.21/54.40 % 54.21/54.40 Changing weight limit from 14 to 15. % 54.21/54.40 % 54.21/54.40 Resetting weight limit to 15 after 8625 givens. % 54.21/54.40 % 54.28/54.48 % 54.28/54.48 % 54.28/54.48 Changing weight limit from 15 to 14. % 54.28/54.48 % 54.28/54.48 Resetting weight limit to 14 after 8630 givens. % 54.28/54.48 % 54.57/54.75 % 54.57/54.75 % 54.57/54.75 Changing weight limit from 14 to 15. % 54.57/54.75 % 54.57/54.75 Resetting weight limit to 15 after 8645 givens. % 54.57/54.75 % 54.66/54.83 % 54.66/54.83 % 54.66/54.83 Changing weight limit from 15 to 14. % 54.66/54.83 % 54.66/54.83 Resetting weight limit to 14 after 8650 givens. % 54.66/54.83 % 54.86/55.10 % 54.86/55.10 % 54.86/55.10 Changing weight limit from 14 to 15. % 54.86/55.10 % 54.86/55.10 Resetting weight limit to 15 after 8665 givens. % 54.86/55.10 % 55.01/55.18 % 55.01/55.18 % 55.01/55.18 Changing weight limit from 15 to 14. % 55.01/55.18 % 55.01/55.18 Resetting weight limit to 14 after 8670 givens. % 55.01/55.18 % 55.26/55.45 % 55.26/55.45 % 55.26/55.45 Changing weight limit from 14 to 15. % 55.26/55.45 % 55.26/55.45 Resetting weight limit to 15 after 8685 givens. % 55.26/55.45 % 55.33/55.54 % 55.33/55.54 % 55.33/55.54 Changing weight limit from 15 to 14. % 55.33/55.54 % 55.33/55.54 Resetting weight limit to 14 after 8690 givens. % 55.33/55.54 % 55.63/55.80 % 55.63/55.80 % 55.63/55.80 Changing weight limit from 14 to 15. % 55.63/55.80 % 55.63/55.80 Resetting weight limit to 15 after 8705 givens. % 55.63/55.80 % 55.70/55.89 % 55.70/55.89 % 55.70/55.89 Changing weight limit from 15 to 14. % 55.70/55.89 % 55.70/55.89 Resetting weight limit to 14 after 8710 givens. % 55.70/55.89 % 55.99/56.16 % 55.99/56.16 % 55.99/56.16 Changing weight limit from 14 to 15. % 55.99/56.16 % 55.99/56.16 Resetting weight limit to 15 after 8725 givens. % 55.99/56.16 % 55.99/56.24 % 55.99/56.24 % 55.99/56.24 Changing weight limit from 15 to 14. % 55.99/56.24 % 55.99/56.24 Resetting weight limit to 14 after 8730 givens. % 55.99/56.24 % 56.28/56.51 % 56.28/56.51 % 56.28/56.51 Changing weight limit from 14 to 15. % 56.28/56.51 % 56.28/56.51 Resetting weight limit to 15 after 8745 givens. % 56.28/56.51 % 56.39/56.60 % 56.39/56.60 % 56.39/56.60 Changing weight limit from 15 to 14. % 56.39/56.60 % 56.39/56.60 Resetting weight limit to 14 after 8750 givens. % 56.39/56.60 % 56.69/56.87 % 56.69/56.87 % 56.69/56.87 Changing weight limit from 14 to 15. % 56.69/56.87 % 56.69/56.87 Resetting weight limit to 15 after 8765 givens. % 56.69/56.87 % 56.79/56.96 % 56.79/56.96 % 56.79/56.96 Changing weight limit from 15 to 14. % 56.79/56.96 % 56.79/56.96 Resetting weight limit to 14 after 8770 givens. % 56.79/56.96 % 56.92/57.14 % 56.92/57.14 % 56.92/57.14 Changing weight limit from 14 to 15. % 56.92/57.14 % 56.92/57.14 Resetting weight limit to 15 after 8780 givens. % 56.92/57.14 % 57.07/57.23 % 57.07/57.23 % 57.07/57.23 Changing weight limit from 15 to 16. % 57.07/57.23 % 57.07/57.23 Resetting weight limit to 16 after 8785 givens. % 57.07/57.23 % 57.09/57.29 % 57.09/57.29 % 57.09/57.29 Changing weight limit from 16 to 15. % 57.09/57.29 % 57.09/57.29 Resetting weight limit to 15 after 8790 givens. % 57.09/57.29 % 57.21/57.40 % 57.21/57.40 % 57.21/57.40 Changing weight limit from 15 to 16. % 57.21/57.40 % 57.21/57.40 Resetting weight limit to 16 after 8805 givens. % 57.21/57.40 % 57.30/57.49 % 57.30/57.49 % 57.30/57.49 Changing weight limit from 16 to 15. % 57.30/57.49 % 57.30/57.49 Resetting weight limit to 15 after 8810 givens. % 57.30/57.49 % 57.59/57.76 % 57.59/57.76 % 57.59/57.76 Changing weight limit from 15 to 16. % 57.59/57.76 % 57.59/57.76 Resetting weight limit to 16 after 8825 givens. % 57.59/57.76 % 57.69/57.85 % 57.69/57.85 % 57.69/57.85 Changing weight limit from 16 to 15. % 57.69/57.85 % 57.69/57.85 Resetting weight limit to 15 after 8830 givens. % 57.69/57.85 % 57.97/58.13 % 57.97/58.13 % 57.97/58.13 Changing weight limit from 15 to 16. % 57.97/58.13 % 57.97/58.13 Resetting weight limit to 16 after 8845 givens. % 57.97/58.13 % 57.98/58.22 % 57.98/58.22 % 57.98/58.22 Changing weight limit from 16 to 15. % 57.98/58.22 % 57.98/58.22 Resetting weight limit to 15 after 8850 givens. % 57.98/58.22 % 58.12/58.32 % 58.12/58.32 % 58.12/58.32 Changing weight limit from 15 to 16. % 58.12/58.32 % 58.12/58.32 Resetting weight limit to 16 after 8855 givens. % 58.12/58.32 % 58.25/58.41 % 58.25/58.41 % 58.25/58.41 Changing weight limit from 16 to 15. % 58.25/58.41 % 58.25/58.41 Resetting weight limit to 15 after 8860 givens. % 58.25/58.41 % 58.26/58.50 % 58.26/58.50 % 58.26/58.50 Changing weight limit from 15 to 16. % 58.26/58.50 % 58.26/58.50 Resetting weight limit to 16 after 8865 givens. % 58.26/58.50 % 58.42/58.60 % 58.42/58.60 % 58.42/58.60 Changing weight limit from 16 to 15. % 58.42/58.60 % 58.42/58.60 Resetting weight limit to 15 after 8870 givens. % 58.42/58.60 % 58.67/58.88 % 58.67/58.88 % 58.67/58.88 Changing weight limit from 15 to 16. % 58.67/58.88 % 58.67/58.88 Resetting weight limit to 16 after 8885 givens. % 58.67/58.88 % 58.75/58.97 % 58.75/58.97 % 58.75/58.97 Changing weight limit from 16 to 15. % 58.75/58.97 % 58.75/58.97 Resetting weight limit to 15 after 8890 givens. % 58.75/58.97 % 59.04/59.25 % 59.04/59.25 % 59.04/59.25 Changing weight limit from 15 to 16. % 59.04/59.25 % 59.04/59.25 Resetting weight limit to 16 after 8905 givens. % 59.04/59.25 % 59.11/59.34 % 59.11/59.34 % 59.11/59.34 Changing weight limit from 16 to 15. % 59.11/59.34 % 59.11/59.34 Resetting weight limit to 15 after 8910 givens. % 59.11/59.34 % 59.40/59.62 % 59.40/59.62 % 59.40/59.62 Changing weight limit from 15 to 16. % 59.40/59.62 % 59.40/59.62 Resetting weight limit to 16 after 8925 givens. % 59.40/59.62 % 59.53/59.71 % 59.53/59.71 % 59.53/59.71 Changing weight limit from 16 to 15. % 59.53/59.71 % 59.53/59.71 Resetting weight limit to 15 after 8930 givens. % 59.53/59.71 % 59.80/59.99 % 59.80/59.99 % 59.80/59.99 Changing weight limit from 15 to 16. % 59.80/59.99 % 59.80/59.99 Resetting weight limit to 16 after 8945 givens. % 59.80/59.99 % 59.90/60.08 % 59.90/60.08 % 59.90/60.08 Changing weight limit from 16 to 15. % 59.90/60.08 % 59.90/60.08 Resetting weight limit to 15 after 8950 givens. % 59.90/60.08 % 60.20/60.36 % 60.20/60.36 % 60.20/60.36 Changing weight limit from 15 to 16. % 60.20/60.36 % 60.20/60.36 Resetting weight limit to 16 after 8965 givens. % 60.20/60.36 % 60.29/60.46 % 60.29/60.46 % 60.29/60.46 Changing weight limit from 16 to 15. % 60.29/60.46 % 60.29/60.46 Resetting weight limit to 15 after 8970 givens. % 60.29/60.46 % 60.57/60.74 % 60.57/60.74 % 60.57/60.74 Changing weight limit from 15 to 16. % 60.57/60.74 % 60.57/60.74 Resetting weight limit to 16 after 8985 givens. % 60.57/60.74 % 60.61/60.84 % 60.61/60.84 % 60.61/60.84 Changing weight limit from 16 to 15. % 60.61/60.84 % 60.61/60.84 Resetting weight limit to 15 after 8990 givens. % 60.61/60.84 % 60.93/61.12 % 60.93/61.12 % 60.93/61.12 Changing weight limit from 15 to 16. % 60.93/61.12 % 60.93/61.12 Resetting weight limit to 16 after 9005 givens. % 60.93/61.12 % 61.02/61.21 % 61.02/61.21 % 61.02/61.21 Changing weight limit from 16 to 15. % 61.02/61.21 % 61.02/61.21 Resetting weight limit to 15 after 9010 givens. % 61.02/61.21 % 61.32/61.50 % 61.32/61.50 % 61.32/61.50 Changing weight limit from 15 to 16. % 61.32/61.50 % 61.32/61.50 Resetting weight limit to 16 after 9025 givens. % 61.32/61.50 % 61.38/61.59 % 61.38/61.59 % 61.38/61.59 Changing weight limit from 16 to 15. % 61.38/61.59 % 61.38/61.59 Resetting weight limit to 15 after 9030 givens. % 61.38/61.59 % 61.66/61.88 % 61.66/61.88 % 61.66/61.88 Changing weight limit from 15 to 16. % 61.66/61.88 % 61.66/61.88 Resetting weight limit to 16 after 9045 givens. % 61.66/61.88 % 61.75/61.98 % 61.75/61.98 % 61.75/61.98 Changing weight limit from 16 to 15. % 61.75/61.98 % 61.75/61.98 Resetting weight limit to 15 after 9050 givens. % 61.75/61.98 % 62.06/62.26 % 62.06/62.26 % 62.06/62.26 Changing weight limit from 15 to 16. % 62.06/62.26 % 62.06/62.26 Resetting weight limit to 16 after 9065 givens. % 62.06/62.26 % 62.15/62.34 % 62.15/62.34 % 62.15/62.34 Changing weight limit from 16 to 15. % 62.15/62.34 % 62.15/62.34 Resetting weight limit to 15 after 9070 givens. % 62.15/62.34 % 62.22/62.42 % 62.22/62.42 % 62.22/62.42 Changing weight limit from 15 to 16. % 62.22/62.42 % 62.22/62.42 Resetting weight limit to 16 after 9075 givens. % 62.22/62.42 % 62.33/62.50 % 62.33/62.50 % 62.33/62.50 Changing weight limit from 16 to 15. % 62.33/62.50 % 62.33/62.50 Resetting weight limit to 15 after 9080 givens. % 62.33/62.50 % 62.36/62.57 % 62.36/62.57 % 62.36/62.57 Changing weight limit from 15 to 16. % 62.36/62.57 % 62.36/62.57 Resetting weight limit to 16 after 9085 givens. % 62.36/62.57 % 62.44/62.67 % 62.44/62.67 % 62.44/62.67 Changing weight limit from 16 to 15. % 62.44/62.67 % 62.44/62.67 Resetting weight limit to 15 after 9090 givens. % 62.44/62.67 % 62.52/62.76 % 62.52/62.76 % 62.52/62.76 Changing weight limit from 15 to 16. % 62.52/62.76 % 62.52/62.76 Resetting weight limit to 16 after 9095 givens. % 62.52/62.76 % 62.68/62.86 % 62.68/62.86 % 62.68/62.86 Changing weight limit from 16 to 15. % 62.68/62.86 % 62.68/62.86 Resetting weight limit to 15 after 9100 givens. % 62.68/62.86 % 62.74/62.95 % 62.74/62.95 % 62.74/62.95 Changing weight limit from 15 to 16. % 62.74/62.95 % 62.74/62.95 Resetting weight limit to 16 after 9105 givens. % 62.74/62.95 % 62.80/63.05 % 62.80/63.05 % 62.80/63.05 Changing weight limit from 16 to 15. % 62.80/63.05 % 62.80/63.05 Resetting weight limit to 15 after 9110 givens. % 62.80/63.05 % 63.10/63.33 % 63.10/63.33 % 63.10/63.33 Changing weight limit from 15 to 16. % 63.10/63.33 % 63.10/63.33 Resetting weight limit to 16 after 9125 givens. % 63.10/63.33 % 63.24/63.43 % 63.24/63.43 % 63.24/63.43 Changing weight limit from 16 to 15. % 63.24/63.43 % 63.24/63.43 Resetting weight limit to 15 after 9130 givens. % 63.24/63.43 % 63.55/63.72 % 63.55/63.72 % 63.55/63.72 Changing weight limit from 15 to 16. % 63.55/63.72 % 63.55/63.72 Resetting weight limit to 16 after 9145 givens. % 63.55/63.72 % 63.59/63.81 % 63.59/63.81 % 63.59/63.81 Changing weight limit from 16 to 15. % 63.59/63.81 % 63.59/63.81 Resetting weight limit to 15 after 9150 givens. % 63.59/63.81 % 63.89/64.10 % 63.89/64.10 % 63.89/64.10 Changing weight limit from 15 to 16. % 63.89/64.10 % 63.89/64.10 Resetting weight limit to 16 after 9165 givens. % 63.89/64.10 % 64.02/64.20 % 64.02/64.20 % 64.02/64.20 Changing weight limit from 16 to 15. % 64.02/64.20 % 64.02/64.20 Resetting weight limit to 15 after 9170 givens. % 64.02/64.20 % 64.11/64.29 % 64.11/64.29 % 64.11/64.29 Changing weight limit from 15 to 16. % 64.11/64.29 % 64.11/64.29 Resetting weight limit to 16 after 9175 givens. % 64.11/64.29 % 64.19/64.39 % 64.19/64.39 % 64.19/64.39 Changing weight limit from 16 to 15. % 64.19/64.39 % 64.19/64.39 Resetting weight limit to 15 after 9180 givens. % 64.19/64.39 % 64.27/64.46 % 64.27/64.46 % 64.27/64.46 Changing weight limit from 15 to 16. % 64.27/64.46 % 64.27/64.46 Resetting weight limit to 16 after 9185 givens. % 64.27/64.46 % 64.33/64.54 % 64.33/64.54 % 64.33/64.54 Changing weight limit from 16 to 15. % 64.33/64.54 % 64.33/64.54 Resetting weight limit to 15 after 9190 givens. % 64.33/64.54 % 64.47/64.64 % 64.47/64.64 % 64.47/64.64 Changing weight limit from 15 to 16. % 64.47/64.64 % 64.47/64.64 Resetting weight limit to 16 after 9195 givens. % 64.47/64.64 % 64.56/64.74 % 64.56/64.74 % 64.56/64.74 Changing weight limit from 16 to 15. % 64.56/64.74 % 64.56/64.74 Resetting weight limit to 15 after 9200 givens. % 64.56/64.74 % 64.61/64.83 % 64.61/64.83 % 64.61/64.83 Changing weight limit from 15 to 16. % 64.61/64.83 % 64.61/64.83 Resetting weight limit to 16 after 9205 givens. % 64.61/64.83 % 64.76/64.93 % 64.76/64.93 % 64.76/64.93 Changing weight limit from 16 to 15. % 64.76/64.93 % 64.76/64.93 Resetting weight limit to 15 after 9210 givens. % 64.76/64.93 % 64.87/65.03 % 64.87/65.03 % 64.87/65.03 Changing weight limit from 15 to 16. % 64.87/65.03 % 64.87/65.03 Resetting weight limit to 16 after 9215 givens. % 64.87/65.03 % 64.93/65.13 % 64.93/65.13 % 64.93/65.13 Changing weight limit from 16 to 15. % 64.93/65.13 % 64.93/65.13 Resetting weight limit to 15 after 9220 givens. % 64.93/65.13 % 65.05/65.21 % 65.05/65.21 % 65.05/65.21 Changing weight limit from 15 to 16. % 65.05/65.21 % 65.05/65.21 Resetting weight limit to 16 after 9225 givens. % 65.05/65.21 % 65.06/65.29 % 65.06/65.29 % 65.06/65.29 Changing weight limit from 16 to 15. % 65.06/65.29 % 65.06/65.29 Resetting weight limit to 15 after 9230 givens. % 65.06/65.29 % 65.15/65.38 % 65.15/65.38 % 65.15/65.38 Changing weight limit from 15 to 16. % 65.15/65.38 % 65.15/65.38 Resetting weight limit to 16 after 9235 givens. % 65.15/65.38 % 65.32/65.48 % 65.32/65.48 % 65.32/65.48 Changing weight limit from 16 to 15. % 65.32/65.48 % 65.32/65.48 Resetting weight limit to 15 after 9240 givens. % 65.32/65.48 % 65.37/65.58 % 65.37/65.58 % 65.37/65.58 Changing weight limit from 15 to 16. % 65.37/65.58 % 65.37/65.58 Resetting weight limit to 16 after 9245 givens. % 65.37/65.58 % 65.46/65.68 % 65.46/65.68 % 65.46/65.68 Changing weight limit from 16 to 15. % 65.46/65.68 % 65.46/65.68 Resetting weight limit to 15 after 9250 givens. % 65.46/65.68 % 65.62/65.78 % 65.62/65.78 % 65.62/65.78 Changing weight limit from 15 to 16. % 65.62/65.78 % 65.62/65.78 Resetting weight limit to 16 after 9255 givens. % 65.62/65.78 % 65.71/65.88 % 65.71/65.88 % 65.71/65.88 Changing weight limit from 16 to 15. % 65.71/65.88 % 65.71/65.88 Resetting weight limit to 15 after 9260 givens. % 65.71/65.88 % 65.77/65.96 % 65.77/65.96 % 65.77/65.96 Changing weight limit from 15 to 16. % 65.77/65.96 % 65.77/65.96 Resetting weight limit to 16 after 9265 givens. % 65.77/65.96 % 65.85/66.05 % 65.85/66.05 % 65.85/66.05 Changing weight limit from 16 to 15. % 65.85/66.05 % 65.85/66.05 Resetting weight limit to 15 after 9270 givens. % 65.85/66.05 % 66.15/66.35 % 66.15/66.35 % 66.15/66.35 Changing weight limit from 15 to 16. % 66.15/66.35 % 66.15/66.35 Resetting weight limit to 16 after 9285 givens. % 66.15/66.35 % 66.20/66.44 % 66.20/66.44 % 66.20/66.44 Changing weight limit from 16 to 15. % 66.20/66.44 % 66.20/66.44 Resetting weight limit to 15 after 9290 givens. % 66.20/66.44 % 66.38/66.54 % 66.38/66.54 % 66.38/66.54 Changing weight limit from 15 to 16. % 66.38/66.54 % 66.38/66.54 Resetting weight limit to 16 after 9295 givens. % 66.38/66.54 % 66.44/66.64 % 66.44/66.64 % 66.44/66.64 Changing weight limit from 16 to 15. % 66.44/66.64 % 66.44/66.64 Resetting weight limit to 15 after 9300 givens. % 66.44/66.64 % 66.49/66.72 % 66.49/66.72 % 66.49/66.72 Changing weight limit from 15 to 16. % 66.49/66.72 % 66.49/66.72 Resetting weight limit to 16 after 9305 givens. % 66.49/66.72 % 66.61/66.80 % 66.61/66.80 % 66.61/66.80 Changing weight limit from 16 to 15. % 66.61/66.80 % 66.61/66.80 Resetting weight limit to 15 after 9310 givens. % 66.61/66.80 % 66.69/66.88 % 66.69/66.88 % 66.69/66.88 Changing weight limit from 15 to 16. % 66.69/66.88 % 66.69/66.88 Resetting weight limit to 16 after 9315 givens. % 66.69/66.88 % 66.79/66.96 % 66.79/66.96 % 66.79/66.96 Changing weight limit from 16 to 15. % 66.79/66.96 % 66.79/66.96 Resetting weight limit to 15 after 9320 givens. % 66.79/66.96 % 66.83/67.04 % 66.83/67.04 % 66.83/67.04 Changing weight limit from 15 to 16. % 66.83/67.04 % 66.83/67.04 Resetting weight limit to 16 after 9325 givens. % 66.83/67.04 % 66.94/67.12 % 66.94/67.12 % 66.94/67.12 Changing weight limit from 16 to 15. % 66.94/67.12 % 66.94/67.12 Resetting weight limit to 15 after 9330 givens. % 66.94/67.12 % 66.99/67.22 % 66.99/67.22 % 66.99/67.22 Changing weight limit from 15 to 16. % 66.99/67.22 % 66.99/67.22 Resetting weight limit to 16 after 9335 givens. % 66.99/67.22 % 67.13/67.30 % 67.13/67.30 % 67.13/67.30 Changing weight limit from 16 to 15. % 67.13/67.30 % 67.13/67.30 Resetting weight limit to 15 after 9340 givens. % 67.13/67.30 % 99.75/99.91 % 99.75/99.91 % 99.75/99.91 Changing weight limit from 15 to 16. % 99.75/99.91 % 99.75/99.91 Resetting weight limit to 16 after 10900 givens. % 99.75/99.91 % 117.81/117.99 % 117.81/117.99 % 117.81/117.99 Changing weight limit from 16 to 17. % 117.81/117.99 % 117.81/117.99 Resetting weight limit to 17 after 11625 givens. % 117.81/117.99 % 117.88/118.13 % 117.88/118.13 % 117.88/118.13 Changing weight limit from 17 to 18. % 117.88/118.13 % 117.88/118.13 Resetting weight limit to 18 after 11630 givens. % 117.88/118.13 % 118.09/118.27 % 118.09/118.27 % 118.09/118.27 Changing weight limit from 18 to 17. % 118.09/118.27 % 118.09/118.27 Resetting weight limit to 17 after 11635 givens. % 118.09/118.27 % 172.19/172.36 % 172.19/172.36 % 172.19/172.36 Changing weight limit from 17 to 18. % 172.19/172.36 % 172.19/172.36 Resetting weight limit to 18 after 13405 givens. % 172.19/172.36 % 172.32/172.53 % 172.32/172.53 % 172.32/172.53 Changing weight limit from 18 to 19. % 172.32/172.53 % 172.32/172.53 Resetting weight limit to 19 after 13410 givens. % 172.32/172.53 % 172.49/172.70 % 172.49/172.70 % 172.49/172.70 Changing weight limit from 19 to 18. % 172.49/172.70 % 172.49/172.70 Resetting weight limit to 18 after 13415 givens. % 172.49/172.70 % 197.16/197.38 % 197.16/197.38 % 197.16/197.38 Changing weight limit from 18 to 19. % 197.16/197.38 % 197.16/197.38 Resetting weight limit to 19 after 14125 givens. % 197.16/197.38 % 270.16/270.36 % 270.16/270.36 % 270.16/270.36 Changing weight limit from 19 to 20. % 270.16/270.36 % 270.16/270.36 Resetting weight limit to 20 after 15905 givens. % 270.16/270.36 % 300.05/300.21 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------