%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : FLD013-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n027.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 : Sat Jul 16 02:27:36 EDT 2022
% Result : Unsatisfiable 115.94s 116.20s
% Output : Refutation 115.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : FLD013-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% 0.08/0.15 % Command : sos-script %s
% 0.14/0.36 % Computer : n027.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Tue Jun 7 03:53:40 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.14/0.38 ----- Otter 3.2, August 2001 -----
% 0.14/0.38 The process was started by sandbox on n027.cluster.edu,
% 0.14/0.38 Tue Jun 7 03:53:40 2022
% 0.14/0.38 The command was "./sos". The process ID is 27482.
% 0.14/0.38
% 0.14/0.38 set(prolog_style_variables).
% 0.14/0.38 set(auto).
% 0.14/0.38 dependent: set(auto1).
% 0.14/0.38 dependent: set(process_input).
% 0.14/0.38 dependent: clear(print_kept).
% 0.14/0.38 dependent: clear(print_new_demod).
% 0.14/0.38 dependent: clear(print_back_demod).
% 0.14/0.38 dependent: clear(print_back_sub).
% 0.14/0.38 dependent: set(control_memory).
% 0.14/0.38 dependent: assign(max_mem, 12000).
% 0.14/0.38 dependent: assign(pick_given_ratio, 4).
% 0.14/0.38 dependent: assign(stats_level, 1).
% 0.14/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.14/0.38 dependent: assign(sos_limit, 5000).
% 0.14/0.38 dependent: assign(max_weight, 60).
% 0.14/0.38 clear(print_given).
% 0.14/0.38
% 0.14/0.38 list(usable).
% 0.14/0.38
% 0.14/0.38 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5.
% 0.14/0.38
% 0.14/0.38 This is a non-Horn set without equality. The strategy
% 0.14/0.38 will be ordered hyper_res, ur_res, unit deletion, and
% 0.14/0.38 factoring, with satellites in sos and nuclei in usable.
% 0.14/0.38
% 0.14/0.38 dependent: set(hyper_res).
% 0.14/0.38 dependent: set(factor).
% 0.14/0.38 dependent: set(unit_deletion).
% 0.14/0.38
% 0.14/0.38 ------------> process usable:
% 0.14/0.38
% 0.14/0.38 ------------> process sos:
% 0.14/0.38
% 0.14/0.38 ======= end of input processing =======
% 0.21/0.47
% 0.21/0.47 Model 1 (0.00 seconds, 0 Inserts)
% 0.21/0.47
% 0.21/0.47 Stopped by limit on number of solutions
% 0.21/0.47
% 0.21/0.47
% 0.21/0.47 -------------- Softie stats --------------
% 0.21/0.47
% 0.21/0.47 UPDATE_STOP: 300
% 0.21/0.47 SFINDER_TIME_LIMIT: 2
% 0.21/0.47 SHORT_CLAUSE_CUTOFF: 4
% 0.21/0.47 number of clauses in intial UL: 48
% 0.21/0.47 number of clauses initially in problem: 56
% 0.21/0.47 percentage of clauses intially in UL: 85
% 0.21/0.47 percentage of distinct symbols occuring in initial UL: 100
% 0.21/0.47 percent of all initial clauses that are short: 100
% 0.21/0.47 absolute distinct symbol count: 14
% 0.21/0.47 distinct predicate count: 4
% 0.21/0.47 distinct function count: 4
% 0.21/0.47 distinct constant count: 6
% 0.21/0.47
% 0.21/0.47 ---------- no more Softie stats ----------
% 0.21/0.47
% 0.21/0.47
% 0.21/0.47
% 0.21/0.47 Model 2 (0.00 seconds, 0 Inserts)
% 0.21/0.47
% 0.21/0.47 Stopped by limit on number of solutions
% 0.21/0.47
% 0.21/0.47 =========== start of search ===========
% 3.64/3.84
% 3.64/3.84
% 3.64/3.84 Changing weight limit from 60 to 14.
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 3 [ 1 1 179 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 4 [ 1 1 233 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 5 [ 1 1 113 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 6 [ 2 1 105 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 7 [ 2 1 534 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 8 [ 3 1 164 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 9 [ 2 1 429 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 10 [ 3 2 155 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 11 [ 4 1 142 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 12 [ 8 1 183 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 13 [ 3 1 168 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 14 [ 3 1 126 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 15 [ 5 2 371 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 16 [ 3 1 188 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 17 [ 5 1 173 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 18 [ 5 2 392 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 19 [ 6 1 11641 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 20 [ 4 1 436 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 21 [ 15 2 126 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 22 [ 3 1 415 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 23 [ 4 1 4882 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 24 [ 4 2 159 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 25 [ 2 2 209 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 26 [ 5 2 170 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 27 [ 3 1 161 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 28 [ 7 7 210059 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 29 [ 5 4 97877 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 30 [ 5 1 535 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 31 [ 3 2 781 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 32 [ 5 2 734 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 33 [ 27 2 209 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Stopped by limit on insertions
% 3.64/3.84
% 3.64/3.84 Model 34 [ 7 1 273 ] (0.00 seconds, 250000 Inserts)
% 3.64/3.84
% 3.64/3.84 Resetting weight limit to 14 after 40 givens.
% 3.64/3.84
% 6.90/7.12
% 6.90/7.12
% 6.90/7.12 Changing weight limit from 14 to 10.
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 35 [ 7 2 21530 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 36 [ 11 5 91484 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 37 [ 9 1 5807 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 38 [ 6 2 11662 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 39 [ 6 1 665 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 40 [ 34 2 210 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 41 [ 9 4 67185 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 42 [ 38 2 116 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 43 [ 8 2 888 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 44 [ 9 1 177 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 45 [ 37 2 193 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 46 [ 9 1 3794 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 47 [ 8 6 72634 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Stopped by limit on insertions
% 6.90/7.12
% 6.90/7.12 Model 48 [ 11 7 110461 ] (0.00 seconds, 250000 Inserts)
% 6.90/7.12
% 6.90/7.12 Resetting weight limit to 10 after 60 givens.
% 6.90/7.12
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 49 [ 12 16 164914 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 50 [ 4 1 211 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 51 [ 43 1 168 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 52 [ 12 16 178827 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 53 [ 46 1 189 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 54 [ 10 17 206674 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 55 [ 4 1 180 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 56 [ 10 1 593 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 57 [ 42 2 341 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 58 [ 11 20 180165 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 59 [ 5 1 719 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 60 [ 53 1 255 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 61 [ 9 1 224 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 62 [ 14 19 152332 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 63 [ 12 28 235632 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 64 [ 6 1 178 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 65 [ 9 1 214 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 66 [ 8 1 736 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 67 [ 24 17 137372 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 68 [ 7 1 175 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 69 [ 64 1 232 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 70 [ 9 3 12236 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 71 [ 59 2 106 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 72 [ 7 2 5385 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 73 [ 16 3 5059 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 74 [ 17 15 87711 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 75 [ 22 17 101857 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 76 [ 7 2 258 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 77 [ 12 4 19080 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 78 [ 22 3 9014 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 79 [ 21 12 60416 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 80 [ 73 1 195 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 81 [ 22 37 195102 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 82 [ 14 22 121551 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 83 [ 13 2 1023 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 84 [ 71 2 417 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 85 [ 13 13 83056 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 86 [ 12 2 673 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 87 [ 72 2 3718 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 88 [ 10 1 123 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 89 [ 85 1 133 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 90 [ 8 2 844 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 91 [ 20 8 27755 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 92 [ 11 7 37370 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 93 [ 13 2 128 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 25.64/25.84 Model 94 [ 83 1 106 ] (0.00 seconds, 250000 Inserts)
% 25.64/25.84
% 25.64/25.84 Stopped by limit on insertions
% 25.64/25.84
% 28.89/29.11 Model 95 [ 12 8 36078 ] (
% 28.89/29.11
% 28.89/29.11 Changing weight limit from 10 to 8.
% 28.89/29.11 0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Stopped by limit on insertions
% 28.89/29.11
% 28.89/29.11 Model 96 [ 15 54 220049 ] (0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Stopped by limit on insertions
% 28.89/29.11
% 28.89/29.11 Model 97 [ 9 2 572 ] (0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Stopped by limit on insertions
% 28.89/29.11
% 28.89/29.11 Model 98 [ 18 1 119 ] (0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Stopped by limit on insertions
% 28.89/29.11
% 28.89/29.11 Model 99 [ 95 1 177 ] (0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Stopped by limit on insertions
% 28.89/29.11
% 28.89/29.11 Model 100 [ 13 21 72672 ] (0.00 seconds, 250000 Inserts)
% 28.89/29.11
% 28.89/29.11 Resetting weight limit to 8 after 125 givens.
% 28.89/29.11
% 52.72/52.98
% 52.72/52.98
% 52.72/52.98 Changing weight limit from 8 to 7.
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 101 [ 17 1 155 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 102 [ 13 35 128644 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 103 [ 20 2 364 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 104 [ 15 2 176 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 105 [ 20 2 143 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 106 [ 76 2 386 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 107 [ 21 2 233 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 108 [ 22 39 164290 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 109 [ 26 2 396 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 110 [ 22 5 11700 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 111 [ 98 1 182 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 112 [ 13 1 554 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 113 [ 28 2 1767 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 114 [ 20 1 116 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 115 [ 20 13 34033 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 116 [ 15 1 133 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 117 [ 85 5 9058 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 118 [ 24 42 125645 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 119 [ 15 2 349 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 120 [ 18 66 234617 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 121 [ 21 6 15107 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 122 [ 13 2 571 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 123 [ 96 1 304 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 124 [ 106 2 175 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 125 [ 30 53 139662 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 126 [ 99 1 104 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 127 [ 23 82 247350 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 128 [ 105 2 114 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 129 [ 23 2 3451 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Stopped by limit on insertions
% 52.72/52.98
% 52.72/52.98 Model 130 [ 25 1 158 ] (0.00 seconds, 250000 Inserts)
% 52.72/52.98
% 52.72/52.98 Resetting weight limit to 7 after 185 givens.
% 52.72/52.98
% 57.97/58.23
% 57.97/58.23
% 57.97/58.23 Changing weight limit from 7 to 8.
% 57.97/58.23
% 57.97/58.23 Stopped by limit on insertions
% 57.97/58.23
% 57.97/58.23 Model 131 [ 102 14 32112 ] (0.00 seconds, 250000 Inserts)
% 57.97/58.23
% 57.97/58.23 Stopped by limit on insertions
% 57.97/58.23
% 57.97/58.23 Model 132 [ 21 2 332 ] (0.00 seconds, 250000 Inserts)
% 57.97/58.23
% 57.97/58.23 Stopped by limit on insertions
% 57.97/58.23
% 57.97/58.23 Model 133 [ 110 2 313 ] (0.00 seconds, 250000 Inserts)
% 57.97/58.23
% 57.97/58.23 Stopped by limit on insertions
% 57.97/58.23
% 57.97/58.23 Resetting weight limit to 8 after 190 givens.
% 57.97/58.23
% 61.39/61.65
% 61.39/61.65
% 61.39/61.65 Changing weight limit from 8 to 9.
% 61.39/61.65
% 61.39/61.65 Stopped by limit on insertions
% 61.39/61.65
% 61.39/61.65 Stopped by limit on insertions
% 61.39/61.65
% 61.39/61.65 Model 134 [ 29 34 99556 ] (0.00 seconds, 250000 Inserts)
% 61.39/61.65
% 61.39/61.65 Stopped by limit on insertions
% 61.39/61.65
% 61.39/61.65 Resetting weight limit to 9 after 195 givens.
% 61.39/61.65
% 64.43/64.62
% 64.43/64.62
% 64.43/64.62 Changing weight limit from 9 to 8.
% 64.43/64.62
% 64.43/64.62 Stopped by limit on insertions
% 64.43/64.62
% 64.43/64.62 Model 135 [ 26 15 29831 ] (0.00 seconds, 250000 Inserts)
% 64.43/64.62
% 64.43/64.62 Stopped by limit on insertions
% 64.43/64.62
% 64.43/64.62 Stopped by limit on insertions
% 64.43/64.62
% 64.43/64.62 Model 136 [ 99 5 5576 ] (0.00 seconds, 250000 Inserts)
% 64.43/64.62
% 64.43/64.62 Resetting weight limit to 8 after 215 givens.
% 64.43/64.62
% 84.55/84.82
% 84.55/84.82
% 84.55/84.82 Changing weight limit from 8 to 7.
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 137 [ 22 2 550 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 138 [ 120 2 211 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 139 [ 136 2 170 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 140 [ 21 2 225 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 141 [ 127 2 115 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 142 [ 111 2 195 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 143 [ 39 3 1854 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 144 [ 29 8 14415 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 145 [ 100 2 652 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 146 [ 29 34 67978 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 147 [ 16 2 301 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 148 [ 26 3 3336 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 149 [ 45 51 94994 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 150 [ 34 2 131 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 151 [ 117 2 127 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Stopped by limit on insertions
% 84.55/84.82
% 84.55/84.82 Model 152 [ 23 85 171810 ] (0.00 seconds, 250000 Inserts)
% 84.55/84.82
% 84.55/84.82 Resetting weight limit to 7 after 255 givens.
% 84.55/84.82
% 86.18/86.39
% 86.18/86.39
% 86.18/86.39 Changing weight limit from 7 to 8.
% 86.18/86.39
% 86.18/86.39 Stopped by limit on insertions
% 86.18/86.39
% 86.18/86.39 Model 153 [ 106 2 393 ] (0.00 seconds, 250000 Inserts)
% 86.18/86.39
% 86.18/86.39 Resetting weight limit to 8 after 265 givens.
% 86.18/86.39
% 89.81/90.03
% 89.81/90.03
% 89.81/90.03 Changing weight limit from 8 to 9.
% 89.81/90.03
% 89.81/90.03 Stopped by limit on insertions
% 89.81/90.03
% 89.81/90.03 Model 154 [ 123 2 268 ] (0.00 seconds, 250000 Inserts)
% 89.81/90.03
% 89.81/90.03 Stopped by limit on insertions
% 89.81/90.03
% 89.81/90.03 Model 155 [ 34 28 47897 ] (0.00 seconds, 250000 Inserts)
% 89.81/90.03
% 89.81/90.03 Stopped by limit on insertions
% 89.81/90.03
% 89.81/90.03 Resetting weight limit to 9 after 275 givens.
% 89.81/90.03
% 91.62/91.80
% 91.62/91.80
% 91.62/91.80 Changing weight limit from 9 to 7.
% 91.62/91.80
% 91.62/91.80 Stopped by limit on insertions
% 91.62/91.80
% 91.62/91.80 Model 156 [ 129 2 247 ] (0.00 seconds, 250000 Inserts)
% 91.62/91.80
% 91.62/91.80 Resetting weight limit to 7 after 280 givens.
% 91.62/91.80
% 100.06/100.26
% 100.06/100.26
% 100.06/100.26 Changing weight limit from 7 to 8.
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 157 [ 112 2 220 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 158 [ 17 53 121596 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 159 [ 116 14 19144 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 160 [ 22 34 68009 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 161 [ 29 2 137 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Stopped by limit on insertions
% 100.06/100.26
% 100.06/100.26 Model 162 [ 103 26 36007 ] (0.00 seconds, 250000 Inserts)
% 100.06/100.26
% 100.06/100.26 Resetting weight limit to 8 after 305 givens.
% 100.06/100.26
% 101.41/101.63
% 101.41/101.63
% 101.41/101.63 Changing weight limit from 8 to 7.
% 101.41/101.63
% 101.41/101.63 Stopped by limit on insertions
% 101.41/101.63
% 101.41/101.63 Model 163 [ 24 102 193386 ] (0.00 seconds, 250000 Inserts)
% 101.41/101.63
% 101.41/101.63 Resetting weight limit to 7 after 310 givens.
% 101.41/101.63
% 105.83/106.09
% 105.83/106.09
% 105.83/106.09 Changing weight limit from 7 to 8.
% 105.83/106.09
% 105.83/106.09 Stopped by limit on insertions
% 105.83/106.09
% 105.83/106.09 Model 164 [ 150 2 225 ] (0.00 seconds, 250000 Inserts)
% 105.83/106.09
% 105.83/106.09 Stopped by limit on insertions
% 105.83/106.09
% 105.83/106.09 Model 165 [ 26 5 5211 ] (0.00 seconds, 250000 Inserts)
% 105.83/106.09
% 105.83/106.09 Stopped by limit on insertions
% 105.83/106.09
% 105.83/106.09 Model 166 [ 123 2 211 ] (0.00 seconds, 250000 Inserts)
% 105.83/106.09
% 105.83/106.09 Resetting weight limit to 8 after 320 givens.
% 105.83/106.09
% 109.43/109.67
% 109.43/109.67
% 109.43/109.67 Changing weight limit from 8 to 9.
% 109.43/109.67
% 109.43/109.67 Stopped by limit on insertions
% 109.43/109.67
% 109.43/109.67 Model 167 [ 27 27 68553 ] (0.00 seconds, 250000 Inserts)
% 109.43/109.67
% 109.43/109.67 Stopped by limit on insertions
% 109.43/109.67
% 109.43/109.67 Model 168 [ 30 90 142362 ] (0.00 seconds, 250000 Inserts)
% 109.43/109.67
% 109.43/109.67 Stopped by limit on insertions
% 109.43/109.67
% 109.43/109.67 Model 169 [ 29 4 4570 ] (0.00 seconds, 250000 Inserts)
% 109.43/109.67
% 109.43/109.67 Resetting weight limit to 9 after 325 givens.
% 109.43/109.67
% 115.94/116.20
% 115.94/116.20 -- HEY sandbox, WE HAVE A PROOF!! --
% 115.94/116.20
% 115.94/116.20 Stopped by limit on insertions
% 115.94/116.20
% 115.94/116.20 Model 170 [ 32 41 86181 ] (0.00 seconds, 250000 Inserts)
% 115.94/116.20
% 115.94/116.20 Stopped by limit on insertions
% 115.94/116.20
% 115.94/116.20 Model 171 [ 148 2 117 ] (0.00 seconds, 250000 Inserts)
% 115.94/116.20
% 115.94/116.20 Stopped by limit on insertions
% 115.94/116.20
% 115.94/116.20 Model 172 [ 21 2 276 ] (0.00 seconds, 250000 Inserts)
% 115.94/116.20
% 115.94/116.20 Stopped by limit on insertions
% 115.94/116.20
% 115.94/116.20 Model 173 [ 28 65 103003 ] (0.00 seconds, 250000 Inserts)
% 115.94/116.20
% 115.94/116.20 Modelling stopped after 300 given clauses and 0.00 seconds
% 115.94/116.20
% 115.94/116.20
% 115.94/116.20 ----> UNIT CONFLICT at 115.57 sec ----> 59061 [binary,59060.1,25.1] {+} $F.
% 115.94/116.20
% 115.94/116.20 Length of proof is 9. Level of proof is 5.
% 115.94/116.20
% 115.94/116.20 ---------------- PROOF ----------------
% 115.94/116.20 % SZS status Unsatisfiable
% 115.94/116.20 % SZS output start Refutation
% 115.94/116.20
% 115.94/116.20 1 [] {+} sum(A,B,C)| -sum(A,D,E)| -sum(D,F,B)| -sum(E,F,C).
% 115.94/116.20 2 [] {+} sum(A,B,C)| -sum(D,E,A)| -sum(E,B,F)| -sum(D,F,C).
% 115.94/116.20 3 [] {+} sum(additive_identity,A,A)| -defined(A).
% 115.94/116.20 4 [] {+} sum(additive_inverse(A),A,additive_identity)| -defined(A).
% 115.94/116.20 5 [] {+} sum(A,B,C)| -sum(B,A,C).
% 115.94/116.20 17 [] {+} sum(A,B,add(A,B))| -defined(A)| -defined(B).
% 115.94/116.20 25 [] {+} -sum(a,c,add(d,b)).
% 115.94/116.20 49 [] {+} defined(additive_identity).
% 115.94/116.20 51 [] {+} defined(a).
% 115.94/116.20 52 [] {+} defined(b).
% 115.94/116.20 53 [] {+} defined(c).
% 115.94/116.20 54 [] {+} defined(d).
% 115.94/116.20 55 [] {+} sum(additive_identity,a,b).
% 115.94/116.20 56 [] {+} sum(additive_identity,c,d).
% 115.94/116.20 66 [hyper,49,4] {+} sum(additive_inverse(additive_identity),additive_identity,additive_identity).
% 115.94/116.20 154 [hyper,51,3] {+} sum(additive_identity,a,a).
% 115.94/116.20 201 [hyper,53,3] {+} sum(additive_identity,c,c).
% 115.94/116.20 228 [hyper,54,17,52] {+} sum(d,b,add(d,b)).
% 115.94/116.20 3285 [hyper,66,1,56,201] {-} sum(additive_inverse(additive_identity),d,c).
% 115.94/116.20 7331 [hyper,154,1,66,55] {-} sum(additive_inverse(additive_identity),a,b).
% 115.94/116.20 31992 [hyper,3285,5] {-} sum(d,additive_inverse(additive_identity),c).
% 115.94/116.20 46611 [hyper,228,2,31992,7331] {-} sum(c,a,add(d,b)).
% 115.94/116.20 59060 [hyper,46611,5] {-} sum(a,c,add(d,b)).
% 115.94/116.20 59061 [binary,59060.1,25.1] {+} $F.
% 115.94/116.20
% 115.94/116.20 % SZS output end Refutation
% 115.94/116.20 ------------ end of proof -------------
% 115.94/116.20
% 115.94/116.20
% 115.94/116.20 Search stopped by max_proofs option.
% 115.94/116.20
% 115.94/116.20
% 115.94/116.20 Search stopped by max_proofs option.
% 115.94/116.20
% 115.94/116.20 ============ end of search ============
% 115.94/116.20
% 115.94/116.20 ----------- soft-scott stats ----------
% 115.94/116.20
% 115.94/116.20 true clauses given 143 (24.9%)
% 115.94/116.20 false clauses given 432
% 115.94/116.20
% 115.94/116.20 FALSE TRUE
% 115.94/116.20 5 0 103
% 115.94/116.20 6 29 2397
% 115.94/116.20 7 156 0
% 115.94/116.20 8 293 0
% 115.94/116.20 9 124 0
% 115.94/116.20 tot: 602 2500 (80.6% true)
% 115.94/116.20
% 115.94/116.20
% 115.94/116.20 Model 173 [ 28 65 103003 ] (0.00 seconds, 250000 Inserts)
% 115.94/116.20
% 115.94/116.20 That finishes the proof of the theorem.
% 115.94/116.20
% 115.94/116.20 Process 27482 finished Tue Jun 7 03:55:35 2022
%------------------------------------------------------------------------------