%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NLP217-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n025.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:50 EDT 2022
% Result : Unknown 126.04s 126.32s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP217-1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.13 % Command : sos-script %s
% 0.12/0.34 % Computer : n025.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 : Thu Jun 30 22:56:23 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.36 ----- Otter 3.2, August 2001 -----
% 0.12/0.36 The process was started by sandbox on n025.cluster.edu,
% 0.12/0.36 Thu Jun 30 22:56:23 2022
% 0.12/0.36 The command was "./sos". The process ID is 26746.
% 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=1, symmetry=0, max_lits=35.
% 0.12/0.36
% 0.12/0.36 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.36 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.36 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.36 clauses in usable.
% 0.12/0.36
% 0.12/0.36 dependent: set(knuth_bendix).
% 0.12/0.36 dependent: set(para_from).
% 0.12/0.36 dependent: set(para_into).
% 0.12/0.36 dependent: clear(para_from_right).
% 0.12/0.36 dependent: clear(para_into_right).
% 0.12/0.36 dependent: set(para_from_vars).
% 0.12/0.36 dependent: set(eq_units_both_ways).
% 0.12/0.36 dependent: set(dynamic_demod_all).
% 0.12/0.36 dependent: set(dynamic_demod).
% 0.12/0.36 dependent: set(order_eq).
% 0.12/0.36 dependent: set(back_demod).
% 0.12/0.36 dependent: set(lrpo).
% 0.12/0.36 dependent: set(hyper_res).
% 0.12/0.36 dependent: set(unit_deletion).
% 0.12/0.36 dependent: set(factor).
% 0.12/0.36
% 0.12/0.36 ------------> process usable:
% 0.12/0.36 99 back subsumes 98.
% 0.12/0.36
% 0.12/0.36 ------------> process sos:
% 0.12/0.36 Following clause subsumed by 136 during input processing: 0 [copy,136,flip.1] {-} A=A.
% 0.12/0.36 136 back subsumes 101.
% 0.12/0.36 136 back subsumes 100.
% 0.12/0.36 136 back subsumes 99.
% 0.12/0.36 136 back subsumes 97.
% 0.12/0.36
% 0.12/0.36 ======= end of input processing =======
% 0.59/0.78
% 0.59/0.78 Model 1 (0.00 seconds, 0 Inserts)
% 0.59/0.78
% 0.59/0.78 Stopped by limit on number of solutions
% 0.59/0.78
% 0.59/0.78
% 0.59/0.78 -------------- Softie stats --------------
% 0.59/0.78
% 0.59/0.78 UPDATE_STOP: 300
% 0.59/0.78 SFINDER_TIME_LIMIT: 2
% 0.59/0.78 SHORT_CLAUSE_CUTOFF: 4
% 0.59/0.78 number of clauses in intial UL: 102
% 0.59/0.78 number of clauses initially in problem: 131
% 0.59/0.78 percentage of clauses intially in UL: 77
% 0.59/0.78 percentage of distinct symbols occuring in initial UL: 94
% 0.59/0.78 percent of all initial clauses that are short: 99
% 0.59/0.78 absolute distinct symbol count: 93
% 0.59/0.78 distinct predicate count: 75
% 0.59/0.78 distinct function count: 11
% 0.59/0.78 distinct constant count: 7
% 0.59/0.78
% 0.59/0.78 ---------- no more Softie stats ----------
% 0.59/0.78
% 0.59/0.78
% 0.59/0.78
% 0.59/0.78 Model 2 (0.00 seconds, 0 Inserts)
% 0.59/0.78
% 0.59/0.78 Stopped by limit on number of solutions
% 0.59/0.78
% 0.59/0.78 =========== start of search ===========
% 15.87/16.05
% 15.87/16.05 Model 3 (0.00 seconds, 0 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Model 4 (0.00 seconds, 0 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Model 5 (0.00 seconds, 0 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 6 [ 2 9 66741 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Model 7 (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Model 8 (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Model 9 (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on number of solutions
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 10 [ 6 7 41100 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 11 [ 5 11 72254 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 12 [ 4 26 170428 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 13 [ 2 22 144154 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 14 [ 2 17 92534 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 15 [ 3 14 86935 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 16 [ 4 18 94032 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 17 [ 6 10 67390 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 18 [ 9 13 82824 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 19 [ 5 26 158393 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 20 [ 7 12 64300 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 21 [ 13 10 64707 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 22 [ 5 21 114096 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 23 [ 10 8 30497 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 24 [ 6 24 130250 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 25 [ 5 37 219822 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 26 [ 17 10 73995 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 27 [ 8 27 152042 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 28 [ 17 7 39801 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 29 [ 19 9 61722 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 30 [ 15 14 95213 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 31 [ 17 19 122303 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 32 [ 9 9 40196 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 33 [ 19 17 108099 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 34 [ 10 20 83036 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 35 [ 18 12 66424 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 36 [ 19 11 60904 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 37 [ 9 23 125331 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 38 [ 23 16 117060 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 39 [ 17 14 94296 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 40 [ 21 17 124480 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 41 [ 28 10 61235 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 42 [ 19 9 61082 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 43 [ 26 17 122515 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 44 [ 21 22 156309 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 45 [ 29 11 61196 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 46 [ 29 8 47925 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 47 [ 30 8 47900 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 15.87/16.05 Stopped by limit on insertions
% 15.87/16.05
% 15.87/16.05 Model 48 [ 32 10 62520 ] (0.00 seconds, 250000 Inserts)
% 15.87/16.05
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 49 [ 15 5 22114 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 50 [ 31 13 84976 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 51 [ 29 19 135135 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 52 [ 25 13 74821 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 53 [ 37 16 101358 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 54 [ 26 14 104818 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 55 [ 29 17 113669 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 56 [ 37 15 99634 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 57 [ 35 11 61527 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 58 [ 45 15 82584 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 59 [ 33 15 87145 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 60 [ 61 26 161642 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 61 [ 34 17 102997 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 62 [ 85 6 26146 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 63 [ 54 20 122143 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 64 [ 48 12 64160 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 65 [ 70 20 120355 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 66 [ 41 10 60738 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 67 [ 54 18 109220 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 68 [ 74 16 102872 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 69 [ 73 9 49635 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 70 [ 102 9 46556 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 71 [ 69 10 55485 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 72 [ 42 10 59508 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 73 [ 77 14 86253 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 74 [ 84 12 67567 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 75 [ 49 7 43026 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 76 [ 77 5 22060 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 77 [ 87 12 74236 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 78 [ 67 11 64073 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 79 [ 37 20 121954 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 80 [ 69 9 43713 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 81 [ 93 7 42092 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 82 [ 75 18 108106 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 83 [ 63 14 87195 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 84 [ 65 11 64153 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 85 [ 85 10 58202 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 86 [ 122 6 19706 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 87 [ 70 14 94322 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 88 [ 96 14 83052 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 89 [ 133 4 14397 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 90 [ 85 13 67507 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 91 [ 66 20 126109 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 92 [ 68 10 63015 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 93 [ 67 20 115997 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 36.87/37.09 Stopped by limit on insertions
% 36.87/37.09
% 36.87/37.09 Model 94 [ 96 7 39738 ] (0.00 seconds, 250000 Inserts)
% 36.87/37.09
% 60.98/61.21 Stopped by
% 60.98/61.21
% 60.98/61.21 Changing weight limit from 60 to 39.
% 60.98/61.21 limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 95 [ 81 5 20490 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 96 [ 106 8 36534 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 97 [ 67 10 51451 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 98 [ 84 15 76878 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 99 [ 66 18 109536 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 100 [ 93 6 20452 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 101 [ 67 23 137121 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 102 [ 79 13 79995 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 103 [ 83 15 77792 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 104 [ 90 9 47349 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 105 [ 119 3 3271 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 106 [ 43 13 77102 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 107 [ 58 14 76387 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 108 [ 117 11 60216 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 109 [ 86 7 33104 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 110 [ 100 15 78827 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 111 [ 126 6 28323 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 112 [ 93 20 117596 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 113 [ 140 13 65461 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 114 [ 112 17 91640 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 115 [ 90 13 71399 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 116 [ 117 10 40674 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 117 [ 82 9 42788 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 118 [ 148 12 54182 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 119 [ 98 23 118278 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Stopped by limit on insertions
% 60.98/61.21
% 60.98/61.21 Model 120 [ 160 10 47869 ] (0.00 seconds, 250000 Inserts)
% 60.98/61.21
% 60.98/61.21 Resetting weight limit to 39 after 150 givens.
% 60.98/61.21
% 65.46/65.67
% 65.46/65.67
% 65.46/65.67 Changing weight limit from 39 to 40.
% 65.46/65.67
% 65.46/65.67 Stopped by limit on insertions
% 65.46/65.67
% 65.46/65.67 Model 121 [ 129 10 41439 ] (0.00 seconds, 250000 Inserts)
% 65.46/65.67
% 65.46/65.67 Stopped by limit on insertions
% 65.46/65.67
% 65.46/65.67 Model 122 [ 139 14 66938 ] (0.00 seconds, 250000 Inserts)
% 65.46/65.67
% 65.46/65.67 Stopped by limit on insertions
% 65.46/65.67
% 65.46/65.67 Model 123 [ 108 17 94092 ] (0.00 seconds, 250000 Inserts)
% 65.46/65.67
% 65.46/65.67 Stopped by limit on insertions
% 65.46/65.67
% 65.46/65.67 Model 124 [ 136 20 101389 ] (0.00 seconds, 250000 Inserts)
% 65.46/65.67
% 65.46/65.67 Resetting weight limit to 40 after 155 givens.
% 65.46/65.67
% 75.43/75.68
% 75.43/75.68
% 75.43/75.68 Changing weight limit from 40 to 41.
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 125 [ 210 7 22476 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 126 [ 122 14 64033 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 127 [ 152 4 9863 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 128 [ 116 12 55213 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 129 [ 156 14 63219 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 130 [ 118 13 63197 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 131 [ 187 17 79473 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Stopped by limit on insertions
% 75.43/75.68
% 75.43/75.68 Model 132 [ 139 25 134411 ] (0.00 seconds, 250000 Inserts)
% 75.43/75.68
% 75.43/75.68 Resetting weight limit to 41 after 165 givens.
% 75.43/75.68
% 79.34/79.56
% 79.34/79.56
% 79.34/79.56 Changing weight limit from 41 to 40.
% 79.34/79.56
% 79.34/79.56 Stopped by limit on insertions
% 79.34/79.56
% 79.34/79.56 Model 133 [ 75 18 97052 ] (0.00 seconds, 250000 Inserts)
% 79.34/79.56
% 79.34/79.56 Stopped by limit on insertions
% 79.34/79.56
% 79.34/79.56 Model 134 [ 128 8 30149 ] (0.00 seconds, 250000 Inserts)
% 79.34/79.56
% 79.34/79.56 Stopped by limit on insertions
% 79.34/79.56
% 79.34/79.56 Model 135 [ 71 14 71640 ] (0.00 seconds, 250000 Inserts)
% 79.34/79.56
% 79.34/79.56 Resetting weight limit to 40 after 170 givens.
% 79.34/79.56
% 89.12/89.35
% 89.12/89.35
% 89.12/89.35 Changing weight limit from 40 to 38.
% 89.12/89.35
% 89.12/89.35 Resetting weight limit to 38 after 300 givens.
% 89.12/89.35
% 89.84/90.07
% 89.84/90.07
% 89.84/90.07 Changing weight limit from 38 to 35.
% 89.84/90.07
% 89.84/90.07 Resetting weight limit to 35 after 305 givens.
% 89.84/90.07
% 90.75/90.97
% 90.75/90.97
% 90.75/90.97 Changing weight limit from 35 to 34.
% 90.75/90.97
% 90.75/90.97 Resetting weight limit to 34 after 315 givens.
% 90.75/90.97
% 91.22/91.43
% 91.22/91.43
% 91.22/91.43 Changing weight limit from 34 to 33.
% 91.22/91.43
% 91.22/91.43 Resetting weight limit to 33 after 320 givens.
% 91.22/91.43
% 92.65/92.91
% 92.65/92.91
% 92.65/92.91 Changing weight limit from 33 to 32.
% 92.65/92.91
% 92.65/92.91 Resetting weight limit to 32 after 335 givens.
% 92.65/92.91
% 93.30/93.56
% 93.30/93.56
% 93.30/93.56 Changing weight limit from 32 to 31.
% 93.30/93.56
% 93.30/93.56 Resetting weight limit to 31 after 340 givens.
% 93.30/93.56
% 96.22/96.47
% 96.22/96.47
% 96.22/96.47 Changing weight limit from 31 to 30.
% 96.22/96.47
% 96.22/96.47 Resetting weight limit to 30 after 370 givens.
% 96.22/96.47
% 104.02/104.25
% 104.02/104.25
% 104.02/104.25 Changing weight limit from 30 to 29.
% 104.02/104.25
% 104.02/104.25 Modelling stopped after 300 given clauses and 0.00 seconds
% 104.02/104.25
% 104.02/104.25
% 104.02/104.25 Resetting weight limit to 29 after 470 givens.
% 104.02/104.25
% 105.16/105.43
% 105.16/105.43
% 105.16/105.43 Changing weight limit from 29 to 28.
% 105.16/105.43
% 105.16/105.43 Resetting weight limit to 28 after 485 givens.
% 105.16/105.43
% 107.10/107.37
% 107.10/107.37
% 107.10/107.37 Changing weight limit from 28 to 27.
% 107.10/107.37
% 107.10/107.37 Resetting weight limit to 27 after 510 givens.
% 107.10/107.37
% 107.71/107.93
% 107.71/107.93
% 107.71/107.93 Changing weight limit from 27 to 26.
% 107.71/107.93
% 107.71/107.93 Resetting weight limit to 26 after 515 givens.
% 107.71/107.93
% 112.07/112.30
% 112.07/112.30
% 112.07/112.30 Changing weight limit from 26 to 25.
% 112.07/112.30
% 112.07/112.30 Resetting weight limit to 25 after 595 givens.
% 112.07/112.30
% 112.25/112.49
% 112.25/112.49
% 112.25/112.49 Changing weight limit from 25 to 24.
% 112.25/112.49
% 112.25/112.49 Resetting weight limit to 24 after 605 givens.
% 112.25/112.49
% 124.59/124.86
% 124.59/124.86
% 124.59/124.86 Changing weight limit from 24 to 23.
% 124.59/124.86
% 124.59/124.86 Resetting weight limit to 23 after 1030 givens.
% 124.59/124.86
% 126.04/126.31 in(skc7,skf13(skf26(skc9,skc7),skc7,skc11),skf26(A,B)).
% 126.04/126.31
% 126.04/126.31 ------------- memory usage ------------
% 126.04/126.31 312 mallocs of 32700 bytes each, 9963.3 K.
% 126.04/126.31 type (bytes each) gets frees in use avail bytes
% 126.04/126.31 sym_ent ( 304) 205 0 205 0 60.9 K
% 126.04/126.31 term ( 32) 6839157 6812153 27004 6189 1037.3 K
% 126.04/126.31 rel ( 40) 5173562 5107433 66129 13174 3097.8 K
% 126.04/126.31 term_ptr ( 16) 2641078 2495411 145667 23071 2636.5 K
% 126.04/126.31 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 126.04/126.31 fpa_head ( 24) 10329 6629 3700 270 93.0 K
% 126.04/126.31 fpa_tree ( 56) 177787 177787 0 54 3.0 K
% 126.04/126.31 context (1288) 792719 792719 0 36 45.3 K
% 126.04/126.31 trail ( 24) 7262581 7262581 0 12 0.3 K
% 126.04/126.31 imd_tree ( 32) 12 0 12 0 0.4 K
% 126.04/126.31 imd_pos (4024) 54 54 0 1 3.9 K
% 126.04/126.31 is_tree ( 24) 33807 29857 3950 2619 154.0 K
% 126.04/126.31 is_pos (2424) 14517921 14517921 0 9 21.3 K
% 126.04/126.31 fsub_pos ( 16) 1040919 1040919 0 1 0.0 K
% 126.04/126.31 literal ( 32) 1663410 1638227 25183 3926 909.7 K
% 126.04/126.31 clause ( 88) 254841 248173 6668 228 592.6 K
% 126.04/126.31 list ( 272) 10 3 7 1 2.1 K
% 126.04/126.31 clash_nd ( 80) 4767 4767 0 34 2.7 K
% 126.04/126.31 clause_ptr ( 16) 53776 47233 6543 227 105.8 K
% 126.04/126.31 int_ptr ( 16) 1155662 1090849 64813 2279 1048.3 K
% 126.04/126.32 ci_ptr ( 24) 0 0 0 0 0.0 K
% 126.04/126.32 link_node ( 120) 0 0 0 0 0.0 K
% 126.04/126.32 ans_lit_node( 24) 0 0 0 0 0.0 K
% 126.04/126.32 formula_box( 168) 0 0 0 0 0.0 K
% 126.04/126.32 formula( 40) 0 0 0 0 0.0 K
% 126.04/126.32 formula_ptr( 16) 0 0 0 0 0.0 K
% 126.04/126.32 cl_attribute( 24) 0 0 0 0 0.0 K
% 126.04/126.32
% 126.04/126.32 ********** is_delete, can't find end.
% 126.04/126.32 ubsume 0.00
% 126.04/126.32 factor time 0.00
% 126.04/126.32 FINDER time 0.00
% 126.04/126.32 unindex time 0.00
% 126.04/126.32
% 126.04/126.32 ----------- soft-scott stats ----------
% 126.04/126.32
% 126.04/126.32 true clauses given 299 (27.7%)
% 126.04/126.32 false clauses given 781
% 126.04/126.32
% 126.04/126.32 FALSE TRUE
% 126.04/126.32 10 0 54
% 126.04/126.32 11 0 71
% 126.04/126.32 12 8 1264
% 126.04/126.32 13 0 292
% 126.04/126.32 14 0 55
% 126.04/126.32 15 0 252
% 126.04/126.32 16 0 141
% 126.04/126.32 17 404 403
% 126.04/126.32 18 41 2
% 126.04/126.32 19 1390 117
% 126.04/126.32 20 122 61
% 126.04/126.32 21 156 0
% 126.04/126.32 22 306 11
% 126.04/126.32 23 138 3
% 126.04/126.32 tot: 2565 2726 (51.5% true)
% 126.04/126.32
% 126.04/126.32
% 126.04/126.32 Model 135 [ 71 14 71640 ] (0.00 seconds, 250000 Inserts)
% 126.04/126.32
% 126.04/126.32 Forward subsumption counts, subsumer:number_subsumed.
% 126.04/126.32 1:1880 2:0 3:0 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 126.04/126.32 11:0 12:0 13:0 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 126.04/126.32 21:0 22:0 23:0 24:0 25:0 26:0 27:0 28:0 29:0 30:0
% 126.04/126.32 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:0 40:0
% 126.04/126.32 41:0 42:0 43:0 44:0 45:0 46:0 47:0 48:0 49:0 50:0
% 126.04/126.32 51:0 52:0 53:0 54:0 55:0 56:0 57:0 58:0 59:0 60:0
% 126.04/126.32 61:0 62:0 63:0 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 126.04/126.32 71:0 72:0 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 126.04/126.32 81:0 82:0 83:0 84:0 85:0 86:0 87:0 88:0 89:0 90:0
% 126.04/126.32 91:0 92:0 93:0 94:0 95:0 96:0 97:0 98:0 99:0
% 126.04/126.32 All others: 29919.
% 126.04/126.32
% 126.04/126.32 ********** ABNORMAL END **********
% 126.04/126.32
% 126.04/126.32 ********** is_delete, can't find end.
%------------------------------------------------------------------------------