%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : FLD061-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n024.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:56 EDT 2022
% Result : Unsatisfiable 139.42s 139.62s
% Output : Refutation 139.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : FLD061-3 : TPTP v8.1.0. Bugfixed v2.1.0.
% 0.04/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n024.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 : Mon Jun 6 23:29:20 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.20/0.36 ----- Otter 3.2, August 2001 -----
% 0.20/0.36 The process was started by sandbox on n024.cluster.edu,
% 0.20/0.36 Mon Jun 6 23:29:20 2022
% 0.20/0.36 The command was "./sos". The process ID is 26219.
% 0.20/0.36
% 0.20/0.36 set(prolog_style_variables).
% 0.20/0.36 set(auto).
% 0.20/0.36 dependent: set(auto1).
% 0.20/0.36 dependent: set(process_input).
% 0.20/0.36 dependent: clear(print_kept).
% 0.20/0.36 dependent: clear(print_new_demod).
% 0.20/0.36 dependent: clear(print_back_demod).
% 0.20/0.36 dependent: clear(print_back_sub).
% 0.20/0.36 dependent: set(control_memory).
% 0.20/0.36 dependent: assign(max_mem, 12000).
% 0.20/0.36 dependent: assign(pick_given_ratio, 4).
% 0.20/0.36 dependent: assign(stats_level, 1).
% 0.20/0.36 dependent: assign(pick_semantic_ratio, 3).
% 0.20/0.36 dependent: assign(sos_limit, 5000).
% 0.20/0.36 dependent: assign(max_weight, 60).
% 0.20/0.36 clear(print_given).
% 0.20/0.36
% 0.20/0.36 list(usable).
% 0.20/0.36
% 0.20/0.36 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5.
% 0.20/0.36
% 0.20/0.36 This is a non-Horn set without equality. The strategy
% 0.20/0.36 will be ordered hyper_res, ur_res, unit deletion, and
% 0.20/0.36 factoring, with satellites in sos and nuclei in usable.
% 0.20/0.36
% 0.20/0.36 dependent: set(hyper_res).
% 0.20/0.36 dependent: set(factor).
% 0.20/0.36 dependent: set(unit_deletion).
% 0.20/0.36
% 0.20/0.36 ------------> process usable:
% 0.20/0.36
% 0.20/0.36 ------------> process sos:
% 0.20/0.36
% 0.20/0.36 ======= end of input processing =======
% 0.20/0.44
% 0.20/0.44 Model 1 (0.00 seconds, 0 Inserts)
% 0.20/0.44
% 0.20/0.44 Stopped by limit on number of solutions
% 0.20/0.44
% 0.20/0.44
% 0.20/0.44 -------------- Softie stats --------------
% 0.20/0.44
% 0.20/0.44 UPDATE_STOP: 300
% 0.20/0.44 SFINDER_TIME_LIMIT: 2
% 0.20/0.44 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.44 number of clauses in intial UL: 48
% 0.20/0.44 number of clauses initially in problem: 56
% 0.20/0.44 percentage of clauses intially in UL: 85
% 0.20/0.44 percentage of distinct symbols occuring in initial UL: 100
% 0.20/0.44 percent of all initial clauses that are short: 100
% 0.20/0.44 absolute distinct symbol count: 14
% 0.20/0.44 distinct predicate count: 4
% 0.20/0.44 distinct function count: 4
% 0.20/0.44 distinct constant count: 6
% 0.20/0.44
% 0.20/0.44 ---------- no more Softie stats ----------
% 0.20/0.44
% 0.20/0.44
% 0.20/0.44
% 0.20/0.44 Model 2 (0.00 seconds, 0 Inserts)
% 0.20/0.44
% 0.20/0.44 Stopped by limit on number of solutions
% 0.20/0.44
% 0.20/0.44 =========== start of search ===========
% 3.10/3.29
% 3.10/3.29
% 3.10/3.29 Changing weight limit from 60 to 15.
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 3 [ 1 2 2537 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 4 [ 1 1 2731 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 5 [ 1 3 40537 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 6 [ 2 2 175 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 7 [ 2 2 371 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 8 [ 3 8 246210 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 9 [ 3 1 987 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 10 [ 3 1 507 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 11 [ 2 4 187127 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 12 [ 8 2 109 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 13 [ 4 1 137 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 14 [ 4 1 106 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 15 [ 10 2 187 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 16 [ 3 1 155 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 17 [ 3 2 160 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 18 [ 4 1 199 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 19 [ 5 1 384 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 20 [ 7 1 429 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 21 [ 6 1 130 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 22 [ 3 2 510 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 23 [ 4 2 39726 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 24 [ 4 3 54812 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 25 [ 4 6 88831 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 26 [ 3 1 113 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 27 [ 4 1 1868 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 28 [ 7 1 1111 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 29 [ 4 2 191 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 30 [ 6 5 116223 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Stopped by limit on insertions
% 3.10/3.29
% 3.10/3.29 Model 31 [ 6 10 247473 ] (0.00 seconds, 250000 Inserts)
% 3.10/3.29
% 3.10/3.29 Resetting weight limit to 15 after 40 givens.
% 3.10/3.29
% 4.90/5.08
% 4.90/5.08
% 4.90/5.08 Changing weight limit from 15 to 10.
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 32 [ 5 11 165524 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 33 [ 3 3 16852 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 34 [ 4 3 21041 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 35 [ 5 2 2789 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 36 [ 3 2 23167 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 37 [ 6 2 788 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Stopped by limit on insertions
% 4.90/5.08
% 4.90/5.08 Model 38 [ 7 1 579 ] (0.00 seconds, 250000 Inserts)
% 4.90/5.08
% 4.90/5.08 Resetting weight limit to 10 after 50 givens.
% 4.90/5.08
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 39 [ 3 3 6421 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 40 [ 8 3 13620 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 41 [ 6 7 71941 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 42 [ 9 13 104966 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 43 [ 7 8 45707 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 44 [ 40 2 126 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 45 [ 10 4 23860 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 46 [ 41 1 400 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 47 [ 7 1 361 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 48 [ 11 32 232820 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 49 [ 7 10 72421 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 50 [ 9 7 40571 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 51 [ 12 27 137982 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 52 [ 9 4 20892 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 53 [ 16 40 221005 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 54 [ 9 12 59954 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 55 [ 13 16 94248 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 56 [ 14 9 45345 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 57 [ 10 3 6895 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 58 [ 12 5 17474 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 59 [ 12 23 177101 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 60 [ 10 2 6827 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 61 [ 15 2 6819 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 62 [ 11 39 214161 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 63 [ 13 2 750 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 64 [ 65 1 141 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 65 [ 18 43 227440 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 66 [ 15 6 22560 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 67 [ 12 19 88041 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 68 [ 18 2 222 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 69 [ 13 2 341 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 70 [ 11 20 113925 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 71 [ 18 1 255 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 72 [ 69 2 106 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 73 [ 63 1 221 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 74 [ 14 18 70601 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 75 [ 18 37 170420 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 76 [ 21 17 85157 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 77 [ 14 3 10670 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 78 [ 9 2 825 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 79 [ 14 1 250 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 80 [ 15 2 160 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 81 [ 22 26 89349 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 27.76/27.94 Model 82 [ 71 2 232 ] (0.00 seconds, 250000 Inserts)
% 27.76/27.94
% 27.76/27.94 Stopped by limit on insertions
% 27.76/27.94
% 57.31/57.55 Model 83 [ 15 1 4
% 57.31/57.55
% 57.31/57.55 Changing weight limit from 10 to 9.
% 57.31/57.55 97 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 84 [ 80 1 416 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 85 [ 16 2 232 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 86 [ 79 18 52862 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 87 [ 15 65 225179 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 88 [ 18 1 652 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 89 [ 76 2 209 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 90 [ 13 7 21812 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 91 [ 83 13 36325 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 92 [ 20 2 238 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 93 [ 10 2 316 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 94 [ 15 44 191270 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 95 [ 18 39 154778 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 96 [ 15 2 674 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 97 [ 78 1 140 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 98 [ 23 11 37222 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 99 [ 88 2 245 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 100 [ 21 50 171220 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 101 [ 19 34 114151 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 102 [ 21 68 221742 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 103 [ 15 2 366 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 104 [ 86 2 108 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 105 [ 19 57 163743 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 106 [ 27 94 244870 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 107 [ 14 9 32264 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 108 [ 17 2 1219 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 109 [ 19 57 181116 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 110 [ 20 39 146968 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 111 [ 87 2 104 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 112 [ 20 6 13350 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 113 [ 22 80 213696 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 114 [ 25 62 203293 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 115 [ 17 2 209 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 116 [ 90 2 408 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 117 [ 98 5 6254 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 118 [ 17 16 45453 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Stopped by limit on insertions
% 57.31/57.55
% 57.31/57.55 Model 119 [ 17 19 58309 ] (0.00 seconds, 250000 Inserts)
% 57.31/57.55
% 57.31/57.55 Resetting weight limit to 9 after 195 givens.
% 57.31/57.55
% 74.42/74.60
% 74.42/74.60
% 74.42/74.60 Changing weight limit from 9 to 7.
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 120 [ 21 25 62971 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 121 [ 26 2 270 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 122 [ 103 2 265 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 123 [ 22 6 15901 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 124 [ 22 73 145851 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 125 [ 18 2 383 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 126 [ 122 1 189 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 127 [ 22 40 86021 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 128 [ 111 2 122 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 129 [ 98 3 2260 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 130 [ 123 2 193 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 131 [ 37 26 48938 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 132 [ 20 2 317 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Stopped by limit on insertions
% 74.42/74.60
% 74.42/74.60 Model 133 [ 121 2 168 ] (0.00 seconds, 250000 Inserts)
% 74.42/74.60
% 74.42/74.60 Resetting weight limit to 7 after 260 givens.
% 74.42/74.60
% 79.64/79.88
% 79.64/79.88
% 79.64/79.88 Changing weight limit from 7 to 8.
% 79.64/79.88
% 79.64/79.88 Stopped by limit on insertions
% 79.64/79.88
% 79.64/79.88 Model 134 [ 113 2 163 ] (0.00 seconds, 250000 Inserts)
% 79.64/79.88
% 79.64/79.88 Stopped by limit on insertions
% 79.64/79.88
% 79.64/79.88 Model 135 [ 44 25 47366 ] (0.00 seconds, 250000 Inserts)
% 79.64/79.88
% 79.64/79.88 Stopped by limit on insertions
% 79.64/79.88
% 79.64/79.88 Model 136 [ 20 2 1487 ] (0.00 seconds, 250000 Inserts)
% 79.64/79.88
% 79.64/79.88 Stopped by limit on insertions
% 79.64/79.88
% 79.64/79.88 Model 137 [ 31 40 79445 ] (0.00 seconds, 250000 Inserts)
% 79.64/79.88
% 79.64/79.88 Resetting weight limit to 8 after 265 givens.
% 79.64/79.88
% 83.52/83.71
% 83.52/83.71
% 83.52/83.71 Changing weight limit from 8 to 9.
% 83.52/83.71
% 83.52/83.71 Stopped by limit on insertions
% 83.52/83.71
% 83.52/83.71 Model 138 [ 126 2 309 ] (0.00 seconds, 250000 Inserts)
% 83.52/83.71
% 83.52/83.71 Stopped by limit on insertions
% 83.52/83.71
% 83.52/83.71 Model 139 [ 21 2 227 ] (0.00 seconds, 250000 Inserts)
% 83.52/83.71
% 83.52/83.71 Stopped by limit on insertions
% 83.52/83.71
% 83.52/83.71 Model 140 [ 29 2 878 ] (0.00 seconds, 250000 Inserts)
% 83.52/83.71
% 83.52/83.71 Resetting weight limit to 9 after 270 givens.
% 83.52/83.71
% 127.90/128.15
% 127.90/128.15
% 127.90/128.15 Changing weight limit from 9 to 8.
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 141 [ 19 2 477 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 142 [ 44 108 203874 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 143 [ 22 55 140306 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 144 [ 134 16 21796 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 145 [ 36 16 32758 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 146 [ 110 5 5098 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 147 [ 21 2 284 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 148 [ 26 51 107618 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 149 [ 132 31 42522 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 150 [ 26 43 80244 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 151 [ 113 2 206 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 152 [ 26 68 168527 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 153 [ 25 14 22189 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 154 [ 21 9 15520 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 155 [ 37 3 305 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 156 [ 26 2 245 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 157 [ 18 26 54814 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 158 [ 144 2 180 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 159 [ 40 2 140 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 160 [ 25 2 198 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 161 [ 25 125 217367 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 162 [ 129 3 169 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 163 [ 21 13 20219 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 164 [ 122 2 175 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 165 [ 141 3 1445 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 166 [ 24 57 112905 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 167 [ 144 2 161 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Stopped by limit on insertions
% 127.90/128.15
% 127.90/128.15 Model 168 [ 25 132 228267 ] (0.00 seconds, 250000 Inserts)
% 127.90/128.15
% 127.90/128.15 Modelling stopped after 300 given clauses and 0.00 seconds
% 127.90/128.15
% 127.90/128.15
% 127.90/128.15 Resetting weight limit to 8 after 750 givens.
% 127.90/128.15
% 139.42/139.62
% 139.42/139.62 -- HEY sandbox, WE HAVE A PROOF!! --
% 139.42/139.62
% 139.42/139.62 ----> UNIT CONFLICT at 136.20 sec ----> 121902 [binary,121901.1,25.1] {+} $F.
% 139.42/139.62
% 139.42/139.62 Length of proof is 7. Level of proof is 4.
% 139.42/139.62
% 139.42/139.62 ---------------- PROOF ----------------
% 139.42/139.62 % SZS status Unsatisfiable
% 139.42/139.62 % SZS output start Refutation
% 139.42/139.62
% 139.42/139.62 5 [] {+} sum(A,B,C)| -sum(B,A,C).
% 139.42/139.62 17 [] {+} sum(A,B,add(A,B))| -defined(A)| -defined(B).
% 139.42/139.62 20 [] {+} less_or_equal(A,B)| -less_or_equal(A,C)| -less_or_equal(C,B).
% 139.42/139.62 22 [] {+} less_or_equal(A,B)| -less_or_equal(C,D)| -sum(C,E,A)| -sum(D,E,B).
% 139.42/139.62 25 [] {+} -less_or_equal(add(a,c),add(d,b)).
% 139.42/139.62 51 [] {+} defined(a).
% 139.42/139.62 52 [] {+} defined(b).
% 139.42/139.62 53 [] {+} defined(c).
% 139.42/139.62 54 [] {+} defined(d).
% 139.42/139.62 55 [] {+} less_or_equal(a,b).
% 139.42/139.62 56 [] {+} less_or_equal(c,d).
% 139.42/139.62 131 [hyper,53,17,51] {+} sum(a,c,add(a,c)).
% 139.42/139.62 171 [hyper,52,17,53] {+} sum(c,b,add(c,b)).
% 139.42/139.62 226 [hyper,54,17,52] {-} sum(d,b,add(d,b)).
% 139.42/139.62 65766 [hyper,171,5] {-} sum(b,c,add(c,b)).
% 139.42/139.62 76134 [hyper,226,22,56,171] {-} less_or_equal(add(c,b),add(d,b)).
% 139.42/139.62 115941 [hyper,65766,22,55,131] {-} less_or_equal(add(a,c),add(c,b)).
% 139.42/139.62 121901 [hyper,115941,20,76134] {-} less_or_equal(add(a,c),add(d,b)).
% 139.42/139.62 121902 [binary,121901.1,25.1] {+} $F.
% 139.42/139.62
% 139.42/139.62 % SZS output end Refutation
% 139.42/139.62 ------------ end of proof -------------
% 139.42/139.62
% 139.42/139.62
% 139.42/139.62 Search stopped by max_proofs option.
% 139.42/139.62
% 139.42/139.62
% 139.42/139.62 Search stopped by max_proofs option.
% 139.42/139.62
% 139.42/139.62 ============ end of search ============
% 139.42/139.62
% 139.42/139.62 ----------- soft-scott stats ----------
% 139.42/139.62
% 139.42/139.62 true clauses given 563 (34.8%)
% 139.42/139.62 false clauses given 1055
% 139.42/139.62
% 139.42/139.62 FALSE TRUE
% 139.42/139.62 6 0 1896
% 139.42/139.62 7 26 517
% 139.42/139.62 8 2478 131
% 139.42/139.62 tot: 2504 2544 (50.4% true)
% 139.42/139.62
% 139.42/139.62
% 139.42/139.62 Model 168 [ 25 132 228267 ] (0.00 seconds, 250000 Inserts)
% 139.42/139.62
% 139.42/139.62 That finishes the proof of the theorem.
% 139.42/139.62
% 139.42/139.62 Process 26219 finished Mon Jun 6 23:31:39 2022
%------------------------------------------------------------------------------