%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : FLD062-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n022.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:57 EDT 2022
% Result : Unsatisfiable 66.77s 66.95s
% Output : Refutation 66.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : FLD062-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% 0.12/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n022.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Tue Jun 7 02:23:20 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.20/0.35 ----- Otter 3.2, August 2001 -----
% 0.20/0.35 The process was started by sandbox2 on n022.cluster.edu,
% 0.20/0.35 Tue Jun 7 02:23:20 2022
% 0.20/0.35 The command was "./sos". The process ID is 8008.
% 0.20/0.35
% 0.20/0.35 set(prolog_style_variables).
% 0.20/0.35 set(auto).
% 0.20/0.35 dependent: set(auto1).
% 0.20/0.35 dependent: set(process_input).
% 0.20/0.35 dependent: clear(print_kept).
% 0.20/0.35 dependent: clear(print_new_demod).
% 0.20/0.35 dependent: clear(print_back_demod).
% 0.20/0.35 dependent: clear(print_back_sub).
% 0.20/0.35 dependent: set(control_memory).
% 0.20/0.35 dependent: assign(max_mem, 12000).
% 0.20/0.35 dependent: assign(pick_given_ratio, 4).
% 0.20/0.35 dependent: assign(stats_level, 1).
% 0.20/0.35 dependent: assign(pick_semantic_ratio, 3).
% 0.20/0.35 dependent: assign(sos_limit, 5000).
% 0.20/0.35 dependent: assign(max_weight, 60).
% 0.20/0.35 clear(print_given).
% 0.20/0.35
% 0.20/0.35 list(usable).
% 0.20/0.35
% 0.20/0.35 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5.
% 0.20/0.35
% 0.20/0.35 This is a non-Horn set without equality. The strategy
% 0.20/0.35 will be ordered hyper_res, ur_res, unit deletion, and
% 0.20/0.35 factoring, with satellites in sos and nuclei in usable.
% 0.20/0.35
% 0.20/0.35 dependent: set(hyper_res).
% 0.20/0.35 dependent: set(factor).
% 0.20/0.35 dependent: set(unit_deletion).
% 0.20/0.35
% 0.20/0.35 ------------> process usable:
% 0.20/0.35
% 0.20/0.35 ------------> process sos:
% 0.20/0.35
% 0.20/0.35 ======= end of input processing =======
% 0.20/0.43
% 0.20/0.43 Model 1 (0.00 seconds, 0 Inserts)
% 0.20/0.43
% 0.20/0.43 Stopped by limit on number of solutions
% 0.20/0.43
% 0.20/0.43
% 0.20/0.43 -------------- Softie stats --------------
% 0.20/0.43
% 0.20/0.43 UPDATE_STOP: 300
% 0.20/0.43 SFINDER_TIME_LIMIT: 2
% 0.20/0.43 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.43 number of clauses in intial UL: 48
% 0.20/0.43 number of clauses initially in problem: 53
% 0.20/0.43 percentage of clauses intially in UL: 90
% 0.20/0.43 percentage of distinct symbols occuring in initial UL: 100
% 0.20/0.43 percent of all initial clauses that are short: 100
% 0.20/0.43 absolute distinct symbol count: 12
% 0.20/0.43 distinct predicate count: 4
% 0.20/0.43 distinct function count: 4
% 0.20/0.43 distinct constant count: 4
% 0.20/0.43
% 0.20/0.43 ---------- no more Softie stats ----------
% 0.20/0.43
% 0.20/0.43
% 0.20/0.43
% 0.20/0.43 Model 2 (0.00 seconds, 0 Inserts)
% 0.20/0.43
% 0.20/0.43 Stopped by limit on number of solutions
% 0.20/0.43
% 0.20/0.43 =========== start of search ===========
% 3.88/4.05
% 3.88/4.05
% 3.88/4.05 Changing weight limit from 60 to 14.
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 3 [ 1 2 349 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 4 [ 2 2 186 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 5 [ 2 2 1061 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 6 [ 3 1 351 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 7 [ 3 1 646 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 8 [ 4 2 313 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 9 [ 3 1 273 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 10 [ 4 1 285 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 11 [ 8 1 147 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 12 [ 5 1 111 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 13 [ 4 2 274 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 14 [ 5 1 356 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 15 [ 4 2 245 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 16 [ 6 1 159 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 17 [ 5 1 402 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 18 [ 17 1 215 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 19 [ 7 2 163 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 20 [ 5 2 296 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 21 [ 18 2 168 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 22 [ 7 2 1132 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 23 [ 9 3 42598 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 24 [ 8 1 2297 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 25 [ 6 2 467 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 26 [ 8 1 144 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 27 [ 23 1 110 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 28 [ 6 1 177 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 29 [ 6 2 907 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 30 [ 9 2 448 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 31 [ 5 2 158 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 32 [ 8 1 150 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 33 [ 24 1 110 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Stopped by limit on insertions
% 3.88/4.05
% 3.88/4.05 Model 34 [ 10 2 191 ] (0.00 seconds, 250000 Inserts)
% 3.88/4.05
% 3.88/4.05 Resetting weight limit to 14 after 40 givens.
% 3.88/4.05
% 5.46/5.69
% 5.46/5.69
% 5.46/5.69 Changing weight limit from 14 to 12.
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 35 [ 25 2 121 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 36 [ 4 1 602 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 37 [ 9 3 18478 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 38 [ 4 1 420 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 39 [ 11 2 3055 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 40 [ 7 10 172712 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Stopped by limit on insertions
% 5.46/5.69
% 5.46/5.69 Model 41 [ 6 1 374 ] (0.00 seconds, 250000 Inserts)
% 5.46/5.69
% 5.46/5.69 Resetting weight limit to 12 after 50 givens.
% 5.46/5.69
% 6.36/6.60
% 6.36/6.60
% 6.36/6.60 Changing weight limit from 12 to 10.
% 6.36/6.60
% 6.36/6.60 Stopped by limit on insertions
% 6.36/6.60
% 6.36/6.60 Model 42 [ 10 5 70861 ] (0.00 seconds, 250000 Inserts)
% 6.36/6.60
% 6.36/6.60 Stopped by limit on insertions
% 6.36/6.60
% 6.36/6.60 Model 43 [ 5 9 88464 ] (0.00 seconds, 250000 Inserts)
% 6.36/6.60
% 6.36/6.60 Stopped by limit on insertions
% 6.36/6.60
% 6.36/6.60 Model 44 [ 5 2 522 ] (0.00 seconds, 250000 Inserts)
% 6.36/6.60
% 6.36/6.60 Stopped by limit on insertions
% 6.36/6.60
% 6.36/6.60 Model 45 [ 8 3 19295 ] (0.00 seconds, 250000 Inserts)
% 6.36/6.60
% 6.36/6.60 Resetting weight limit to 10 after 55 givens.
% 6.36/6.60
% 15.20/15.36
% 15.20/15.36
% 15.20/15.36 Changing weight limit from 10 to 8.
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 46 [ 8 12 94108 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 47 [ 40 2 109 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 48 [ 13 1 530 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 49 [ 15 1 145 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 50 [ 4 13 160055 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 51 [ 12 34 227173 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 52 [ 41 1 139 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 53 [ 11 2 617 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 54 [ 42 2 148 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 55 [ 5 1 117 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 56 [ 48 1 102 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 57 [ 14 2 4186 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 58 [ 16 2 861 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 59 [ 12 25 173728 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 60 [ 15 2 4634 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 61 [ 48 2 213 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 62 [ 9 11 93792 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 63 [ 53 1 317 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 64 [ 21 35 213405 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 65 [ 55 2 155 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 66 [ 10 8 53285 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 67 [ 20 1 134 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 68 [ 45 2 289 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 69 [ 49 3 15865 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Stopped by limit on insertions
% 15.20/15.36
% 15.20/15.36 Model 70 [ 8 2 579 ] (0.00 seconds, 250000 Inserts)
% 15.20/15.36
% 15.20/15.36 Resetting weight limit to 8 after 105 givens.
% 15.20/15.36
% 15.52/15.68
% 15.52/15.68
% 15.52/15.68 Changing weight limit from 8 to 9.
% 15.52/15.68
% 15.52/15.68 Stopped by limit on insertions
% 15.52/15.68
% 15.52/15.68 Model 71 [ 16 2 233 ] (0.00 seconds, 250000 Inserts)
% 15.52/15.68
% 15.52/15.68 Resetting weight limit to 9 after 110 givens.
% 15.52/15.68
% 16.15/16.32
% 16.15/16.32
% 16.15/16.32 Changing weight limit from 9 to 8.
% 16.15/16.32
% 16.15/16.32 Stopped by limit on insertions
% 16.15/16.32
% 16.15/16.32 Model 72 [ 19 29 199884 ] (0.00 seconds, 250000 Inserts)
% 16.15/16.32
% 16.15/16.32 Stopped by limit on insertions
% 16.15/16.32
% 16.15/16.32 Model 73 [ 10 2 441 ] (0.00 seconds, 250000 Inserts)
% 16.15/16.32
% 16.15/16.32 Resetting weight limit to 8 after 115 givens.
% 16.15/16.32
% 16.45/16.62
% 16.45/16.62
% 16.45/16.62 Changing weight limit from 8 to 9.
% 16.45/16.62
% 16.45/16.62 Stopped by limit on insertions
% 16.45/16.62
% 16.45/16.62 Model 74 [ 10 2 182 ] (0.00 seconds, 250000 Inserts)
% 16.45/16.62
% 16.45/16.62 Resetting weight limit to 9 after 120 givens.
% 16.45/16.62
% 18.37/18.59
% 18.37/18.59
% 18.37/18.59 Changing weight limit from 9 to 8.
% 18.37/18.59
% 18.37/18.59 Stopped by limit on insertions
% 18.37/18.59
% 18.37/18.59 Model 75 [ 51 2 3884 ] (0.00 seconds, 250000 Inserts)
% 18.37/18.59
% 18.37/18.59 Stopped by limit on insertions
% 18.37/18.59
% 18.37/18.59 Model 76 [ 17 13 99825 ] (0.00 seconds, 250000 Inserts)
% 18.37/18.59
% 18.37/18.59 Stopped by limit on insertions
% 18.37/18.59
% 18.37/18.59 Model 77 [ 61 84 229815 ] (0.00 seconds, 250000 Inserts)
% 18.37/18.59
% 18.37/18.59 Resetting weight limit to 8 after 140 givens.
% 18.37/18.59
% 18.67/18.87
% 18.67/18.87
% 18.67/18.87 Changing weight limit from 8 to 9.
% 18.67/18.87
% 18.67/18.87 Stopped by limit on insertions
% 18.67/18.87
% 18.67/18.87 Model 78 [ 20 2 134 ] (0.00 seconds, 250000 Inserts)
% 18.67/18.87
% 18.67/18.87 Resetting weight limit to 9 after 145 givens.
% 18.67/18.87
% 25.50/25.69
% 25.50/25.69
% 25.50/25.69 Changing weight limit from 9 to 8.
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 79 [ 67 2 2545 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 80 [ 18 1 4239 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 81 [ 65 1 203 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 82 [ 12 14 102106 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 83 [ 70 2 373 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 84 [ 63 2 948 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 85 [ 21 1 623 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 86 [ 66 2 1823 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 87 [ 74 2 285 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 88 [ 20 13 116732 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Stopped by limit on insertions
% 25.50/25.69
% 25.50/25.69 Model 89 [ 84 2 104 ] (0.00 seconds, 250000 Inserts)
% 25.50/25.69
% 25.50/25.69 Resetting weight limit to 8 after 170 givens.
% 25.50/25.69
% 26.45/26.69
% 26.45/26.69
% 26.45/26.69 Changing weight limit from 8 to 9.
% 26.45/26.69
% 26.45/26.69 Stopped by limit on insertions
% 26.45/26.69
% 26.45/26.69 Model 90 [ 14 2 179 ] (0.00 seconds, 250000 Inserts)
% 26.45/26.69
% 26.45/26.69 Stopped by limit on insertions
% 26.45/26.69
% 26.45/26.69 Model 91 [ 14 1 169 ] (0.00 seconds, 250000 Inserts)
% 26.45/26.69
% 26.45/26.69 Stopped by limit on insertions
% 26.45/26.69
% 26.45/26.69 Model 92 [ 15 1 149 ] (0.00 seconds, 250000 Inserts)
% 26.45/26.69
% 26.45/26.69 Resetting weight limit to 9 after 175 givens.
% 26.45/26.69
% 28.21/28.49
% 28.21/28.49
% 28.21/28.49 Changing weight limit from 9 to 10.
% 28.21/28.49
% 28.21/28.49 Stopped by limit on insertions
% 28.21/28.49
% 28.21/28.49 Model 93 [ 77 4 4377 ] (0.00 seconds, 250000 Inserts)
% 28.21/28.49
% 28.21/28.49 Stopped by limit on insertions
% 28.21/28.49
% 28.21/28.49 Stopped by limit on insertions
% 28.21/28.49
% 28.21/28.49 Model 94 [ 18 2 161 ] (0.00 seconds, 250000 Inserts)
% 28.21/28.49
% 28.21/28.49 Resetting weight limit to 10 after 185 givens.
% 28.21/28.49
% 29.65/29.88
% 29.65/29.88
% 29.65/29.88 Changing weight limit from 10 to 8.
% 29.65/29.88
% 29.65/29.88 Stopped by limit on insertions
% 29.65/29.88
% 29.65/29.88 Model 95 [ 15 2 130 ] (0.00 seconds, 250000 Inserts)
% 29.65/29.88
% 29.65/29.88 Stopped by limit on insertions
% 29.65/29.88
% 29.65/29.88 Model 96 [ 18 2 224 ] (0.00 seconds, 250000 Inserts)
% 29.65/29.88
% 29.65/29.88 Stopped by limit on insertions
% 29.65/29.88
% 29.65/29.88 Model 97 [ 30 1 141 ] (0.00 seconds, 250000 Inserts)
% 29.65/29.88
% 29.65/29.88 Resetting weight limit to 8 after 200 givens.
% 29.65/29.88
% 33.47/33.68
% 33.47/33.68
% 33.47/33.68 Changing weight limit from 8 to 9.
% 33.47/33.68
% 33.47/33.68 Stopped by limit on insertions
% 33.47/33.68
% 33.47/33.68 Model 98 [ 91 1 198 ] (0.00 seconds, 250000 Inserts)
% 33.47/33.68
% 33.47/33.68 Stopped by limit on insertions
% 33.47/33.68
% 33.47/33.69 Model 99 [ 18 2 456 ] (0.00 seconds, 250000 Inserts)
% 33.47/33.69
% 33.47/33.69 Stopped by limit on insertions
% 33.47/33.69
% 33.47/33.69 Model 100 [ 78 1 200 ] (0.00 seconds, 250000 Inserts)
% 33.47/33.69
% 33.47/33.69 Stopped by limit on insertions
% 33.47/33.69
% 33.47/33.69 Model 101 [ 18 18 48775 ] (0.00 seconds, 250000 Inserts)
% 33.47/33.69
% 33.47/33.69 Stopped by limit on insertions
% 33.47/33.69
% 33.47/33.69 Model 102 [ 23 64 183037 ] (0.00 seconds, 250000 Inserts)
% 33.47/33.69
% 33.47/33.69 Resetting weight limit to 9 after 210 givens.
% 33.47/33.69
% 40.73/40.93
% 40.73/40.93
% 40.73/40.93 Changing weight limit from 9 to 8.
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 103 [ 25 2 876 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 104 [ 77 2 195 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 105 [ 20 2 150 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 106 [ 85 2 244 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 107 [ 20 22 226053 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 108 [ 12 14 61582 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 109 [ 13 9 25806 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Stopped by limit on insertions
% 40.73/40.93
% 40.73/40.93 Model 110 [ 86 2 200 ] (0.00 seconds, 250000 Inserts)
% 40.73/40.93
% 40.73/40.93 Resetting weight limit to 8 after 280 givens.
% 40.73/40.93
% 42.27/42.48
% 42.27/42.48
% 42.27/42.48 Changing weight limit from 8 to 9.
% 42.27/42.48
% 42.27/42.48 Stopped by limit on insertions
% 42.27/42.48
% 42.27/42.48 Model 111 [ 25 2 1123 ] (0.00 seconds, 250000 Inserts)
% 42.27/42.48
% 42.27/42.48 Stopped by limit on insertions
% 42.27/42.48
% 42.27/42.48 Model 112 [ 14 2 2869 ] (0.00 seconds, 250000 Inserts)
% 42.27/42.48
% 42.27/42.48 Resetting weight limit to 9 after 285 givens.
% 42.27/42.48
% 43.62/43.84
% 43.62/43.84
% 43.62/43.84 Changing weight limit from 9 to 8.
% 43.62/43.84
% 43.62/43.84 Stopped by limit on insertions
% 43.62/43.84
% 43.62/43.84 Model 113 [ 19 51 198466 ] (0.00 seconds, 250000 Inserts)
% 43.62/43.84
% 43.62/43.84 Stopped by limit on insertions
% 43.62/43.84
% 43.62/43.84 Model 114 [ 21 2 144 ] (0.00 seconds, 250000 Inserts)
% 43.62/43.84
% 43.62/43.84 Resetting weight limit to 8 after 320 givens.
% 43.62/43.84
% 49.51/49.76
% 49.51/49.76
% 49.51/49.76 Changing weight limit from 8 to 7.
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 115 [ 35 21 47526 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 116 [ 26 2 118 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 117 [ 105 2 417 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 118 [ 110 2 114 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 119 [ 85 43 90853 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Stopped by limit on insertions
% 49.51/49.76
% 49.51/49.76 Model 120 [ 14 3 6668 ] (0.00 seconds, 250000 Inserts)
% 49.51/49.76
% 49.51/49.76 Resetting weight limit to 7 after 340 givens.
% 49.51/49.76
% 50.93/51.12
% 50.93/51.12
% 50.93/51.12 Changing weight limit from 7 to 8.
% 50.93/51.12
% 50.93/51.12 Stopped by limit on insertions
% 50.93/51.12
% 50.93/51.12 Model 121 [ 100 2 139 ] (0.00 seconds, 250000 Inserts)
% 50.93/51.12
% 50.93/51.12 Resetting weight limit to 8 after 345 givens.
% 50.93/51.12
% 51.64/51.84
% 51.64/51.84
% 51.64/51.84 Changing weight limit from 8 to 9.
% 51.64/51.84
% 51.64/51.84 Stopped by limit on insertions
% 51.64/51.84
% 51.64/51.84 Model 122 [ 33 1 152 ] (0.00 seconds, 250000 Inserts)
% 51.64/51.84
% 51.64/51.84 Resetting weight limit to 9 after 350 givens.
% 51.64/51.84
% 53.19/53.45
% 53.19/53.45
% 53.19/53.45 Changing weight limit from 9 to 10.
% 53.19/53.45
% 53.19/53.45 Stopped by limit on insertions
% 53.19/53.45
% 53.19/53.45 Model 123 [ 49 45 122461 ] (0.00 seconds, 250000 Inserts)
% 53.19/53.45
% 53.19/53.45 Stopped by limit on insertions
% 53.19/53.45
% 53.19/53.45 Model 124 [ 19 2 481 ] (0.00 seconds, 250000 Inserts)
% 53.19/53.45
% 53.19/53.45 Resetting weight limit to 10 after 355 givens.
% 53.19/53.45
% 56.21/56.45
% 56.21/56.45
% 56.21/56.45 Changing weight limit from 10 to 9.
% 56.21/56.45
% 56.21/56.45 Stopped by limit on insertions
% 56.21/56.45
% 56.21/56.45 Model 125 [ 25 22 135196 ] (0.00 seconds, 250000 Inserts)
% 56.21/56.45
% 56.21/56.45 Stopped by limit on insertions
% 56.21/56.45
% 56.21/56.45 Model 126 [ 22 68 181186 ] (0.00 seconds, 250000 Inserts)
% 56.21/56.45
% 56.21/56.45 Stopped by limit on insertions
% 56.21/56.45
% 56.21/56.45 Model 127 [ 48 16 40023 ] (0.00 seconds, 250000 Inserts)
% 56.21/56.45
% 56.21/56.45 Modelling stopped after 300 given clauses and 0.00 seconds
% 56.21/56.45
% 56.21/56.45
% 56.21/56.45 Resetting weight limit to 9 after 500 givens.
% 56.21/56.45
% 66.25/66.48
% 66.25/66.48
% 66.25/66.48 Changing weight limit from 9 to 8.
% 66.25/66.48
% 66.25/66.48 Resetting weight limit to 8 after 1530 givens.
% 66.25/66.48
% 66.77/66.95
% 66.77/66.95 -- HEY sandbox2, WE HAVE A PROOF!! --
% 66.77/66.95
% 66.77/66.95 ----> UNIT CONFLICT at 64.19 sec ----> 68552 [binary,68551.1,25.1] {+} $F.
% 66.77/66.95
% 66.77/66.95 Length of proof is 22. Level of proof is 8.
% 66.77/66.95
% 66.77/66.95 ---------------- PROOF ----------------
% 66.77/66.95 % SZS status Unsatisfiable
% 66.77/66.95 % SZS output start Refutation
% 66.77/66.95
% 66.77/66.95 1 [] {+} sum(A,B,C)| -sum(A,D,E)| -sum(D,F,B)| -sum(E,F,C).
% 66.77/66.95 2 [] {+} sum(A,B,C)| -sum(D,E,A)| -sum(E,B,F)| -sum(D,F,C).
% 66.77/66.95 3 [] {+} sum(additive_identity,A,A)| -defined(A).
% 66.77/66.95 4 [] {+} sum(additive_inverse(A),A,additive_identity)| -defined(A).
% 66.77/66.95 5 [] {+} sum(A,B,C)| -sum(B,A,C).
% 66.77/66.95 14 [] {+} defined(additive_inverse(A))| -defined(A).
% 66.77/66.95 17 [] {+} sum(A,B,add(A,B))| -defined(A)| -defined(B).
% 66.77/66.95 19 [] {+} sum(additive_identity,A,B)| -less_or_equal(A,B)| -less_or_equal(B,A).
% 66.77/66.95 21 [] {+} less_or_equal(A,B)|less_or_equal(B,A)| -defined(A)| -defined(B).
% 66.77/66.95 22 [] {+} less_or_equal(A,B)| -less_or_equal(C,D)| -sum(C,E,A)| -sum(D,E,B).
% 66.77/66.95 25 [] {+} -less_or_equal(additive_inverse(b),additive_inverse(a)).
% 66.77/66.95 44 [factor,21.1.2,factor_simp] {+} less_or_equal(A,A)| -defined(A).
% 66.77/66.95 49 [] {+} defined(additive_identity).
% 66.77/66.95 51 [] {+} defined(a).
% 66.77/66.95 52 [] {+} defined(b).
% 66.77/66.95 53 [] {+} less_or_equal(a,b).
% 66.77/66.95 54 [hyper,49,44] {+} less_or_equal(additive_identity,additive_identity).
% 66.77/66.95 105 [hyper,51,14] {+} defined(additive_inverse(a)).
% 66.77/66.95 112 [hyper,51,4] {+} sum(additive_inverse(a),a,additive_identity).
% 66.77/66.95 113 [hyper,51,3] {+} sum(additive_identity,a,a).
% 66.77/66.95 130 [hyper,52,17,51] {+} sum(b,a,add(b,a)).
% 66.77/66.95 140 [hyper,52,14] {+} defined(additive_inverse(b)).
% 66.77/66.95 149 [hyper,52,4] {+} sum(additive_inverse(b),b,additive_identity).
% 66.77/66.95 150 [hyper,52,3] {+} sum(additive_identity,b,b).
% 66.77/66.95 197 [hyper,105,3] {+} sum(additive_identity,additive_inverse(a),additive_inverse(a)).
% 66.77/66.95 259 [hyper,140,21,105,unit_del,25] {-} less_or_equal(additive_inverse(a),additive_inverse(b)).
% 66.77/66.95 318 [hyper,140,3] {+} sum(additive_identity,additive_inverse(b),additive_inverse(b)).
% 66.77/66.95 6093 [hyper,112,5] {+} sum(a,additive_inverse(a),additive_identity).
% 66.77/66.95 17836 [hyper,130,5] {-} sum(a,b,add(b,a)).
% 66.77/66.95 17838 [hyper,130,1,149,113] {-} sum(additive_inverse(b),add(b,a),a).
% 66.77/66.95 26376 [hyper,318,5] {-} sum(additive_inverse(b),additive_identity,additive_inverse(b)).
% 66.77/66.95 48367 [hyper,17836,1,112,150] {-} sum(additive_inverse(a),add(b,a),b).
% 66.77/66.95 66098 [hyper,48367,22,259,17838] {-} less_or_equal(b,a).
% 66.77/66.95 66140 [hyper,66098,19,53] {-} sum(additive_identity,a,b).
% 66.77/66.95 66184 [hyper,66140,2,26376,149] {-} sum(additive_inverse(b),a,additive_identity).
% 66.77/66.95 66874 [hyper,66184,2,6093,26376] {-} sum(additive_identity,additive_inverse(a),additive_inverse(b)).
% 66.77/66.95 68551 [hyper,66874,22,54,197] {-} less_or_equal(additive_inverse(b),additive_inverse(a)).
% 66.77/66.95 68552 [binary,68551.1,25.1] {+} $F.
% 66.77/66.95
% 66.77/66.95 % SZS output end Refutation
% 66.77/66.95 ------------ end of proof -------------
% 66.77/66.95
% 66.77/66.95
% 66.77/66.95 Search stopped by max_proofs option.
% 66.77/66.95
% 66.77/66.95
% 66.77/66.95 Search stopped by max_proofs option.
% 66.77/66.95
% 66.77/66.95 ============ end of search ============
% 66.77/66.95
% 66.77/66.95 ----------- soft-scott stats ----------
% 66.77/66.95
% 66.77/66.95 true clauses given 533 (32.3%)
% 66.77/66.95 false clauses given 1117
% 66.77/66.95
% 66.77/66.95 FALSE TRUE
% 66.77/66.95 6 5 437
% 66.77/66.95 7 104 1504
% 66.77/66.95 8 2391 559
% 66.77/66.95 tot: 2500 2500 (50.0% true)
% 66.77/66.95
% 66.77/66.95
% 66.77/66.95 Model 127 [ 48 16 40023 ] (0.00 seconds, 250000 Inserts)
% 66.77/66.95
% 66.77/66.95 That finishes the proof of the theorem.
% 66.77/66.95
% 66.77/66.95 Process 8008 finished Tue Jun 7 02:24:27 2022
%------------------------------------------------------------------------------