%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : SET031-4 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n023.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 : Tue Jul 19 05:14:37 EDT 2022
% Result : Unknown 62.44s 62.64s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SET031-4 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.13 % Command : sos-script %s
% 0.12/0.34 % Computer : n023.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 : Sat Jul 9 22:48:25 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.38 ----- Otter 3.2, August 2001 -----
% 0.12/0.38 The process was started by sandbox2 on n023.cluster.edu,
% 0.12/0.38 Sat Jul 9 22:48:25 2022
% 0.12/0.38 The command was "./sos". The process ID is 12554.
% 0.12/0.38
% 0.12/0.38 set(prolog_style_variables).
% 0.12/0.38 set(auto).
% 0.12/0.38 dependent: set(auto1).
% 0.12/0.38 dependent: set(process_input).
% 0.12/0.38 dependent: clear(print_kept).
% 0.12/0.38 dependent: clear(print_new_demod).
% 0.12/0.38 dependent: clear(print_back_demod).
% 0.12/0.38 dependent: clear(print_back_sub).
% 0.12/0.38 dependent: set(control_memory).
% 0.12/0.38 dependent: assign(max_mem, 12000).
% 0.12/0.38 dependent: assign(pick_given_ratio, 4).
% 0.12/0.38 dependent: assign(stats_level, 1).
% 0.12/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.38 dependent: assign(sos_limit, 5000).
% 0.12/0.38 dependent: assign(max_weight, 60).
% 0.12/0.38 clear(print_given).
% 0.12/0.38
% 0.12/0.38 list(usable).
% 0.12/0.38
% 0.12/0.38 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=8.
% 0.12/0.38
% 0.12/0.38 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.38 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.38 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.38 clauses in usable.
% 0.12/0.38
% 0.12/0.38 dependent: set(knuth_bendix).
% 0.12/0.38 dependent: set(para_from).
% 0.12/0.38 dependent: set(para_into).
% 0.12/0.38 dependent: clear(para_from_right).
% 0.12/0.38 dependent: clear(para_into_right).
% 0.12/0.38 dependent: set(para_from_vars).
% 0.12/0.38 dependent: set(eq_units_both_ways).
% 0.12/0.38 dependent: set(dynamic_demod_all).
% 0.12/0.38 dependent: set(dynamic_demod).
% 0.12/0.38 dependent: set(order_eq).
% 0.12/0.38 dependent: set(back_demod).
% 0.12/0.38 dependent: set(lrpo).
% 0.12/0.38 dependent: set(hyper_res).
% 0.12/0.38 dependent: set(unit_deletion).
% 0.12/0.38 dependent: set(factor).
% 0.12/0.38
% 0.12/0.38 ------------> process usable:
% 0.12/0.38
% 0.12/0.38 ------------> process sos:
% 0.12/0.38 Following clause subsumed by 228 during input processing: 0 [copy,228,flip.1] {-} A=A.
% 0.12/0.38 228 back subsumes 131.
% 0.12/0.38
% 0.12/0.38 ======= end of input processing =======
% 0.19/0.51
% 0.19/0.51 Model 1 (0.00 seconds, 0 Inserts)
% 0.19/0.51
% 0.19/0.51 Stopped by limit on number of solutions
% 0.19/0.51
% 0.19/0.51
% 0.19/0.51 -------------- Softie stats --------------
% 0.19/0.51
% 0.19/0.51 UPDATE_STOP: 300
% 0.19/0.51 SFINDER_TIME_LIMIT: 2
% 0.19/0.51 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.51 number of clauses in intial UL: 108
% 0.19/0.51 number of clauses initially in problem: 208
% 0.19/0.51 percentage of clauses intially in UL: 51
% 0.19/0.51 percentage of distinct symbols occuring in initial UL: 86
% 0.19/0.51 percent of all initial clauses that are short: 100
% 0.19/0.51 absolute distinct symbol count: 75
% 0.19/0.51 distinct predicate count: 14
% 0.19/0.51 distinct function count: 53
% 0.19/0.51 distinct constant count: 8
% 0.19/0.51
% 0.19/0.51 ---------- no more Softie stats ----------
% 0.19/0.51
% 0.19/0.51
% 0.19/0.51
% 0.19/0.51 Model 2 (0.00 seconds, 0 Inserts)
% 0.19/0.51
% 0.19/0.51 Stopped by limit on number of solutions
% 0.19/0.51
% 0.19/0.51 =========== start of search ===========
% 19.86/20.09
% 19.86/20.09 Model 3 (0.00 seconds, 0 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on number of solutions
% 19.86/20.09
% 19.86/20.09 Model 4 (0.00 seconds, 0 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on number of solutions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 5 [ 1 2 5896 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 6 [ 5 6 34023 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 7 [ 3 2 9355 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 8 [ 8 1 1581 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 9 [ 9 1 4921 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 10 [ 11 8 33930 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 11 [ 13 3 18788 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 12 [ 13 4 22173 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 13 [ 14 1 3526 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 14 [ 12 1 1362 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 15 [ 11 2 2075 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 16 [ 15 1 2094 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 17 [ 15 12 67872 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 18 [ 12 1 1474 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 19 [ 16 4 26351 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 20 [ 14 2 7832 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 21 [ 17 7 23588 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 22 [ 20 1 1392 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 23 [ 24 1 1376 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 24 [ 35 1 2914 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 25 [ 30 1 1362 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 26 [ 35 2 2569 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 27 [ 46 4 22850 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 28 [ 33 2 5108 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 29 [ 44 2 4538 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 30 [ 45 3 16674 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 31 [ 41 8 30635 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 32 [ 32 4 16251 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 33 [ 42 2 4356 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 34 [ 55 3 7136 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 35 [ 33 6 22758 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 36 [ 45 1 2802 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 37 [ 47 2 5060 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 38 [ 57 1 2806 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 39 [ 40 1 2123 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 40 [ 44 1 1382 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 41 [ 65 1 1372 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 42 [ 58 2 5593 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 19.86/20.09 Stopped by limit on insertions
% 19.86/20.09
% 19.86/20.09 Model 43 [ 43 4 14608 ] (0.00 seconds, 250000 Inserts)
% 19.86/20.09
% 22.27/22.46 St
% 22.27/22.46
% 22.27/22.46 Changing weight limit from 60 to 58.
% 22.27/22.46 opped by limit on insertions
% 22.27/22.46
% 22.27/22.46 Model 44 [ 59 2 4332 ] (0.00 seconds, 250000 Inserts)
% 22.27/22.46
% 22.27/22.46 Stopped by limit on insertions
% 22.27/22.46
% 22.27/22.46 Model 45 [ 55 2 2814 ] (0.00 seconds, 250000 Inserts)
% 22.27/22.46
% 22.27/22.46 Stopped by limit on insertions
% 22.27/22.46
% 22.27/22.46 Model 46 [ 64 2 4904 ] (0.00 seconds, 250000 Inserts)
% 22.27/22.46
% 22.27/22.46 Stopped by limit on insertions
% 22.27/22.46
% 22.27/22.46 Stopped by limit on insertions
% 22.27/22.46
% 22.27/22.46 Resetting weight limit to 58 after 110 givens.
% 22.27/22.46
% 24.17/24.41
% 24.17/24.41
% 24.17/24.41 Changing weight limit from 58 to 37.
% 24.17/24.41
% 24.17/24.41 Stopped by limit on insertions
% 24.17/24.41
% 24.17/24.41 Model 47 [ 40 1 1373 ] (0.00 seconds, 250000 Inserts)
% 24.17/24.41
% 24.17/24.41 Resetting weight limit to 37 after 135 givens.
% 24.17/24.41
% 28.75/28.96
% 28.75/28.96
% 28.75/28.96 Changing weight limit from 37 to 16.
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Model 48 [ 55 1 2084 ] (0.00 seconds, 250000 Inserts)
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Model 49 [ 55 8 43222 ] (0.00 seconds, 250000 Inserts)
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Model 50 [ 63 2 3871 ] (0.00 seconds, 250000 Inserts)
% 28.75/28.96
% 28.75/28.96 Stopped by limit on insertions
% 28.75/28.96
% 28.75/28.96 Resetting weight limit to 16 after 170 givens.
% 28.75/28.96
% 60.96/61.19
% 60.96/61.19
% 60.96/61.19 Changing weight limit from 16 to 15.
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 51 [ 55 1 2351 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 52 [ 39 3 9887 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 53 [ 38 3 7722 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 54 [ 53 1 3657 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 55 [ 69 4 20034 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 56 [ 54 13 47881 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 57 [ 82 4 23352 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 58 [ 59 2 1362 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 59 [ 89 4 22665 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 60 [ 63 4 12877 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 61 [ 113 2 2220 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 62 [ 54 6 23887 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 63 [ 87 2 2797 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 64 [ 52 5 13669 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 65 [ 111 2 4799 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 66 [ 70 2 1357 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 67 [ 54 2 2308 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 68 [ 98 2 1374 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 69 [ 72 2 1375 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 70 [ 97 2 2801 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 71 [ 59 2 1383 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 72 [ 61 7 23093 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 73 [ 84 1 1364 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 74 [ 84 2 1360 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 75 [ 67 2 2329 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 76 [ 84 3 4271 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 77 [ 92 2 1386 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 78 [ 76 3 5815 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 79 [ 61 5 15711 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 80 [ 60 3 7564 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Stopped by limit on insertions
% 60.96/61.19
% 60.96/61.19 Model 81 [ 105 3 2083 ] (0.00 seconds, 250000 Inserts)
% 60.96/61.19
% 60.96/61.19 Resetting weight limit to 15 after 370 givens.
% 60.96/61.19
% 61.09/61.29
% 61.09/61.29
% 61.09/61.29 Changing weight limit from 15 to 14.
% 61.09/61.29
% 61.09/61.29 Resetting weight limit to 14 after 375 givens.
% 61.09/61.29
% 62.29/62.51
% 62.29/62.51
% 62.29/62.51 Changing weight limit from 14 to 13.
% 62.29/62.51
% 62.29/62.51 Stopped by limit on insertions
% 62.29/62.51
% 62.29/62.51 Model 82 [ 105 2 1907 ] (0.00 seconds, 250000 Inserts)
% 62.29/62.51
% 62.29/62.51 Resetting weight limit to 13 after 385 givens.
% 62.29/62.51
% 62.44/62.63 member(infinity,intersection(complement(complement(universal_set)),complement(f24(universal_set)))).
% 62.44/62.63
% 62.44/62.63 ------------- memory usage ------------
% 62.44/62.63 353 mallocs of 32700 bytes each, 11272.6 K.
% 62.44/62.63 type (bytes each) gets frees in use avail bytes
% 62.44/62.63 sym_ent ( 304) 190 0 190 0 56.4 K
% 62.44/62.63 term ( 32) 7840264 7825336 14928 16148 971.1 K
% 62.44/62.63 rel ( 40) 7285623 7263914 21709 26076 1866.6 K
% 62.44/62.63 term_ptr ( 16) 1189843 1104961 84882 199032 4436.2 K
% 62.44/62.63 formula_ptr_2 ( 56) 0 0 0 0 0.0 K
% 62.44/62.63 fpa_head ( 24) 38669 29214 9455 1480 256.3 K
% 62.44/62.63 fpa_tree ( 56) 2230000 2230000 0 1447 79.1 K
% 62.44/62.63 context (1288) 429336 429336 0 8 10.1 K
% 62.44/62.63 trail ( 24) 8960022 8960022 0 14 0.3 K
% 62.44/62.63 imd_tree ( 32) 37 0 37 0 1.2 K
% 62.44/62.63 imd_pos (4024) 66079 66079 0 5 19.6 K
% 62.44/62.63 is_tree ( 24) 66678 56844 9834 11626 503.0 K
% 62.44/62.63 is_pos (2424) 3284821 3284821 0 25 59.2 K
% 62.44/62.63 fsub_pos ( 16) 256899 256899 0 1 0.0 K
% 62.44/62.63 literal ( 32) 259488 249026 10462 6404 527.1 K
% 62.44/62.63 clause ( 88) 112884 106903 5981 3504 815.1 K
% 62.44/62.63 list ( 272) 10 3 7 1 2.1 K
% 62.44/62.63 clash_nd ( 80) 15557 15557 0 5 0.4 K
% 62.44/62.63 clause_ptr ( 16) 31829 25947 5882 3476 146.2 K
% 62.44/62.63 int_ptr ( 16) 715579 678318 37261 21013 910.5 K
% 62.44/62.63 ci_ptr ( 24) 0 0 0 0 0.0 K
% 62.44/62.63 link_node ( 120) 0 0 0 0 0.0 K
% 62.44/62.63 ans_lit_node( 24) 0 0 0 0 0.0 K
% 62.44/62.63 formula_box( 168) 0 0 0 0 0.0 K
% 62.44/62.63 formula( 40) 0 0 0 0 0.0 K
% 62.44/62.63 formula_ptr( 16) 0 0 0 0 0.0 K
% 62.44/62.63 cl_attribute( 24) 0 0 0 0 0.0 K
% 62.44/62.63
% 62.44/62.63 ********** is_delete, can't find end.
% 62.44/62.63 0.00
% 62.44/62.63 back demod time 0.00
% 62.44/62.63 back subsume 0.00
% 62.44/62.63 factor time 0.00
% 62.44/62.63 FINDER time 0.00
% 62.44/62.63 unindex time 0.00
% 62.44/62.63
% 62.44/62.63 ----------- soft-scott stats ----------
% 62.44/62.63
% 62.44/62.63 true clauses given 109 (27.9%)
% 62.44/62.63 false clauses given 282
% 62.44/62.63
% 62.44/62.63 FALSE TRUE
% 62.44/62.63 5 0 5
% 62.44/62.63 6 50 211
% 62.44/62.63 7 269 249
% 62.44/62.63 8 333 546
% 62.44/62.63 9 673 1228
% 62.44/62.63 10 443 267
% 62.44/62.63 11 493 22
% 62.44/62.63 12 223 3
% 62.44/62.63 13 36 4
% 62.44/62.63 tot: 2520 2535 (50.1% true)
% 62.44/62.63
% 62.44/62.63
% 62.44/62.63 Model 82 [ 105 2 1907 ] (0.00 seconds, 250000 Inserts)
% 62.44/62.63
% 62.44/62.63 Forward subsumption counts, subsumer:number_subsumed.
% 62.44/62.63 1:0 2:6 3:1 4:3 5:3 6:1 7:1 8:0 9:0 10:0
% 62.44/62.63 11:2 12:2 13:0 14:0 15:2 16:0 17:2 18:2 19:0 20:0
% 62.44/62.63 21:2 22:0 23:1 24:3 25:5 26:1 27:1 28:3 29:1 30:5
% 62.44/62.63 31:2 32:2 33:0 34:3 35:3 36:1 37:2 38:2 39:5 40:1
% 62.44/62.63 41:0 42:0 43:2 44:2 45:2 46:0 47:0 48:0 49:0 50:2
% 62.44/62.63 51:2 52:2 53:0 54:0 55:0 56:0 57:377 58:8 59:0 60:2
% 62.44/62.63 61:2 62:3 63:1 64:0 65:1 66:0 67:0 68:0 69:1 70:3
% 62.44/62.63 71:1 72:0 73:1 74:0 75:0 76:1 77:0 78:0 79:0 80:2
% 62.44/62.63 81:2 82:3 83:3 84:5 85:1 86:0 87:8 88:0 89:2 90:2
% 62.44/62.63 91:0 92:3 93:3 94:1 95:0 96:2 97:0 98:4 99:0
% 62.44/62.63 All others: 17239.
% 62.44/62.63
% 62.44/62.63 ********** ABNORMAL END **********
% 62.44/62.63
% 62.44/62.63 ********** is_delete, can't find end.
%------------------------------------------------------------------------------