%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO194+3 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n026.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 06:18:59 EDT 2022
% Result : Theorem 136.42s 136.61s
% Output : Refutation 136.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : GEO194+3 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jun 18 06:54:09 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.35 ----- Otter 3.2, August 2001 -----
% 0.12/0.35 The process was started by sandbox2 on n026.cluster.edu,
% 0.12/0.35 Sat Jun 18 06:54:09 2022
% 0.12/0.35 The command was "./sos". The process ID is 5881.
% 0.12/0.35
% 0.12/0.35 set(prolog_style_variables).
% 0.12/0.35 set(auto).
% 0.12/0.35 dependent: set(auto1).
% 0.12/0.35 dependent: set(process_input).
% 0.12/0.35 dependent: clear(print_kept).
% 0.12/0.35 dependent: clear(print_new_demod).
% 0.12/0.35 dependent: clear(print_back_demod).
% 0.12/0.35 dependent: clear(print_back_sub).
% 0.12/0.35 dependent: set(control_memory).
% 0.12/0.35 dependent: assign(max_mem, 12000).
% 0.12/0.35 dependent: assign(pick_given_ratio, 4).
% 0.12/0.35 dependent: assign(stats_level, 1).
% 0.12/0.35 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.35 dependent: assign(sos_limit, 5000).
% 0.12/0.35 dependent: assign(max_weight, 60).
% 0.12/0.35 clear(print_given).
% 0.12/0.35
% 0.12/0.35 formula_list(usable).
% 0.12/0.35
% 0.12/0.35 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6.
% 0.12/0.35
% 0.12/0.35 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.35 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.35 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.35 clauses in usable.
% 0.12/0.35
% 0.12/0.35 dependent: set(knuth_bendix).
% 0.12/0.35 dependent: set(para_from).
% 0.12/0.35 dependent: set(para_into).
% 0.12/0.35 dependent: clear(para_from_right).
% 0.12/0.35 dependent: clear(para_into_right).
% 0.12/0.35 dependent: set(para_from_vars).
% 0.12/0.35 dependent: set(eq_units_both_ways).
% 0.12/0.35 dependent: set(dynamic_demod_all).
% 0.12/0.35 dependent: set(dynamic_demod).
% 0.12/0.35 dependent: set(order_eq).
% 0.12/0.35 dependent: set(back_demod).
% 0.12/0.35 dependent: set(lrpo).
% 0.12/0.35 dependent: set(hyper_res).
% 0.12/0.35 dependent: set(unit_deletion).
% 0.12/0.35 dependent: set(factor).
% 0.12/0.35
% 0.12/0.35 ------------> process usable:
% 0.12/0.35 Following clause subsumed by 15 during input processing: 0 [] {-} -distinct_lines(A,B)|apart_point_and_line(C,A)|apart_point_and_line(C,B)|convergent_lines(A,B).
% 0.12/0.35 Following clause subsumed by 6 during input processing: 0 [] {-} -convergent_lines(A,B)| -unorthogonal_lines(A,B)|convergent_lines(A,C)|convergent_lines(B,C).
% 0.12/0.35 28 back subsumes 27.
% 0.12/0.35
% 0.12/0.35 ------------> process sos:
% 0.12/0.35 Following clause subsumed by 39 during input processing: 0 [] {-} convergent_lines(A,B)|unorthogonal_lines(A,B).
% 0.12/0.35
% 0.12/0.35 ======= end of input processing =======
% 0.18/0.39
% 0.18/0.39 Model 1 (0.00 seconds, 0 Inserts)
% 0.18/0.39
% 0.18/0.39 Stopped by limit on number of solutions
% 0.18/0.39
% 0.18/0.39
% 0.18/0.39 -------------- Softie stats --------------
% 0.18/0.39
% 0.18/0.39 UPDATE_STOP: 300
% 0.18/0.39 SFINDER_TIME_LIMIT: 2
% 0.18/0.39 SHORT_CLAUSE_CUTOFF: 4
% 0.18/0.39 number of clauses in intial UL: 37
% 0.18/0.39 number of clauses initially in problem: 47
% 0.18/0.39 percentage of clauses intially in UL: 78
% 0.18/0.39 percentage of distinct symbols occuring in initial UL: 100
% 0.18/0.39 percent of all initial clauses that are short: 100
% 0.18/0.39 absolute distinct symbol count: 19
% 0.18/0.39 distinct predicate count: 12
% 0.18/0.39 distinct function count: 4
% 0.18/0.39 distinct constant count: 3
% 0.18/0.39
% 0.18/0.39 ---------- no more Softie stats ----------
% 0.18/0.39
% 0.18/0.39
% 0.18/0.39
% 0.18/0.39 Model 2 (0.00 seconds, 0 Inserts)
% 0.18/0.39
% 0.18/0.39 Stopped by limit on number of solutions
% 0.18/0.39
% 0.18/0.39 =========== start of search ===========
% 22.70/22.92
% 22.70/22.92 Model 3 (0.00 seconds, 0 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on number of solutions
% 22.70/22.92
% 22.70/22.92 Model 4 (0.00 seconds, 0 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on number of solutions
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 5 [ 1 0 944 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 6 [ 6 0 519 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 7 [ 1 0 1189 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 8 [ 15 0 623 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 9 [ 1 1 336 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 10 [ 15 1 460 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 11 [ 15 0 555 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 12 [ 15 1 249 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 13 [ 2 0 636 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 14 [ 18 0 357 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 15 [ 1 1 847 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 16 [ 22 0 247 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 17 [ 22 0 244 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 18 [ 16 1 190 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 19 [ 5 0 151 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 20 [ 25 1 359 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 21 [ 25 1 244 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 22 [ 29 0 457 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 23 [ 4 1 211 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 24 [ 34 1 3142 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 25 [ 21 0 606 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 26 [ 56 1 289 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 27 [ 21 1 570 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 28 [ 22 1 559 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 29 [ 34 1 281 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 30 [ 49 1 314 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 31 [ 23 1 958 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 32 [ 66 1 267 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 33 [ 34 0 158 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 34 [ 68 1 279 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 35 [ 24 1 177 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 36 [ 25 1 577 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 37 [ 55 0 444 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 38 [ 28 1 855 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 39 [ 73 1 284 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 40 [ 29 1 307 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 41 [ 76 0 404 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 42 [ 39 0 874 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 43 [ 65 1 314 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 44 [ 46 1 154 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 45 [ 86 1 446 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 46 [ 47 1 558 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 47 [ 87 0 420 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 22.70/22.92 Model 48 [ 73 1 440 ] (0.00 seconds, 250000 Inserts)
% 22.70/22.92
% 22.70/22.92 Stopped by limit on insertions
% 22.70/22.92
% 109.29/109.50 Model 49 [ 40 0 1281 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 50 [ 88 1 192 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 51 [ 42 0 562 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 52 [ 93 1 407 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 53 [ 43 0 157 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 54 [ 84 1 350 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 55 [ 97 1 514 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 56 [ 53 1 577 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 57 [ 105 1 308 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 58 [ 62 1 196 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 59 [ 120 1 758 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 60 [ 76 1 583 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 61 [ 75 0 158 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 62 [ 75 1 880 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 63 [ 99 1 471 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 64 [ 80 1 159 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 65 [ 129 1 562 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 66 [ 124 1 1070 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 67 [ 130 1 442 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 68 [ 140 1 398 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 69 [ 140 1 173 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 70 [ 128 1 431 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 71 [ 142 1 479 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 72 [ 142 1 359 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 73 [ 123 1 850 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 74 [ 126 1 567 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 75 [ 96 1 151 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 76 [ 157 1 444 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 77 [ 124 1 573 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 78 [ 122 1 575 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 79 [ 164 2 288 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 80 [ 130 2 860 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 81 [ 155 2 788 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 82 [ 112 2 151 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 83 [ 178 2 198 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 84 [ 141 1 765 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 85 [ 150 2 572 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 86 [ 185 2 276 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 87 [ 144 2 153 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 88 [ 193 2 780 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 89 [ 151 1 1088 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 90 [ 177 2 162 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 91 [ 210 2 812 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 92 [ 179 2 1202 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 93 [ 218 2 681 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 94 [ 205 2 585 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 109.29/109.50 Stopped by limit on insertions
% 109.29/109.50
% 109.29/109.50 Model 95 [ 178 2 277 ] (0.00 seconds, 250000 Inserts)
% 109.29/109.50
% 113.89/114.13 Stopped by limit on insertio
% 113.89/114.13
% 113.89/114.13 Changing weight limit from 60 to 25.
% 113.89/114.13 ns
% 113.89/114.13
% 113.89/114.13 Model 96 [ 205 2 293 ] (0.00 seconds, 250000 Inserts)
% 113.89/114.13
% 113.89/114.13 Stopped by limit on insertions
% 113.89/114.13
% 113.89/114.13 Model 97 [ 205 2 619 ] (0.00 seconds, 250000 Inserts)
% 113.89/114.13
% 113.89/114.13 Stopped by limit on insertions
% 113.89/114.13
% 113.89/114.13 Model 98 [ 181 2 1025 ] (0.00 seconds, 250000 Inserts)
% 113.89/114.13
% 113.89/114.13 Resetting weight limit to 25 after 185 givens.
% 113.89/114.13
% 116.57/116.77
% 116.57/116.77
% 116.57/116.77 Changing weight limit from 25 to 22.
% 116.57/116.77
% 116.57/116.77 Stopped by limit on insertions
% 116.57/116.77
% 116.57/116.77 Model 99 [ 227 2 549 ] (0.00 seconds, 250000 Inserts)
% 116.57/116.77
% 116.57/116.77 Resetting weight limit to 22 after 190 givens.
% 116.57/116.77
% 119.18/119.35
% 119.18/119.35
% 119.18/119.35 Changing weight limit from 22 to 23.
% 119.18/119.35
% 119.18/119.35 Stopped by limit on insertions
% 119.18/119.35
% 119.18/119.35 Model 100 [ 208 1 570 ] (0.00 seconds, 250000 Inserts)
% 119.18/119.35
% 119.18/119.35 Resetting weight limit to 23 after 195 givens.
% 119.18/119.35
% 124.20/124.40
% 124.20/124.40
% 124.20/124.40 Changing weight limit from 23 to 20.
% 124.20/124.40
% 124.20/124.40 Stopped by limit on insertions
% 124.20/124.40
% 124.20/124.40 Model 101 [ 264 2 1125 ] (0.00 seconds, 250000 Inserts)
% 124.20/124.40
% 124.20/124.40 Stopped by limit on insertions
% 124.20/124.40
% 124.20/124.40 Model 102 [ 284 2 184 ] (0.00 seconds, 250000 Inserts)
% 124.20/124.40
% 124.20/124.40 Resetting weight limit to 20 after 205 givens.
% 124.20/124.40
% 126.99/127.17
% 126.99/127.17
% 126.99/127.17 Changing weight limit from 20 to 21.
% 126.99/127.17
% 126.99/127.17 Stopped by limit on insertions
% 126.99/127.17
% 126.99/127.17 Model 103 [ 235 2 737 ] (0.00 seconds, 250000 Inserts)
% 126.99/127.17
% 126.99/127.17 Resetting weight limit to 21 after 210 givens.
% 126.99/127.17
% 136.42/136.60
% 136.42/136.60
% 136.42/136.60 Changing weight limit from 21 to 20.
% 136.42/136.60
% 136.42/136.60 Stopped by limit on insertions
% 136.42/136.60
% 136.42/136.60 Model 104 [ 490 2 1608 ] (0.00 seconds, 250000 Inserts)
% 136.42/136.60
% 136.42/136.60 Stopped by limit on insertions
% 136.42/136.60
% 136.42/136.60 Model 105 [ 295 2 589 ] (0.00 seconds, 250000 Inserts)
% 136.42/136.60
% 136.42/136.60 Stopped by limit on insertions
% 136.42/136.60
% 136.42/136.60 Model 106 [ 306 2 1397 ] (0.00 seconds, 250000 Inserts)
% 136.42/136.60
% 136.42/136.60 Stopped by limit on insertions
% 136.42/136.60
% 136.42/136.60 Model 107 [ 250 2 1038 ] (0.00 seconds, 250000 Inserts)
% 136.42/136.60
% 136.42/136.60 Resetting weight limit to 20 after 220 givens.
% 136.42/136.60
% 136.42/136.61
% 136.42/136.61 -- HEY sandbox2, WE HAVE A PROOF!! --
% 136.42/136.61
% 136.42/136.61 ----> UNIT CONFLICT at 136.19 sec ----> 4703 [binary,4702.1,16.1] {+} $F.
% 136.42/136.61
% 136.42/136.61 Length of proof is 3. Level of proof is 3.
% 136.42/136.61
% 136.42/136.61 ---------------- PROOF ----------------
% 136.42/136.61 % SZS status Theorem
% 136.42/136.61 % SZS output start Refutation
% 136.42/136.61
% 136.42/136.61 15 [] {+} -distinct_lines(A,B)|convergent_lines(A,B).
% 136.42/136.61 16 [] {+} -convergent_lines(parallel_through_point(A,B),A).
% 136.42/136.61 17 [] {+} -apart_point_and_line(A,parallel_through_point(B,A)).
% 136.42/136.61 41 [] {+} equal_lines(A,B)|distinct_lines(A,B).
% 136.42/136.61 48 [] {-} apart_point_and_line(intersection_point($c3,$c2),$c1).
% 136.42/136.61 104 [para_from,41.1.1,17.1.2] {+} -apart_point_and_line(A,B)|distinct_lines(parallel_through_point(C,A),B).
% 136.42/136.61 4677 [hyper,104,48] {-} distinct_lines(parallel_through_point(A,intersection_point($c3,$c2)),$c1).
% 136.42/136.61 4702 [hyper,4677,15] {-} convergent_lines(parallel_through_point(A,intersection_point($c3,$c2)),$c1).
% 136.42/136.61 4703 [binary,4702.1,16.1] {+} $F.
% 136.42/136.61
% 136.42/136.61 % SZS output end Refutation
% 136.42/136.61 ------------ end of proof -------------
% 136.42/136.61
% 136.42/136.61
% 136.42/136.61 Search stopped by max_proofs option.
% 136.42/136.61
% 136.42/136.61
% 136.42/136.61 Search stopped by max_proofs option.
% 136.42/136.61
% 136.42/136.61 ============ end of search ============
% 136.42/136.61
% 136.42/136.61 ----------- soft-scott stats ----------
% 136.42/136.61
% 136.42/136.61 true clauses given 40 (17.9%)
% 136.42/136.61 false clauses given 183
% 136.42/136.61
% 136.42/136.61 FALSE TRUE
% 136.42/136.61 6 0 3
% 136.42/136.61 7 0 11
% 136.42/136.61 8 135 83
% 136.42/136.61 9 327 258
% 136.42/136.61 10 265 16
% 136.42/136.61 11 71 109
% 136.42/136.61 12 57 150
% 136.42/136.61 13 23 75
% 136.42/136.61 14 21 80
% 136.42/136.61 15 241 49
% 136.42/136.61 16 54 53
% 136.42/136.61 17 48 34
% 136.42/136.61 18 875 5
% 136.42/136.61 19 250 16
% 136.42/136.61 20 162 0
% 136.42/136.61 tot: 2529 942 (27.1% true)
% 136.42/136.61
% 136.42/136.61
% 136.42/136.61 Model 107 [ 250 2 1038 ] (0.00 seconds, 250000 Inserts)
% 136.42/136.61
% 136.42/136.61 That finishes the proof of the theorem.
% 136.42/136.61
% 136.42/136.61 Process 5881 finished Sat Jun 18 06:56:25 2022
%------------------------------------------------------------------------------