%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NLP180-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n009.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 05:24:28 EDT 2022
% Result : Unknown 157.42s 157.61s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NLP180-1 : TPTP v8.1.0. Released v2.4.0.
% 0.12/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n009.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jul 1 04:31:22 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.36
% 0.13/0.36
% 0.13/0.36 WARNING, multiple arity: set/1, set/2.
% 0.13/0.36
% 0.13/0.37 ----- Otter 3.2, August 2001 -----
% 0.13/0.37 The process was started by sandbox on n009.cluster.edu,
% 0.13/0.37 Fri Jul 1 04:31:22 2022
% 0.13/0.37 The command was "./sos". The process ID is 10516.
% 0.13/0.37
% 0.13/0.37 set(prolog_style_variables).
% 0.13/0.37 set(auto).
% 0.13/0.37 dependent: set(auto1).
% 0.13/0.37 dependent: set(process_input).
% 0.13/0.37 dependent: clear(print_kept).
% 0.13/0.37 dependent: clear(print_new_demod).
% 0.13/0.37 dependent: clear(print_back_demod).
% 0.13/0.37 dependent: clear(print_back_sub).
% 0.13/0.37 dependent: set(control_memory).
% 0.13/0.37 dependent: assign(max_mem, 12000).
% 0.13/0.37 dependent: assign(pick_given_ratio, 4).
% 0.13/0.37 dependent: assign(stats_level, 1).
% 0.13/0.37 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.37 dependent: assign(sos_limit, 5000).
% 0.13/0.37 dependent: assign(max_weight, 60).
% 0.13/0.37 clear(print_given).
% 0.13/0.37
% 0.13/0.37 list(usable).
% 0.13/0.37
% 0.13/0.37 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=28.
% 0.13/0.37
% 0.13/0.37 This ia a non-Horn set with equality. The strategy will be
% 0.13/0.37 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.13/0.37 unit deletion, with positive clauses in sos and nonpositive
% 0.13/0.37 clauses in usable.
% 0.13/0.37
% 0.13/0.37 dependent: set(knuth_bendix).
% 0.13/0.37 dependent: set(para_from).
% 0.13/0.37 dependent: set(para_into).
% 0.13/0.37 dependent: clear(para_from_right).
% 0.13/0.37 dependent: clear(para_into_right).
% 0.13/0.37 dependent: set(para_from_vars).
% 0.13/0.37 dependent: set(eq_units_both_ways).
% 0.13/0.37 dependent: set(dynamic_demod_all).
% 0.13/0.37 dependent: set(dynamic_demod).
% 0.13/0.37 dependent: set(order_eq).
% 0.13/0.37 dependent: set(back_demod).
% 0.13/0.37 dependent: set(lrpo).
% 0.13/0.37 dependent: set(hyper_res).
% 0.13/0.37 dependent: set(unit_deletion).
% 0.13/0.37 dependent: set(factor).
% 0.13/0.37
% 0.13/0.37 ------------> process usable:
% 0.13/0.37 85 back subsumes 84.
% 0.13/0.37
% 0.13/0.37 ------------> process sos:
% 0.13/0.37 Following clause subsumed by 113 during input processing: 0 [copy,113,flip.1] {-} A=A.
% 0.13/0.37 113 back subsumes 86.
% 0.13/0.37 113 back subsumes 85.
% 0.13/0.37 113 back subsumes 83.
% 0.13/0.37
% 0.13/0.37 ======= end of input processing =======
% 0.19/0.48
% 0.19/0.48 Model 1 (0.00 seconds, 0 Inserts)
% 0.19/0.48
% 0.19/0.48 Stopped by limit on number of solutions
% 0.19/0.48
% 0.19/0.48
% 0.19/0.48 -------------- Softie stats --------------
% 0.19/0.48
% 0.19/0.48 UPDATE_STOP: 300
% 0.19/0.48 SFINDER_TIME_LIMIT: 2
% 0.19/0.48 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.48 number of clauses in intial UL: 82
% 0.19/0.48 number of clauses initially in problem: 109
% 0.19/0.48 percentage of clauses intially in UL: 75
% 0.19/0.48 percentage of distinct symbols occuring in initial UL: 91
% 0.19/0.48 percent of all initial clauses that are short: 99
% 0.19/0.48 absolute distinct symbol count: 87
% 0.19/0.48 distinct predicate count: 70
% 0.19/0.48 distinct function count: 10
% 0.19/0.48 distinct constant count: 7
% 0.19/0.48
% 0.19/0.48 ---------- no more Softie stats ----------
% 0.19/0.48
% 0.19/0.48
% 0.19/0.48
% 0.19/0.48 =========== start of search ===========
% 12.04/12.24
% 12.04/12.24 Model 2 (0.00 seconds, 0 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Model 3 (0.00 seconds, 0 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Model 4 (0.00 seconds, 0 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 5 [ 3 10 69388 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Model 6 (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Model 7 (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Model 8 (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on number of solutions
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 9 [ 2 8 51405 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 10 [ 6 5 38292 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 11 [ 2 8 38270 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 12 [ 4 5 30685 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 13 [ 6 4 24008 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 14 [ 8 9 69643 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 15 [ 7 4 15859 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 16 [ 3 7 20350 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 17 [ 3 6 20525 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 18 [ 4 7 33550 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 19 [ 8 6 29345 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 20 [ 7 8 52390 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 21 [ 10 5 26621 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 22 [ 11 5 29639 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 23 [ 4 8 34388 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 24 [ 9 3 1221 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 25 [ 13 7 41622 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 26 [ 11 7 35313 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 27 [ 14 8 57566 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 28 [ 10 6 39076 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 29 [ 16 3 14070 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 30 [ 9 11 38940 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 31 [ 12 5 36866 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 32 [ 15 6 38946 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 33 [ 14 5 37495 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 34 [ 13 3 13329 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 35 [ 22 7 50665 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 36 [ 19 1 1188 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 37 [ 13 4 25336 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 38 [ 16 2 12913 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 39 [ 16 4 17908 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 40 [ 19 7 47527 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 41 [ 25 5 27793 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 42 [ 21 4 23864 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 43 [ 18 7 36627 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 44 [ 20 2 17436 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 45 [ 21 7 47261 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 46 [ 20 4 25581 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 47 [ 27 5 31427 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 12.04/12.24 Model 48 [ 26 9 42110 ] (0.00 seconds, 250000 Inserts)
% 12.04/12.24
% 12.04/12.24 Stopped by limit on insertions
% 12.04/12.24
% 41.74/41.95 Model 49 [ 33 3 18211 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 50 [ 46 1 1188 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 51 [ 36 5 26312 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 52 [ 31 10 67209 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 53 [ 23 4 18518 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 54 [ 69 2 6451 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 55 [ 38 10 62386 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 56 [ 42 2 1186 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 57 [ 33 8 57233 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 58 [ 44 5 27233 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 59 [ 27 4 28561 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 60 [ 43 4 29911 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 61 [ 31 7 47119 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 62 [ 63 4 18994 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 63 [ 53 6 39348 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 64 [ 51 6 30830 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 65 [ 33 5 16611 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 66 [ 58 4 30110 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 67 [ 25 6 33399 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 68 [ 74 4 18197 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 69 [ 87 4 14884 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 70 [ 74 7 43447 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 71 [ 66 4 14069 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 72 [ 44 6 32191 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 73 [ 47 6 30236 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 74 [ 87 6 35553 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 75 [ 55 4 17320 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 76 [ 72 5 30253 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 77 [ 46 8 35725 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 78 [ 78 3 18719 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 79 [ 98 1 1183 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 80 [ 42 7 40511 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 81 [ 70 3 16623 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 82 [ 47 4 22854 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 83 [ 99 4 25499 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 84 [ 78 5 27522 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 85 [ 86 4 22707 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 86 [ 110 4 14590 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 87 [ 97 5 25647 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 88 [ 89 5 22588 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 89 [ 105 6 27282 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 90 [ 94 1 1206 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 91 [ 112 8 45921 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 92 [ 99 3 12603 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 93 [ 103 8 41672 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 41.74/41.95 Model 94 [ 75 4 24636 ] (0.00 seconds, 250000 Inserts)
% 41.74/41.95
% 41.74/41.95 Stopped by limit on insertions
% 41.74/41.95
% 66.36/66.59 Model 95 [ 116 6 28538 ] (0.00 seconds, 250000 In
% 66.36/66.59
% 66.36/66.59 Changing weight limit from 60 to 39.
% 66.36/66.59 serts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 96 [ 98 9 46405 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 97 [ 86 3 13347 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 98 [ 77 4 12108 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 99 [ 55 9 49195 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 100 [ 131 6 29849 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 101 [ 113 8 40326 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 102 [ 114 2 1182 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 103 [ 85 7 34164 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 104 [ 115 5 23652 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 105 [ 90 5 23042 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 106 [ 102 8 44871 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 107 [ 83 7 35352 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 108 [ 121 5 15631 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Stopped by limit on insertions
% 66.36/66.59
% 66.36/66.59 Model 109 [ 132 7 31682 ] (0.00 seconds, 250000 Inserts)
% 66.36/66.59
% 66.36/66.59 Resetting weight limit to 39 after 145 givens.
% 66.36/66.59
% 75.40/75.60
% 75.40/75.60
% 75.40/75.60 Changing weight limit from 39 to 40.
% 75.40/75.60
% 75.40/75.60 Stopped by limit on insertions
% 75.40/75.60
% 75.40/75.60 Model 110 [ 159 7 35766 ] (0.00 seconds, 250000 Inserts)
% 75.40/75.60
% 75.40/75.60 Stopped by limit on insertions
% 75.40/75.60
% 75.40/75.60 Model 111 [ 130 3 1193 ] (0.00 seconds, 250000 Inserts)
% 75.40/75.60
% 75.40/75.60 Stopped by limit on insertions
% 75.40/75.60
% 75.40/75.60 Model 112 [ 142 6 20908 ] (0.00 seconds, 250000 Inserts)
% 75.40/75.60
% 75.40/75.60 Resetting weight limit to 40 after 150 givens.
% 75.40/75.60
% 75.51/75.72
% 75.51/75.72
% 75.51/75.72 Changing weight limit from 40 to 41.
% 75.51/75.72
% 75.51/75.72 Resetting weight limit to 41 after 155 givens.
% 75.51/75.72
% 75.63/75.86
% 75.63/75.86
% 75.63/75.86 Changing weight limit from 41 to 42.
% 75.63/75.86
% 75.63/75.86 Resetting weight limit to 42 after 160 givens.
% 75.63/75.86
% 75.89/76.10
% 75.89/76.10
% 75.89/76.10 Changing weight limit from 42 to 43.
% 75.89/76.10
% 75.89/76.10 Resetting weight limit to 43 after 165 givens.
% 75.89/76.10
% 84.59/84.82
% 84.59/84.82
% 84.59/84.82 Changing weight limit from 43 to 44.
% 84.59/84.82
% 84.59/84.82 Stopped by limit on insertions
% 84.59/84.82
% 84.59/84.82 Model 113 [ 138 9 30477 ] (0.00 seconds, 250000 Inserts)
% 84.59/84.82
% 84.59/84.82 Stopped by limit on insertions
% 84.59/84.82
% 84.59/84.82 Model 114 [ 221 12 36619 ] (0.00 seconds, 250000 Inserts)
% 84.59/84.82
% 84.59/84.82 Stopped by limit on insertions
% 84.59/84.82
% 84.59/84.82 Model 115 [ 224 10 27790 ] (0.00 seconds, 250000 Inserts)
% 84.59/84.82
% 84.59/84.82 Resetting weight limit to 44 after 170 givens.
% 84.59/84.82
% 98.54/98.76
% 98.54/98.76
% 98.54/98.76 Changing weight limit from 44 to 43.
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 116 [ 214 8 13277 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 117 [ 102 10 29266 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 118 [ 198 8 12873 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 119 [ 150 9 19498 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 120 [ 249 12 25651 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Stopped by limit on insertions
% 98.54/98.76
% 98.54/98.76 Model 121 [ 206 9 19906 ] (0.00 seconds, 250000 Inserts)
% 98.54/98.76
% 98.54/98.76 Resetting weight limit to 43 after 180 givens.
% 98.54/98.76
% 113.10/113.32
% 113.10/113.32
% 113.10/113.32 Changing weight limit from 43 to 39.
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 122 [ 288 12 36382 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 123 [ 194 8 12228 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 124 [ 205 10 29064 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 125 [ 212 8 9835 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 126 [ 183 10 18706 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 127 [ 293 15 46384 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 128 [ 204 9 15279 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 129 [ 220 8 13141 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Stopped by limit on insertions
% 113.10/113.32
% 113.10/113.32 Model 130 [ 118 17 68609 ] (0.00 seconds, 250000 Inserts)
% 113.10/113.32
% 113.10/113.32 Resetting weight limit to 39 after 195 givens.
% 113.10/113.32
% 119.23/119.48
% 119.23/119.48
% 119.23/119.48 Changing weight limit from 39 to 33.
% 119.23/119.48
% 119.23/119.48 Resetting weight limit to 33 after 310 givens.
% 119.23/119.48
% 119.69/119.88
% 119.69/119.88
% 119.69/119.88 Changing weight limit from 33 to 32.
% 119.69/119.88
% 119.69/119.88 Resetting weight limit to 32 after 315 givens.
% 119.69/119.88
% 120.00/120.21
% 120.00/120.21
% 120.00/120.21 Changing weight limit from 32 to 31.
% 120.00/120.21
% 120.00/120.21 Resetting weight limit to 31 after 320 givens.
% 120.00/120.21
% 120.33/120.61
% 120.33/120.61
% 120.33/120.61 Changing weight limit from 31 to 30.
% 120.33/120.61
% 120.33/120.61 Resetting weight limit to 30 after 325 givens.
% 120.33/120.61
% 121.11/121.38
% 121.11/121.38
% 121.11/121.38 Changing weight limit from 30 to 29.
% 121.11/121.38
% 121.11/121.38 Resetting weight limit to 29 after 335 givens.
% 121.11/121.38
% 121.52/121.80
% 121.52/121.80
% 121.52/121.80 Changing weight limit from 29 to 28.
% 121.52/121.80
% 121.52/121.80 Resetting weight limit to 28 after 345 givens.
% 121.52/121.80
% 121.90/122.16
% 121.90/122.16
% 121.90/122.16 Changing weight limit from 28 to 27.
% 121.90/122.16
% 121.90/122.16 Resetting weight limit to 27 after 355 givens.
% 121.90/122.16
% 122.11/122.34
% 122.11/122.34
% 122.11/122.34 Changing weight limit from 27 to 26.
% 122.11/122.34
% 122.11/122.34 Resetting weight limit to 26 after 360 givens.
% 122.11/122.34
% 125.22/125.45
% 125.22/125.45
% 125.22/125.45 Changing weight limit from 26 to 25.
% 125.22/125.45
% 125.22/125.45 Modelling stopped after 300 given clauses and 0.00 seconds
% 125.22/125.45
% 125.22/125.45
% 125.22/125.45 Resetting weight limit to 25 after 450 givens.
% 125.22/125.45
% 125.93/126.16
% 125.93/126.16
% 125.93/126.16 Changing weight limit from 25 to 24.
% 125.93/126.16
% 125.93/126.16 Resetting weight limit to 24 after 475 givens.
% 125.93/126.16
% 126.70/126.92
% 126.70/126.92
% 126.70/126.92 Changing weight limit from 24 to 23.
% 126.70/126.92
% 126.70/126.92 Resetting weight limit to 23 after 500 givens.
% 126.70/126.92
% 127.13/127.34
% 127.13/127.34
% 127.13/127.34 Changing weight limit from 23 to 20.
% 127.13/127.34
% 127.13/127.34 Resetting weight limit to 20 after 515 givens.
% 127.13/127.34
% 127.51/127.74
% 127.51/127.74
% 127.51/127.74 Changing weight limit from 20 to 19.
% 127.51/127.74
% 127.51/127.74 Resetting weight limit to 19 after 525 givens.
% 127.51/127.74
% 142.62/142.83
% 142.62/142.83
% 142.62/142.83 Changing weight limit from 19 to 18.
% 142.62/142.83
% 142.62/142.83 Resetting weight limit to 18 after 1140 givens.
% 142.62/142.83
% 144.21/144.44
% 144.21/144.44
% 144.21/144.44 Changing weight limit from 18 to 17.
% 144.21/144.44
% 144.21/144.44 Resetting weight limit to 17 after 1160 givens.
% 144.21/144.44
% 157.41/157.60 in(skc7,skf12(skf24(skc8,skc7),skc7,A),A).
% 157.41/157.60
% 157.41/157.60 ------------- memory usage ------------
% 157.41/157.60 365 mallocs of 32700 bytes each, 11655.8 K.
% 157.41/157.60 type (bytes each) gets frees in use avail bytes
% 157.41/157.60 sym_ent ( 304) 197 0 197 0 58.5 K
% 157.41/157.60 term ( 32) 39649832 39618603 31229 1056 1008.9 K
% 157.41/157.60 rel ( 40) 30507739 30430999 76740 1079 3039.8 K
% 157.41/157.60 term_ptr ( 16) 2506382 2276731 229651 2015 3619.8 K
% 157.41/157.60 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 157.41/157.60 fpa_head ( 24) 8330 3693 4637 1 108.7 K
% 157.41/157.60 fpa_tree ( 56) 292992 292992 0 97 5.3 K
% 157.41/157.60 context (1288) 4319332 4319332 0 29 36.5 K
% 157.41/157.60 trail ( 24) 7594487 7594487 0 17 0.4 K
% 157.41/157.60 imd_tree ( 32) 12 0 12 0 0.4 K
% 157.41/157.60 imd_pos (4024) 19530 19530 0 1 3.9 K
% 157.41/157.60 is_tree ( 24) 22662 18368 4294 1665 139.7 K
% 157.41/157.60 is_pos (2424) 39315493 39315493 0 9 21.3 K
% 157.41/157.60 fsub_pos ( 16) 5576781 5576781 0 1 0.0 K
% 157.41/157.60 literal ( 32) 9123693 9093938 29755 390 942.0 K
% 157.41/157.60 clause ( 88) 1572933 1563478 9455 98 821.0 K
% 157.41/157.60 list ( 272) 10 3 7 1 2.1 K
% 157.41/157.60 clash_nd ( 80) 8418 8418 0 27 2.1 K
% 157.41/157.60 clause_ptr ( 16) 60055 50709 9346 97 147.5 K
% 157.41/157.60 int_ptr ( 16) 9721021 9622361 98660 1023 1557.5 K
% 157.41/157.60 ci_ptr ( 24) 0 0 0 0 0.0 K
% 157.41/157.60 link_node ( 120) 0 0 0 0 0.0 K
% 157.41/157.60 ans_lit_node( 24) 0 0 0 0 0.0 K
% 157.41/157.60 formula_box( 168) 0 0 0 0 0.0 K
% 157.41/157.60 formula( 40) 0 0 0 0 0.0 K
% 157.41/157.60 formula_ptr( 16) 0 0 0 0 0.0 K
% 157.41/157.60 cl_attribute( 24) 0 0 0 0 0.0 K
% 157.41/157.60
% 157.41/157.60 ********** is_delete, can't find end.
% 157.41/157.60 demod time 0.00
% 157.41/157.60 back subsume 0.00
% 157.41/157.60 factor time 0.00
% 157.41/157.60 FINDER time 0.00
% 157.41/157.60 unindex time 0.00
% 157.41/157.60
% 157.41/157.60 ----------- soft-scott stats ----------
% 157.41/157.60
% 157.41/157.60 true clauses given 1172 (20.8%)
% 157.41/157.60 false clauses given 4468
% 157.41/157.60
% 157.41/157.60 FALSE TRUE
% 157.41/157.60 12 4 671
% 157.41/157.60 13 0 513
% 157.41/157.60 14 0 50
% 157.41/157.60 15 14 1267
% 157.41/157.60 17 1966 0
% 157.41/157.60 tot: 1984 2501 (55.8% true)
% 157.41/157.60
% 157.41/157.60
% 157.41/157.60 Model 130 [ 118 17 68609 ] (0.00 seconds, 250000 Inserts)
% 157.41/157.60
% 157.41/157.60 Forward subsumption counts, subsumer:number_subsumed.
% 157.41/157.60 1:9063 2:0 3:0 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 157.41/157.60 11:0 12:0 13:0 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 157.41/157.60 21:0 22:0 23:0 24:0 25:0 26:0 27:0 28:0 29:0 30:0
% 157.41/157.60 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:0 40:0
% 157.41/157.60 41:0 42:0 43:0 44:0 45:0 46:0 47:0 48:0 49:0 50:0
% 157.41/157.60 51:0 52:0 53:0 54:0 55:0 56:0 57:0 58:0 59:0 60:0
% 157.41/157.60 61:0 62:0 63:0 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 157.41/157.60 71:0 72:0 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 157.41/157.60 81:0 82:0 83:0 84:0 85:0 86:1 87:1833 88:1338 89:989 90:1224
% 157.41/157.60 91:529 92:798 93:1118 94:1073 95:1008 96:701 97:930 98:789 99:466
% 157.41/157.60 All others: 145212.
% 157.41/157.60
% 157.41/157.60 ********** ABNORMAL END **********
% 157.41/157.60
% 157.41/157.60 ********** is_delete, can't find end.
%------------------------------------------------------------------------------