%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO065-2 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n005.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:17:50 EDT 2022
% Result : Unsatisfiable 41.35s 41.55s
% Output : Refutation 41.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : GEO065-2 : TPTP v8.1.0. Released v1.0.0.
% 0.10/0.12 % Command : sos-script %s
% 0.13/0.33 % Computer : n005.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 : Fri Jun 17 22:17:53 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.13/0.35 ----- Otter 3.2, August 2001 -----
% 0.13/0.35 The process was started by sandbox on n005.cluster.edu,
% 0.13/0.35 Fri Jun 17 22:17:53 2022
% 0.13/0.35 The command was "./sos". The process ID is 32320.
% 0.13/0.35
% 0.13/0.35 set(prolog_style_variables).
% 0.13/0.35 set(auto).
% 0.13/0.35 dependent: set(auto1).
% 0.13/0.35 dependent: set(process_input).
% 0.13/0.35 dependent: clear(print_kept).
% 0.13/0.35 dependent: clear(print_new_demod).
% 0.13/0.35 dependent: clear(print_back_demod).
% 0.13/0.35 dependent: clear(print_back_sub).
% 0.13/0.35 dependent: set(control_memory).
% 0.13/0.35 dependent: assign(max_mem, 12000).
% 0.13/0.35 dependent: assign(pick_given_ratio, 4).
% 0.13/0.35 dependent: assign(stats_level, 1).
% 0.13/0.35 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.35 dependent: assign(sos_limit, 5000).
% 0.13/0.35 dependent: assign(max_weight, 60).
% 0.13/0.35 clear(print_given).
% 0.13/0.35
% 0.13/0.35 list(usable).
% 0.13/0.35
% 0.13/0.35 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=8.
% 0.13/0.35
% 0.13/0.35 This ia a non-Horn set with equality. The strategy will be
% 0.13/0.35 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.13/0.35 unit deletion, with positive clauses in sos and nonpositive
% 0.13/0.35 clauses in usable.
% 0.13/0.35
% 0.13/0.35 dependent: set(knuth_bendix).
% 0.13/0.35 dependent: set(para_from).
% 0.13/0.35 dependent: set(para_into).
% 0.13/0.35 dependent: clear(para_from_right).
% 0.13/0.35 dependent: clear(para_into_right).
% 0.13/0.35 dependent: set(para_from_vars).
% 0.13/0.35 dependent: set(eq_units_both_ways).
% 0.13/0.35 dependent: set(dynamic_demod_all).
% 0.13/0.35 dependent: set(dynamic_demod).
% 0.13/0.35 dependent: set(order_eq).
% 0.13/0.35 dependent: set(back_demod).
% 0.13/0.35 dependent: set(lrpo).
% 0.13/0.35 dependent: set(hyper_res).
% 0.13/0.35 dependent: set(unit_deletion).
% 0.13/0.35 dependent: set(factor).
% 0.13/0.35
% 0.13/0.35 ------------> process usable:
% 0.13/0.35
% 0.13/0.35 ------------> process sos:
% 0.13/0.35 40 back subsumes 37.
% 0.13/0.35 Following clause subsumed by 44 during input processing: 0 [copy,44,flip.1] {-} A=A.
% 0.13/0.35
% 0.13/0.35 ======= end of input processing =======
% 1.08/1.28
% 1.08/1.28 Model 1 (0.00 seconds, 0 Inserts)
% 1.08/1.28
% 1.08/1.28 Stopped by limit on number of solutions
% 1.08/1.28
% 1.08/1.28
% 1.08/1.28 -------------- Softie stats --------------
% 1.08/1.28
% 1.08/1.28 UPDATE_STOP: 300
% 1.08/1.28 SFINDER_TIME_LIMIT: 2
% 1.08/1.28 SHORT_CLAUSE_CUTOFF: 4
% 1.08/1.28 number of clauses in intial UL: 38
% 1.08/1.28 number of clauses initially in problem: 43
% 1.08/1.28 percentage of clauses intially in UL: 88
% 1.08/1.28 percentage of distinct symbols occuring in initial UL: 93
% 1.08/1.28 percent of all initial clauses that are short: 100
% 1.08/1.28 absolute distinct symbol count: 15
% 1.08/1.28 distinct predicate count: 4
% 1.08/1.28 distinct function count: 5
% 1.08/1.28 distinct constant count: 6
% 1.08/1.28
% 1.08/1.28 ---------- no more Softie stats ----------
% 1.08/1.28
% 1.08/1.28
% 1.08/1.28
% 1.08/1.28 Model 2 (0.00 seconds, 0 Inserts)
% 1.08/1.28
% 1.08/1.28 Stopped by limit on number of solutions
% 1.08/1.28
% 1.08/1.28 =========== start of search ===========
% 41.35/41.55
% 41.35/41.55 -- HEY sandbox, WE HAVE A PROOF!! --
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 3 [ 5 55 215972 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 4 [ 69 2 5138 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 5 [ 72 17 52102 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 6 [ 60 24 112663 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 7 [ 87 6 12787 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 8 [ 49 28 118010 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 9 [ 44 26 118924 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 10 [ 78 36 148391 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 11 [ 70 60 224310 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 Model 12 [ 96 49 177018 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 Stopped by limit on insertions
% 41.35/41.55
% 41.35/41.55 ----> UNIT CONFLICT at 41.16 sec ----> 6327 [binary,6326.1,20.1] {+} $F.
% 41.35/41.55
% 41.35/41.55 Length of proof is 8. Level of proof is 6.
% 41.35/41.55
% 41.35/41.55 ---------------- PROOF ----------------
% 41.35/41.55 % SZS status Unsatisfiable
% 41.35/41.55 % SZS output start Refutation
% 41.35/41.55
% 41.35/41.55 2 [] {+} -equidistant(A,B,C,C)|A=B.
% 41.35/41.55 4 [] {+} -between(A,B,A)|A=B.
% 41.35/41.55 5 [] {+} -between(A,B,C)| -between(D,E,C)|between(B,inner_pasch(A,B,C,E,D),D).
% 41.35/41.55 6 [] {+} -between(A,B,C)| -between(D,E,C)|between(E,inner_pasch(A,B,C,E,D),A).
% 41.35/41.55 17 [] {+} -between(A,B,C)|colinear(C,A,B).
% 41.35/41.55 20 [] {+} -colinear(u,v,w).
% 41.35/41.55 41 [] {+} between(A,B,extension(A,B,C,D)).
% 41.35/41.55 42 [] {+} equidistant(A,extension(B,A,C,D),C,D).
% 41.35/41.55 43 [] {-} between(u,w,v).
% 41.35/41.55 460,459 [hyper,42,2,flip.1] {+} extension(A,B,C,C)=B.
% 41.35/41.55 589 [para_into,459.1.1,4.2.1,demod,460,460] {+} A=B| -between(B,A,B).
% 41.35/41.55 593 [para_from,459.1.1,41.1.3] {+} between(A,B,B).
% 41.35/41.55 635 [hyper,593,6,43] {-} between(v,inner_pasch(u,w,v,v,A),u).
% 41.35/41.55 640 [hyper,593,5,43] {-} between(w,inner_pasch(u,w,v,v,A),A).
% 41.35/41.55 5919 [hyper,640,589] {-} inner_pasch(u,w,v,v,w)=w.
% 41.35/41.55 6311 [para_from,5919.1.1,635.1.2] {-} between(v,w,u).
% 41.35/41.55 6326 [hyper,6311,17] {-} colinear(u,v,w).
% 41.35/41.55 6327 [binary,6326.1,20.1] {+} $F.
% 41.35/41.55
% 41.35/41.55 % SZS output end Refutation
% 41.35/41.55 ------------ end of proof -------------
% 41.35/41.55
% 41.35/41.55
% 41.35/41.55 Search stopped by max_proofs option.
% 41.35/41.55
% 41.35/41.55
% 41.35/41.55 Search stopped by max_proofs option.
% 41.35/41.55
% 41.35/41.55 ============ end of search ============
% 41.35/41.55
% 41.35/41.55 ----------- soft-scott stats ----------
% 41.35/41.55
% 41.35/41.55 true clauses given 17 (20.5%)
% 41.35/41.55 false clauses given 66
% 41.35/41.55
% 41.35/41.55 FALSE TRUE
% 41.35/41.55 5 0 6
% 41.35/41.55 8 0 45
% 41.35/41.55 9 20 71
% 41.35/41.55 10 0 2
% 41.35/41.55 11 0 2
% 41.35/41.55 12 142 2
% 41.35/41.55 13 247 70
% 41.35/41.55 14 94 32
% 41.35/41.55 15 0 6
% 41.35/41.55 16 11 16
% 41.35/41.55 17 34 116
% 41.35/41.55 18 7 26
% 41.35/41.55 19 4 14
% 41.35/41.55 20 8 6
% 41.35/41.55 21 129 236
% 41.35/41.55 22 89 137
% 41.35/41.55 23 9 135
% 41.35/41.55 24 9 13
% 41.35/41.55 25 197 44
% 41.35/41.55 26 208 112
% 41.35/41.55 27 128 182
% 41.35/41.55 28 35 37
% 41.35/41.55 29 5 40
% 41.35/41.55 30 107 91
% 41.35/41.55 31 176 57
% 41.35/41.55 32 69 51
% 41.35/41.55 33 16 75
% 41.35/41.55 34 32 93
% 41.35/41.55 35 109 86
% 41.35/41.55 36 77 106
% 41.35/41.55 37 32 174
% 41.35/41.55 38 28 7
% 41.35/41.55 39 32 90
% 41.35/41.55 40 43 116
% 41.35/41.55 41 116 96
% 41.35/41.55 42 66 39
% 41.35/41.55 43 26 2
% 41.35/41.55 44 53 54
% 41.35/41.55 45 31 70
% 41.35/41.55 46 25 0
% 41.35/41.55 47 5 0
% 41.35/41.55 48 26 1
% 41.35/41.55 49 37 0
% 41.35/41.55 50 46 1
% 41.35/41.55 51 12 1
% 41.35/41.55 52 10 4
% 41.35/41.55 53 15 0
% 41.35/41.55 54 37 0
% 41.35/41.55 55 24 2
% 41.35/41.55 56 11 0
% 41.35/41.55 58 7 0
% 41.35/41.55 59 17 0
% 41.35/41.55 60 21 0
% 41.35/41.55 tot: 2682 2566 (48.9% true)
% 41.35/41.55
% 41.35/41.55
% 41.35/41.55 Model 12 [ 96 -520 177018 ] (0.00 seconds, 250000 Inserts)
% 41.35/41.55
% 41.35/41.55 That finishes the proof of the theorem.
% 41.35/41.55
% 41.35/41.55 Process 32320 finished Fri Jun 17 22:18:34 2022
%------------------------------------------------------------------------------