%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NLP186-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n008.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:31 EDT 2022
% Result : Unknown 220.11s 220.34s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP186-1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : sos-script %s
% 0.12/0.34 % Computer : n008.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 : Fri Jul 1 09:41:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.36
% 0.12/0.36
% 0.12/0.36 WARNING, multiple arity: set/1, set/2.
% 0.12/0.36
% 0.12/0.37 ----- Otter 3.2, August 2001 -----
% 0.12/0.37 The process was started by sandbox2 on n008.cluster.edu,
% 0.12/0.37 Fri Jul 1 09:41:08 2022
% 0.12/0.37 The command was "./sos". The process ID is 9316.
% 0.12/0.37
% 0.12/0.37 set(prolog_style_variables).
% 0.12/0.37 set(auto).
% 0.12/0.37 dependent: set(auto1).
% 0.12/0.37 dependent: set(process_input).
% 0.12/0.37 dependent: clear(print_kept).
% 0.12/0.37 dependent: clear(print_new_demod).
% 0.12/0.37 dependent: clear(print_back_demod).
% 0.12/0.37 dependent: clear(print_back_sub).
% 0.12/0.37 dependent: set(control_memory).
% 0.12/0.37 dependent: assign(max_mem, 12000).
% 0.12/0.37 dependent: assign(pick_given_ratio, 4).
% 0.12/0.37 dependent: assign(stats_level, 1).
% 0.12/0.37 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.37 dependent: assign(sos_limit, 5000).
% 0.12/0.37 dependent: assign(max_weight, 60).
% 0.12/0.37 clear(print_given).
% 0.12/0.37
% 0.12/0.37 list(usable).
% 0.12/0.37
% 0.12/0.37 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=28.
% 0.12/0.37
% 0.12/0.37 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.37 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.37 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.37 clauses in usable.
% 0.12/0.37
% 0.12/0.37 dependent: set(knuth_bendix).
% 0.12/0.37 dependent: set(para_from).
% 0.12/0.37 dependent: set(para_into).
% 0.12/0.37 dependent: clear(para_from_right).
% 0.12/0.37 dependent: clear(para_into_right).
% 0.12/0.37 dependent: set(para_from_vars).
% 0.12/0.37 dependent: set(eq_units_both_ways).
% 0.12/0.37 dependent: set(dynamic_demod_all).
% 0.12/0.37 dependent: set(dynamic_demod).
% 0.12/0.37 dependent: set(order_eq).
% 0.12/0.37 dependent: set(back_demod).
% 0.12/0.37 dependent: set(lrpo).
% 0.12/0.37 dependent: set(hyper_res).
% 0.12/0.37 dependent: set(unit_deletion).
% 0.12/0.37 dependent: set(factor).
% 0.12/0.37
% 0.12/0.37 ------------> process usable:
% 0.12/0.37 85 back subsumes 84.
% 0.12/0.37
% 0.12/0.37 ------------> process sos:
% 0.12/0.37 Following clause subsumed by 113 during input processing: 0 [copy,113,flip.1] {-} A=A.
% 0.12/0.37 113 back subsumes 86.
% 0.12/0.37 113 back subsumes 85.
% 0.12/0.37 113 back subsumes 83.
% 0.12/0.37
% 0.12/0.37 ======= end of input processing =======
% 0.19/0.47
% 0.19/0.47 Model 1 (0.00 seconds, 0 Inserts)
% 0.19/0.47
% 0.19/0.47 Stopped by limit on number of solutions
% 0.19/0.47
% 0.19/0.47
% 0.19/0.47 -------------- Softie stats --------------
% 0.19/0.47
% 0.19/0.47 UPDATE_STOP: 300
% 0.19/0.47 SFINDER_TIME_LIMIT: 2
% 0.19/0.47 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.47 number of clauses in intial UL: 82
% 0.19/0.47 number of clauses initially in problem: 109
% 0.19/0.47 percentage of clauses intially in UL: 75
% 0.19/0.47 percentage of distinct symbols occuring in initial UL: 91
% 0.19/0.47 percent of all initial clauses that are short: 99
% 0.19/0.47 absolute distinct symbol count: 87
% 0.19/0.47 distinct predicate count: 70
% 0.19/0.47 distinct function count: 10
% 0.19/0.47 distinct constant count: 7
% 0.19/0.47
% 0.19/0.47 ---------- no more Softie stats ----------
% 0.19/0.47
% 0.19/0.47
% 0.19/0.47
% 0.19/0.47 =========== start of search ===========
% 12.72/12.91
% 12.72/12.91 Model 2 (0.00 seconds, 0 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on number of solutions
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 3 [ 1 7 35502 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Model 4 (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on number of solutions
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 5 [ 3 8 68331 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 6 [ 2 6 41730 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 7 [ 3 3 13365 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 8 [ 4 3 14607 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 9 [ 3 7 39289 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 10 [ 4 8 54347 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 11 [ 6 4 27640 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 12 [ 3 9 52853 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 13 [ 6 6 38779 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 14 [ 6 6 30566 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 15 [ 8 3 11548 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 16 [ 3 5 20329 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 17 [ 7 4 26003 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 18 [ 7 11 63497 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 19 [ 6 11 79274 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 20 [ 4 9 49015 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 21 [ 4 9 44384 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 22 [ 11 4 26038 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 23 [ 13 5 41977 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 24 [ 13 6 40314 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 25 [ 13 4 17444 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 26 [ 8 11 36531 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 27 [ 14 6 35909 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 28 [ 14 1 1201 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 29 [ 13 5 38115 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 30 [ 14 1 1189 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 31 [ 10 8 23320 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 32 [ 15 1 1185 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 33 [ 18 4 25494 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 34 [ 19 4 25686 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 35 [ 21 8 59440 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 36 [ 24 8 55136 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 37 [ 20 5 26826 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 38 [ 24 8 51793 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 39 [ 21 5 14595 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 40 [ 18 3 4206 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 41 [ 26 5 28655 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 42 [ 24 6 26816 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 43 [ 22 3 15767 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 44 [ 31 7 40851 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 45 [ 20 5 27114 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 46 [ 32 6 38509 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 47 [ 31 6 45630 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 12.72/12.91 Stopped by limit on insertions
% 12.72/12.91
% 12.72/12.91 Model 48 [ 34 5 29714 ] (0.00 seconds, 250000 Inserts)
% 12.72/12.91
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 49 [ 30 6 40938 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 50 [ 26 5 21831 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 51 [ 35 3 6472 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 52 [ 40 8 56394 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 53 [ 42 6 43184 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 54 [ 38 10 60261 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 55 [ 52 4 18219 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 56 [ 65 5 32806 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 57 [ 25 9 62212 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 58 [ 39 7 45737 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 59 [ 57 3 18336 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 60 [ 39 6 41559 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 61 [ 74 7 36121 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 62 [ 54 7 32981 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 63 [ 53 5 27597 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 64 [ 56 7 43766 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 65 [ 44 7 45005 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 66 [ 58 5 31956 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 67 [ 79 5 29097 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 68 [ 59 2 9260 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 69 [ 60 4 10359 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 70 [ 50 4 19603 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 71 [ 77 4 18438 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 72 [ 55 7 41827 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 73 [ 49 8 44147 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 74 [ 79 8 42659 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 75 [ 84 3 14207 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 76 [ 80 8 43134 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 77 [ 85 8 47500 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 78 [ 79 6 26186 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 79 [ 85 3 12159 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 80 [ 42 7 42562 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 81 [ 67 5 26368 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 82 [ 82 6 37592 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 83 [ 70 6 31284 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 84 [ 79 9 45624 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 85 [ 113 4 23622 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 86 [ 118 6 33606 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 87 [ 90 4 13878 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 88 [ 73 7 35704 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 89 [ 98 6 20437 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 90 [ 60 12 72539 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 91 [ 114 4 13153 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 92 [ 99 2 4798 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 93 [ 65 5 26840 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 38.88/39.14 Model 94 [ 98 3 1208 ] (0.00 seconds, 250000 Inserts)
% 38.88/39.14
% 38.88/39.14 Stopped by limit on insertions
% 38.88/39.14
% 88.44/88.62 Model 95 [ 112 2 12
% 88.44/88.62
% 88.44/88.62 Changing weight limit from 60 to 48.
% 88.44/88.62 08 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 96 [ 76 9 41403 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 97 [ 101 16 93222 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 98 [ 139 4 13152 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 99 [ 64 10 43806 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 100 [ 179 4 1218 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 101 [ 118 12 55196 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 102 [ 141 8 36001 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 103 [ 73 7 26400 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 104 [ 160 8 26095 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 105 [ 167 7 28521 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 106 [ 119 7 28396 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 107 [ 160 9 32181 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 108 [ 219 10 35006 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 109 [ 210 9 25889 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 110 [ 154 7 26586 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 111 [ 142 9 37911 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 112 [ 145 9 26599 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 113 [ 112 7 16565 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 114 [ 64 16 79194 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 115 [ 155 11 41450 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 116 [ 189 4 6810 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 117 [ 177 10 33305 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 118 [ 225 9 33731 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 119 [ 122 10 31329 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 120 [ 199 12 45475 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Stopped by limit on insertions
% 88.44/88.62
% 88.44/88.62 Model 121 [ 177 6 14873 ] (0.00 seconds, 250000 Inserts)
% 88.44/88.62
% 88.44/88.62 Resetting weight limit to 48 after 180 givens.
% 88.44/88.62
% 97.13/97.31
% 97.13/97.31
% 97.13/97.31 Changing weight limit from 48 to 47.
% 97.13/97.31
% 97.13/97.31 Stopped by limit on insertions
% 97.13/97.31
% 97.13/97.31 Model 122 [ 219 6 13452 ] (0.00 seconds, 250000 Inserts)
% 97.13/97.31
% 97.13/97.31 Stopped by limit on insertions
% 97.13/97.31
% 97.13/97.31 Model 123 [ 152 11 39099 ] (0.00 seconds, 250000 Inserts)
% 97.13/97.31
% 97.13/97.31 Stopped by limit on insertions
% 97.13/97.31
% 97.13/97.31 Model 124 [ 153 8 23449 ] (0.00 seconds, 250000 Inserts)
% 97.13/97.31
% 97.13/97.31 Resetting weight limit to 47 after 185 givens.
% 97.13/97.31
% 134.29/134.51
% 134.29/134.51
% 134.29/134.51 Changing weight limit from 47 to 48.
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 125 [ 206 6 3154 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 126 [ 153 20 82799 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 127 [ 223 10 35105 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 128 [ 91 7 17329 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 129 [ 228 11 16750 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 130 [ 123 10 22006 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 131 [ 206 11 29805 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Stopped by limit on insertions
% 134.29/134.51
% 134.29/134.51 Model 132 [ 207 10 27009 ] (0.00 seconds, 250000 Inserts)
% 134.29/134.51
% 134.29/134.51 Resetting weight limit to 48 after 275 givens.
% 134.29/134.51
% 163.08/163.27
% 163.08/163.27
% 163.08/163.27 Changing weight limit from 48 to 47.
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 133 [ 167 10 26777 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 134 [ 107 11 35335 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 135 [ 222 12 35737 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 136 [ 190 13 49473 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 137 [ 292 13 50339 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 138 [ 213 9 17767 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 139 [ 147 11 42987 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Stopped by limit on insertions
% 163.08/163.27
% 163.08/163.27 Model 140 [ 242 7 3285 ] (0.00 seconds, 250000 Inserts)
% 163.08/163.27
% 163.08/163.27 Resetting weight limit to 47 after 300 givens.
% 163.08/163.27
% 164.87/165.11
% 164.87/165.11
% 164.87/165.11 Changing weight limit from 47 to 37.
% 164.87/165.11
% 164.87/165.11 Stopped by limit on insertions
% 164.87/165.11
% 164.87/165.11 Model 141 [ 127 13 42631 ] (0.00 seconds, 250000 Inserts)
% 164.87/165.11
% 164.87/165.11 Resetting weight limit to 37 after 305 givens.
% 164.87/165.11
% 185.43/185.61
% 185.43/185.61
% 185.43/185.61 Changing weight limit from 37 to 36.
% 185.43/185.61
% 185.43/185.61 Stopped by limit on insertions
% 185.43/185.61
% 185.43/185.61 Model 142 [ 108 12 29969 ] (0.00 seconds, 250000 Inserts)
% 185.43/185.61
% 185.43/185.61 Stopped by limit on insertions
% 185.43/185.61
% 185.43/185.61 Model 143 [ 299 15 47628 ] (0.00 seconds, 250000 Inserts)
% 185.43/185.61
% 185.43/185.61 Stopped by limit on insertions
% 185.43/185.61
% 185.43/185.61 Model 144 [ 120 10 20657 ] (0.00 seconds, 250000 Inserts)
% 185.43/185.61
% 185.43/185.61 Modelling stopped after 300 given clauses and 0.00 seconds
% 185.43/185.61
% 185.43/185.61
% 185.43/185.61 Resetting weight limit to 36 after 500 givens.
% 185.43/185.61
% 185.62/185.84
% 185.62/185.84
% 185.62/185.84 Changing weight limit from 36 to 35.
% 185.62/185.84
% 185.62/185.84 Resetting weight limit to 35 after 505 givens.
% 185.62/185.84
% 185.85/186.06
% 185.85/186.06
% 185.85/186.06 Changing weight limit from 35 to 33.
% 185.85/186.06
% 185.85/186.06 Resetting weight limit to 33 after 510 givens.
% 185.85/186.06
% 186.11/186.31
% 186.11/186.31
% 186.11/186.31 Changing weight limit from 33 to 32.
% 186.11/186.31
% 186.11/186.31 Resetting weight limit to 32 after 515 givens.
% 186.11/186.31
% 186.77/186.96
% 186.77/186.96
% 186.77/186.96 Changing weight limit from 32 to 31.
% 186.77/186.96
% 186.77/186.96 Resetting weight limit to 31 after 530 givens.
% 186.77/186.96
% 188.82/189.08
% 188.82/189.08
% 188.82/189.08 Changing weight limit from 31 to 30.
% 188.82/189.08
% 188.82/189.08 Resetting weight limit to 30 after 585 givens.
% 188.82/189.08
% 189.65/189.86
% 189.65/189.86
% 189.65/189.86 Changing weight limit from 30 to 29.
% 189.65/189.86
% 189.65/189.86 Resetting weight limit to 29 after 625 givens.
% 189.65/189.86
% 191.46/191.67
% 191.46/191.67
% 191.46/191.67 Changing weight limit from 29 to 28.
% 191.46/191.67
% 191.46/191.67 Resetting weight limit to 28 after 690 givens.
% 191.46/191.67
% 197.72/197.92
% 197.72/197.92
% 197.72/197.92 Changing weight limit from 28 to 27.
% 197.72/197.92
% 197.72/197.92 Resetting weight limit to 27 after 825 givens.
% 197.72/197.92
% 199.23/199.49
% 199.23/199.49
% 199.23/199.49 Changing weight limit from 27 to 26.
% 199.23/199.49
% 199.23/199.49 Resetting weight limit to 26 after 860 givens.
% 199.23/199.49
% 209.53/209.74
% 209.53/209.74
% 209.53/209.74 Changing weight limit from 26 to 25.
% 209.53/209.74
% 209.53/209.74 Resetting weight limit to 25 after 1065 givens.
% 209.53/209.74
% 209.84/210.02
% 209.84/210.02
% 209.84/210.02 Changing weight limit from 25 to 24.
% 209.84/210.02
% 209.84/210.02 Resetting weight limit to 24 after 1075 givens.
% 209.84/210.02
% 217.01/217.21
% 217.01/217.21
% 217.01/217.21 Changing weight limit from 24 to 23.
% 217.01/217.21
% 217.01/217.21 Resetting weight limit to 23 after 1415 givens.
% 217.01/217.21
% 217.25/217.45
% 217.25/217.45
% 217.25/217.45 Changing weight limit from 23 to 22.
% 217.25/217.45
% 217.25/217.45 Resetting weight limit to 22 after 1430 givens.
% 217.25/217.45
% 219.93/220.12
% 219.93/220.12
% 219.93/220.12 Changing weight limit from 22 to 21.
% 219.93/220.12
% 219.93/220.12 Resetting weight limit to 21 after 1545 givens.
% 219.93/220.12
% 220.11/220.34 member(skc7,skf16(A,skc7,skc8),skc8).
% 220.11/220.34
% 220.11/220.34 ------------- memory usage ------------
% 220.11/220.34 295 mallocs of 32700 bytes each, 9420.4 K.
% 220.11/220.34 type (bytes each) gets frees in use avail bytes
% 220.11/220.34 sym_ent ( 304) 197 0 197 0 58.5 K
% 220.11/220.34 term ( 32) 6888821 6864798 24023 5581 925.1 K
% 220.11/220.34 rel ( 40) 5281435 5213973 67462 6374 2884.2 K
% 220.11/220.34 term_ptr ( 16) 2646864 2498500 148364 10411 2480.9 K
% 220.11/220.34 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 220.11/220.34 fpa_head ( 24) 12156 8170 3986 58 94.8 K
% 220.11/220.34 fpa_tree ( 56) 138661 138661 0 95 5.2 K
% 220.11/220.34 context (1288) 764960 764960 0 29 36.5 K
% 220.11/220.34 trail ( 24) 14754960 14754960 0 17 0.4 K
% 220.11/220.34 imd_tree ( 32) 7 0 7 0 0.2 K
% 220.11/220.34 imd_pos (4024) 348 348 0 1 3.9 K
% 220.11/220.34 is_tree ( 24) 54510 50023 4487 2078 153.9 K
% 220.11/220.34 is_pos (2424) 15313853 15313853 0 9 21.3 K
% 220.11/220.34 fsub_pos ( 16) 987706 987706 0 1 0.0 K
% 220.11/220.34 literal ( 32) 1605496 1582770 22726 3098 807.0 K
% 220.11/220.34 clause ( 88) 265053 258163 6890 274 615.7 K
% 220.11/220.34 list ( 272) 10 3 7 1 2.1 K
% 220.11/220.34 clash_nd ( 80) 5007 5007 0 27 2.1 K
% 220.11/220.34 clause_ptr ( 16) 53480 46699 6781 273 110.2 K
% 220.11/220.34 int_ptr ( 16) 1230307 1166389 63918 3106 1047.2 K
% 220.11/220.34 ci_ptr ( 24) 0 0 0 0 0.0 K
% 220.11/220.34 link_node ( 120) 0 0 0 0 0.0 K
% 220.11/220.34 ans_lit_node( 24) 0 0 0 0 0.0 K
% 220.11/220.34 formula_box( 168) 0 0 0 0 0.0 K
% 220.11/220.34 formula( 40) 0 0 0 0 0.0 K
% 220.11/220.34 formula_ptr( 16) 0 0 0 0 0.0 K
% 220.11/220.34 cl_attribute( 24) 0 0 0 0 0.0 K
% 220.11/220.34
% 220.11/220.34 ********** is_delete, can't find term.
% 220.11/220.34 .00
% 220.11/220.34 factor time 0.00
% 220.11/220.34 FINDER time 0.00
% 220.11/220.34 unindex time 0.00
% 220.11/220.34
% 220.11/220.34 ----------- soft-scott stats ----------
% 220.11/220.34
% 220.11/220.34 true clauses given 422 (27.2%)
% 220.11/220.34 false clauses given 1128
% 220.11/220.34
% 220.11/220.34 FALSE TRUE
% 220.11/220.34 8 0 4
% 220.11/220.34 11 0 5
% 220.11/220.34 12 0 1335
% 220.11/220.34 13 35 305
% 220.11/220.34 14 5 63
% 220.11/220.34 15 22 838
% 220.11/220.34 16 11 0
% 220.11/220.34 17 496 0
% 220.11/220.34 18 267 0
% 220.11/220.34 19 130 0
% 220.11/220.34 20 1416 0
% 220.11/220.34 21 118 0
% 220.11/220.34 tot: 2500 2550 (50.5% true)
% 220.11/220.34
% 220.11/220.34
% 220.11/220.34 Model 144 [ 120 10 20657 ] (0.00 seconds, 250000 Inserts)
% 220.11/220.34
% 220.11/220.34 Forward subsumption counts, subsumer:number_subsumed.
% 220.11/220.34 1:2275 2:0 3:0 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 220.11/220.34 11:0 12:0 13:0 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 220.11/220.34 21:0 22:0 23:0 24:0 25:0 26:0 27:0 28:0 29:0 30:0
% 220.11/220.34 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:0 40:0
% 220.11/220.34 41:0 42:0 43:0 44:0 45:0 46:0 47:0 48:0 49:0 50:0
% 220.11/220.34 51:0 52:0 53:0 54:0 55:0 56:0 57:0 58:0 59:0 60:0
% 220.11/220.34 61:0 62:0 63:0 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 220.11/220.34 71:0 72:0 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 220.11/220.34 81:0 82:0 83:0 84:0 85:0 86:1 87:286 88:329 89:234 90:177
% 220.11/220.34 91:230 92:121 93:128 94:129 95:143 96:104 97:91 98:103 99:90
% 220.11/220.34 All others: 32406.
% 220.11/220.34
% 220.11/220.34 ********** ABNORMAL END **********
% 220.11/220.34
% 220.11/220.34 ********** is_delete, can't find term.
%------------------------------------------------------------------------------