%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : FLD057-3 : TPTP v8.1.0. Bugfixed v2.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 : Sat Jul 16 02:27:54 EDT 2022 % Result : Timeout 300.05s 300.24s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : FLD057-3 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.12/0.13 % Command : sos-script %s % 0.12/0.34 % Computer : n017.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.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 6 15:05:46 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.36 ----- Otter 3.2, August 2001 ----- % 0.12/0.36 The process was started by sandbox2 on n017.cluster.edu, % 0.12/0.36 Mon Jun 6 15:05:46 2022 % 0.12/0.36 The command was "./sos". The process ID is 29203. % 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=0, equality=0, symmetry=0, max_lits=5. % 0.12/0.36 % 0.12/0.36 This is a non-Horn set without equality. The strategy % 0.12/0.36 will be ordered hyper_res, ur_res, unit deletion, and % 0.12/0.36 factoring, with satellites in sos and nuclei in usable. % 0.12/0.36 % 0.12/0.36 dependent: set(hyper_res). % 0.12/0.36 dependent: set(factor). % 0.12/0.36 dependent: set(unit_deletion). % 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.19/0.44 % 0.19/0.44 Model 1 (0.00 seconds, 0 Inserts) % 0.19/0.44 % 0.19/0.44 Stopped by limit on number of solutions % 0.19/0.44 % 0.19/0.44 % 0.19/0.44 -------------- Softie stats -------------- % 0.19/0.44 % 0.19/0.44 UPDATE_STOP: 300 % 0.19/0.44 SFINDER_TIME_LIMIT: 2 % 0.19/0.44 SHORT_CLAUSE_CUTOFF: 4 % 0.19/0.44 number of clauses in intial UL: 48 % 0.19/0.44 number of clauses initially in problem: 50 % 0.19/0.44 percentage of clauses intially in UL: 96 % 0.19/0.44 percentage of distinct symbols occuring in initial UL: 100 % 0.19/0.44 percent of all initial clauses that are short: 100 % 0.19/0.44 absolute distinct symbol count: 10 % 0.19/0.44 distinct predicate count: 4 % 0.19/0.44 distinct function count: 4 % 0.19/0.44 distinct constant count: 2 % 0.19/0.44 % 0.19/0.44 ---------- no more Softie stats ---------- % 0.19/0.44 % 0.19/0.44 % 0.19/0.44 % 0.19/0.44 Model 2 (0.00 seconds, 0 Inserts) % 0.19/0.44 % 0.19/0.44 Stopped by limit on number of solutions % 0.19/0.44 % 0.19/0.44 =========== start of search =========== % 5.40/5.58 % 5.40/5.58 % 5.40/5.58 Changing weight limit from 60 to 18. % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 3 [ 1 1 330 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 4 [ 1 9 106697 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 5 [ 1 2 29587 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 6 [ 1 1 265 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 7 [ 1 4 44118 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 8 [ 1 1 337 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 9 [ 1 3 38525 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 10 [ 1 2 913 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 11 [ 1 1 457 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 12 [ 11 2 151 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 13 [ 1 3 25259 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 14 [ 2 2 264 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 15 [ 11 1 100 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 16 [ 3 2 16604 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 17 [ 15 2 134 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 18 [ 14 1 141 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 19 [ 3 11 149195 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 20 [ 18 2 137 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 21 [ 4 1 263 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 22 [ 19 1 254 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 23 [ 5 1 173 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 24 [ 5 1 148 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 25 [ 7 1 405 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 26 [ 6 1 100 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 27 [ 20 1 766 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 28 [ 19 2 137 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 29 [ 6 2 467 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 30 [ 7 2 295 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 31 [ 9 2 29320 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 32 [ 8 1 278 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 33 [ 30 2 386 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 34 [ 9 2 190 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 35 [ 6 2 101 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 36 [ 7 1 192 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 37 [ 25 1 294 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 38 [ 27 2 20184 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Stopped by limit on insertions % 5.40/5.58 % 5.40/5.58 Model 39 [ 11 2 131 ] (0.00 seconds, 250000 Inserts) % 5.40/5.58 % 5.40/5.58 Resetting weight limit to 18 after 60 givens. % 5.40/5.58 % 5.84/6.06 % 5.84/6.06 % 5.84/6.06 Changing weight limit from 18 to 12. % 5.84/6.06 % 5.84/6.06 Stopped by limit on insertions % 5.84/6.06 % 5.84/6.06 Model 40 [ 37 6 177310 ] (0.00 seconds, 250000 Inserts) % 5.84/6.06 % 5.84/6.06 Stopped by limit on insertions % 5.84/6.06 % 5.84/6.06 Model 41 [ 29 1 943 ] (0.00 seconds, 250000 Inserts) % 5.84/6.06 % 5.84/6.06 Stopped by limit on insertions % 5.84/6.06 % 5.84/6.06 Model 42 [ 10 2 35068 ] (0.00 seconds, 250000 Inserts) % 5.84/6.06 % 5.84/6.06 Resetting weight limit to 12 after 65 givens. % 5.84/6.06 % 6.42/6.65 % 6.42/6.65 % 6.42/6.65 Changing weight limit from 12 to 10. % 6.42/6.65 % 6.42/6.65 Stopped by limit on insertions % 6.42/6.65 % 6.42/6.65 Model 43 [ 32 1 175 ] (0.00 seconds, 250000 Inserts) % 6.42/6.65 % 6.42/6.65 Stopped by limit on insertions % 6.42/6.65 % 6.42/6.65 Model 44 [ 16 2 451 ] (0.00 seconds, 250000 Inserts) % 6.42/6.65 % 6.42/6.65 Stopped by limit on insertions % 6.42/6.65 % 6.42/6.65 Model 45 [ 10 2 223 ] (0.00 seconds, 250000 Inserts) % 6.42/6.65 % 6.42/6.65 Stopped by limit on insertions % 6.42/6.65 % 6.42/6.65 Model 46 [ 11 1 255 ] (0.00 seconds, 250000 Inserts) % 6.42/6.65 % 6.42/6.65 Resetting weight limit to 10 after 70 givens. % 6.42/6.65 % 11.24/11.42 % 11.24/11.42 % 11.24/11.42 Changing weight limit from 10 to 11. % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 47 [ 12 2 272 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 48 [ 10 21 88966 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 49 [ 12 1 224 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 50 [ 43 1 261 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 51 [ 14 2 782 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 52 [ 14 1 102 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 53 [ 41 46 177257 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 54 [ 41 2 199 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 55 [ 14 2 754 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 56 [ 50 1 277 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 57 [ 46 8 177464 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 58 [ 42 2 364 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 59 [ 18 2 522 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 60 [ 12 2 900 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 61 [ 49 1 175 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 62 [ 19 3 68744 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Stopped by limit on insertions % 11.24/11.42 % 11.24/11.42 Model 63 [ 25 1 571 ] (0.00 seconds, 250000 Inserts) % 11.24/11.42 % 11.24/11.42 Resetting weight limit to 11 after 95 givens. % 11.24/11.42 % 15.46/15.69 % 15.46/15.69 % 15.46/15.69 Changing weight limit from 11 to 10. % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 64 [ 21 2 560 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 65 [ 20 1 201 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 66 [ 14 2 431 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 67 [ 17 2 271 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 68 [ 46 1 141 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 69 [ 69 2 105 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 70 [ 20 2 185 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 71 [ 59 1 111 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 72 [ 20 2 11183 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 73 [ 36 2 10180 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 74 [ 19 1 128 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 75 [ 21 2 174 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 76 [ 26 10 149771 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Stopped by limit on insertions % 15.46/15.69 % 15.46/15.69 Model 77 [ 65 10 75574 ] (0.00 seconds, 250000 Inserts) % 15.46/15.69 % 15.46/15.69 Resetting weight limit to 10 after 135 givens. % 15.46/15.69 % 17.23/17.49 % 17.23/17.49 % 17.23/17.49 Changing weight limit from 10 to 11. % 17.23/17.49 % 17.23/17.49 Stopped by limit on insertions % 17.23/17.49 % 17.23/17.49 Model 78 [ 47 2 242 ] (0.00 seconds, 250000 Inserts) % 17.23/17.49 % 17.23/17.49 Stopped by limit on insertions % 17.23/17.49 % 17.23/17.49 Model 79 [ 17 21 55483 ] (0.00 seconds, 250000 Inserts) % 17.23/17.49 % 17.23/17.49 Stopped by limit on insertions % 17.23/17.49 % 17.23/17.49 Model 80 [ 59 13 76517 ] (0.00 seconds, 250000 Inserts) % 17.23/17.49 % 17.23/17.49 Stopped by limit on insertions % 17.23/17.49 % 17.23/17.49 Model 81 [ 31 7 92226 ] (0.00 seconds, 250000 Inserts) % 17.23/17.49 % 17.23/17.49 Resetting weight limit to 11 after 140 givens. % 17.23/17.49 % 17.71/17.91 % 17.71/17.91 % 17.71/17.91 Changing weight limit from 11 to 10. % 17.71/17.91 % 17.71/17.91 Stopped by limit on insertions % 17.71/17.91 % 17.71/17.91 Model 82 [ 64 27 187997 ] (0.00 seconds, 250000 Inserts) % 17.71/17.91 % 17.71/17.91 Resetting weight limit to 10 after 145 givens. % 17.71/17.91 % 21.77/21.97 % 21.77/21.97 % 21.77/21.97 Changing weight limit from 10 to 11. % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 83 [ 72 2 410 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 84 [ 69 1 143 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 85 [ 28 18 156983 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 86 [ 57 2 1965 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 87 [ 19 3 11535 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 88 [ 41 2 163 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 89 [ 56 3 3887 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 90 [ 28 2 104 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 91 [ 67 2 269 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 92 [ 31 2 102 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Stopped by limit on insertions % 21.77/21.97 % 21.77/21.97 Model 93 [ 29 7 118961 ] (0.00 seconds, 250000 Inserts) % 21.77/21.97 % 21.77/21.97 Resetting weight limit to 11 after 205 givens. % 21.77/21.97 % 27.92/28.15 % 27.92/28.15 % 27.92/28.15 Changing weight limit from 11 to 12. % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 94 [ 61 2 221 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 95 [ 16 1 158 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 96 [ 30 2 104 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 97 [ 66 29 193064 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 98 [ 23 2 388 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 99 [ 83 6 30880 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 100 [ 77 3 1235 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 101 [ 89 2 293 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 102 [ 36 2 2628 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 103 [ 25 2 139 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 104 [ 78 2 385 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 105 [ 91 3 405 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 106 [ 45 2 260 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Stopped by limit on insertions % 27.92/28.15 % 27.92/28.15 Model 107 [ 34 3 1270 ] (0.00 seconds, 250000 Inserts) % 27.92/28.15 % 27.92/28.15 Resetting weight limit to 12 after 230 givens. % 27.92/28.15 % 29.80/30.00 % 29.80/30.00 % 29.80/30.00 Changing weight limit from 12 to 9. % 29.80/30.00 % 29.80/30.00 Stopped by limit on insertions % 29.80/30.00 % 29.80/30.00 Model 108 [ 96 53 184260 ] (0.00 seconds, 250000 Inserts) % 29.80/30.00 % 29.80/30.00 Stopped by limit on insertions % 29.80/30.00 % 29.80/30.00 Model 109 [ 68 2 423 ] (0.00 seconds, 250000 Inserts) % 29.80/30.00 % 29.80/30.00 Stopped by limit on insertions % 29.80/30.00 % 29.80/30.00 Model 110 [ 70 9 59217 ] (0.00 seconds, 250000 Inserts) % 29.80/30.00 % 29.80/30.00 Stopped by limit on insertions % 29.80/30.00 % 29.80/30.00 Model 111 [ 25 4 12329 ] (0.00 seconds, 250000 Inserts) % 29.80/30.00 % 29.80/30.00 Resetting weight limit to 9 after 235 givens. % 29.80/30.00 % 32.46/32.65 % 32.46/32.65 % 32.46/32.65 Changing weight limit from 9 to 10. % 32.46/32.65 % 32.46/32.65 Stopped by limit on insertions % 32.46/32.65 % 32.46/32.65 Model 112 [ 77 12 74709 ] (0.00 seconds, 250000 Inserts) % 32.46/32.65 % 32.46/32.65 Stopped by limit on insertions % 32.46/32.65 % 32.46/32.65 Model 113 [ 97 3 103 ] (0.00 seconds, 250000 Inserts) % 32.46/32.65 % 32.46/32.65 Stopped by limit on insertions % 32.46/32.65 % 32.46/32.65 Model 114 [ 82 2 348 ] (0.00 seconds, 250000 Inserts) % 32.46/32.65 % 32.46/32.65 Resetting weight limit to 10 after 240 givens. % 32.46/32.65 % 34.95/35.17 % 34.95/35.17 % 34.95/35.17 Changing weight limit from 10 to 11. % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 115 [ 51 23 228536 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 116 [ 90 8 47495 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 117 [ 56 27 219072 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 118 [ 67 2 651 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 119 [ 74 2 115 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Stopped by limit on insertions % 34.95/35.17 % 34.95/35.17 Model 120 [ 16 6 44577 ] (0.00 seconds, 250000 Inserts) % 34.95/35.17 % 34.95/35.17 Resetting weight limit to 11 after 265 givens. % 34.95/35.17 % 35.79/36.04 % 35.79/36.04 % 35.79/36.04 Changing weight limit from 11 to 10. % 35.79/36.04 % 35.79/36.04 Modelling stopped after 300 given clauses and 0.00 seconds % 35.79/36.04 % 35.79/36.04 % 35.79/36.04 Resetting weight limit to 10 after 490 givens. % 35.79/36.04 % 300.05/300.24 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------