%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO602+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n017.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:21:06 EDT 2022
% Result : Theorem 52.23s 52.49s
% Output : Refutation 52.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GEO602+1 : TPTP v8.1.0. Released v7.5.0.
% 0.04/0.13 % Command : sos-script %s
% 0.12/0.35 % Computer : n017.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 600
% 0.12/0.35 % DateTime : Fri Jun 17 20:15:12 EDT 2022
% 0.12/0.35 % CPUTime :
% 0.20/0.41 ----- Otter 3.2, August 2001 -----
% 0.20/0.41 The process was started by sandbox2 on n017.cluster.edu,
% 0.20/0.41 Fri Jun 17 20:15:12 2022
% 0.20/0.41 The command was "./sos". The process ID is 11655.
% 0.20/0.41
% 0.20/0.41 set(prolog_style_variables).
% 0.20/0.41 set(auto).
% 0.20/0.41 dependent: set(auto1).
% 0.20/0.41 dependent: set(process_input).
% 0.20/0.41 dependent: clear(print_kept).
% 0.20/0.41 dependent: clear(print_new_demod).
% 0.20/0.41 dependent: clear(print_back_demod).
% 0.20/0.41 dependent: clear(print_back_sub).
% 0.20/0.41 dependent: set(control_memory).
% 0.20/0.41 dependent: assign(max_mem, 12000).
% 0.20/0.41 dependent: assign(pick_given_ratio, 4).
% 0.20/0.41 dependent: assign(stats_level, 1).
% 0.20/0.41 dependent: assign(pick_semantic_ratio, 3).
% 0.20/0.41 dependent: assign(sos_limit, 5000).
% 0.20/0.41 dependent: assign(max_weight, 60).
% 0.20/0.41 clear(print_given).
% 0.20/0.41
% 0.20/0.41 formula_list(usable).
% 0.20/0.41
% 0.20/0.41 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.20/0.41
% 0.20/0.41 This ia a non-Horn set with equality. The strategy will be
% 0.20/0.41 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.20/0.41 unit deletion, with positive clauses in sos and nonpositive
% 0.20/0.41 clauses in usable.
% 0.20/0.41
% 0.20/0.41 dependent: set(knuth_bendix).
% 0.20/0.41 dependent: set(para_from).
% 0.20/0.41 dependent: set(para_into).
% 0.20/0.41 dependent: clear(para_from_right).
% 0.20/0.41 dependent: clear(para_into_right).
% 0.20/0.41 dependent: set(para_from_vars).
% 0.20/0.41 dependent: set(eq_units_both_ways).
% 0.20/0.41 dependent: set(dynamic_demod_all).
% 0.20/0.41 dependent: set(dynamic_demod).
% 0.20/0.41 dependent: set(order_eq).
% 0.20/0.41 dependent: set(back_demod).
% 0.20/0.41 dependent: set(lrpo).
% 0.20/0.41 dependent: set(hyper_res).
% 0.20/0.41 dependent: set(unit_deletion).
% 0.20/0.41 dependent: set(factor).
% 0.20/0.41
% 0.20/0.41 ------------> process usable:
% 0.20/0.41 Following clause subsumed by 72 during input processing: 0 [] {-} -eqangle(A,B,C,D,C,D,A,B)|perp(A,B,C,D)|para(A,B,C,D).
% 0.20/0.41
% 0.20/0.41 ------------> process sos:
% 0.20/0.41 Following clause subsumed by 170 during input processing: 0 [copy,170,flip.1] {-} A=A.
% 0.20/0.41 170 back subsumes 146.
% 0.20/0.41 170 back subsumes 145.
% 0.20/0.41 170 back subsumes 144.
% 0.20/0.41 170 back subsumes 143.
% 0.20/0.41
% 0.20/0.41 ======= end of input processing =======
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47 Failed to model usable list: disabling FINDER
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47 -------------- Softie stats --------------
% 0.20/0.47
% 0.20/0.47 UPDATE_STOP: 300
% 0.20/0.47 SFINDER_TIME_LIMIT: 2
% 0.20/0.47 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.47 number of clauses in intial UL: 154
% 0.20/0.47 number of clauses initially in problem: 166
% 0.20/0.47 percentage of clauses intially in UL: 92
% 0.20/0.47 percentage of distinct symbols occuring in initial UL: 73
% 0.20/0.47 percent of all initial clauses that are short: 100
% 0.20/0.47 absolute distinct symbol count: 49
% 0.20/0.47 distinct predicate count: 12
% 0.20/0.47 distinct function count: 20
% 0.20/0.47 distinct constant count: 17
% 0.20/0.47
% 0.20/0.47 ---------- no more Softie stats ----------
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47
% 0.20/0.47 =========== start of search ===========
% 8.39/8.61
% 8.39/8.61
% 8.39/8.61 Changing weight limit from 60 to 57.
% 8.39/8.61
% 8.39/8.61 Resetting weight limit to 57 after 250 givens.
% 8.39/8.61
% 9.16/9.43
% 9.16/9.43
% 9.16/9.43 Changing weight limit from 57 to 56.
% 9.16/9.43
% 9.16/9.43 Resetting weight limit to 56 after 255 givens.
% 9.16/9.43
% 11.83/12.02
% 11.83/12.02
% 11.83/12.02 Changing weight limit from 56 to 55.
% 11.83/12.02
% 11.83/12.02 Resetting weight limit to 55 after 275 givens.
% 11.83/12.02
% 14.08/14.30
% 14.08/14.30
% 14.08/14.30 Changing weight limit from 55 to 54.
% 14.08/14.30
% 14.08/14.30 Modelling stopped after 300 given clauses and 0.00 seconds
% 14.08/14.30
% 14.08/14.30
% 14.08/14.30 Resetting weight limit to 54 after 300 givens.
% 14.08/14.30
% 15.10/15.29
% 15.10/15.29
% 15.10/15.29 Changing weight limit from 54 to 52.
% 15.10/15.29
% 15.10/15.29 Resetting weight limit to 52 after 315 givens.
% 15.10/15.29
% 16.28/16.48
% 16.28/16.48
% 16.28/16.48 Changing weight limit from 52 to 51.
% 16.28/16.48
% 16.28/16.48 Resetting weight limit to 51 after 330 givens.
% 16.28/16.48
% 20.48/20.73
% 20.48/20.73
% 20.48/20.73 Changing weight limit from 51 to 50.
% 20.48/20.73
% 20.48/20.73 Resetting weight limit to 50 after 380 givens.
% 20.48/20.73
% 24.58/24.78
% 24.58/24.78
% 24.58/24.78 Changing weight limit from 50 to 49.
% 24.58/24.78
% 24.58/24.78 Resetting weight limit to 49 after 440 givens.
% 24.58/24.78
% 26.05/26.28
% 26.05/26.28
% 26.05/26.28 Changing weight limit from 49 to 46.
% 26.05/26.28
% 26.05/26.28 Resetting weight limit to 46 after 460 givens.
% 26.05/26.28
% 26.96/27.16
% 26.96/27.16
% 26.96/27.17 Changing weight limit from 46 to 45.
% 26.96/27.17
% 26.96/27.17 Resetting weight limit to 45 after 470 givens.
% 26.96/27.17
% 27.75/28.01
% 27.75/28.01
% 27.75/28.01 Changing weight limit from 45 to 44.
% 27.75/28.01
% 27.75/28.01 Resetting weight limit to 44 after 480 givens.
% 27.75/28.01
% 28.03/28.27
% 28.03/28.27
% 28.03/28.27 Changing weight limit from 44 to 35.
% 28.03/28.27
% 28.03/28.27 Resetting weight limit to 35 after 485 givens.
% 28.03/28.27
% 28.29/28.50
% 28.29/28.50
% 28.29/28.50 Changing weight limit from 35 to 31.
% 28.29/28.50
% 28.29/28.50 Resetting weight limit to 31 after 490 givens.
% 28.29/28.50
% 28.58/28.79
% 28.58/28.79
% 28.58/28.79 Changing weight limit from 31 to 30.
% 28.58/28.79
% 28.58/28.79 Resetting weight limit to 30 after 495 givens.
% 28.58/28.79
% 35.13/35.37
% 35.13/35.37
% 35.13/35.37 Changing weight limit from 30 to 29.
% 35.13/35.37
% 35.13/35.37 Resetting weight limit to 29 after 665 givens.
% 35.13/35.37
% 36.17/36.36
% 36.17/36.36
% 36.17/36.36 Changing weight limit from 29 to 18.
% 36.17/36.36
% 36.17/36.36 Resetting weight limit to 18 after 1000 givens.
% 36.17/36.36
% 36.17/36.47
% 36.17/36.47
% 36.17/36.47 Changing weight limit from 18 to 14.
% 36.17/36.47
% 36.17/36.47 Resetting weight limit to 14 after 1090 givens.
% 36.17/36.47
% 36.28/36.48
% 36.28/36.48
% 36.28/36.48 Changing weight limit from 14 to 13.
% 36.28/36.48
% 36.28/36.48 Resetting weight limit to 13 after 1100 givens.
% 36.28/36.48
% 36.54/36.75
% 36.54/36.75
% 36.54/36.75 Changing weight limit from 13 to 11.
% 36.54/36.75
% 36.54/36.75 Resetting weight limit to 11 after 1185 givens.
% 36.54/36.75
% 36.62/36.81
% 36.62/36.81
% 36.62/36.81 Changing weight limit from 11 to 10.
% 36.62/36.81
% 36.62/36.81 Resetting weight limit to 10 after 1205 givens.
% 36.62/36.81
% 37.39/37.60
% 37.39/37.60
% 37.39/37.60 Changing weight limit from 10 to 9.
% 37.39/37.60
% 37.39/37.60 Resetting weight limit to 9 after 1525 givens.
% 37.39/37.60
% 51.33/51.56
% 51.33/51.56
% 51.33/51.56 Changing weight limit from 9 to 8.
% 51.33/51.56
% 51.33/51.56 Resetting weight limit to 8 after 7645 givens.
% 51.33/51.56
% 51.85/52.08
% 51.85/52.08
% 51.85/52.08 Changing weight limit from 8 to 7.
% 51.85/52.08
% 51.85/52.08 Resetting weight limit to 7 after 7865 givens.
% 51.85/52.08
% 52.00/52.25
% 52.00/52.25
% 52.00/52.25 Changing weight limit from 7 to 5.
% 52.00/52.25
% 52.00/52.25 Resetting weight limit to 5 after 8100 givens.
% 52.00/52.25
% 52.23/52.49
% 52.23/52.49 -- HEY sandbox2, WE HAVE A PROOF!! --
% 52.23/52.49
% 52.23/52.49 ----> UNIT CONFLICT at 51.56 sec ----> 188045 [binary,188044.1,113.1] {-} $F.
% 52.23/52.49
% 52.23/52.49 Length of proof is 110. Level of proof is 19.
% 52.23/52.49
% 52.23/52.49 ---------------- PROOF ----------------
% 52.23/52.49 % SZS status Theorem
% 52.23/52.49 % SZS output start Refutation
% 52.23/52.49
% 52.23/52.49 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 52.23/52.49 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 52.23/52.49 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 52.23/52.49 4 [] {+} -para(A,B,C,D)|para(A,B,D,C).
% 52.23/52.49 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 52.23/52.49 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 52.23/52.49 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 52.23/52.49 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 52.23/52.49 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 52.23/52.49 10 [] {+} -para(A,B,C,D)| -perp(C,D,E,F)|perp(A,B,E,F).
% 52.23/52.49 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 52.23/52.49 14 [] {+} -cyclic(A,B,C,D)|cyclic(A,B,D,C).
% 52.23/52.49 15 [] {+} -cyclic(A,B,C,D)|cyclic(A,C,B,D).
% 52.23/52.49 16 [] {+} -cyclic(A,B,C,D)|cyclic(B,A,C,D).
% 52.23/52.49 17 [] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)|cyclic(B,C,D,E).
% 52.23/52.49 19 [] {+} -eqangle(A,B,C,D,E,F,G,H)|eqangle(C,D,A,B,G,H,E,F).
% 52.23/52.49 39 [] {+} -eqangle(A,B,C,D,E,F,C,D)|para(A,B,E,F).
% 52.23/52.49 40 [] {+} -para(A,B,C,D)|eqangle(A,B,E,F,C,D,E,F).
% 52.23/52.49 41 [] {+} -cyclic(A,B,C,D)|eqangle(C,A,C,B,D,A,D,B).
% 52.23/52.49 43 [] {+} -eqangle(A,B,A,C,D,B,D,C)| -coll(A,D,C)|cyclic(B,C,A,D).
% 52.23/52.49 44 [] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)| -cyclic(A,B,C,F)| -eqangle(C,A,C,B,F,D,F,E)|cong(A,B,D,E).
% 52.23/52.49 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 52.23/52.49 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 52.23/52.49 58 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)| -cyclic(A,C,B,D)|perp(B,A,A,D).
% 52.23/52.49 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 52.23/52.49 67 [] {+} -para(A,B,A,C)|coll(A,B,C).
% 52.23/52.49 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 52.23/52.49 99 [] {+} -circle(A,B,C,D)|perp($f12(B,C,D,A),B,B,A).
% 52.23/52.49 113 [] {+} -perp($c11,$c10,$c12,$c16).
% 52.23/52.49 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 52.23/52.49 120 [factor,17.1.2] {+} -cyclic(A,B,C,D)|cyclic(B,C,D,D).
% 52.23/52.49 123 [factor,44.2.3] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)| -eqangle(C,A,C,B,E,D,E,E)|cong(A,B,D,E).
% 52.23/52.49 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 52.23/52.49 159 [] {-} circle($c16,$c15,$c9,$c8).
% 52.23/52.49 160 [] {-} circle($c17,$c15,$c7,$c6).
% 52.23/52.49 163 [] {-} coll($c13,$c17,$c16).
% 52.23/52.49 164 [] {-} coll($c13,$c15,$c14).
% 52.23/52.49 167 [] {-} coll($c11,$c15,$c12).
% 52.23/52.49 168 [] {-} coll($c10,$c14,$c12).
% 52.23/52.49 171 [hyper,159,99] {-} perp($f12($c15,$c9,$c8,$c16),$c15,$c15,$c16).
% 52.23/52.49 188 [hyper,163,114] {-} coll($c16,$c16,$c13).
% 52.23/52.49 189 [hyper,163,2] {-} coll($c17,$c13,$c16).
% 52.23/52.49 204 [hyper,164,2] {-} coll($c15,$c13,$c14).
% 52.23/52.49 205 [hyper,164,1] {-} coll($c13,$c14,$c15).
% 52.23/52.49 219 [hyper,167,2] {-} coll($c15,$c11,$c12).
% 52.23/52.49 220 [hyper,167,1] {-} coll($c11,$c12,$c15).
% 52.23/52.49 233 [hyper,160,99] {-} perp($f12($c15,$c7,$c6,$c17),$c15,$c15,$c17).
% 52.23/52.49 250 [hyper,168,114] {-} coll($c12,$c12,$c10).
% 52.23/52.49 265 [hyper,188,114] {-} coll($c13,$c13,$c16).
% 52.23/52.49 279 [hyper,189,114] {-} coll($c16,$c16,$c17).
% 52.23/52.49 339 [hyper,204,1] {-} coll($c15,$c14,$c13).
% 52.23/52.49 352 [hyper,205,114] {-} coll($c15,$c15,$c13).
% 52.23/52.49 397 [hyper,219,114] {-} coll($c12,$c12,$c15).
% 52.23/52.49 411 [hyper,220,114] {-} coll($c15,$c15,$c11).
% 52.23/52.49 486 [hyper,265,1] {-} coll($c13,$c16,$c13).
% 52.23/52.49 513 [hyper,279,114] {-} coll($c17,$c17,$c16).
% 52.23/52.49 644 [hyper,339,114] {-} coll($c13,$c13,$c15).
% 52.23/52.49 658 [hyper,352,1] {-} coll($c15,$c13,$c15).
% 52.23/52.49 679 [hyper,171,8] {-} perp($c15,$c16,$f12($c15,$c9,$c8,$c16),$c15).
% 52.23/52.49 753 [hyper,397,114] {-} coll($c15,$c15,$c12).
% 52.23/52.49 754 [hyper,397,3,250] {-} coll($c10,$c15,$c12).
% 52.23/52.49 1367 [hyper,513,1] {-} coll($c17,$c16,$c17).
% 52.23/52.49 1785 [hyper,644,3,265] {-} coll($c16,$c15,$c13).
% 52.23/52.49 1787 [hyper,644,3,265] {-} coll($c15,$c16,$c13).
% 52.23/52.49 1892 [hyper,658,114] {-} coll($c15,$c15,$c15).
% 52.23/52.49 2036 [hyper,754,1] {-} coll($c10,$c12,$c15).
% 52.23/52.49 3279 [hyper,1785,1] {-} coll($c16,$c13,$c15).
% 52.23/52.49 3353 [hyper,1787,1] {-} coll($c15,$c13,$c16).
% 52.23/52.49 3648 [hyper,2036,114] {-} coll($c15,$c15,$c10).
% 52.23/52.49 4981 [hyper,3279,114] {-} coll($c15,$c15,$c16).
% 52.23/52.49 5022 [hyper,3353,3,658] {-} coll($c15,$c16,$c15).
% 52.23/52.49 5025 [hyper,3353,3,658] {-} coll($c16,$c15,$c15).
% 52.23/52.49 6434 [hyper,233,8] {-} perp($c15,$c17,$f12($c15,$c7,$c6,$c17),$c15).
% 52.23/52.49 10763 [hyper,679,9,171] {-} para($c15,$c16,$c15,$c16).
% 52.23/52.49 10901 [hyper,10763,40] {-} eqangle($c15,$c16,A,B,$c15,$c16,A,B).
% 52.23/52.49 10902 [hyper,10763,4] {-} para($c15,$c16,$c16,$c15).
% 52.23/52.49 11048 [hyper,10902,5] {-} para($c16,$c15,$c15,$c16).
% 52.23/52.49 11195 [hyper,11048,6,10902] {-} para($c16,$c15,$c16,$c15).
% 52.23/52.49 11353 [hyper,6434,9,233] {-} para($c15,$c17,$c15,$c17).
% 52.23/52.49 12001 [hyper,10901,43,4981] {-} cyclic($c16,$c16,$c15,$c15).
% 52.23/52.49 12003 [hyper,10901,43,3648] {-} cyclic($c16,$c10,$c15,$c15).
% 52.23/52.49 12004 [hyper,10901,43,1892] {-} cyclic($c16,$c15,$c15,$c15).
% 52.23/52.49 12005 [hyper,10901,43,753] {-} cyclic($c16,$c12,$c15,$c15).
% 52.23/52.49 12007 [hyper,10901,43,411] {-} cyclic($c16,$c11,$c15,$c15).
% 52.23/52.49 12010 [hyper,10901,19] {-} eqangle(A,B,$c15,$c16,A,B,$c15,$c16).
% 52.23/52.49 12011 [hyper,12001,15] {-} cyclic($c16,$c15,$c16,$c15).
% 52.23/52.49 12017 [hyper,12003,15] {-} cyclic($c16,$c15,$c10,$c15).
% 52.23/52.49 12022 [hyper,12005,15] {-} cyclic($c16,$c15,$c12,$c15).
% 52.23/52.49 12026 [hyper,12007,120] {-} cyclic($c11,$c15,$c15,$c15).
% 52.23/52.49 12027 [hyper,12007,16] {-} cyclic($c11,$c16,$c15,$c15).
% 52.23/52.49 12028 [hyper,12007,15] {-} cyclic($c16,$c15,$c11,$c15).
% 52.23/52.49 12033 [hyper,12011,16] {-} cyclic($c15,$c16,$c16,$c15).
% 52.23/52.49 12034 [hyper,12011,14] {-} cyclic($c16,$c15,$c15,$c16).
% 52.23/52.49 12044 [hyper,12017,16] {-} cyclic($c15,$c16,$c10,$c15).
% 52.23/52.49 12045 [hyper,12017,14] {-} cyclic($c16,$c15,$c15,$c10).
% 52.23/52.49 12052 [hyper,12022,16] {-} cyclic($c15,$c16,$c12,$c15).
% 52.23/52.49 12053 [hyper,12022,14] {-} cyclic($c16,$c15,$c15,$c12).
% 52.23/52.49 12061 [hyper,12026,16] {-} cyclic($c15,$c11,$c15,$c15).
% 52.23/52.49 12062 [hyper,12027,15] {-} cyclic($c11,$c15,$c16,$c15).
% 52.23/52.49 12065 [hyper,12028,14] {-} cyclic($c16,$c15,$c15,$c11).
% 52.23/52.49 12074 [hyper,12033,14] {-} cyclic($c15,$c16,$c15,$c16).
% 52.23/52.49 12075 [hyper,12034,123,12004,10901] {-} cong($c16,$c15,$c16,$c15).
% 52.23/52.49 12076 [hyper,12034,120] {-} cyclic($c15,$c15,$c16,$c16).
% 52.23/52.49 12098 [hyper,12044,14] {-} cyclic($c15,$c16,$c15,$c10).
% 52.23/52.49 12102 [hyper,12045,17,12034] {-} cyclic($c15,$c15,$c16,$c10).
% 52.23/52.49 12113 [hyper,12052,14] {-} cyclic($c15,$c16,$c15,$c12).
% 52.23/52.49 12118 [hyper,12053,17,12034] {-} cyclic($c15,$c15,$c16,$c12).
% 52.23/52.49 12142 [hyper,12061,15] {-} cyclic($c15,$c15,$c11,$c15).
% 52.23/52.49 12143 [hyper,12062,41] {-} eqangle($c16,$c11,$c16,$c15,$c15,$c11,$c15,$c15).
% 52.23/52.49 12144 [hyper,12062,16] {-} cyclic($c15,$c11,$c16,$c15).
% 52.23/52.49 12148 [hyper,12065,120] {-} cyclic($c15,$c15,$c11,$c11).
% 52.23/52.49 12197 [hyper,12075,68,5025] {-} midp($c16,$c15,$c15).
% 52.23/52.49 12207 [hyper,12197,129,10763] {-} midp($c16,$c16,$c16).
% 52.23/52.49 12259 [hyper,12207,46,11195,5022] {-} midp($c15,$c16,$c15).
% 52.23/52.49 12367 [hyper,12259,46,11353,1367] {-} midp($c17,$c16,$c17).
% 52.23/52.49 12538 [hyper,12098,120] {-} cyclic($c16,$c15,$c10,$c10).
% 52.23/52.49 12543 [hyper,12098,17,12074] {-} cyclic($c16,$c15,$c10,$c16).
% 52.23/52.49 12559 [hyper,12102,17,12076] {-} cyclic($c15,$c16,$c16,$c10).
% 52.23/52.49 12579 [hyper,12113,120] {-} cyclic($c16,$c15,$c12,$c12).
% 52.23/52.49 12586 [hyper,12113,17,12074] {-} cyclic($c16,$c15,$c12,$c16).
% 52.23/52.49 12615 [hyper,12118,17,12076] {-} cyclic($c15,$c16,$c16,$c12).
% 52.23/52.49 12743 [hyper,12144,14] {-} cyclic($c15,$c11,$c15,$c16).
% 52.23/52.49 12759 [hyper,12148,17,12142] {-} cyclic($c15,$c11,$c15,$c11).
% 52.23/52.49 14873 [hyper,12538,15] {-} cyclic($c16,$c10,$c15,$c10).
% 52.23/52.49 14881 [hyper,12543,15] {-} cyclic($c16,$c10,$c15,$c16).
% 52.23/52.49 15028 [hyper,12579,15] {-} cyclic($c16,$c12,$c15,$c12).
% 52.23/52.49 15040 [hyper,12586,15] {-} cyclic($c16,$c12,$c15,$c16).
% 52.23/52.49 15216 [hyper,12615,17,12559] {-} cyclic($c16,$c16,$c10,$c12).
% 52.23/52.49 16120 [hyper,12759,17,12743] {-} cyclic($c11,$c15,$c16,$c11).
% 52.23/52.49 20810 [hyper,14881,44,14873,12003,10901] {-} cong($c16,$c10,$c16,$c10).
% 52.23/52.49 21028 [hyper,15040,44,15028,12005,10901] {-} cong($c16,$c12,$c16,$c12).
% 52.23/52.49 21380 [hyper,12010,39] {-} para(A,B,A,B).
% 52.23/52.49 22390 [hyper,16120,123,12062,12143] {-} cong($c11,$c15,$c11,$c15).
% 52.23/52.49 29928 [hyper,21028,58,20810,15216] {-} perp($c10,$c16,$c16,$c12).
% 52.23/52.49 31041 [hyper,21380,67] {-} coll(A,B,B).
% 52.23/52.49 31478 [hyper,21380,46,12367,486] {-} midp($c13,$c16,$c13).
% 52.23/52.49 31788 [hyper,31041,114] {-} coll(A,A,B).
% 52.23/52.49 33852 [hyper,31788,3,31788] {-} coll(A,B,C).
% 52.23/52.49 36775 [hyper,33852,46,31478,21380] {-} midp(A,$c16,A).
% 52.23/52.49 36960 [hyper,36775,11] {-} midp(A,A,$c16).
% 52.23/52.49 38217 [hyper,22390,68,33852] {-} midp($c11,$c15,$c15).
% 52.23/52.49 38227 [hyper,38217,129,21380] {-} midp($c11,A,A).
% 52.23/52.49 38478 [hyper,38227,45,36960] {-} para($c11,A,A,$c16).
% 52.23/52.49 43743 [hyper,29928,7] {-} perp($c10,$c16,$c12,$c16).
% 52.23/52.49 188044 [hyper,43743,10,38478] {-} perp($c11,$c10,$c12,$c16).
% 52.23/52.49 188045 [binary,188044.1,113.1] {-} $F.
% 52.23/52.49
% 52.23/52.49 % SZS output end Refutation
% 52.23/52.49 ------------ end of proof -------------
% 52.23/52.49
% 52.23/52.49
% 52.23/52.49 Search stopped by max_proofs option.
% 52.23/52.49
% 52.23/52.49
% 52.23/52.49 Search stopped by max_proofs option.
% 52.23/52.49
% 52.23/52.49 ============ end of search ============
% 52.23/52.49
% 52.23/52.49 That finishes the proof of the theorem.
% 52.23/52.49
% 52.23/52.49 Process 11655 finished Fri Jun 17 20:16:04 2022
%------------------------------------------------------------------------------