%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO646+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n018.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:19 EDT 2022
% Result : Theorem 55.53s 55.78s
% Output : Refutation 55.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GEO646+1 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.14 % Command : sos-script %s
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 18 16:29:03 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.38 ----- Otter 3.2, August 2001 -----
% 0.13/0.38 The process was started by sandbox on n018.cluster.edu,
% 0.13/0.38 Sat Jun 18 16:29:03 2022
% 0.13/0.38 The command was "./sos". The process ID is 31096.
% 0.13/0.38
% 0.13/0.38 set(prolog_style_variables).
% 0.13/0.38 set(auto).
% 0.13/0.38 dependent: set(auto1).
% 0.13/0.38 dependent: set(process_input).
% 0.13/0.38 dependent: clear(print_kept).
% 0.13/0.38 dependent: clear(print_new_demod).
% 0.13/0.38 dependent: clear(print_back_demod).
% 0.13/0.38 dependent: clear(print_back_sub).
% 0.13/0.38 dependent: set(control_memory).
% 0.13/0.38 dependent: assign(max_mem, 12000).
% 0.13/0.38 dependent: assign(pick_given_ratio, 4).
% 0.13/0.38 dependent: assign(stats_level, 1).
% 0.13/0.38 dependent: assign(pick_semantic_ratio, 3).
% 0.13/0.38 dependent: assign(sos_limit, 5000).
% 0.13/0.38 dependent: assign(max_weight, 60).
% 0.13/0.38 clear(print_given).
% 0.13/0.38
% 0.13/0.38 formula_list(usable).
% 0.13/0.38
% 0.13/0.38 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.13/0.38
% 0.13/0.38 This ia a non-Horn set with equality. The strategy will be
% 0.13/0.38 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.13/0.38 unit deletion, with positive clauses in sos and nonpositive
% 0.13/0.38 clauses in usable.
% 0.13/0.38
% 0.13/0.38 dependent: set(knuth_bendix).
% 0.13/0.38 dependent: set(para_from).
% 0.13/0.38 dependent: set(para_into).
% 0.13/0.38 dependent: clear(para_from_right).
% 0.13/0.38 dependent: clear(para_into_right).
% 0.13/0.38 dependent: set(para_from_vars).
% 0.13/0.38 dependent: set(eq_units_both_ways).
% 0.13/0.38 dependent: set(dynamic_demod_all).
% 0.13/0.38 dependent: set(dynamic_demod).
% 0.13/0.38 dependent: set(order_eq).
% 0.13/0.38 dependent: set(back_demod).
% 0.13/0.38 dependent: set(lrpo).
% 0.13/0.38 dependent: set(hyper_res).
% 0.13/0.38 dependent: set(unit_deletion).
% 0.13/0.38 dependent: set(factor).
% 0.13/0.38
% 0.13/0.38 ------------> process usable:
% 0.13/0.38 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.13/0.38
% 0.13/0.38 ------------> process sos:
% 0.13/0.38 Following clause subsumed by 169 during input processing: 0 [copy,169,flip.1] {-} A=A.
% 0.13/0.38 169 back subsumes 146.
% 0.13/0.38 169 back subsumes 145.
% 0.13/0.38 169 back subsumes 144.
% 0.13/0.38 169 back subsumes 143.
% 0.13/0.38
% 0.13/0.38 ======= end of input processing =======
% 0.20/0.45
% 0.20/0.45
% 0.20/0.45 Failed to model usable list: disabling FINDER
% 0.20/0.45
% 0.20/0.45
% 0.20/0.45
% 0.20/0.45 -------------- Softie stats --------------
% 0.20/0.45
% 0.20/0.45 UPDATE_STOP: 300
% 0.20/0.45 SFINDER_TIME_LIMIT: 2
% 0.20/0.45 SHORT_CLAUSE_CUTOFF: 4
% 0.20/0.45 number of clauses in intial UL: 154
% 0.20/0.45 number of clauses initially in problem: 165
% 0.20/0.45 percentage of clauses intially in UL: 93
% 0.20/0.45 percentage of distinct symbols occuring in initial UL: 78
% 0.20/0.45 percent of all initial clauses that are short: 100
% 0.20/0.45 absolute distinct symbol count: 46
% 0.20/0.45 distinct predicate count: 12
% 0.20/0.45 distinct function count: 20
% 0.20/0.45 distinct constant count: 14
% 0.20/0.45
% 0.20/0.45 ---------- no more Softie stats ----------
% 0.20/0.45
% 0.20/0.45
% 0.20/0.45
% 0.20/0.45 =========== start of search ===========
% 5.81/6.03
% 5.81/6.03
% 5.81/6.03 Changing weight limit from 60 to 57.
% 5.81/6.03
% 5.81/6.03 Resetting weight limit to 57 after 240 givens.
% 5.81/6.03
% 6.82/7.08
% 6.82/7.08
% 6.82/7.08 Changing weight limit from 57 to 56.
% 6.82/7.08
% 6.82/7.08 Resetting weight limit to 56 after 245 givens.
% 6.82/7.08
% 9.63/9.85
% 9.63/9.85
% 9.63/9.85 Changing weight limit from 56 to 55.
% 9.63/9.85
% 9.63/9.85 Resetting weight limit to 55 after 260 givens.
% 9.63/9.85
% 12.68/12.92
% 12.68/12.92
% 12.68/12.92 Changing weight limit from 55 to 52.
% 12.68/12.92
% 12.68/12.92 Resetting weight limit to 52 after 280 givens.
% 12.68/12.92
% 14.03/14.26
% 14.03/14.26
% 14.03/14.26 Changing weight limit from 52 to 51.
% 14.03/14.26
% 14.03/14.26 Resetting weight limit to 51 after 285 givens.
% 14.03/14.26
% 16.71/16.92
% 16.71/16.92
% 16.71/16.92 Changing weight limit from 51 to 50.
% 16.71/16.92
% 16.71/16.92 Modelling stopped after 300 given clauses and 0.00 seconds
% 16.71/16.92
% 16.71/16.92
% 16.71/16.92 Resetting weight limit to 50 after 305 givens.
% 16.71/16.92
% 19.10/19.31
% 19.10/19.31
% 19.10/19.31 Changing weight limit from 50 to 49.
% 19.10/19.31
% 19.10/19.31 Resetting weight limit to 49 after 340 givens.
% 19.10/19.31
% 19.75/19.96
% 19.75/19.96
% 19.75/19.96 Changing weight limit from 49 to 47.
% 19.75/19.96
% 19.75/19.96 Resetting weight limit to 47 after 355 givens.
% 19.75/19.96
% 20.04/20.25
% 20.04/20.25
% 20.04/20.25 Changing weight limit from 47 to 46.
% 20.04/20.25
% 20.04/20.25 Resetting weight limit to 46 after 360 givens.
% 20.04/20.25
% 20.63/20.82
% 20.63/20.82
% 20.63/20.82 Changing weight limit from 46 to 45.
% 20.63/20.82
% 20.63/20.82 Resetting weight limit to 45 after 370 givens.
% 20.63/20.82
% 21.31/21.51
% 21.31/21.51
% 21.31/21.51 Changing weight limit from 45 to 37.
% 21.31/21.51
% 21.31/21.51 Resetting weight limit to 37 after 385 givens.
% 21.31/21.51
% 21.54/21.77
% 21.54/21.77
% 21.54/21.77 Changing weight limit from 37 to 35.
% 21.54/21.77
% 21.54/21.77 Resetting weight limit to 35 after 390 givens.
% 21.54/21.77
% 21.89/22.11
% 21.89/22.11
% 21.89/22.11 Changing weight limit from 35 to 34.
% 21.89/22.11
% 21.89/22.11 Resetting weight limit to 34 after 400 givens.
% 21.89/22.11
% 22.07/22.31
% 22.07/22.31
% 22.07/22.31 Changing weight limit from 34 to 31.
% 22.07/22.31
% 22.07/22.31 Resetting weight limit to 31 after 405 givens.
% 22.07/22.31
% 22.59/22.80
% 22.59/22.80
% 22.59/22.80 Changing weight limit from 31 to 30.
% 22.59/22.80
% 22.59/22.80 Resetting weight limit to 30 after 420 givens.
% 22.59/22.80
% 28.97/29.21
% 28.97/29.21
% 28.97/29.21 Changing weight limit from 30 to 29.
% 28.97/29.21
% 28.97/29.21 Resetting weight limit to 29 after 670 givens.
% 28.97/29.21
% 29.85/30.06
% 29.85/30.06
% 29.85/30.06 Changing weight limit from 29 to 20.
% 29.85/30.06
% 29.85/30.06 Resetting weight limit to 20 after 725 givens.
% 29.85/30.06
% 29.85/30.08
% 29.85/30.08
% 29.85/30.08 Changing weight limit from 20 to 17.
% 29.85/30.08
% 29.85/30.08 Resetting weight limit to 17 after 730 givens.
% 29.85/30.08
% 30.01/30.20
% 30.01/30.20
% 30.01/30.20 Changing weight limit from 17 to 10.
% 30.01/30.20
% 30.01/30.20 Resetting weight limit to 10 after 745 givens.
% 30.01/30.20
% 33.65/33.88
% 33.65/33.88
% 33.65/33.88 Changing weight limit from 10 to 9.
% 33.65/33.88
% 33.65/33.88 Resetting weight limit to 9 after 2900 givens.
% 33.65/33.88
% 34.33/34.55
% 34.33/34.55
% 34.33/34.55 Changing weight limit from 9 to 8.
% 34.33/34.55
% 34.33/34.55 Resetting weight limit to 8 after 3490 givens.
% 34.33/34.55
% 35.88/36.08
% 35.88/36.08
% 35.88/36.08 Changing weight limit from 8 to 9.
% 35.88/36.08
% 35.88/36.08 Resetting weight limit to 9 after 5670 givens.
% 35.88/36.08
% 35.88/36.08
% 35.88/36.08
% 35.88/36.08 Changing weight limit from 9 to 10.
% 35.88/36.08
% 35.88/36.08 Resetting weight limit to 10 after 5675 givens.
% 35.88/36.08
% 35.88/36.09
% 35.88/36.09
% 35.88/36.09 Changing weight limit from 10 to 11.
% 35.88/36.09
% 35.88/36.09 Resetting weight limit to 11 after 5680 givens.
% 35.88/36.09
% 35.88/36.09
% 35.88/36.09
% 35.88/36.09 Changing weight limit from 11 to 12.
% 35.88/36.09
% 35.88/36.09 Resetting weight limit to 12 after 5685 givens.
% 35.88/36.09
% 35.88/36.10
% 35.88/36.10
% 35.88/36.10 Changing weight limit from 12 to 13.
% 35.88/36.10
% 35.88/36.10 Resetting weight limit to 13 after 5690 givens.
% 35.88/36.10
% 35.88/36.11
% 35.88/36.11
% 35.88/36.11 Changing weight limit from 13 to 14.
% 35.88/36.11
% 35.88/36.11 Resetting weight limit to 14 after 5695 givens.
% 35.88/36.11
% 35.88/36.11
% 35.88/36.11
% 35.88/36.11 Changing weight limit from 14 to 15.
% 35.88/36.11
% 35.88/36.11 Resetting weight limit to 15 after 5700 givens.
% 35.88/36.11
% 35.88/36.11
% 35.88/36.11
% 35.88/36.11 Changing weight limit from 15 to 16.
% 35.88/36.11
% 35.88/36.11 Resetting weight limit to 16 after 5705 givens.
% 35.88/36.11
% 36.55/36.73
% 36.55/36.73
% 36.55/36.73 Changing weight limit from 16 to 14.
% 36.55/36.73
% 36.55/36.73 Resetting weight limit to 14 after 6450 givens.
% 36.55/36.73
% 37.01/37.23
% 37.01/37.23
% 37.01/37.23 Changing weight limit from 14 to 11.
% 37.01/37.23
% 37.01/37.23 Resetting weight limit to 11 after 6725 givens.
% 37.01/37.23
% 37.07/37.31
% 37.07/37.31
% 37.07/37.31 Changing weight limit from 11 to 10.
% 37.07/37.31
% 37.07/37.31 Resetting weight limit to 10 after 6730 givens.
% 37.07/37.31
% 37.24/37.43
% 37.24/37.43
% 37.24/37.43 Changing weight limit from 10 to 9.
% 37.24/37.43
% 37.24/37.43 Resetting weight limit to 9 after 6740 givens.
% 37.24/37.43
% 39.97/40.20
% 39.97/40.20
% 39.97/40.20 Changing weight limit from 9 to 8.
% 39.97/40.20
% 39.97/40.20 Resetting weight limit to 8 after 8425 givens.
% 39.97/40.20
% 55.53/55.78
% 55.53/55.78 -- HEY sandbox, WE HAVE A PROOF!! --
% 55.53/55.78
% 55.53/55.78 ----> UNIT CONFLICT at 54.41 sec ----> 58895 [binary,58894.1,113.1] {-} $F.
% 55.53/55.78
% 55.53/55.78 Length of proof is 246. Level of proof is 28.
% 55.53/55.78
% 55.53/55.78 ---------------- PROOF ----------------
% 55.53/55.78 % SZS status Theorem
% 55.53/55.78 % SZS output start Refutation
% 55.53/55.78
% 55.53/55.78 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 55.53/55.78 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 55.53/55.78 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 55.53/55.78 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 55.53/55.78 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 55.53/55.78 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 55.53/55.78 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 55.53/55.78 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 55.53/55.78 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 55.53/55.78 12 [] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|circle(A,B,C,D).
% 55.53/55.78 14 [] {+} -cyclic(A,B,C,D)|cyclic(A,B,D,C).
% 55.53/55.78 15 [] {+} -cyclic(A,B,C,D)|cyclic(A,C,B,D).
% 55.53/55.78 16 [] {+} -cyclic(A,B,C,D)|cyclic(B,A,C,D).
% 55.53/55.78 17 [] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)|cyclic(B,C,D,E).
% 55.53/55.78 23 [] {+} -cong(A,B,C,D)|cong(A,B,D,C).
% 55.53/55.78 24 [] {+} -cong(A,B,C,D)|cong(C,D,A,B).
% 55.53/55.78 25 [] {+} -cong(A,B,C,D)| -cong(C,D,E,F)|cong(A,B,E,F).
% 55.53/55.78 40 [] {+} -para(A,B,C,D)|eqangle(A,B,E,F,C,D,E,F).
% 55.53/55.78 43 [] {+} -eqangle(A,B,A,C,D,B,D,C)| -coll(A,D,C)|cyclic(B,C,A,D).
% 55.53/55.78 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).
% 55.53/55.78 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 55.53/55.78 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 55.53/55.78 53 [] {+} -perp(A,B,B,C)| -midp(D,A,C)|cong(A,D,B,D).
% 55.53/55.78 54 [] {+} -circle(A,B,C,D)| -coll(A,B,D)|perp(B,C,C,D).
% 55.53/55.78 58 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)| -cyclic(A,C,B,D)|perp(B,A,A,D).
% 55.53/55.78 64 [] {+} -midp(A,B,C)| -midp(A,D,E)|para(B,D,C,E).
% 55.53/55.78 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 55.53/55.78 67 [] {+} -para(A,B,A,C)|coll(A,B,C).
% 55.53/55.78 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 55.53/55.78 69 [] {+} -midp(A,B,C)|cong(A,B,A,C).
% 55.53/55.78 70 [] {+} -midp(A,B,C)|coll(A,B,C).
% 55.53/55.78 113 [] {+} -para($c10,$c9,$c13,$c7).
% 55.53/55.78 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 55.53/55.78 116 [factor,12.1.2] {+} -cong(A,B,A,C)|circle(A,B,C,C).
% 55.53/55.78 120 [factor,17.1.2] {+} -cyclic(A,B,C,D)|cyclic(B,C,D,D).
% 55.53/55.78 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).
% 55.53/55.78 124 [factor,45.1.2] {+} -midp(A,B,C)|para(A,A,C,C).
% 55.53/55.78 126 [factor,58.1.2] {+} -cong(A,B,C,B)| -cyclic(A,C,B,B)|perp(B,A,A,B).
% 55.53/55.78 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 55.53/55.78 160 [] {-} perp($c14,$c13,$c13,$c11).
% 55.53/55.78 162 [] {-} perp($c14,$c12,$c12,$c11).
% 55.53/55.78 164 [] {-} coll($c9,$c11,$c10).
% 55.53/55.78 166 [] {-} midp($c8,$c10,$c9).
% 55.53/55.78 167 [] {-} coll($c12,$c8,$c7).
% 55.53/55.78 187 [hyper,164,114] {-} coll($c10,$c10,$c9).
% 55.53/55.78 188 [hyper,164,2] {-} coll($c11,$c9,$c10).
% 55.53/55.78 189 [hyper,164,1] {-} coll($c9,$c10,$c11).
% 55.53/55.78 208 [hyper,166,70] {-} coll($c8,$c10,$c9).
% 55.53/55.78 209 [hyper,166,69] {-} cong($c8,$c10,$c8,$c9).
% 55.53/55.78 210 [hyper,166,11] {-} midp($c8,$c9,$c10).
% 55.53/55.78 223 [hyper,167,114] {-} coll($c7,$c7,$c12).
% 55.53/55.78 224 [hyper,167,2] {-} coll($c8,$c12,$c7).
% 55.53/55.78 225 [hyper,167,1] {-} coll($c12,$c7,$c8).
% 55.53/55.78 239 [hyper,160,8] {-} perp($c13,$c11,$c14,$c13).
% 55.53/55.78 258 [hyper,187,1] {-} coll($c10,$c9,$c10).
% 55.53/55.78 271 [hyper,188,114] {-} coll($c10,$c10,$c11).
% 55.53/55.78 274 [hyper,188,1] {-} coll($c11,$c10,$c9).
% 55.53/55.78 287 [hyper,189,114] {-} coll($c11,$c11,$c9).
% 55.53/55.78 301 [hyper,208,114] {-} coll($c9,$c9,$c8).
% 55.53/55.78 302 [hyper,208,2] {-} coll($c10,$c8,$c9).
% 55.53/55.78 303 [hyper,208,1] {-} coll($c8,$c9,$c10).
% 55.53/55.78 339 [hyper,210,124] {-} para($c8,$c8,$c10,$c10).
% 55.53/55.78 348 [hyper,210,69] {-} cong($c8,$c9,$c8,$c10).
% 55.53/55.78 363 [hyper,223,114] {-} coll($c12,$c12,$c7).
% 55.53/55.78 377 [hyper,224,114] {-} coll($c7,$c7,$c8).
% 55.53/55.78 378 [hyper,224,1] {-} coll($c8,$c7,$c12).
% 55.53/55.78 391 [hyper,225,114] {-} coll($c8,$c8,$c12).
% 55.53/55.78 407 [hyper,162,8] {-} perp($c12,$c11,$c14,$c12).
% 55.53/55.78 454 [hyper,271,114] {-} coll($c11,$c11,$c10).
% 55.53/55.78 468 [hyper,274,114] {-} coll($c9,$c9,$c11).
% 55.53/55.78 534 [hyper,301,114] {-} coll($c8,$c8,$c9).
% 55.53/55.78 548 [hyper,302,1] {-} coll($c10,$c9,$c8).
% 55.53/55.78 593 [hyper,363,1] {-} coll($c12,$c7,$c12).
% 55.53/55.78 620 [hyper,377,114] {-} coll($c8,$c8,$c7).
% 55.53/55.78 621 [hyper,377,1] {-} coll($c7,$c8,$c7).
% 55.53/55.78 653 [hyper,378,2] {-} coll($c7,$c8,$c12).
% 55.53/55.78 897 [hyper,468,3,301] {-} coll($c8,$c11,$c9).
% 55.53/55.78 1058 [hyper,534,3,391] {-} coll($c12,$c9,$c8).
% 55.53/55.78 1059 [hyper,534,3,391] {-} coll($c9,$c12,$c8).
% 55.53/55.78 1060 [hyper,534,1] {-} coll($c8,$c9,$c8).
% 55.53/55.78 1086 [hyper,548,114] {-} coll($c8,$c8,$c10).
% 55.53/55.78 1090 [hyper,548,3,258] {-} coll($c8,$c10,$c10).
% 55.53/55.78 1230 [hyper,593,3,225] {-} coll($c12,$c8,$c12).
% 55.53/55.78 1368 [hyper,620,3,534] {-} coll($c9,$c7,$c8).
% 55.53/55.78 1369 [hyper,620,3,534] {-} coll($c7,$c9,$c8).
% 55.53/55.78 1674 [hyper,897,1] {-} coll($c8,$c9,$c11).
% 55.53/55.78 1904 [hyper,1058,1] {-} coll($c12,$c8,$c9).
% 55.53/55.78 1917 [hyper,1059,1] {-} coll($c9,$c8,$c12).
% 55.53/55.78 1930 [hyper,1060,3,303] {-} coll($c10,$c8,$c8).
% 55.53/55.78 1931 [hyper,1060,3,303] {-} coll($c8,$c10,$c8).
% 55.53/55.78 1932 [hyper,1060,2] {-} coll($c9,$c8,$c8).
% 55.53/55.78 2017 [hyper,1086,3,620] {-} coll($c7,$c10,$c8).
% 55.53/55.78 2267 [hyper,1368,1] {-} coll($c9,$c8,$c7).
% 55.53/55.78 2280 [hyper,1369,1] {-} coll($c7,$c8,$c9).
% 55.53/55.78 2441 [hyper,1674,114] {-} coll($c11,$c11,$c8).
% 55.53/55.78 2443 [hyper,1674,3,1060] {-} coll($c8,$c11,$c8).
% 55.53/55.78 2446 [hyper,1674,2] {-} coll($c9,$c8,$c11).
% 55.53/55.78 2481 [hyper,1904,3,1230] {-} coll($c12,$c9,$c12).
% 55.53/55.78 2591 [hyper,2017,1] {-} coll($c7,$c8,$c10).
% 55.53/55.78 2773 [hyper,2280,3,653] {-} coll($c12,$c9,$c7).
% 55.53/55.78 2774 [hyper,2280,3,621] {-} coll($c7,$c9,$c7).
% 55.53/55.78 2971 [hyper,2446,3,2267] {-} coll($c7,$c11,$c9).
% 55.53/55.78 2972 [hyper,2446,3,1917] {-} coll($c12,$c11,$c9).
% 55.53/55.78 3403 [hyper,2591,3,621] {-} coll($c7,$c10,$c7).
% 55.53/55.78 3823 [hyper,2971,1] {-} coll($c7,$c9,$c11).
% 55.53/55.78 3876 [hyper,2972,1] {-} coll($c12,$c9,$c11).
% 55.53/55.78 4693 [hyper,209,116] {-} circle($c8,$c10,$c9,$c9).
% 55.53/55.78 4695 [hyper,209,23] {-} cong($c8,$c10,$c9,$c8).
% 55.53/55.78 4998 [hyper,3823,114] {-} coll($c11,$c11,$c7).
% 55.53/55.78 5000 [hyper,3823,3,2774] {-} coll($c7,$c11,$c7).
% 55.53/55.78 5019 [hyper,3876,114] {-} coll($c11,$c11,$c12).
% 55.53/55.78 5023 [hyper,3876,3,2481] {-} coll($c12,$c11,$c12).
% 55.53/55.78 6128 [hyper,239,9,160] {-} para($c14,$c13,$c14,$c13).
% 55.53/55.78 6129 [hyper,239,9,160] {-} para($c13,$c11,$c13,$c11).
% 55.53/55.78 6130 [hyper,239,7] {-} perp($c13,$c11,$c13,$c14).
% 55.53/55.78 6368 [hyper,339,5] {-} para($c10,$c10,$c8,$c8).
% 55.53/55.78 6388 [hyper,348,25,209] {-} cong($c8,$c10,$c8,$c10).
% 55.53/55.78 6597 [hyper,407,9,162] {-} para($c14,$c12,$c14,$c12).
% 55.53/55.78 6598 [hyper,407,9,162] {-} para($c12,$c11,$c12,$c11).
% 55.53/55.78 6753 [hyper,4693,54,208] {-} perp($c10,$c9,$c9,$c9).
% 55.53/55.78 6771 [hyper,4695,24] {-} cong($c9,$c8,$c8,$c10).
% 55.53/55.78 6788 [hyper,6128,67] {-} coll($c14,$c13,$c13).
% 55.53/55.78 6789 [hyper,6128,40] {-} eqangle($c14,$c13,A,B,$c14,$c13,A,B).
% 55.53/55.78 6807 [hyper,6788,114] {-} coll($c13,$c13,$c14).
% 55.53/55.78 6810 [hyper,6788,2] {-} coll($c13,$c14,$c13).
% 55.53/55.78 6823 [hyper,6807,114] {-} coll($c14,$c14,$c13).
% 55.53/55.78 6836 [hyper,6810,114] {-} coll($c13,$c13,$c13).
% 55.53/55.78 6851 [hyper,6823,1] {-} coll($c14,$c13,$c14).
% 55.53/55.78 6876 [hyper,6851,114] {-} coll($c14,$c14,$c14).
% 55.53/55.78 6879 [hyper,6851,3,6788] {-} coll($c13,$c14,$c14).
% 55.53/55.78 6928 [hyper,6129,67] {-} coll($c13,$c11,$c11).
% 55.53/55.78 6929 [hyper,6129,40] {-} eqangle($c13,$c11,A,B,$c13,$c11,A,B).
% 55.53/55.78 6946 [hyper,6928,114] {-} coll($c11,$c11,$c13).
% 55.53/55.78 6961 [hyper,6946,114] {-} coll($c13,$c13,$c11).
% 55.53/55.78 6966 [hyper,6946,3,5019] {-} coll($c12,$c13,$c11).
% 55.53/55.78 6967 [hyper,6946,3,4998] {-} coll($c7,$c13,$c11).
% 55.53/55.78 6968 [hyper,6946,3,2441] {-} coll($c8,$c13,$c11).
% 55.53/55.78 6969 [hyper,6946,3,454] {-} coll($c10,$c13,$c11).
% 55.53/55.78 6970 [hyper,6946,3,287] {-} coll($c9,$c13,$c11).
% 55.53/55.78 6971 [hyper,6946,3,5019] {-} coll($c13,$c12,$c11).
% 55.53/55.78 6974 [hyper,6946,3,454] {-} coll($c13,$c10,$c11).
% 55.53/55.78 6975 [hyper,6946,3,287] {-} coll($c13,$c9,$c11).
% 55.53/55.78 7008 [hyper,6961,3,6836] {-} coll($c13,$c11,$c13).
% 55.53/55.78 7011 [hyper,6961,3,6807] {-} coll($c11,$c14,$c13).
% 55.53/55.78 7026 [hyper,6966,1] {-} coll($c12,$c11,$c13).
% 55.53/55.78 7041 [hyper,6967,1] {-} coll($c7,$c11,$c13).
% 55.53/55.78 7056 [hyper,6968,1] {-} coll($c8,$c11,$c13).
% 55.53/55.78 7071 [hyper,6969,1] {-} coll($c10,$c11,$c13).
% 55.53/55.78 7086 [hyper,6970,1] {-} coll($c9,$c11,$c13).
% 55.53/55.78 7099 [hyper,6971,1] {-} coll($c13,$c11,$c12).
% 55.53/55.78 7138 [hyper,6974,1] {-} coll($c13,$c11,$c10).
% 55.53/55.78 7151 [hyper,6975,1] {-} coll($c13,$c11,$c9).
% 55.53/55.78 7230 [hyper,7011,1] {-} coll($c11,$c13,$c14).
% 55.53/55.78 7243 [hyper,7026,114] {-} coll($c13,$c13,$c12).
% 55.53/55.78 7245 [hyper,7026,3,5023] {-} coll($c12,$c13,$c12).
% 55.53/55.78 7268 [hyper,7041,114] {-} coll($c13,$c13,$c7).
% 55.53/55.78 7276 [hyper,7041,3,5000] {-} coll($c13,$c7,$c7).
% 55.53/55.78 7293 [hyper,7056,114] {-} coll($c13,$c13,$c8).
% 55.53/55.78 7302 [hyper,7056,3,2443] {-} coll($c13,$c8,$c8).
% 55.53/55.78 7318 [hyper,7071,114] {-} coll($c13,$c13,$c10).
% 55.53/55.78 7343 [hyper,7086,114] {-} coll($c13,$c13,$c9).
% 55.53/55.78 7369 [hyper,7099,3,7008] {-} coll($c13,$c12,$c13).
% 55.53/55.78 7370 [hyper,7099,3,7008] {-} coll($c12,$c13,$c13).
% 55.53/55.78 7458 [hyper,7138,3,7099] {-} coll($c12,$c10,$c13).
% 55.53/55.78 7481 [hyper,7151,3,7008] {-} coll($c13,$c9,$c13).
% 55.53/55.78 7522 [hyper,7230,114] {-} coll($c14,$c14,$c11).
% 55.53/55.78 7710 [hyper,7268,3,6807] {-} coll($c7,$c14,$c13).
% 55.53/55.78 7878 [hyper,7293,3,6807] {-} coll($c8,$c14,$c13).
% 55.53/55.78 8083 [hyper,7318,3,6807] {-} coll($c10,$c14,$c13).
% 55.53/55.78 8303 [hyper,7343,3,6807] {-} coll($c9,$c14,$c13).
% 55.53/55.78 9298 [hyper,7710,1] {-} coll($c7,$c13,$c14).
% 55.53/55.78 9392 [hyper,7878,1] {-} coll($c8,$c13,$c14).
% 55.53/55.78 9454 [hyper,8083,1] {-} coll($c10,$c13,$c14).
% 55.53/55.78 9516 [hyper,8303,1] {-} coll($c9,$c13,$c14).
% 55.53/55.78 9649 [hyper,9298,114] {-} coll($c14,$c14,$c7).
% 55.53/55.78 9723 [hyper,9392,114] {-} coll($c14,$c14,$c8).
% 55.53/55.78 9799 [hyper,9454,114] {-} coll($c14,$c14,$c10).
% 55.53/55.78 9877 [hyper,9516,114] {-} coll($c14,$c14,$c9).
% 55.53/55.78 11667 [hyper,6130,8] {-} perp($c13,$c14,$c13,$c11).
% 55.53/55.78 12411 [hyper,6388,68,1090] {-} midp($c8,$c10,$c10).
% 55.53/55.78 12451 [hyper,12411,64,210] {-} para($c9,$c10,$c10,$c10).
% 55.53/55.78 12453 [hyper,12411,64,210] {-} para($c10,$c9,$c10,$c10).
% 55.53/55.78 12454 [hyper,12411,64,166] {-} para($c10,$c10,$c10,$c9).
% 55.53/55.78 13589 [hyper,6753,53,166] {-} cong($c10,$c8,$c9,$c8).
% 55.53/55.78 13593 [hyper,6771,25,4695] {-} cong($c9,$c8,$c9,$c8).
% 55.53/55.78 13742 [hyper,11667,9,6130] {-} para($c13,$c14,$c13,$c14).
% 55.53/55.78 14478 [hyper,12451,6,6368] {-} para($c9,$c10,$c8,$c8).
% 55.53/55.78 16491 [hyper,13593,68,1932] {-} midp($c9,$c8,$c8).
% 55.53/55.78 17364 [hyper,14478,46,16491,1930] {-} midp($c10,$c8,$c8).
% 55.53/55.78 26776 [hyper,6789,43,9877] {-} cyclic($c13,$c9,$c14,$c14).
% 55.53/55.78 26777 [hyper,6789,43,9799] {-} cyclic($c13,$c10,$c14,$c14).
% 55.53/55.78 26778 [hyper,6789,43,9723] {-} cyclic($c13,$c8,$c14,$c14).
% 55.53/55.78 26779 [hyper,6789,43,9649] {-} cyclic($c13,$c7,$c14,$c14).
% 55.53/55.78 26781 [hyper,6789,43,7522] {-} cyclic($c13,$c11,$c14,$c14).
% 55.53/55.78 26782 [hyper,6789,43,6876] {-} cyclic($c13,$c14,$c14,$c14).
% 55.53/55.78 26783 [hyper,6789,43,6823] {-} cyclic($c13,$c13,$c14,$c14).
% 55.53/55.78 26788 [hyper,26776,15] {-} cyclic($c13,$c14,$c9,$c14).
% 55.53/55.78 26791 [hyper,26777,15] {-} cyclic($c13,$c14,$c10,$c14).
% 55.53/55.78 26794 [hyper,26778,15] {-} cyclic($c13,$c14,$c8,$c14).
% 55.53/55.78 26797 [hyper,26779,15] {-} cyclic($c13,$c14,$c7,$c14).
% 55.53/55.78 26804 [hyper,26781,16] {-} cyclic($c11,$c13,$c14,$c14).
% 55.53/55.78 26808 [hyper,26783,15] {-} cyclic($c13,$c14,$c13,$c14).
% 55.53/55.78 26818 [hyper,26788,14] {-} cyclic($c13,$c14,$c14,$c9).
% 55.53/55.78 26832 [hyper,6929,43,7268] {-} cyclic($c11,$c7,$c13,$c13).
% 55.53/55.78 26833 [hyper,6929,43,7243] {-} cyclic($c11,$c12,$c13,$c13).
% 55.53/55.78 26834 [hyper,6929,43,6961] {-} cyclic($c11,$c11,$c13,$c13).
% 55.53/55.78 26836 [hyper,6929,43,6807] {-} cyclic($c11,$c14,$c13,$c13).
% 55.53/55.78 26843 [hyper,26791,14] {-} cyclic($c13,$c14,$c14,$c10).
% 55.53/55.78 26852 [hyper,26794,16] {-} cyclic($c14,$c13,$c8,$c14).
% 55.53/55.78 26853 [hyper,26794,14] {-} cyclic($c13,$c14,$c14,$c8).
% 55.53/55.78 26859 [hyper,26797,16] {-} cyclic($c14,$c13,$c7,$c14).
% 55.53/55.78 26875 [hyper,26804,15] {-} cyclic($c11,$c14,$c13,$c14).
% 55.53/55.78 26887 [hyper,26808,14] {-} cyclic($c13,$c14,$c14,$c13).
% 55.53/55.78 26916 [hyper,26832,15] {-} cyclic($c11,$c13,$c7,$c13).
% 55.53/55.78 26919 [hyper,26833,15] {-} cyclic($c11,$c13,$c12,$c13).
% 55.53/55.78 26920 [hyper,26834,15] {-} cyclic($c11,$c13,$c11,$c13).
% 55.53/55.78 26941 [hyper,26843,17,26818] {-} cyclic($c14,$c14,$c10,$c9).
% 55.53/55.78 26948 [hyper,26852,14] {-} cyclic($c14,$c13,$c14,$c8).
% 55.53/55.78 26952 [hyper,26853,120] {-} cyclic($c14,$c14,$c8,$c8).
% 55.53/55.78 26954 [hyper,26853,17,26843] {-} cyclic($c14,$c14,$c10,$c8).
% 55.53/55.78 26957 [hyper,26853,17,26843] {-} cyclic($c14,$c14,$c8,$c10).
% 55.53/55.78 26965 [hyper,26859,14] {-} cyclic($c14,$c13,$c14,$c7).
% 55.53/55.78 27003 [hyper,26875,17,26836] {-} cyclic($c14,$c13,$c14,$c13).
% 55.53/55.78 27029 [hyper,26887,123,26782,6789] {-} cong($c13,$c14,$c13,$c14).
% 55.53/55.78 27099 [hyper,26916,14] {-} cyclic($c11,$c13,$c13,$c7).
% 55.53/55.78 27109 [hyper,26919,14] {-} cyclic($c11,$c13,$c13,$c12).
% 55.53/55.78 27112 [hyper,26920,14] {-} cyclic($c11,$c13,$c13,$c11).
% 55.53/55.78 27164 [hyper,26948,120] {-} cyclic($c13,$c14,$c8,$c8).
% 55.53/55.78 27179 [hyper,26954,17,26941] {-} cyclic($c14,$c10,$c9,$c8).
% 55.53/55.78 27196 [hyper,26957,17,26952] {-} cyclic($c14,$c8,$c8,$c10).
% 55.53/55.78 27218 [hyper,26965,120] {-} cyclic($c13,$c14,$c7,$c7).
% 55.53/55.78 27409 [hyper,27003,17,26965] {-} cyclic($c13,$c14,$c7,$c13).
% 55.53/55.78 27410 [hyper,27003,17,26948] {-} cyclic($c13,$c14,$c8,$c13).
% 55.53/55.78 27577 [hyper,27029,68,6879] {-} midp($c13,$c14,$c14).
% 55.53/55.78 27581 [hyper,27577,129,6597] {-} midp($c13,$c12,$c12).
% 55.53/55.78 27582 [hyper,27577,129,6128] {-} midp($c13,$c13,$c13).
% 55.53/55.78 27599 [hyper,27581,129,6598] {-} midp($c13,$c11,$c11).
% 55.53/55.78 27615 [hyper,27581,69] {-} cong($c13,$c12,$c13,$c12).
% 55.53/55.78 27636 [hyper,27582,64,27581] {-} para($c12,$c13,$c12,$c13).
% 55.53/55.78 27637 [hyper,27582,64,27581] {-} para($c13,$c12,$c13,$c12).
% 55.53/55.78 27638 [hyper,27582,46,13742,6851] {-} midp($c14,$c13,$c14).
% 55.53/55.78 27680 [hyper,27599,69] {-} cong($c13,$c11,$c13,$c11).
% 55.53/55.78 27706 [hyper,27638,46,6597,7245] {-} midp($c12,$c13,$c12).
% 55.53/55.78 27792 [hyper,27706,69] {-} cong($c12,$c13,$c12,$c12).
% 55.53/55.78 27793 [hyper,27706,11] {-} midp($c12,$c12,$c13).
% 55.53/55.78 27826 [hyper,27793,69] {-} cong($c12,$c12,$c12,$c13).
% 55.53/55.78 28093 [hyper,27112,17,27109] {-} cyclic($c13,$c13,$c11,$c12).
% 55.53/55.78 28094 [hyper,27112,17,27099] {-} cyclic($c13,$c13,$c11,$c7).
% 55.53/55.78 28199 [hyper,27164,15] {-} cyclic($c13,$c8,$c14,$c8).
% 55.53/55.78 28229 [hyper,27179,120] {-} cyclic($c10,$c9,$c8,$c8).
% 55.53/55.78 28341 [hyper,27196,120] {-} cyclic($c8,$c8,$c10,$c10).
% 55.53/55.78 28424 [hyper,27218,15] {-} cyclic($c13,$c7,$c14,$c7).
% 55.53/55.78 29532 [hyper,27409,15] {-} cyclic($c13,$c7,$c14,$c13).
% 55.53/55.78 29533 [hyper,27410,15] {-} cyclic($c13,$c8,$c14,$c13).
% 55.53/55.78 30613 [hyper,27826,25,27792] {-} cong($c12,$c13,$c12,$c13).
% 55.53/55.78 31871 [hyper,28093,58,27680,27615] {-} perp($c11,$c13,$c13,$c12).
% 55.53/55.78 31874 [hyper,28229,126,13589] {-} perp($c8,$c10,$c10,$c8).
% 55.53/55.78 31876 [hyper,28341,126,6388] {-} perp($c10,$c8,$c8,$c10).
% 55.53/55.78 31880 [hyper,29532,44,28424,26779,6789] {-} cong($c13,$c7,$c13,$c7).
% 55.53/55.78 31881 [hyper,29533,44,28199,26778,6789] {-} cong($c13,$c8,$c13,$c8).
% 55.53/55.78 40692 [hyper,30613,68,7370] {-} midp($c12,$c13,$c13).
% 55.53/55.78 40698 [hyper,40692,129,27637] {-} midp($c12,$c12,$c12).
% 55.53/55.78 40920 [hyper,40698,46,27636,7369] {-} midp($c13,$c12,$c13).
% 55.53/55.78 48707 [hyper,31871,8] {-} perp($c13,$c12,$c11,$c13).
% 55.53/55.78 49159 [hyper,31876,9,31874] {-} para($c8,$c10,$c8,$c10).
% 55.53/55.78 49161 [hyper,31876,9,31874] {-} para($c10,$c8,$c10,$c8).
% 55.53/55.78 49439 [hyper,31880,68,7276] {-} midp($c13,$c7,$c7).
% 55.53/55.78 49440 [hyper,31880,58,27680,28094] {-} perp($c11,$c13,$c13,$c7).
% 55.53/55.78 49636 [hyper,49439,64,40920] {-} para($c7,$c12,$c7,$c13).
% 55.53/55.78 49645 [hyper,49439,64,27582] {-} para($c7,$c13,$c7,$c13).
% 55.53/55.78 49651 [hyper,31881,68,7302] {-} midp($c13,$c8,$c8).
% 55.53/55.78 49835 [hyper,49651,64,49439] {-} para($c8,$c7,$c8,$c7).
% 55.53/55.78 51882 [hyper,49159,129,17364] {-} midp($c10,$c10,$c10).
% 55.53/55.78 51887 [hyper,51882,65,12453,12454] {-} midp($c10,$c9,$c10).
% 55.53/55.78 51951 [hyper,49161,46,51887,1060] {-} midp($c8,$c9,$c8).
% 55.53/55.78 51952 [hyper,49161,46,51882,1931] {-} midp($c8,$c10,$c8).
% 55.53/55.78 52119 [hyper,49440,9,48707] {-} para($c13,$c12,$c13,$c7).
% 55.53/55.78 53766 [hyper,49835,46,51952,3403] {-} midp($c7,$c10,$c7).
% 55.53/55.78 53767 [hyper,49835,46,51951,2774] {-} midp($c7,$c9,$c7).
% 55.53/55.78 53952 [hyper,53766,46,49636,7458] {-} midp($c12,$c10,$c13).
% 55.53/55.78 53961 [hyper,53767,46,49645,7481] {-} midp($c13,$c9,$c13).
% 55.53/55.78 58718 [hyper,52119,46,53961,2773] {-} midp($c12,$c9,$c7).
% 55.53/55.78 58894 [hyper,58718,64,53952] {-} para($c10,$c9,$c13,$c7).
% 55.53/55.78 58895 [binary,58894.1,113.1] {-} $F.
% 55.53/55.78
% 55.53/55.78 % SZS output end Refutation
% 55.53/55.78 ------------ end of proof -------------
% 55.53/55.78
% 55.53/55.78
% 55.53/55.78 Search stopped by max_proofs option.
% 55.53/55.78
% 55.53/55.78
% 55.53/55.78 Search stopped by max_proofs option.
% 55.53/55.78
% 55.53/55.78 ============ end of search ============
% 55.53/55.78
% 55.53/55.78 That finishes the proof of the theorem.
% 55.53/55.78
% 55.53/55.78 Process 31096 finished Sat Jun 18 16:29:58 2022
%------------------------------------------------------------------------------