%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : NLP182-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:29 EDT 2022
% Result : Unknown 160.83s 161.05s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP182-1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n025.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 03:13:53 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.36 ----- Otter 3.2, August 2001 -----
% 0.13/0.36 The process was started by sandbox on n025.cluster.edu,
% 0.13/0.36 Fri Jul 1 03:13:53 2022
% 0.13/0.36 The command was "./sos". The process ID is 15319.
% 0.13/0.36
% 0.13/0.36 set(prolog_style_variables).
% 0.13/0.36 set(auto).
% 0.13/0.36 dependent: set(auto1).
% 0.13/0.36 dependent: set(process_input).
% 0.13/0.36 dependent: clear(print_kept).
% 0.13/0.36 dependent: clear(print_new_demod).
% 0.13/0.36 dependent: clear(print_back_demod).
% 0.13/0.36 dependent: clear(print_back_sub).
% 0.13/0.36 dependent: set(control_memory).
% 0.13/0.36 dependent: assign(max_mem, 12000).
% 0.13/0.36 dependent: assign(pick_given_ratio, 4).
% 0.13/0.36 dependent: assign(stats_level, 1).
% 0.13/0.36 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.36 dependent: assign(sos_limit, 5000).
% 0.13/0.36 dependent: assign(max_weight, 60).
% 0.13/0.36 clear(print_given).
% 0.13/0.36
% 0.13/0.36 list(usable).
% 0.13/0.36
% 0.13/0.36 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=28.
% 0.13/0.36
% 0.13/0.36 This ia a non-Horn set with equality. The strategy will be
% 0.13/0.36 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.13/0.36 unit deletion, with positive clauses in sos and nonpositive
% 0.13/0.36 clauses in usable.
% 0.13/0.36
% 0.13/0.36 dependent: set(knuth_bendix).
% 0.13/0.36 dependent: set(para_from).
% 0.13/0.36 dependent: set(para_into).
% 0.13/0.36 dependent: clear(para_from_right).
% 0.13/0.36 dependent: clear(para_into_right).
% 0.13/0.36 dependent: set(para_from_vars).
% 0.13/0.36 dependent: set(eq_units_both_ways).
% 0.13/0.36 dependent: set(dynamic_demod_all).
% 0.13/0.36 dependent: set(dynamic_demod).
% 0.13/0.36 dependent: set(order_eq).
% 0.13/0.36 dependent: set(back_demod).
% 0.13/0.36 dependent: set(lrpo).
% 0.13/0.36 dependent: set(hyper_res).
% 0.13/0.36 dependent: set(unit_deletion).
% 0.13/0.36 dependent: set(factor).
% 0.13/0.36
% 0.13/0.36 ------------> process usable:
% 0.13/0.36 85 back subsumes 84.
% 0.13/0.36
% 0.13/0.36 ------------> process sos:
% 0.13/0.36 Following clause subsumed by 113 during input processing: 0 [copy,113,flip.1] {-} A=A.
% 0.13/0.36 113 back subsumes 86.
% 0.13/0.36 113 back subsumes 85.
% 0.13/0.36 113 back subsumes 83.
% 0.13/0.36
% 0.13/0.36 ======= end of input processing =======
% 0.20/0.47
% 0.20/0.47 Model 1 (0.00 seconds, 0 Inserts)
% 0.20/0.47
% 0.20/0.47 Stopped by limit on number of solutions
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47 -------------- Softie stats --------------
% 0.20/0.47
% 0.20/0.47 UPDATE_STOP: 300
% 0.20/0.47 SFINDER_TIME_LIMIT: 2
% 0.20/0.47 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.47 number of clauses in intial UL: 82
% 0.20/0.47 number of clauses initially in problem: 109
% 0.20/0.47 percentage of clauses intially in UL: 75
% 0.20/0.47 percentage of distinct symbols occuring in initial UL: 91
% 0.20/0.47 percent of all initial clauses that are short: 99
% 0.20/0.47 absolute distinct symbol count: 87
% 0.20/0.47 distinct predicate count: 70
% 0.20/0.47 distinct function count: 10
% 0.20/0.47 distinct constant count: 7
% 0.20/0.47
% 0.20/0.47 ---------- no more Softie stats ----------
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47 =========== start of search ===========
% 12.30/12.47
% 12.30/12.47 Model 2 (0.00 seconds, 0 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on number of solutions
% 12.30/12.47
% 12.30/12.47 Model 3 (0.00 seconds, 0 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on number of solutions
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 4 [ 1 3 14489 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Model 5 (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on number of solutions
% 12.30/12.47
% 12.30/12.47 Model 6 (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on number of solutions
% 12.30/12.47
% 12.30/12.47 Model 7 (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on number of solutions
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 8 [ 2 6 29340 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 9 [ 5 5 35720 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 10 [ 4 2 12499 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 11 [ 2 9 51179 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 12 [ 6 5 26943 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 13 [ 3 18 179947 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 14 [ 7 4 25750 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 15 [ 8 6 38383 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 16 [ 7 1 1206 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 17 [ 5 8 36576 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 18 [ 4 5 19458 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 19 [ 6 9 61406 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 20 [ 10 2 15017 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 21 [ 9 6 40268 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 22 [ 7 8 51399 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 23 [ 7 5 19544 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 24 [ 4 7 31575 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 25 [ 4 9 29874 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 26 [ 12 6 44224 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 27 [ 12 3 14963 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 28 [ 13 3 14302 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 29 [ 16 2 13185 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 30 [ 14 4 28035 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 31 [ 15 5 35555 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 32 [ 16 4 29460 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 33 [ 16 6 47033 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 34 [ 19 6 37487 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 35 [ 20 6 47896 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 36 [ 16 3 14949 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 37 [ 15 6 39238 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 38 [ 18 3 15183 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 39 [ 13 5 24306 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 40 [ 18 2 1217 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 41 [ 19 5 37894 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 42 [ 19 4 17670 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 43 [ 13 5 28699 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 44 [ 21 5 28065 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 45 [ 28 5 37094 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 46 [ 21 5 18725 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 47 [ 24 7 41982 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 12.30/12.47 Stopped by limit on insertions
% 12.30/12.47
% 12.30/12.47 Model 48 [ 30 6 31035 ] (0.00 seconds, 250000 Inserts)
% 12.30/12.47
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 49 [ 26 7 53331 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 50 [ 29 7 29224 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 51 [ 43 4 19827 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 52 [ 38 4 14129 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 53 [ 64 4 18006 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 54 [ 37 7 36157 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 55 [ 43 6 40907 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 56 [ 44 6 39261 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 57 [ 77 5 33136 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 58 [ 81 5 14530 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 59 [ 59 3 19363 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 60 [ 48 6 29104 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 61 [ 59 1 1191 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 62 [ 41 4 22104 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 63 [ 57 7 50295 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 64 [ 45 10 69032 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 65 [ 74 4 24751 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 66 [ 57 5 31300 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 67 [ 53 7 37697 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 68 [ 69 4 15325 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 69 [ 56 5 19485 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 70 [ 45 4 17622 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 71 [ 55 3 14115 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 72 [ 60 2 1215 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 73 [ 59 5 29910 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 74 [ 51 6 31757 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 75 [ 66 6 30222 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 76 [ 61 5 24178 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 77 [ 63 5 33331 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 78 [ 114 3 12826 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 79 [ 85 3 17980 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 80 [ 73 6 37150 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 81 [ 98 8 45295 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 82 [ 94 5 27006 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 83 [ 89 4 20224 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 84 [ 85 2 4873 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 85 [ 102 3 12898 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 86 [ 111 6 26006 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 87 [ 95 5 22461 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 88 [ 87 6 31134 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 89 [ 109 5 20375 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 90 [ 90 4 22227 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 91 [ 102 6 36114 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 92 [ 100 6 28801 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 93 [ 95 8 36303 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 41.21/41.45 Model 94 [ 98 6 28908 ] (0.00 seconds, 250000 Inserts)
% 41.21/41.45
% 41.21/41.45 Stopped by limit on insertions
% 41.21/41.45
% 66.01/66.22 Model 95 [ 96 6 28291 ] (0.00 seconds
% 66.01/66.22
% 66.01/66.22 Changing weight limit from 60 to 38.
% 66.01/66.22 , 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 96 [ 72 9 47735 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 97 [ 124 7 37963 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 98 [ 90 3 10354 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 99 [ 104 8 51296 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 100 [ 116 6 20624 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 101 [ 109 7 35991 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 102 [ 100 9 48118 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 103 [ 124 10 44768 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 104 [ 91 4 12855 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 105 [ 127 8 42298 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 106 [ 160 7 33809 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 107 [ 100 4 2967 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 108 [ 114 3 4297 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 109 [ 101 8 40544 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 110 [ 193 14 76210 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Stopped by limit on insertions
% 66.01/66.22
% 66.01/66.22 Model 111 [ 166 9 32039 ] (0.00 seconds, 250000 Inserts)
% 66.01/66.22
% 66.01/66.22 Resetting weight limit to 38 after 165 givens.
% 66.01/66.22
% 70.76/70.98
% 70.76/70.98
% 70.76/70.98 Changing weight limit from 38 to 39.
% 70.76/70.98
% 70.76/70.98 Stopped by limit on insertions
% 70.76/70.98
% 70.76/70.98 Model 112 [ 143 8 29433 ] (0.00 seconds, 250000 Inserts)
% 70.76/70.98
% 70.76/70.98 Stopped by limit on insertions
% 70.76/70.98
% 70.76/70.98 Model 113 [ 151 8 25430 ] (0.00 seconds, 250000 Inserts)
% 70.76/70.98
% 70.76/70.98 Stopped by limit on insertions
% 70.76/70.98
% 70.76/70.98 Model 114 [ 95 7 19408 ] (0.00 seconds, 250000 Inserts)
% 70.76/70.98
% 70.76/70.98 Resetting weight limit to 39 after 170 givens.
% 70.76/70.98
% 75.44/75.63
% 75.44/75.63
% 75.44/75.63 Changing weight limit from 39 to 40.
% 75.44/75.63
% 75.44/75.63 Stopped by limit on insertions
% 75.44/75.63
% 75.44/75.63 Model 115 [ 159 5 14656 ] (0.00 seconds, 250000 Inserts)
% 75.44/75.63
% 75.44/75.63 Stopped by limit on insertions
% 75.44/75.63
% 75.44/75.63 Model 116 [ 128 5 17919 ] (0.00 seconds, 250000 Inserts)
% 75.44/75.63
% 75.44/75.63 Stopped by limit on insertions
% 75.44/75.63
% 75.44/75.63 Model 117 [ 177 6 14500 ] (0.00 seconds, 250000 Inserts)
% 75.44/75.63
% 75.44/75.63 Stopped by limit on insertions
% 75.44/75.63
% 75.44/75.63 Model 118 [ 224 10 40649 ] (0.00 seconds, 250000 Inserts)
% 75.44/75.63
% 75.44/75.63 Resetting weight limit to 40 after 175 givens.
% 75.44/75.63
% 81.64/81.86
% 81.64/81.86
% 81.64/81.86 Changing weight limit from 40 to 35.
% 81.64/81.86
% 81.64/81.86 Stopped by limit on insertions
% 81.64/81.86
% 81.64/81.86 Model 119 [ 136 8 31489 ] (0.00 seconds, 250000 Inserts)
% 81.64/81.86
% 81.64/81.86 Stopped by limit on insertions
% 81.64/81.86
% 81.64/81.86 Model 120 [ 140 8 26526 ] (0.00 seconds, 250000 Inserts)
% 81.64/81.86
% 81.64/81.86 Stopped by limit on insertions
% 81.64/81.86
% 81.64/81.86 Model 121 [ 178 8 24698 ] (0.00 seconds, 250000 Inserts)
% 81.64/81.86
% 81.64/81.86 Stopped by limit on insertions
% 81.64/81.86
% 81.64/81.86 Model 122 [ 216 6 13696 ] (0.00 seconds, 250000 Inserts)
% 81.64/81.86
% 81.64/81.86 Resetting weight limit to 35 after 180 givens.
% 81.64/81.86
% 85.73/86.01
% 85.73/86.01
% 85.73/86.01 Changing weight limit from 35 to 36.
% 85.73/86.01
% 85.73/86.01 Stopped by limit on insertions
% 85.73/86.01
% 85.73/86.01 Model 123 [ 127 8 25911 ] (0.00 seconds, 250000 Inserts)
% 85.73/86.01
% 85.73/86.01 Stopped by limit on insertions
% 85.73/86.01
% 85.73/86.01 Model 124 [ 219 4 1189 ] (0.00 seconds, 250000 Inserts)
% 85.73/86.01
% 85.73/86.01 Stopped by limit on insertions
% 85.73/86.01
% 85.73/86.01 Model 125 [ 172 12 55783 ] (0.00 seconds, 250000 Inserts)
% 85.73/86.01
% 85.73/86.01 Stopped by limit on insertions
% 85.73/86.01
% 85.73/86.01 Model 126 [ 176 14 64956 ] (0.00 seconds, 250000 Inserts)
% 85.73/86.01
% 85.73/86.01 Resetting weight limit to 36 after 185 givens.
% 85.73/86.01
% 88.11/88.36
% 88.11/88.36
% 88.11/88.36 Changing weight limit from 36 to 37.
% 88.11/88.36
% 88.11/88.36 Stopped by limit on insertions
% 88.11/88.36
% 88.11/88.36 Model 127 [ 173 9 27511 ] (0.00 seconds, 250000 Inserts)
% 88.11/88.36
% 88.11/88.36 Stopped by limit on insertions
% 88.11/88.36
% 88.11/88.36 Model 128 [ 91 10 38523 ] (0.00 seconds, 250000 Inserts)
% 88.11/88.36
% 88.11/88.36 Resetting weight limit to 37 after 190 givens.
% 88.11/88.36
% 88.19/88.47
% 88.19/88.47
% 88.19/88.47 Changing weight limit from 37 to 38.
% 88.19/88.47
% 88.19/88.47 Resetting weight limit to 38 after 195 givens.
% 88.19/88.47
% 88.43/88.62
% 88.43/88.62
% 88.43/88.62 Changing weight limit from 38 to 37.
% 88.43/88.62
% 88.43/88.62 Resetting weight limit to 37 after 200 givens.
% 88.43/88.62
% 93.10/93.39
% 93.10/93.39
% 93.10/93.39 Changing weight limit from 37 to 32.
% 93.10/93.39
% 93.10/93.39 Resetting weight limit to 32 after 280 givens.
% 93.10/93.39
% 93.61/93.81
% 93.61/93.81
% 93.61/93.81 Changing weight limit from 32 to 31.
% 93.61/93.81
% 93.61/93.81 Resetting weight limit to 31 after 285 givens.
% 93.61/93.81
% 94.23/94.44
% 94.23/94.44
% 94.23/94.44 Changing weight limit from 31 to 30.
% 94.23/94.44
% 94.23/94.44 Resetting weight limit to 30 after 295 givens.
% 94.23/94.44
% 98.24/98.45
% 98.24/98.45
% 98.24/98.45 Changing weight limit from 30 to 29.
% 98.24/98.45
% 98.24/98.45 Resetting weight limit to 29 after 360 givens.
% 98.24/98.45
% 99.73/99.96
% 99.73/99.96
% 99.73/99.96 Changing weight limit from 29 to 28.
% 99.73/99.96
% 99.73/99.96 Resetting weight limit to 28 after 390 givens.
% 99.73/99.96
% 155.09/155.36
% 155.09/155.36
% 155.09/155.36 Changing weight limit from 28 to 27.
% 155.09/155.36
% 155.09/155.36 Stopped by limit on insertions
% 155.09/155.36
% 155.09/155.36 Model 129 [ 213 5 1189 ] (0.00 seconds, 250000 Inserts)
% 155.09/155.36
% 155.09/155.36 Modelling stopped after 300 given clauses and 0.00 seconds
% 155.09/155.36
% 155.09/155.36
% 155.09/155.36 Resetting weight limit to 27 after 1480 givens.
% 155.09/155.36
% 157.30/157.59
% 157.30/157.59
% 157.30/157.59 Changing weight limit from 27 to 26.
% 157.30/157.59
% 157.30/157.59 Resetting weight limit to 26 after 1515 givens.
% 157.30/157.59
% 158.04/158.24
% 158.04/158.24
% 158.04/158.24 Changing weight limit from 26 to 24.
% 158.04/158.24
% 158.04/158.24 Resetting weight limit to 24 after 1540 givens.
% 158.04/158.24
% 158.70/158.90
% 158.70/158.90
% 158.70/158.90 Changing weight limit from 24 to 23.
% 158.70/158.90
% 158.70/158.90 Resetting weight limit to 23 after 1560 givens.
% 158.70/158.90
% 159.62/159.87
% 159.62/159.87
% 159.62/159.87 Changing weight limit from 23 to 21.
% 159.62/159.87
% 159.62/159.87 Resetting weight limit to 21 after 1610 givens.
% 159.62/159.87
% 160.83/161.04 in(skc7,skf12(skf22(skc8,skc7),skc7,A),A).
% 160.83/161.04
% 160.83/161.04 ------------- memory usage ------------
% 160.83/161.04 326 mallocs of 32700 bytes each, 10410.4 K.
% 160.83/161.04 type (bytes each) gets frees in use avail bytes
% 160.83/161.04 sym_ent ( 304) 197 0 197 0 58.5 K
% 160.83/161.04 term ( 32) 7960020 7935833 24187 7960 1004.6 K
% 160.83/161.04 rel ( 40) 6117702 6050243 67459 15389 3236.2 K
% 160.83/161.04 term_ptr ( 16) 4169407 4023618 145789 29529 2739.3 K
% 160.83/161.04 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 160.83/161.04 fpa_head ( 24) 21275 16870 4405 9 103.5 K
% 160.83/161.04 fpa_tree ( 56) 250906 250906 0 95 5.2 K
% 160.83/161.04 context (1288) 985770 985770 0 29 36.5 K
% 160.83/161.04 trail ( 24) 24293407 24293407 0 17 0.4 K
% 160.83/161.04 imd_tree ( 32) 12 0 12 0 0.4 K
% 160.83/161.04 imd_pos (4024) 1352 1352 0 1 3.9 K
% 160.83/161.04 is_tree ( 24) 90500 84903 5597 462 142.0 K
% 160.83/161.04 is_pos (2424) 23967977 23967977 0 9 21.3 K
% 160.83/161.04 fsub_pos ( 16) 1367962 1367962 0 1 0.0 K
% 160.83/161.04 literal ( 32) 1841516 1818614 22902 5697 893.7 K
% 160.83/161.04 clause ( 88) 311958 304662 7296 421 663.2 K
% 160.83/161.04 list ( 272) 10 3 7 1 2.1 K
% 160.83/161.04 clash_nd ( 80) 7544 7544 0 27 2.1 K
% 160.83/161.04 clause_ptr ( 16) 84754 77567 7187 429 119.0 K
% 160.83/161.04 int_ptr ( 16) 1575567 1509399 66168 4562 1105.2 K
% 160.83/161.04 ci_ptr ( 24) 0 0 0 0 0.0 K
% 160.83/161.04 link_node ( 120) 0 0 0 0 0.0 K
% 160.83/161.04 ans_lit_node( 24) 0 0 0 0 0.0 K
% 160.83/161.04 formula_box( 168) 0 0 0 0 0.0 K
% 160.83/161.04 formula( 40) 0 0 0 0 0.0 K
% 160.83/161.04 formula_ptr( 16) 0 0 0 0 0.0 K
% 160.83/161.04 cl_attribute( 24) 0 0 0 0 0.0 K
% 160.83/161.04
% 160.83/161.04 ********** is_delete, can't find end.
% 160.83/161.04 0.00
% 160.83/161.04 factor time 0.00
% 160.83/161.04 FINDER time 0.00
% 160.83/161.04 unindex time 0.00
% 160.83/161.04
% 160.83/161.04 ----------- soft-scott stats ----------
% 160.83/161.04
% 160.83/161.04 true clauses given 508 (30.1%)
% 160.83/161.04 false clauses given 1177
% 160.83/161.04
% 160.83/161.04 FALSE TRUE
% 160.83/161.04 12 0 1517
% 160.83/161.04 13 62 332
% 160.83/161.04 14 9 55
% 160.83/161.04 15 9 585
% 160.83/161.04 16 73 1
% 160.83/161.04 17 494 8
% 160.83/161.04 18 388 0
% 160.83/161.04 19 234 1
% 160.83/161.04 20 1208 67
% 160.83/161.04 21 26 0
% 160.83/161.04 tot: 2503 2566 (50.6% true)
% 160.83/161.04
% 160.83/161.04
% 160.83/161.04 Model 129 [ 213 5 1189 ] (0.01 seconds, 250000 Inserts)
% 160.83/161.04
% 160.83/161.04 Forward subsumption counts, subsumer:number_subsumed.
% 160.83/161.04 1:4011 2:0 3:0 4:0 5:0 6:0 7:0 8:0 9:0 10:0
% 160.83/161.04 11:0 12:0 13:0 14:0 15:0 16:0 17:0 18:0 19:0 20:0
% 160.83/161.04 21:0 22:0 23:0 24:0 25:0 26:0 27:0 28:0 29:0 30:0
% 160.83/161.04 31:0 32:0 33:0 34:0 35:0 36:0 37:0 38:0 39:0 40:0
% 160.83/161.04 41:0 42:0 43:0 44:0 45:0 46:0 47:0 48:0 49:0 50:0
% 160.83/161.04 51:0 52:0 53:0 54:0 55:0 56:0 57:0 58:0 59:0 60:0
% 160.83/161.04 61:0 62:0 63:0 64:0 65:0 66:0 67:0 68:0 69:0 70:0
% 160.83/161.04 71:0 72:0 73:0 74:0 75:0 76:0 77:0 78:0 79:0 80:0
% 160.83/161.04 81:0 82:0 83:0 84:0 85:0 86:1 87:804 88:989 89:507 90:417
% 160.83/161.04 91:352 92:619 93:110 94:109 95:112 96:99 97:111 98:95 99:107
% 160.83/161.04 All others: 40873.
% 160.83/161.04
% 160.83/161.04 ********** ABNORMAL END **********
% 160.83/161.04
% 160.83/161.04 ********** is_delete, can't find end.
%------------------------------------------------------------------------------