%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : FLD012-3 : TPTP v8.1.0. Bugfixed v2.1.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n032.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:35 EDT 2022 % Result : Timeout 300.01s 300.21s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : FLD012-3 : TPTP v8.1.0. Bugfixed v2.1.0. % 0.05/0.11 % Command : sos-script %s % 0.10/0.30 % Computer : n032.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 600 % 0.10/0.30 % DateTime : Mon Jun 6 17:14:49 EDT 2022 % 0.10/0.30 % CPUTime : % 0.15/0.32 ----- Otter 3.2, August 2001 ----- % 0.15/0.32 The process was started by sandbox on n032.cluster.edu, % 0.15/0.32 Mon Jun 6 17:14:49 2022 % 0.15/0.32 The command was "./sos". The process ID is 23785. % 0.15/0.32 % 0.15/0.32 set(prolog_style_variables). % 0.15/0.32 set(auto). % 0.15/0.32 dependent: set(auto1). % 0.15/0.32 dependent: set(process_input). % 0.15/0.32 dependent: clear(print_kept). % 0.15/0.32 dependent: clear(print_new_demod). % 0.15/0.32 dependent: clear(print_back_demod). % 0.15/0.32 dependent: clear(print_back_sub). % 0.15/0.32 dependent: set(control_memory). % 0.15/0.32 dependent: assign(max_mem, 12000). % 0.15/0.32 dependent: assign(pick_given_ratio, 4). % 0.15/0.32 dependent: assign(stats_level, 1). % 0.15/0.32 dependent: assign(pick_semantic_ratio, 3). % 0.15/0.32 dependent: assign(sos_limit, 5000). % 0.15/0.32 dependent: assign(max_weight, 60). % 0.15/0.32 clear(print_given). % 0.15/0.32 % 0.15/0.32 list(usable). % 0.15/0.32 % 0.15/0.32 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5. % 0.15/0.32 % 0.15/0.32 This is a non-Horn set without equality. The strategy % 0.15/0.32 will be ordered hyper_res, ur_res, unit deletion, and % 0.15/0.32 factoring, with satellites in sos and nuclei in usable. % 0.15/0.32 % 0.15/0.32 dependent: set(hyper_res). % 0.15/0.32 dependent: set(factor). % 0.15/0.32 dependent: set(unit_deletion). % 0.15/0.32 % 0.15/0.32 ------------> process usable: % 0.15/0.32 % 0.15/0.32 ------------> process sos: % 0.15/0.32 % 0.15/0.32 ======= end of input processing ======= % 0.15/0.53 % 0.15/0.53 Model 1 (0.00 seconds, 0 Inserts) % 0.15/0.53 % 0.15/0.53 Stopped by limit on number of solutions % 0.15/0.53 % 0.15/0.53 % 0.15/0.53 -------------- Softie stats -------------- % 0.15/0.53 % 0.15/0.53 UPDATE_STOP: 300 % 0.15/0.53 SFINDER_TIME_LIMIT: 2 % 0.15/0.53 SHORT_CLAUSE_CUTOFF: 4 % 0.15/0.53 number of clauses in intial UL: 50 % 0.15/0.53 number of clauses initially in problem: 54 % 0.15/0.53 percentage of clauses intially in UL: 92 % 0.15/0.53 percentage of distinct symbols occuring in initial UL: 100 % 0.15/0.53 percent of all initial clauses that are short: 100 % 0.15/0.53 absolute distinct symbol count: 12 % 0.15/0.53 distinct predicate count: 4 % 0.15/0.53 distinct function count: 4 % 0.15/0.53 distinct constant count: 4 % 0.15/0.53 % 0.15/0.53 ---------- no more Softie stats ---------- % 0.15/0.53 % 0.15/0.53 % 0.15/0.53 % 0.15/0.53 Stopped by limit on insertions % 0.15/0.53 % 0.15/0.53 =========== start of search =========== % 6.46/6.68 % 6.46/6.68 % 6.46/6.68 Changing weight limit from 60 to 12. % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 2 [ 3 2 522 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 3 [ 3 1 479 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 4 [ 5 1 148 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 5 [ 4 2 156 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 6 [ 3 1 486 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 7 [ 3 2 126 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 8 [ 6 2 598 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 9 [ 10 1 165 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 10 [ 3 1 816 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 11 [ 5 2 297 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 12 [ 3 2 355 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 13 [ 3 2 1775 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 14 [ 3 1 119 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 15 [ 3 1 283 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 16 [ 16 1 143 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 17 [ 7 2 536 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 18 [ 19 1 213 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 19 [ 3 2 102 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 20 [ 7 1 420 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 21 [ 23 2 105 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 22 [ 4 2 367 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 23 [ 6 2 6597 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 24 [ 23 1 480 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 25 [ 24 2 191 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 26 [ 6 2 207 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 27 [ 10 4 93314 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 28 [ 6 2 119 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 29 [ 27 1 346 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 30 [ 10 6 158545 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 31 [ 11 1 2187 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 32 [ 14 1 3705 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 33 [ 12 5 60514 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 34 [ 13 3 20810 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 35 [ 33 2 299 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Stopped by limit on insertions % 6.46/6.68 % 6.46/6.68 Model 36 [ 12 1 1019 ] (0.00 seconds, 250000 Inserts) % 6.46/6.68 % 6.46/6.68 Resetting weight limit to 12 after 50 givens. % 6.46/6.68 % 7.72/7.89 % 7.72/7.89 % 7.72/7.89 Changing weight limit from 12 to 10. % 7.72/7.89 % 7.72/7.89 Stopped by limit on insertions % 7.72/7.89 % 7.72/7.89 Model 37 [ 31 1 150 ] (0.00 seconds, 250000 Inserts) % 7.72/7.89 % 7.72/7.89 Stopped by limit on insertions % 7.72/7.89 % 7.72/7.89 Model 38 [ 16 17 190170 ] (0.00 seconds, 250000 Inserts) % 7.72/7.89 % 7.72/7.89 Stopped by limit on insertions % 7.72/7.89 % 7.72/7.89 Model 39 [ 16 1 396 ] (0.00 seconds, 250000 Inserts) % 7.72/7.89 % 7.72/7.89 Stopped by limit on insertions % 7.72/7.89 % 7.72/7.89 Model 40 [ 7 4 25107 ] (0.00 seconds, 250000 Inserts) % 7.72/7.89 % 7.72/7.89 Resetting weight limit to 10 after 55 givens. % 7.72/7.89 % 8.47/8.68 % 8.47/8.68 % 8.47/8.68 Changing weight limit from 10 to 11. % 8.47/8.68 % 8.47/8.68 Stopped by limit on insertions % 8.47/8.68 % 8.47/8.68 Model 41 [ 34 2 432 ] (0.00 seconds, 250000 Inserts) % 8.47/8.68 % 8.47/8.68 Stopped by limit on insertions % 8.47/8.68 % 8.47/8.68 Model 42 [ 15 17 120720 ] (0.00 seconds, 250000 Inserts) % 8.47/8.68 % 8.47/8.68 Resetting weight limit to 11 after 60 givens. % 8.47/8.68 % 10.33/10.56 % 10.33/10.56 % 10.33/10.56 Changing weight limit from 11 to 10. % 10.33/10.56 % 10.33/10.56 Stopped by limit on insertions % 10.33/10.56 % 10.33/10.56 Model 43 [ 41 2 230 ] (0.00 seconds, 250000 Inserts) % 10.33/10.56 % 10.33/10.56 Stopped by limit on insertions % 10.33/10.56 % 10.33/10.56 Model 44 [ 11 2 139 ] (0.00 seconds, 250000 Inserts) % 10.33/10.56 % 10.33/10.56 Stopped by limit on insertions % 10.33/10.56 % 10.33/10.56 Stopped by limit on insertions % 10.33/10.56 % 10.33/10.56 Model 45 [ 25 36 225485 ] (0.00 seconds, 250000 Inserts) % 10.33/10.56 % 10.33/10.56 Stopped by limit on insertions % 10.33/10.56 % 10.33/10.56 Model 46 [ 13 2 664 ] (0.00 seconds, 250000 Inserts) % 10.33/10.56 % 10.33/10.56 Resetting weight limit to 10 after 65 givens. % 10.33/10.56 % 24.12/24.31 % 24.12/24.31 % 24.12/24.31 Changing weight limit from 10 to 8. % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 47 [ 11 2 3146 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 48 [ 16 1 641 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 49 [ 41 2 269 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 50 [ 15 2 711 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 51 [ 18 33 232642 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 52 [ 22 18 243626 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 53 [ 49 2 144 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 54 [ 20 5 121976 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 55 [ 53 2 187 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 56 [ 52 11 33043 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 57 [ 14 2 5119 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 58 [ 17 1 319 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 59 [ 24 19 104390 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 60 [ 13 1 1027 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 61 [ 59 2 7008 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 62 [ 18 6 46931 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 63 [ 18 2 7915 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 64 [ 28 1 290 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 65 [ 60 1 133 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 66 [ 56 2 125 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 67 [ 58 33 126346 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 68 [ 49 1 117 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 69 [ 20 2 545 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 70 [ 56 49 128086 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 71 [ 28 2 602 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 72 [ 28 13 112396 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 73 [ 16 2 3040 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 74 [ 39 9 34152 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 75 [ 22 2 435 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 76 [ 76 4 59222 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 77 [ 66 2 407 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 78 [ 77 1 332 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Stopped by limit on insertions % 24.12/24.31 % 24.12/24.31 Model 79 [ 22 2 581 ] (0.00 seconds, 250000 Inserts) % 24.12/24.31 % 24.12/24.31 Resetting weight limit to 8 after 125 givens. % 24.12/24.31 % 25.07/25.27 % 25.07/25.27 % 25.07/25.27 Changing weight limit from 8 to 9. % 25.07/25.27 % 25.07/25.27 Stopped by limit on insertions % 25.07/25.27 % 25.07/25.27 Model 80 [ 64 2 1690 ] (0.00 seconds, 250000 Inserts) % 25.07/25.27 % 25.07/25.27 Stopped by limit on insertions % 25.07/25.27 % 25.07/25.27 Model 81 [ 30 3 57777 ] (0.00 seconds, 250000 Inserts) % 25.07/25.27 % 25.07/25.27 Resetting weight limit to 9 after 130 givens. % 25.07/25.27 % 37.00/37.17 % 37.00/37.17 % 37.00/37.17 Changing weight limit from 9 to 8. % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 82 [ 67 1 172 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 83 [ 27 47 228563 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 84 [ 15 3 12826 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 85 [ 66 2 410 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 86 [ 37 1 187 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 87 [ 29 49 231279 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 88 [ 81 48 129963 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 89 [ 81 2 160 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 90 [ 41 50 179307 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 91 [ 66 101 240025 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 92 [ 86 2 254 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 93 [ 20 2 297 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 94 [ 20 2 294 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 95 [ 25 2 386 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 96 [ 35 14 112158 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 97 [ 26 31 122327 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 98 [ 22 2 1197 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Stopped by limit on insertions % 37.00/37.17 % 37.00/37.17 Model 99 [ 23 13 33082 ] (0.00 seconds, 250000 Inserts) % 37.00/37.17 % 37.00/37.17 Resetting weight limit to 8 after 185 givens. % 37.00/37.17 % 41.80/41.99 % 41.80/41.99 % 41.80/41.99 Changing weight limit from 8 to 9. % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 100 [ 82 2 490 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 101 [ 24 3 890 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 102 [ 79 5 15098 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 103 [ 85 2 111 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 104 [ 44 2 462 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 105 [ 39 4 32231 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 106 [ 86 3 2490 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Stopped by limit on insertions % 41.80/41.99 % 41.80/41.99 Model 107 [ 40 75 248243 ] (0.00 seconds, 250000 Inserts) % 41.80/41.99 % 41.80/41.99 Resetting weight limit to 9 after 200 givens. % 41.80/41.99 % 60.76/61.00 % 60.76/61.00 % 60.76/61.00 Changing weight limit from 9 to 10. % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 108 [ 92 63 117200 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 109 [ 109 2 282 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 110 [ 34 21 81478 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 111 [ 36 1 168 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 112 [ 35 2 573 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 113 [ 78 75 140163 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 114 [ 31 33 182477 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 115 [ 79 2 1815 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 116 [ 38 53 207131 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 117 [ 35 3 11868 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 118 [ 85 7 9444 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 119 [ 43 96 181320 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 120 [ 38 2 371 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 121 [ 93 2 723 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 122 [ 23 2 511 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 123 [ 32 13 134337 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 124 [ 102 2 138 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 125 [ 118 14 174442 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 126 [ 42 3 3964 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 127 [ 122 2 114 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Stopped by limit on insertions % 60.76/61.00 % 60.76/61.00 Model 128 [ 49 6 12140 ] (0.00 seconds, 250000 Inserts) % 60.76/61.00 % 60.76/61.00 Resetting weight limit to 10 after 260 givens. % 60.76/61.00 % 67.54/67.75 % 67.54/67.75 % 67.54/67.75 Changing weight limit from 10 to 9. % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 129 [ 54 78 216290 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 130 [ 60 2 184 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 131 [ 45 2 2177 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 132 [ 38 2 625 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 133 [ 96 3 2039 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 134 [ 41 3 2531 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Stopped by limit on insertions % 67.54/67.75 % 67.54/67.75 Model 135 [ 93 3 386 ] (0.00 seconds, 250000 Inserts) % 67.54/67.75 % 67.54/67.75 Resetting weight limit to 9 after 275 givens. % 67.54/67.75 % 68.10/68.32 % 68.10/68.32 % 68.10/68.32 Changing weight limit from 9 to 10. % 68.10/68.32 % 68.10/68.32 Stopped by limit on insertions % 68.10/68.32 % 68.10/68.32 Model 136 [ 25 5 8905 ] (0.00 seconds, 250000 Inserts) % 68.10/68.32 % 68.10/68.32 Resetting weight limit to 10 after 280 givens. % 68.10/68.32 % 73.97/74.15 % 73.97/74.15 % 73.97/74.15 Changing weight limit from 10 to 11. % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 137 [ 42 22 71479 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 138 [ 36 3 15976 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 139 [ 30 2 138 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 140 [ 42 2 184 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 141 [ 66 72 209021 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 142 [ 107 35 71145 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Stopped by limit on insertions % 73.97/74.15 % 73.97/74.15 Model 143 [ 50 23 47699 ] (0.00 seconds, 250000 Inserts) % 73.97/74.15 % 73.97/74.15 Resetting weight limit to 11 after 345 givens. % 73.97/74.15 % 219.32/219.50 % 219.32/219.50 % 219.32/219.50 Changing weight limit from 11 to 10. % 219.32/219.50 % 219.32/219.50 Stopped by limit on insertions % 219.32/219.50 % 219.32/219.50 Model 144 [ 31 3 2957 ] (0.00 seconds, 250000 Inserts) % 219.32/219.50 % 219.32/219.50 Stopped by limit on insertions % 219.32/219.50 % 219.32/219.50 Model 145 [ 118 8 5941 ] (0.00 seconds, 250000 Inserts) % 219.32/219.50 % 219.32/219.50 Modelling stopped after 300 given clauses and 0.00 seconds % 219.32/219.50 % 219.32/219.50 % 219.32/219.50 Resetting weight limit to 10 after 5095 givens. % 219.32/219.50 % 300.01/300.21 Wow, sos-wrapper got a signal XCPU %------------------------------------------------------------------------------