%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO551+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:20:51 EDT 2022
% Result : Theorem 48.72s 48.92s
% Output : Refutation 48.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO551+1 : TPTP v8.1.0. Released v7.5.0.
% 0.07/0.13 % Command : sos-script %s
% 0.13/0.34 % Computer : n018.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 : Sat Jun 18 10:43:18 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.38 ----- Otter 3.2, August 2001 -----
% 0.13/0.38 The process was started by sandbox2 on n018.cluster.edu,
% 0.13/0.38 Sat Jun 18 10:43:18 2022
% 0.13/0.38 The command was "./sos". The process ID is 25998.
% 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 164 during input processing: 0 [copy,164,flip.1] {-} A=A.
% 0.13/0.38 164 back subsumes 146.
% 0.13/0.38 164 back subsumes 145.
% 0.13/0.38 164 back subsumes 144.
% 0.13/0.38 164 back subsumes 143.
% 0.13/0.38
% 0.13/0.38 ======= end of input processing =======
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 Failed to model usable list: disabling FINDER
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 -------------- Softie stats --------------
% 0.21/0.44
% 0.21/0.44 UPDATE_STOP: 300
% 0.21/0.44 SFINDER_TIME_LIMIT: 2
% 0.21/0.44 SHORT_CLAUSE_CUTOFF: 4
% 0.21/0.44 number of clauses in intial UL: 154
% 0.21/0.44 number of clauses initially in problem: 160
% 0.21/0.44 percentage of clauses intially in UL: 96
% 0.21/0.44 percentage of distinct symbols occuring in initial UL: 92
% 0.21/0.44 percent of all initial clauses that are short: 100
% 0.21/0.44 absolute distinct symbol count: 39
% 0.21/0.44 distinct predicate count: 12
% 0.21/0.44 distinct function count: 20
% 0.21/0.44 distinct constant count: 7
% 0.21/0.44
% 0.21/0.44 ---------- no more Softie stats ----------
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44
% 0.21/0.44 =========== start of search ===========
% 6.36/6.55
% 6.36/6.55
% 6.36/6.55 Changing weight limit from 60 to 57.
% 6.36/6.55
% 6.36/6.55 Resetting weight limit to 57 after 230 givens.
% 6.36/6.55
% 7.02/7.21
% 7.02/7.21
% 7.02/7.21 Changing weight limit from 57 to 56.
% 7.02/7.21
% 7.02/7.21 Resetting weight limit to 56 after 235 givens.
% 7.02/7.21
% 9.28/9.48
% 9.28/9.48
% 9.28/9.48 Changing weight limit from 56 to 55.
% 9.28/9.48
% 9.28/9.48 Resetting weight limit to 55 after 250 givens.
% 9.28/9.48
% 11.48/11.72
% 11.48/11.72
% 11.48/11.72 Changing weight limit from 55 to 52.
% 11.48/11.72
% 11.48/11.72 Resetting weight limit to 52 after 270 givens.
% 11.48/11.72
% 13.12/13.30
% 13.12/13.30
% 13.12/13.30 Changing weight limit from 52 to 51.
% 13.12/13.30
% 13.12/13.30 Resetting weight limit to 51 after 280 givens.
% 13.12/13.30
% 16.19/16.40
% 16.19/16.40
% 16.19/16.40 Changing weight limit from 51 to 50.
% 16.19/16.40
% 16.19/16.40 Modelling stopped after 300 given clauses and 0.00 seconds
% 16.19/16.40
% 16.19/16.40
% 16.19/16.40 Resetting weight limit to 50 after 300 givens.
% 16.19/16.40
% 18.48/18.66
% 18.48/18.66
% 18.48/18.66 Changing weight limit from 50 to 49.
% 18.48/18.66
% 18.48/18.66 Resetting weight limit to 49 after 315 givens.
% 18.48/18.66
% 19.27/19.45
% 19.27/19.45
% 19.27/19.45 Changing weight limit from 49 to 47.
% 19.27/19.45
% 19.27/19.45 Resetting weight limit to 47 after 325 givens.
% 19.27/19.45
% 19.59/19.79
% 19.59/19.79
% 19.59/19.79 Changing weight limit from 47 to 46.
% 19.59/19.79
% 19.59/19.79 Resetting weight limit to 46 after 330 givens.
% 19.59/19.79
% 20.08/20.31
% 20.08/20.31
% 20.08/20.31 Changing weight limit from 46 to 45.
% 20.08/20.31
% 20.08/20.31 Resetting weight limit to 45 after 340 givens.
% 20.08/20.31
% 20.59/20.80
% 20.59/20.80
% 20.59/20.80 Changing weight limit from 45 to 44.
% 20.59/20.80
% 20.59/20.80 Resetting weight limit to 44 after 350 givens.
% 20.59/20.80
% 20.66/20.91
% 20.66/20.91
% 20.66/20.91 Changing weight limit from 44 to 37.
% 20.66/20.91
% 20.66/20.91 Resetting weight limit to 37 after 355 givens.
% 20.66/20.91
% 20.99/21.18
% 20.99/21.18
% 20.99/21.18 Changing weight limit from 37 to 36.
% 20.99/21.18
% 20.99/21.18 Resetting weight limit to 36 after 365 givens.
% 20.99/21.18
% 21.51/21.70
% 21.51/21.70
% 21.51/21.70 Changing weight limit from 36 to 35.
% 21.51/21.70
% 21.51/21.70 Resetting weight limit to 35 after 390 givens.
% 21.51/21.70
% 21.76/21.97
% 21.76/21.97
% 21.76/21.97 Changing weight limit from 35 to 34.
% 21.76/21.97
% 21.76/21.97 Resetting weight limit to 34 after 400 givens.
% 21.76/21.97
% 22.09/22.28
% 22.09/22.28
% 22.09/22.28 Changing weight limit from 34 to 30.
% 22.09/22.28
% 22.09/22.28 Resetting weight limit to 30 after 405 givens.
% 22.09/22.28
% 25.32/25.51
% 25.32/25.51
% 25.32/25.51 Changing weight limit from 30 to 29.
% 25.32/25.51
% 25.32/25.51 Resetting weight limit to 29 after 465 givens.
% 25.32/25.51
% 26.07/26.28
% 26.07/26.28
% 26.07/26.28 Changing weight limit from 29 to 22.
% 26.07/26.28
% 26.07/26.28 Resetting weight limit to 22 after 500 givens.
% 26.07/26.28
% 26.16/26.33
% 26.16/26.33
% 26.16/26.33 Changing weight limit from 22 to 17.
% 26.16/26.33
% 26.16/26.33 Resetting weight limit to 17 after 505 givens.
% 26.16/26.33
% 26.21/26.44
% 26.21/26.44
% 26.21/26.44 Changing weight limit from 17 to 15.
% 26.21/26.44
% 26.21/26.44 Resetting weight limit to 15 after 510 givens.
% 26.21/26.44
% 26.29/26.50
% 26.29/26.50
% 26.29/26.50 Changing weight limit from 15 to 11.
% 26.29/26.50
% 26.29/26.50 Resetting weight limit to 11 after 515 givens.
% 26.29/26.50
% 26.39/26.57
% 26.39/26.57
% 26.39/26.57 Changing weight limit from 11 to 10.
% 26.39/26.57
% 26.39/26.57 Resetting weight limit to 10 after 525 givens.
% 26.39/26.57
% 28.31/28.54
% 28.31/28.54
% 28.31/28.54 Changing weight limit from 10 to 9.
% 28.31/28.54
% 28.31/28.54 Resetting weight limit to 9 after 1015 givens.
% 28.31/28.54
% 39.40/39.59
% 39.40/39.59
% 39.40/39.59 Changing weight limit from 9 to 8.
% 39.40/39.59
% 39.40/39.59 Resetting weight limit to 8 after 4620 givens.
% 39.40/39.59
% 48.72/48.92
% 48.72/48.92 -- HEY sandbox2, WE HAVE A PROOF!! --
% 48.72/48.92
% 48.72/48.92 ----> UNIT CONFLICT at 47.78 sec ----> 190712 [binary,190711.1,113.1] {-} $F.
% 48.72/48.92
% 48.72/48.92 Length of proof is 197. Level of proof is 19.
% 48.72/48.92
% 48.72/48.92 ---------------- PROOF ----------------
% 48.72/48.92 % SZS status Theorem
% 48.72/48.92 % SZS output start Refutation
% 48.72/48.92
% 48.72/48.92 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 48.72/48.92 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 48.72/48.92 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 48.72/48.92 4 [] {+} -para(A,B,C,D)|para(A,B,D,C).
% 48.72/48.92 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 48.72/48.92 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 48.72/48.92 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 48.72/48.92 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 48.72/48.92 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 48.72/48.92 10 [] {+} -para(A,B,C,D)| -perp(C,D,E,F)|perp(A,B,E,F).
% 48.72/48.92 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 48.72/48.92 13 [] {+} -cong(A,B,A,C)| -cong(A,B,A,D)| -cong(A,B,A,E)|cyclic(B,C,D,E).
% 48.72/48.92 23 [] {+} -cong(A,B,C,D)|cong(A,B,D,C).
% 48.72/48.92 24 [] {+} -cong(A,B,C,D)|cong(C,D,A,B).
% 48.72/48.92 25 [] {+} -cong(A,B,C,D)| -cong(C,D,E,F)|cong(A,B,E,F).
% 48.72/48.92 40 [] {+} -para(A,B,C,D)|eqangle(A,B,E,F,C,D,E,F).
% 48.72/48.92 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).
% 48.72/48.92 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 48.72/48.92 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 48.72/48.92 57 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)|perp(A,C,B,D).
% 48.72/48.92 64 [] {+} -midp(A,B,C)| -midp(A,D,E)|para(B,D,C,E).
% 48.72/48.92 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 48.72/48.92 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 48.72/48.92 69 [] {+} -midp(A,B,C)|cong(A,B,A,C).
% 48.72/48.92 70 [] {+} -midp(A,B,C)|coll(A,B,C).
% 48.72/48.92 113 [] {+} -cyclic($c3,$c4,$c2,$c1).
% 48.72/48.92 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 48.72/48.92 117 [factor,13.1.2] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|cyclic(B,C,C,D).
% 48.72/48.92 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).
% 48.72/48.92 124 [factor,45.1.2] {+} -midp(A,B,C)|para(A,A,C,C).
% 48.72/48.92 128 [factor,64.1.2] {+} -midp(A,B,C)|para(B,B,C,C).
% 48.72/48.92 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 48.72/48.92 154 [factor,117.1.2] {+} -cong(A,B,A,C)|cyclic(B,C,C,C).
% 48.72/48.92 159 [] {-} perp($c4,$c7,$c6,$c5).
% 48.72/48.92 160 [] {-} coll($c4,$c6,$c5).
% 48.72/48.92 161 [] {-} midp($c3,$c7,$c6).
% 48.72/48.92 162 [] {-} midp($c2,$c5,$c6).
% 48.72/48.92 163 [] {-} midp($c1,$c7,$c5).
% 48.72/48.92 165 [hyper,159,8] {-} perp($c6,$c5,$c4,$c7).
% 48.72/48.92 183 [hyper,160,114] {-} coll($c5,$c5,$c4).
% 48.72/48.92 184 [hyper,160,2] {-} coll($c6,$c4,$c5).
% 48.72/48.92 185 [hyper,160,1] {-} coll($c4,$c5,$c6).
% 48.72/48.92 202 [hyper,161,128] {-} para($c7,$c7,$c6,$c6).
% 48.72/48.92 204 [hyper,161,70] {-} coll($c3,$c7,$c6).
% 48.72/48.92 205 [hyper,161,69] {-} cong($c3,$c7,$c3,$c6).
% 48.72/48.92 206 [hyper,161,11] {-} midp($c3,$c6,$c7).
% 48.72/48.92 223 [hyper,162,128] {-} para($c5,$c5,$c6,$c6).
% 48.72/48.92 224 [hyper,162,124] {-} para($c2,$c2,$c6,$c6).
% 48.72/48.92 233 [hyper,162,70] {-} coll($c2,$c5,$c6).
% 48.72/48.92 234 [hyper,162,69] {-} cong($c2,$c5,$c2,$c6).
% 48.72/48.92 235 [hyper,162,11] {-} midp($c2,$c6,$c5).
% 48.72/48.92 252 [hyper,163,128] {-} para($c7,$c7,$c5,$c5).
% 48.72/48.92 253 [hyper,163,124] {-} para($c1,$c1,$c5,$c5).
% 48.72/48.92 270 [hyper,163,70] {-} coll($c1,$c7,$c5).
% 48.72/48.92 271 [hyper,163,69] {-} cong($c1,$c7,$c1,$c5).
% 48.72/48.92 272 [hyper,163,45,161] {-} para($c3,$c1,$c6,$c5).
% 48.72/48.92 273 [hyper,163,45,161] {-} para($c1,$c3,$c5,$c6).
% 48.72/48.92 274 [hyper,163,11] {-} midp($c1,$c5,$c7).
% 48.72/48.92 288 [hyper,183,1] {-} coll($c5,$c4,$c5).
% 48.72/48.92 301 [hyper,184,114] {-} coll($c5,$c5,$c6).
% 48.72/48.92 315 [hyper,185,114] {-} coll($c6,$c6,$c4).
% 48.72/48.92 329 [hyper,204,114] {-} coll($c6,$c6,$c3).
% 48.72/48.92 330 [hyper,204,2] {-} coll($c7,$c3,$c6).
% 48.72/48.92 331 [hyper,204,1] {-} coll($c3,$c6,$c7).
% 48.72/48.92 345 [hyper,165,9,159] {-} para($c6,$c5,$c6,$c5).
% 48.72/48.92 346 [hyper,165,7] {-} perp($c6,$c5,$c7,$c4).
% 48.72/48.92 368 [hyper,206,124] {-} para($c3,$c3,$c7,$c7).
% 48.72/48.92 393 [hyper,206,69] {-} cong($c3,$c6,$c3,$c7).
% 48.72/48.92 394 [hyper,206,64,161] {-} para($c7,$c6,$c6,$c7).
% 48.72/48.92 395 [hyper,206,64,161] {-} para($c6,$c7,$c7,$c6).
% 48.72/48.92 408 [hyper,233,114] {-} coll($c6,$c6,$c2).
% 48.72/48.92 409 [hyper,233,2] {-} coll($c5,$c2,$c6).
% 48.72/48.92 410 [hyper,233,1] {-} coll($c2,$c6,$c5).
% 48.72/48.92 461 [hyper,235,69] {-} cong($c2,$c6,$c2,$c5).
% 48.72/48.92 462 [hyper,235,64,162] {-} para($c5,$c6,$c6,$c5).
% 48.72/48.92 464 [hyper,235,45,206] {-} para($c3,$c2,$c7,$c5).
% 48.72/48.92 465 [hyper,235,45,206] {-} para($c2,$c3,$c5,$c7).
% 48.72/48.92 478 [hyper,270,114] {-} coll($c5,$c5,$c1).
% 48.72/48.92 479 [hyper,270,2] {-} coll($c7,$c1,$c5).
% 48.72/48.92 480 [hyper,270,1] {-} coll($c1,$c5,$c7).
% 48.72/48.92 514 [hyper,274,128] {-} para($c5,$c5,$c7,$c7).
% 48.72/48.92 515 [hyper,274,124] {-} para($c1,$c1,$c7,$c7).
% 48.72/48.92 556 [hyper,274,69] {-} cong($c1,$c5,$c1,$c7).
% 48.72/48.92 557 [hyper,274,64,163] {-} para($c7,$c5,$c5,$c7).
% 48.72/48.92 558 [hyper,274,64,163] {-} para($c5,$c7,$c7,$c5).
% 48.72/48.92 559 [hyper,274,45,162] {-} para($c2,$c1,$c6,$c7).
% 48.72/48.92 560 [hyper,274,45,162] {-} para($c1,$c2,$c7,$c6).
% 48.72/48.92 586 [hyper,288,114] {-} coll($c5,$c5,$c5).
% 48.72/48.92 601 [hyper,301,1] {-} coll($c5,$c6,$c5).
% 48.72/48.92 728 [hyper,315,1] {-} coll($c6,$c4,$c6).
% 48.72/48.92 755 [hyper,329,3,315] {-} coll($c4,$c3,$c6).
% 48.72/48.92 757 [hyper,329,1] {-} coll($c6,$c3,$c6).
% 48.72/48.92 870 [hyper,330,114] {-} coll($c6,$c6,$c7).
% 48.72/48.92 884 [hyper,331,114] {-} coll($c7,$c7,$c3).
% 48.72/48.92 900 [hyper,408,3,315] {-} coll($c4,$c2,$c6).
% 48.72/48.92 903 [hyper,408,1] {-} coll($c6,$c2,$c6).
% 48.72/48.92 916 [hyper,409,1] {-} coll($c5,$c6,$c2).
% 48.72/48.92 1029 [hyper,410,114] {-} coll($c5,$c5,$c2).
% 48.72/48.92 1043 [hyper,478,114] {-} coll($c1,$c1,$c5).
% 48.72/48.92 1046 [hyper,478,3,301] {-} coll($c1,$c6,$c5).
% 48.72/48.92 1047 [hyper,478,3,183] {-} coll($c1,$c4,$c5).
% 48.72/48.92 1061 [hyper,479,114] {-} coll($c5,$c5,$c7).
% 48.72/48.92 1075 [hyper,480,114] {-} coll($c7,$c7,$c1).
% 48.72/48.92 1205 [hyper,586,3,478] {-} coll($c1,$c5,$c5).
% 48.72/48.92 1364 [hyper,728,3,184] {-} coll($c5,$c6,$c6).
% 48.72/48.92 1483 [hyper,755,1] {-} coll($c4,$c6,$c3).
% 48.72/48.92 1589 [hyper,757,2] {-} coll($c3,$c6,$c6).
% 48.72/48.92 1602 [hyper,870,114] {-} coll($c7,$c7,$c6).
% 48.72/48.92 1605 [hyper,870,3,315] {-} coll($c4,$c7,$c6).
% 48.72/48.92 1636 [hyper,884,1] {-} coll($c7,$c3,$c7).
% 48.72/48.92 1768 [hyper,900,1] {-} coll($c4,$c6,$c2).
% 48.72/48.92 1863 [hyper,903,2] {-} coll($c2,$c6,$c6).
% 48.72/48.92 1880 [hyper,916,3,601] {-} coll($c2,$c5,$c5).
% 48.72/48.92 1950 [hyper,1029,3,478] {-} coll($c1,$c2,$c5).
% 48.72/48.92 1976 [hyper,1043,1] {-} coll($c1,$c5,$c1).
% 48.72/48.92 2071 [hyper,1046,1] {-} coll($c1,$c5,$c6).
% 48.72/48.92 2084 [hyper,1047,1] {-} coll($c1,$c5,$c4).
% 48.72/48.92 2165 [hyper,1061,114] {-} coll($c7,$c7,$c5).
% 48.72/48.92 2166 [hyper,1061,3,1029] {-} coll($c2,$c7,$c5).
% 48.72/48.92 2200 [hyper,1075,3,884] {-} coll($c3,$c1,$c7).
% 48.72/48.92 2201 [hyper,1075,3,884] {-} coll($c1,$c3,$c7).
% 48.72/48.92 2202 [hyper,1075,1] {-} coll($c7,$c1,$c7).
% 48.72/48.92 2587 [hyper,1602,3,1075] {-} coll($c1,$c6,$c7).
% 48.72/48.92 2686 [hyper,1605,1] {-} coll($c4,$c6,$c7).
% 48.72/48.92 2897 [hyper,1636,2] {-} coll($c3,$c7,$c7).
% 48.72/48.92 3024 [hyper,1768,3,160] {-} coll($c2,$c5,$c4).
% 48.72/48.92 3254 [hyper,1950,1] {-} coll($c1,$c5,$c2).
% 48.72/48.92 3329 [hyper,1976,3,1205] {-} coll($c5,$c1,$c1).
% 48.72/48.92 3469 [hyper,2165,3,884] {-} coll($c3,$c5,$c7).
% 48.72/48.92 3738 [hyper,2200,1] {-} coll($c3,$c7,$c1).
% 48.72/48.92 3751 [hyper,2201,1] {-} coll($c1,$c7,$c3).
% 48.72/48.92 3765 [hyper,2202,2] {-} coll($c1,$c7,$c7).
% 48.72/48.92 4279 [hyper,2587,1] {-} coll($c1,$c7,$c6).
% 48.72/48.92 4383 [hyper,2686,3,1483] {-} coll($c3,$c7,$c4).
% 48.72/48.92 5575 [hyper,3254,3,2084] {-} coll($c2,$c4,$c1).
% 48.72/48.92 5579 [hyper,3254,2] {-} coll($c5,$c1,$c2).
% 48.72/48.92 6637 [hyper,224,5] {-} para($c6,$c6,$c2,$c2).
% 48.72/48.92 6766 [hyper,3738,2] {-} coll($c7,$c3,$c1).
% 48.72/48.92 7536 [hyper,4279,3,3751] {-} coll($c6,$c3,$c1).
% 48.72/48.92 7660 [hyper,234,154] {-} cyclic($c5,$c6,$c6,$c6).
% 48.72/48.92 7790 [hyper,4383,3,3738] {-} coll($c1,$c4,$c3).
% 48.72/48.92 8963 [hyper,253,6,223] {-} para($c1,$c1,$c6,$c6).
% 48.72/48.92 8964 [hyper,253,5] {-} para($c5,$c5,$c1,$c1).
% 48.72/48.92 9208 [hyper,271,23] {-} cong($c1,$c7,$c5,$c1).
% 48.72/48.92 9324 [hyper,272,5] {-} para($c6,$c5,$c3,$c1).
% 48.72/48.92 9325 [hyper,272,4] {-} para($c3,$c1,$c5,$c6).
% 48.72/48.92 9440 [hyper,273,5] {-} para($c5,$c6,$c1,$c3).
% 48.72/48.92 9674 [hyper,345,40] {-} eqangle($c6,$c5,A,B,$c6,$c5,A,B).
% 48.72/48.92 9685 [hyper,346,8] {-} perp($c7,$c4,$c6,$c5).
% 48.72/48.92 9924 [hyper,368,6,252] {-} para($c3,$c3,$c5,$c5).
% 48.72/48.92 9937 [hyper,393,25,205] {-} cong($c3,$c7,$c3,$c7).
% 48.72/48.92 9938 [hyper,393,25,205] {-} cong($c3,$c6,$c3,$c6).
% 48.72/48.92 10053 [hyper,394,4] {-} para($c7,$c6,$c7,$c6).
% 48.72/48.92 10167 [hyper,395,6,394] {-} para($c6,$c7,$c6,$c7).
% 48.72/48.92 10413 [hyper,461,25,234] {-} cong($c2,$c5,$c2,$c5).
% 48.72/48.92 10414 [hyper,461,25,234] {-} cong($c2,$c6,$c2,$c6).
% 48.72/48.92 10529 [hyper,462,10,346] {-} perp($c5,$c6,$c7,$c4).
% 48.72/48.92 10761 [hyper,464,5] {-} para($c7,$c5,$c3,$c2).
% 48.72/48.92 11240 [hyper,515,5] {-} para($c7,$c7,$c1,$c1).
% 48.72/48.92 11252 [hyper,556,25,271] {-} cong($c1,$c7,$c1,$c7).
% 48.72/48.92 11719 [hyper,559,5] {-} para($c6,$c7,$c2,$c1).
% 48.72/48.92 11826 [hyper,560,6,394] {-} para($c1,$c2,$c6,$c7).
% 48.72/48.92 11827 [hyper,560,5] {-} para($c7,$c6,$c1,$c2).
% 48.72/48.92 12487 [hyper,8963,6,6637] {-} para($c1,$c1,$c2,$c2).
% 48.72/48.92 12612 [hyper,9208,24] {-} cong($c5,$c1,$c1,$c7).
% 48.72/48.92 12723 [hyper,9324,6,462] {-} para($c5,$c6,$c3,$c1).
% 48.72/48.92 12727 [hyper,9324,4] {-} para($c6,$c5,$c1,$c3).
% 48.72/48.92 12940 [hyper,9440,6,9325] {-} para($c3,$c1,$c1,$c3).
% 48.72/48.92 12941 [hyper,9440,6,273] {-} para($c1,$c3,$c1,$c3).
% 48.72/48.92 13163 [hyper,9685,9,346] {-} para($c7,$c4,$c7,$c4).
% 48.72/48.92 13592 [hyper,9924,6,8964] {-} para($c3,$c3,$c1,$c1).
% 48.72/48.92 13721 [hyper,9937,68,2897] {-} midp($c3,$c7,$c7).
% 48.72/48.92 13865 [hyper,13721,64,206] {-} para($c6,$c7,$c7,$c7).
% 48.72/48.92 13870 [hyper,13721,46,464,2166] {-} midp($c2,$c7,$c5).
% 48.72/48.92 14034 [hyper,13870,65,557,252] {-} midp($c2,$c5,$c7).
% 48.72/48.92 14231 [hyper,9938,68,1589] {-} midp($c3,$c6,$c6).
% 48.72/48.92 14273 [hyper,14231,129,345] {-} midp($c3,$c5,$c5).
% 48.72/48.92 14508 [hyper,14273,46,9325,2071] {-} midp($c1,$c5,$c6).
% 48.72/48.92 15235 [hyper,10413,117,234] {-} cyclic($c5,$c6,$c6,$c5).
% 48.72/48.92 15238 [hyper,10413,68,1880] {-} midp($c2,$c5,$c5).
% 48.72/48.92 15308 [hyper,15238,46,465,3469] {-} midp($c3,$c5,$c7).
% 48.72/48.92 15313 [hyper,15238,45,162] {-} para($c2,$c2,$c6,$c5).
% 48.72/48.92 15314 [hyper,15238,45,14508] {-} para($c2,$c1,$c5,$c6).
% 48.72/48.92 15315 [hyper,15238,45,14273] {-} para($c2,$c3,$c5,$c5).
% 48.72/48.92 15377 [hyper,15308,65,558,514] {-} midp($c3,$c7,$c5).
% 48.72/48.92 15464 [hyper,15377,46,9325,4279] {-} midp($c1,$c7,$c6).
% 48.72/48.92 15535 [hyper,15464,65,394,202] {-} midp($c1,$c6,$c7).
% 48.72/48.92 15618 [hyper,15535,46,560,1863] {-} midp($c2,$c6,$c6).
% 48.72/48.92 15624 [hyper,15618,129,10167] {-} midp($c2,$c7,$c7).
% 48.72/48.92 15790 [hyper,15624,45,161] {-} para($c2,$c3,$c7,$c6).
% 48.72/48.92 15798 [hyper,10414,57,10413] {-} perp($c2,$c2,$c5,$c6).
% 48.72/48.92 16466 [hyper,11252,68,3765] {-} midp($c1,$c7,$c7).
% 48.72/48.92 16475 [hyper,16466,129,10053] {-} midp($c1,$c6,$c6).
% 48.72/48.92 17686 [hyper,11826,6,11719] {-} para($c1,$c2,$c2,$c1).
% 48.72/48.92 19309 [hyper,12612,25,9208] {-} cong($c5,$c1,$c5,$c1).
% 48.72/48.92 20061 [hyper,13163,129,16466] {-} midp($c1,$c4,$c4).
% 48.72/48.92 20284 [hyper,20061,64,16475] {-} para($c6,$c4,$c6,$c4).
% 48.72/48.92 20913 [hyper,13865,6,11240] {-} para($c6,$c7,$c1,$c1).
% 48.72/48.92 26881 [hyper,15313,6,12727] {-} para($c2,$c2,$c1,$c3).
% 48.72/48.92 26992 [hyper,15314,6,9440] {-} para($c2,$c1,$c1,$c3).
% 48.72/48.92 27105 [hyper,15315,6,8964] {-} para($c2,$c3,$c1,$c1).
% 48.72/48.92 34210 [hyper,15790,6,11827] {-} para($c2,$c3,$c1,$c2).
% 48.72/48.92 34251 [hyper,15798,9,10529] {-} para($c2,$c2,$c7,$c4).
% 48.72/48.92 37008 [hyper,19309,68,3329] {-} midp($c5,$c1,$c1).
% 48.72/48.92 37012 [hyper,37008,129,12941] {-} midp($c5,$c3,$c3).
% 48.72/48.92 37471 [hyper,37012,46,12723,7536] {-} midp($c6,$c3,$c1).
% 48.72/48.92 42692 [hyper,20913,46,37471,6766] {-} midp($c7,$c3,$c1).
% 48.72/48.92 42801 [hyper,42692,65,12940,13592] {-} midp($c7,$c1,$c3).
% 48.72/48.92 42908 [hyper,42801,46,10761,5579] {-} midp($c5,$c1,$c2).
% 48.72/48.92 43126 [hyper,42908,65,17686,12487] {-} midp($c5,$c2,$c1).
% 48.72/48.92 45399 [hyper,34251,46,14034,3024] {-} midp($c2,$c5,$c4).
% 48.72/48.92 45821 [hyper,45399,64,15618] {-} para($c5,$c6,$c4,$c6).
% 48.72/48.92 48319 [hyper,9674,123,15235,7660] {-} cong($c5,$c6,$c5,$c6).
% 48.72/48.92 55122 [hyper,48319,68,1364] {-} midp($c5,$c6,$c6).
% 48.72/48.92 55132 [hyper,55122,129,20284] {-} midp($c5,$c4,$c4).
% 48.72/48.92 55332 [hyper,55122,64,43126] {-} para($c6,$c2,$c6,$c1).
% 48.72/48.92 55333 [hyper,55122,64,42908] {-} para($c6,$c1,$c6,$c2).
% 48.72/48.92 55588 [hyper,55132,46,45821,728] {-} midp($c6,$c4,$c6).
% 48.72/48.92 78682 [hyper,55332,46,55588,5575] {-} midp($c2,$c4,$c1).
% 48.72/48.92 79701 [hyper,78682,46,26992,7790] {-} midp($c1,$c4,$c3).
% 48.72/48.92 87268 [hyper,79701,11] {-} midp($c1,$c3,$c4).
% 48.72/48.92 101669 [hyper,87268,69] {-} cong($c1,$c3,$c1,$c4).
% 48.72/48.92 105947 [hyper,55333,65,16475,55332] {-} midp($c1,$c2,$c1).
% 48.72/48.92 106413 [hyper,105947,65,34210,26881] {-} midp($c1,$c3,$c2).
% 48.72/48.92 106414 [hyper,105947,65,27105,26992] {-} midp($c1,$c3,$c1).
% 48.72/48.92 110872 [hyper,106413,69] {-} cong($c1,$c3,$c1,$c2).
% 48.72/48.92 111353 [hyper,106414,69] {-} cong($c1,$c3,$c1,$c1).
% 48.72/48.92 190711 [hyper,111353,13,101669,110872] {-} cyclic($c3,$c4,$c2,$c1).
% 48.72/48.92 190712 [binary,190711.1,113.1] {-} $F.
% 48.72/48.92
% 48.72/48.92 % SZS output end Refutation
% 48.72/48.92 ------------ end of proof -------------
% 48.72/48.92
% 48.72/48.92
% 48.72/48.92 Search stopped by max_proofs option.
% 48.72/48.92
% 48.72/48.92
% 48.72/48.92 Search stopped by max_proofs option.
% 48.72/48.92
% 48.72/48.92 ============ end of search ============
% 48.72/48.92
% 48.72/48.92 That finishes the proof of the theorem.
% 48.72/48.92
% 48.72/48.92 Process 25998 finished Sat Jun 18 10:44:06 2022
%------------------------------------------------------------------------------