%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : FLD073-4 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n020.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 : Sat Jul 16 02:28:01 EDT 2022 % Result : Timeout 300.01s 300.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : FLD073-4 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.11/0.12 % Command : sos-script %s % 0.11/0.32 % Computer : n020.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Tue Jun 7 04:27:06 EDT 2022 % 0.11/0.32 % CPUTime : % 0.17/0.34 ----- Otter 3.2, August 2001 ----- % 0.17/0.34 The process was started by sandbox on n020.cluster.edu, % 0.17/0.34 Tue Jun 7 04:27:06 2022 % 0.17/0.34 The command was "./sos". The process ID is 2989. % 0.17/0.34 % 0.17/0.34 set(prolog_style_variables). % 0.17/0.34 set(auto). % 0.17/0.34 dependent: set(auto1). % 0.17/0.34 dependent: set(process_input). % 0.17/0.34 dependent: clear(print_kept). % 0.17/0.34 dependent: clear(print_new_demod). % 0.17/0.34 dependent: clear(print_back_demod). % 0.17/0.34 dependent: clear(print_back_sub). % 0.17/0.34 dependent: set(control_memory). % 0.17/0.34 dependent: assign(max_mem, 12000). % 0.17/0.34 dependent: assign(pick_given_ratio, 4). % 0.17/0.34 dependent: assign(stats_level, 1). % 0.17/0.34 dependent: assign(pick_semantic_ratio, 3). % 0.17/0.34 dependent: assign(sos_limit, 5000). % 0.17/0.34 dependent: assign(max_weight, 60). % 0.17/0.34 clear(print_given). % 0.17/0.34 % 0.17/0.34 list(usable). % 0.17/0.34 % 0.17/0.34 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5. % 0.17/0.34 % 0.17/0.34 This is a non-Horn set without equality. The strategy % 0.17/0.34 will be ordered hyper_res, ur_res, unit deletion, and % 0.17/0.34 factoring, with satellites in sos and nuclei in usable. % 0.17/0.34 % 0.17/0.34 dependent: set(hyper_res). % 0.17/0.34 dependent: set(factor). % 0.17/0.34 dependent: set(unit_deletion). % 0.17/0.34 % 0.17/0.34 ------------> process usable: % 0.17/0.34 % 0.17/0.34 ------------> process sos: % 0.17/0.34 % 0.17/0.34 ======= end of input processing ======= % 0.17/0.41 % 0.17/0.41 Model 1 (0.00 seconds, 0 Inserts) % 0.17/0.41 % 0.17/0.41 Stopped by limit on number of solutions % 0.17/0.41 % 0.17/0.41 % 0.17/0.41 -------------- Softie stats -------------- % 0.17/0.41 % 0.17/0.41 UPDATE_STOP: 300 % 0.17/0.41 SFINDER_TIME_LIMIT: 2 % 0.17/0.41 SHORT_CLAUSE_CUTOFF: 4 % 0.17/0.41 number of clauses in intial UL: 48 % 0.17/0.41 number of clauses initially in problem: 56 % 0.17/0.41 percentage of clauses intially in UL: 85 % 0.17/0.41 percentage of distinct symbols occuring in initial UL: 84 % 0.17/0.41 percent of all initial clauses that are short: 100 % 0.17/0.41 absolute distinct symbol count: 13 % 0.17/0.41 distinct predicate count: 4 % 0.17/0.41 distinct function count: 4 % 0.17/0.41 distinct constant count: 5 % 0.17/0.41 % 0.17/0.41 ---------- no more Softie stats ---------- % 0.17/0.41 % 0.17/0.41 % 0.17/0.41 % 0.17/0.41 Model 2 (0.00 seconds, 0 Inserts) % 0.17/0.41 % 0.17/0.41 Stopped by limit on number of solutions % 0.17/0.41 % 0.17/0.41 =========== start of search =========== % 9.73/10.00 % 9.73/10.00 % 9.73/10.00 Changing weight limit from 60 to 12. % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 3 [ 2 2 328 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 4 [ 2 2 389 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 5 [ 2 3 7061 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 6 [ 2 3 351 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 7 [ 2 2 318 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 8 [ 2 3 671 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 9 [ 9 3 8610 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 10 [ 8 2 268 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 11 [ 5 2 511 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 12 [ 5 2 154 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 13 [ 5 2 177 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 14 [ 6 2 297 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 15 [ 7 3 738 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 16 [ 4 2 111 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 17 [ 5 3 112 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 18 [ 4 2 156 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 19 [ 6 2 146 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 20 [ 20 1 203 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 21 [ 16 2 147 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 22 [ 9 4 27453 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 23 [ 7 3 123 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 24 [ 21 2 103 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 25 [ 6 2 6126 ] (0.00 seconds, 250000 Inserts) % 9.73/10.00 % 9.73/10.00 Stopped by limit on insertions % 9.73/10.00 % 9.73/10.00 Model 26 [ 7 3 23630 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 27 [ 6 13 168621 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 28 [ 25 2 240 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 29 [ 4 2 110 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 30 [ 9 2 560 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 31 [ 4 7 48280 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 32 [ 8 2 362 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 33 [ 7 20 188248 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 34 [ 29 2 341 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 35 [ 13 8 56903 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 36 [ 35 2 109 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 37 [ 13 2 123 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 38 [ 7 14 184145 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Stopped by limit on insertions % 9.73/10.01 % 9.73/10.01 Model 39 [ 10 5 35868 ] (0.00 seconds, 250000 Inserts) % 9.73/10.01 % 9.73/10.01 Resetting weight limit to 12 after 50 givens. % 9.73/10.01 % 12.91/13.12 % 12.91/13.12 % 12.91/13.12 Changing weight limit from 12 to 10. % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 40 [ 13 3 124 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 41 [ 13 3 9595 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 42 [ 15 2 113 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 43 [ 6 3 106 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 44 [ 35 3 374 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 45 [ 14 2 167 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 46 [ 29 5 14362 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Stopped by limit on insertions % 12.91/13.12 % 12.91/13.12 Model 47 [ 9 3 804 ] (0.00 seconds, 250000 Inserts) % 12.91/13.12 % 12.91/13.12 Resetting weight limit to 10 after 60 givens. % 12.91/13.12 % 21.39/21.61 % 21.39/21.61 % 21.39/21.61 Changing weight limit from 10 to 8. % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 48 [ 45 2 505 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 49 [ 17 2 508 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 50 [ 37 27 69042 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 51 [ 12 5 16133 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 52 [ 20 2 117 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 53 [ 15 3 108 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 54 [ 35 2 205 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 55 [ 34 3 265 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 56 [ 17 4 6148 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 57 [ 21 2 109 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 58 [ 45 2 158 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 59 [ 13 20 90333 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 60 [ 44 3 128 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 61 [ 21 2 127 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 62 [ 52 3 302 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 63 [ 17 12 48445 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Stopped by limit on insertions % 21.39/21.61 % 21.39/21.61 Model 64 [ 17 3 562 ] (0.00 seconds, 250000 Inserts) % 21.39/21.61 % 21.39/21.61 Resetting weight limit to 8 after 80 givens. % 21.39/21.61 % 39.96/40.20 % 39.96/40.20 % 39.96/40.20 Changing weight limit from 8 to 9. % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 65 [ 53 2 263 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 66 [ 31 3 1008 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 67 [ 53 3 326 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 68 [ 15 2 770 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 69 [ 18 13 40626 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 70 [ 52 1 132 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 71 [ 57 2 1262 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 72 [ 21 2 235 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 73 [ 61 1 237 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 74 [ 38 4 13813 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 75 [ 25 2 2711 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 76 [ 21 1 107 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 77 [ 24 1 105 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 78 [ 58 1 265 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 79 [ 19 16 90378 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 80 [ 27 16 80976 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 81 [ 19 2 1096 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 82 [ 69 1 537 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 83 [ 26 1 124 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 84 [ 22 1 554 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 85 [ 30 41 201575 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 86 [ 29 1 130 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 87 [ 75 1 108 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 88 [ 23 24 92408 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 89 [ 61 2 293 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 90 [ 80 2 263 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 91 [ 22 2 645 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 92 [ 78 3 3001 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 93 [ 25 1 188 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 94 [ 68 1 106 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 95 [ 24 1 364 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 96 [ 28 2 131 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 97 [ 20 2 185 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 98 [ 76 2 315 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 99 [ 27 3 1177 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Stopped by limit on insertions % 39.96/40.20 % 39.96/40.20 Model 100 [ 35 3 3126 ] (0.00 seconds, 250000 Inserts) % 39.96/40.20 % 39.96/40.20 Resetting weight limit to 9 after 155 givens. % 39.96/40.20 % 41.65/41.88 % 41.65/41.88 % 41.65/41.88 Changing weight limit from 9 to 10. % 41.65/41.88 % 41.65/41.88 Stopped by limit on insertions % 41.65/41.88 % 41.65/41.88 Model 101 [ 25 2 145 ] (0.00 seconds, 250000 Inserts) % 41.65/41.88 % 41.65/41.88 Stopped by limit on insertions % 41.65/41.88 % 41.65/41.88 Model 102 [ 74 2 174 ] (0.00 seconds, 250000 Inserts) % 41.65/41.88 % 41.65/41.88 Stopped by limit on insertions % 41.65/41.88 % 41.65/41.88 Model 103 [ 25 29 121294 ] (0.00 seconds, 250000 Inserts) % 41.65/41.88 % 41.65/41.88 Resetting weight limit to 10 after 160 givens. % 41.65/41.88 % 43.48/43.76 % 43.48/43.76 % 43.48/43.76 Changing weight limit from 10 to 9. % 43.48/43.76 % 43.48/43.76 Stopped by limit on insertions % 43.48/43.76 % 43.48/43.76 Stopped by limit on insertions % 43.48/43.76 % 43.48/43.76 Model 104 [ 36 1 108 ] (0.00 seconds, 250000 Inserts) % 43.48/43.76 % 43.48/43.76 Stopped by limit on insertions % 43.48/43.76 % 43.48/43.76 Model 105 [ 23 2 197 ] (0.00 seconds, 250000 Inserts) % 43.48/43.76 % 43.48/43.76 Stopped by limit on insertions % 43.48/43.76 % 43.48/43.76 Model 106 [ 52 2 153 ] (0.00 seconds, 250000 Inserts) % 43.48/43.76 % 43.48/43.76 Stopped by limit on insertions % 43.48/43.76 % 43.48/43.76 Model 107 [ 49 1 103 ] (0.00 seconds, 250000 Inserts) % 43.48/43.76 % 43.48/43.76 Resetting weight limit to 9 after 170 givens. % 43.48/43.76 % 51.38/51.60 % 51.38/51.60 % 51.38/51.60 Changing weight limit from 9 to 10. % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 108 [ 35 1 104 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 109 [ 81 1 104 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 110 [ 32 20 220960 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 111 [ 35 2 104 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 112 [ 47 53 134444 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 113 [ 30 1 188 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 114 [ 79 2 2705 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 115 [ 88 109 172772 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 116 [ 38 2 104 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 117 [ 80 2 767 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Model 118 [ 35 2 209 ] (0.00 seconds, 250000 Inserts) % 51.38/51.60 % 51.38/51.60 Stopped by limit on insertions % 51.38/51.60 % 51.38/51.60 Resetting weight limit to 10 after 200 givens. % 51.38/51.60 % 55.94/56.19 % 55.94/56.19 % 55.94/56.19 Changing weight limit from 10 to 9. % 55.94/56.19 % 55.94/56.19 Stopped by limit on insertions % 55.94/56.19 % 55.94/56.19 Model 119 [ 30 2 142 ] (0.00 seconds, 250000 Inserts) % 55.94/56.19 % 55.94/56.19 Stopped by limit on insertions % 55.94/56.19 % 55.94/56.19 Model 120 [ 106 1 403 ] (0.00 seconds, 250000 Inserts) % 55.94/56.19 % 55.94/56.19 Stopped by limit on insertions % 55.94/56.19 % 55.94/56.19 Model 121 [ 29 22 123753 ] (0.00 seconds, 250000 Inserts) % 55.94/56.19 % 55.94/56.19 Stopped by limit on insertions % 55.94/56.19 % 55.94/56.19 Model 122 [ 31 21 51442 ] (0.00 seconds, 250000 Inserts) % 55.94/56.19 % 55.94/56.19 Stopped by limit on insertions % 55.94/56.19 % 55.94/56.19 Model 123 [ 41 1 113 ] (0.00 seconds, 250000 Inserts) % 55.94/56.19 % 55.94/56.19 Resetting weight limit to 9 after 230 givens. % 55.94/56.19 % 66.60/66.83 % 66.60/66.83 % 66.60/66.83 Changing weight limit from 9 to 8. % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 124 [ 97 2 119 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 125 [ 100 2 132 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 126 [ 33 2 166 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 127 [ 35 2 176 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 128 [ 40 2 111 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 129 [ 40 1 173 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 130 [ 44 2 883 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 131 [ 89 49 91082 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 132 [ 43 31 76869 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Stopped by limit on insertions % 66.60/66.83 % 66.60/66.83 Model 133 [ 99 2 186 ] (0.00 seconds, 250000 Inserts) % 66.60/66.83 % 66.60/66.83 Resetting weight limit to 8 after 265 givens. % 66.60/66.83 % 71.57/71.88 % 71.57/71.88 % 71.57/71.88 Changing weight limit from 8 to 9. % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 134 [ 86 2 1170 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 135 [ 42 11 19498 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 136 [ 88 2 137 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 137 [ 43 2 130 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 138 [ 82 3 2278 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Stopped by limit on insertions % 71.57/71.88 % 71.57/71.88 Model 139 [ 39 2 104 ] (0.00 seconds, 250000 Inserts) % 71.57/71.88 % 71.57/71.88 Resetting weight limit to 9 after 275 givens. % 71.57/71.88 % 72.75/72.98 % 72.75/72.98 % 72.75/72.98 Changing weight limit from 9 to 10. % 72.75/72.98 % 72.75/72.98 Stopped by limit on insertions % 72.75/72.98 % 72.75/72.98 Model 140 [ 45 2 181 ] (0.00 seconds, 250000 Inserts) % 72.75/72.98 % 72.75/72.98 Stopped by limit on insertions % 72.75/72.98 % 72.75/72.98 Model 141 [ 34 2 3943 ] (0.00 seconds, 250000 Inserts) % 72.75/72.98 % 72.75/72.98 Stopped by limit on insertions % 72.75/72.98 % 72.75/72.98 Model 142 [ 36 5 23368 ] (0.00 seconds, 250000 Inserts) % 72.75/72.98 % 72.75/72.98 Resetting weight limit to 10 after 295 givens. % 72.75/72.98 % 74.18/74.46 % 74.18/74.46 % 74.18/74.46 Changing weight limit from 10 to 8. % 74.18/74.46 % 74.18/74.46 Stopped by limit on insertions % 74.18/74.46 % 74.18/74.46 Model 143 [ 59 2 111 ] (0.00 seconds, 250000 Inserts) % 74.18/74.46 % 74.18/74.46 Stopped by limit on insertions % 74.18/74.46 % 74.18/74.46 Model 144 [ 40 6 33549 ] (0.00 seconds, 250000 Inserts) % 74.18/74.46 % 74.18/74.46 Stopped by limit on insertions % 74.18/74.46 % 74.18/74.46 Model 145 [ 33 2 124 ] (0.00 seconds, 250000 Inserts) % 74.18/74.46 % 74.18/74.46 Stopped by limit on insertions % 74.18/74.46 % 74.18/74.46 Model 146 [ 45 2 156 ] (0.00 seconds, 250000 Inserts) % 74.18/74.46 % 74.18/74.46 Resetting weight limit to 8 after 310 givens. % 74.18/74.46 % 79.07/79.37 % 79.07/79.37 % 79.07/79.37 Changing weight limit from 8 to 9. % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Model 147 [ 33 2 561 ] (0.00 seconds, 250000 Inserts) % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Model 148 [ 135 3 401 ] (0.00 seconds, 250000 Inserts) % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Model 149 [ 35 2 109 ] (0.00 seconds, 250000 Inserts) % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Model 150 [ 42 2 192 ] (0.00 seconds, 250000 Inserts) % 79.07/79.37 % 79.07/79.37 Stopped by limit on insertions % 79.07/79.37 % 79.07/79.37 Model 151 [ 89 70 83388 ] (0.00 seconds, 250000 Inserts) % 79.07/79.37 % 79.07/79.37 Resetting weight limit to 9 after 320 givens. % 79.07/79.37 % 80.77/81.03 % 80.77/81.03 % 80.77/81.03 Changing weight limit from 9 to 8. % 80.77/81.03 % 80.77/81.03 Stopped by limit on insertions % 80.77/81.03 % 80.77/81.03 Model 152 [ 33 10 16787 ] (0.00 seconds, 250000 Inserts) % 80.77/81.03 % 80.77/81.03 Stopped by limit on insertions % 80.77/81.03 % 80.77/81.03 Model 153 [ 62 2 936 ] (0.00 seconds, 250000 Inserts) % 80.77/81.03 % 80.77/81.03 Resetting weight limit to 8 after 330 givens. % 80.77/81.03 % 82.07/82.37 % 82.07/82.37 % 82.07/82.37 Changing weight limit from 8 to 9. % 82.07/82.37 % 82.07/82.37 Stopped by limit on insertions % 82.07/82.37 % 82.07/82.37 Model 154 [ 104 45 83704 ] (0.00 seconds, 250000 Inserts) % 82.07/82.37 % 82.07/82.37 Resetting weight limit to 9 after 335 givens. % 82.07/82.37 % 82.67/82.90 % 82.67/82.90 % 82.67/82.90 Changing weight limit from 9 to 8. % 82.67/82.90 % 82.67/82.90 Stopped by limit on insertions % 82.67/82.90 % 82.67/82.90 Model 155 [ 47 31 157824 ] (0.00 seconds, 250000 Inserts) % 82.67/82.90 % 82.67/82.90 Resetting weight limit to 8 after 340 givens. % 82.67/82.90 % 85.29/85.59 % 85.29/85.59 % 85.29/85.59 Changing weight limit from 8 to 9. % 85.29/85.59 % 85.29/85.59 Stopped by limit on insertions % 85.29/85.59 % 85.29/85.59 Model 156 [ 47 2 1121 ] (0.00 seconds, 250000 Inserts) % 85.29/85.59 % 85.29/85.59 Stopped by limit on insertions % 85.29/85.59 % 85.29/85.59 Model 157 [ 37 2 122 ] (0.00 seconds, 250000 Inserts) % 85.29/85.59 % 85.29/85.59 Stopped by limit on insertions % 85.29/85.59 % 85.29/85.59 Model 158 [ 89 7 7186 ] (0.00 seconds, 250000 Inserts) % 85.29/85.59 % 85.29/85.59 Resetting weight limit to 9 after 350 givens. % 85.29/85.59 % 300.01/300.24 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------