%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO651+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n028.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:20 EDT 2022
% Result : Theorem 46.98s 47.19s
% Output : Refutation 46.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO651+1 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.13 % Command : sos-script %s
% 0.12/0.34 % Computer : n028.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Fri Jun 17 19:14:43 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.12/0.37 ----- Otter 3.2, August 2001 -----
% 0.12/0.37 The process was started by sandbox2 on n028.cluster.edu,
% 0.12/0.37 Fri Jun 17 19:14:43 2022
% 0.12/0.37 The command was "./sos". The process ID is 7348.
% 0.12/0.37
% 0.12/0.37 set(prolog_style_variables).
% 0.12/0.37 set(auto).
% 0.12/0.37 dependent: set(auto1).
% 0.12/0.37 dependent: set(process_input).
% 0.12/0.37 dependent: clear(print_kept).
% 0.12/0.37 dependent: clear(print_new_demod).
% 0.12/0.37 dependent: clear(print_back_demod).
% 0.12/0.37 dependent: clear(print_back_sub).
% 0.12/0.37 dependent: set(control_memory).
% 0.12/0.37 dependent: assign(max_mem, 12000).
% 0.12/0.37 dependent: assign(pick_given_ratio, 4).
% 0.12/0.37 dependent: assign(stats_level, 1).
% 0.12/0.37 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.37 dependent: assign(sos_limit, 5000).
% 0.12/0.37 dependent: assign(max_weight, 60).
% 0.12/0.37 clear(print_given).
% 0.12/0.37
% 0.12/0.37 formula_list(usable).
% 0.12/0.37
% 0.12/0.37 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.12/0.37
% 0.12/0.37 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.37 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.37 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.37 clauses in usable.
% 0.12/0.37
% 0.12/0.37 dependent: set(knuth_bendix).
% 0.12/0.37 dependent: set(para_from).
% 0.12/0.37 dependent: set(para_into).
% 0.12/0.37 dependent: clear(para_from_right).
% 0.12/0.37 dependent: clear(para_into_right).
% 0.12/0.37 dependent: set(para_from_vars).
% 0.12/0.37 dependent: set(eq_units_both_ways).
% 0.12/0.37 dependent: set(dynamic_demod_all).
% 0.12/0.37 dependent: set(dynamic_demod).
% 0.12/0.37 dependent: set(order_eq).
% 0.12/0.37 dependent: set(back_demod).
% 0.12/0.37 dependent: set(lrpo).
% 0.12/0.37 dependent: set(hyper_res).
% 0.12/0.37 dependent: set(unit_deletion).
% 0.12/0.37 dependent: set(factor).
% 0.12/0.37
% 0.12/0.37 ------------> process usable:
% 0.12/0.37 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.12/0.37
% 0.12/0.37 ------------> process sos:
% 0.12/0.37 Following clause subsumed by 169 during input processing: 0 [copy,169,flip.1] {-} A=A.
% 0.12/0.37 169 back subsumes 146.
% 0.12/0.37 169 back subsumes 145.
% 0.12/0.37 169 back subsumes 144.
% 0.12/0.37 169 back subsumes 143.
% 0.12/0.37
% 0.12/0.37 ======= end of input processing =======
% 0.19/0.43
% 0.19/0.43
% 0.19/0.43 Failed to model usable list: disabling FINDER
% 0.19/0.43
% 0.19/0.43
% 0.19/0.43
% 0.19/0.43 -------------- Softie stats --------------
% 0.19/0.43
% 0.19/0.43 UPDATE_STOP: 300
% 0.19/0.43 SFINDER_TIME_LIMIT: 2
% 0.19/0.43 SHORT_CLAUSE_CUTOFF: 4
% 0.19/0.43 number of clauses in intial UL: 154
% 0.19/0.43 number of clauses initially in problem: 165
% 0.19/0.43 percentage of clauses intially in UL: 93
% 0.19/0.43 percentage of distinct symbols occuring in initial UL: 87
% 0.19/0.43 percent of all initial clauses that are short: 100
% 0.19/0.43 absolute distinct symbol count: 41
% 0.19/0.43 distinct predicate count: 12
% 0.19/0.43 distinct function count: 20
% 0.19/0.43 distinct constant count: 9
% 0.19/0.43
% 0.19/0.43 ---------- no more Softie stats ----------
% 0.19/0.43
% 0.19/0.43
% 0.19/0.43
% 0.19/0.43 =========== start of search ===========
% 4.10/4.34
% 4.10/4.34
% 4.10/4.34 Changing weight limit from 60 to 56.
% 4.10/4.34
% 4.10/4.34 Resetting weight limit to 56 after 240 givens.
% 4.10/4.34
% 4.90/5.11
% 4.90/5.11
% 4.90/5.11 Changing weight limit from 56 to 55.
% 4.90/5.11
% 4.90/5.11 Resetting weight limit to 55 after 245 givens.
% 4.90/5.11
% 5.97/6.15
% 5.97/6.15
% 5.97/6.15 Changing weight limit from 55 to 54.
% 5.97/6.15
% 5.97/6.15 Resetting weight limit to 54 after 250 givens.
% 5.97/6.15
% 6.74/6.93
% 6.74/6.93
% 6.74/6.93 Changing weight limit from 54 to 51.
% 6.74/6.93
% 6.74/6.93 Resetting weight limit to 51 after 260 givens.
% 6.74/6.93
% 7.49/7.72
% 7.49/7.72
% 7.49/7.72 Changing weight limit from 51 to 50.
% 7.49/7.72
% 7.49/7.72 Resetting weight limit to 50 after 270 givens.
% 7.49/7.72
% 9.18/9.36
% 9.18/9.36
% 9.18/9.36 Changing weight limit from 50 to 49.
% 9.18/9.36
% 9.18/9.36 Resetting weight limit to 49 after 295 givens.
% 9.18/9.36
% 10.04/10.22
% 10.04/10.22
% 10.04/10.22 Changing weight limit from 49 to 45.
% 10.04/10.22
% 10.04/10.22 Modelling stopped after 300 given clauses and 0.00 seconds
% 10.04/10.22
% 10.04/10.22
% 10.04/10.22 Resetting weight limit to 45 after 310 givens.
% 10.04/10.22
% 10.45/10.64
% 10.45/10.64
% 10.45/10.64 Changing weight limit from 45 to 37.
% 10.45/10.64
% 10.45/10.64 Resetting weight limit to 37 after 320 givens.
% 10.45/10.64
% 10.79/11.02
% 10.79/11.02
% 10.79/11.02 Changing weight limit from 37 to 36.
% 10.79/11.02
% 10.79/11.02 Resetting weight limit to 36 after 335 givens.
% 10.79/11.02
% 11.39/11.60
% 11.39/11.60
% 11.39/11.60 Changing weight limit from 36 to 35.
% 11.39/11.60
% 11.39/11.60 Resetting weight limit to 35 after 350 givens.
% 11.39/11.60
% 12.00/12.18
% 12.00/12.18
% 12.00/12.18 Changing weight limit from 35 to 31.
% 12.00/12.18
% 12.00/12.18 Resetting weight limit to 31 after 360 givens.
% 12.00/12.18
% 12.30/12.50
% 12.30/12.50
% 12.30/12.50 Changing weight limit from 31 to 30.
% 12.30/12.50
% 12.30/12.50 Resetting weight limit to 30 after 365 givens.
% 12.30/12.50
% 15.46/15.67
% 15.46/15.67
% 15.46/15.67 Changing weight limit from 30 to 29.
% 15.46/15.67
% 15.46/15.67 Resetting weight limit to 29 after 455 givens.
% 15.46/15.67
% 16.16/16.38
% 16.16/16.38
% 16.16/16.38 Changing weight limit from 29 to 23.
% 16.16/16.38
% 16.16/16.38 Resetting weight limit to 23 after 530 givens.
% 16.16/16.38
% 16.19/16.43
% 16.19/16.43
% 16.19/16.43 Changing weight limit from 23 to 22.
% 16.19/16.43
% 16.19/16.43 Resetting weight limit to 22 after 540 givens.
% 16.19/16.43
% 16.26/16.45
% 16.26/16.45
% 16.26/16.45 Changing weight limit from 22 to 21.
% 16.26/16.45
% 16.26/16.45 Resetting weight limit to 21 after 545 givens.
% 16.26/16.45
% 16.29/16.49
% 16.29/16.49
% 16.29/16.49 Changing weight limit from 21 to 17.
% 16.29/16.49
% 16.29/16.49 Resetting weight limit to 17 after 555 givens.
% 16.29/16.49
% 16.35/16.55
% 16.35/16.55
% 16.35/16.55 Changing weight limit from 17 to 16.
% 16.35/16.55
% 16.35/16.55 Resetting weight limit to 16 after 595 givens.
% 16.35/16.55
% 16.39/16.61
% 16.39/16.61
% 16.39/16.61 Changing weight limit from 16 to 15.
% 16.39/16.61
% 16.39/16.61 Resetting weight limit to 15 after 630 givens.
% 16.39/16.61
% 16.48/16.68
% 16.48/16.68
% 16.48/16.68 Changing weight limit from 15 to 11.
% 16.48/16.68
% 16.48/16.68 Resetting weight limit to 11 after 650 givens.
% 16.48/16.68
% 16.48/16.71
% 16.48/16.71
% 16.48/16.71 Changing weight limit from 11 to 10.
% 16.48/16.71
% 16.48/16.71 Resetting weight limit to 10 after 665 givens.
% 16.48/16.71
% 17.97/18.17
% 17.97/18.17
% 17.97/18.17 Changing weight limit from 10 to 9.
% 17.97/18.17
% 17.97/18.17 Resetting weight limit to 9 after 1185 givens.
% 17.97/18.17
% 28.37/28.58
% 28.37/28.58
% 28.37/28.58 Changing weight limit from 9 to 5.
% 28.37/28.58
% 28.37/28.58 Resetting weight limit to 5 after 3650 givens.
% 28.37/28.58
% 46.98/47.19
% 46.98/47.19 -- HEY sandbox2, WE HAVE A PROOF!! --
% 46.98/47.19
% 46.98/47.19 ----> UNIT CONFLICT at 44.95 sec ----> 367393 [binary,367392.1,113.1] {-} $F.
% 46.98/47.19
% 46.98/47.19 Length of proof is 245. Level of proof is 27.
% 46.98/47.19
% 46.98/47.19 ---------------- PROOF ----------------
% 46.98/47.19 % SZS status Theorem
% 46.98/47.19 % SZS output start Refutation
% 46.98/47.19
% 46.98/47.19 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 46.98/47.19 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 46.98/47.19 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 46.98/47.19 4 [] {+} -para(A,B,C,D)|para(A,B,D,C).
% 46.98/47.19 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 46.98/47.19 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 46.98/47.19 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 46.98/47.19 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 46.98/47.19 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 46.98/47.19 10 [] {+} -para(A,B,C,D)| -perp(C,D,E,F)|perp(A,B,E,F).
% 46.98/47.19 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 46.98/47.19 12 [] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|circle(A,B,C,D).
% 46.98/47.19 23 [] {+} -cong(A,B,C,D)|cong(A,B,D,C).
% 46.98/47.19 24 [] {+} -cong(A,B,C,D)|cong(C,D,A,B).
% 46.98/47.19 25 [] {+} -cong(A,B,C,D)| -cong(C,D,E,F)|cong(A,B,E,F).
% 46.98/47.19 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 46.98/47.19 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 46.98/47.19 53 [] {+} -perp(A,B,B,C)| -midp(D,A,C)|cong(A,D,B,D).
% 46.98/47.19 54 [] {+} -circle(A,B,C,D)| -coll(A,B,D)|perp(B,C,C,D).
% 46.98/47.19 56 [] {+} -midp(A,B,C)| -perp(D,A,B,C)|cong(D,B,D,C).
% 46.98/47.19 64 [] {+} -midp(A,B,C)| -midp(A,D,E)|para(B,D,C,E).
% 46.98/47.19 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 46.98/47.19 67 [] {+} -para(A,B,A,C)|coll(A,B,C).
% 46.98/47.19 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 46.98/47.19 69 [] {+} -midp(A,B,C)|cong(A,B,A,C).
% 46.98/47.19 70 [] {+} -midp(A,B,C)|coll(A,B,C).
% 46.98/47.19 113 [] {+} -cong($c7,$c4,$c6,$c8).
% 46.98/47.19 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 46.98/47.19 116 [factor,12.1.2] {+} -cong(A,B,A,C)|circle(A,B,C,C).
% 46.98/47.19 124 [factor,45.1.2] {+} -midp(A,B,C)|para(A,A,C,C).
% 46.98/47.19 128 [factor,64.1.2] {+} -midp(A,B,C)|para(B,B,C,C).
% 46.98/47.19 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 46.98/47.19 159 [] {-} coll($c6,$c9,$c8).
% 46.98/47.19 161 [] {-} midp($c3,$c9,$c8).
% 46.98/47.19 162 [] {-} perp($c9,$c8,$c3,$c5).
% 46.98/47.19 163 [] {-} midp($c2,$c9,$c7).
% 46.98/47.19 165 [] {-} midp($c1,$c8,$c7).
% 46.98/47.19 166 [] {-} perp($c8,$c7,$c1,$c5).
% 46.98/47.19 167 [] {-} perp($c7,$c5,$c7,$c4).
% 46.98/47.19 168 [] {-} para($c9,$c7,$c4,$c6).
% 46.98/47.19 170 [hyper,159,114] {-} coll($c8,$c8,$c6).
% 46.98/47.19 171 [hyper,159,2] {-} coll($c9,$c6,$c8).
% 46.98/47.19 172 [hyper,159,1] {-} coll($c6,$c8,$c9).
% 46.98/47.19 189 [hyper,161,128] {-} para($c9,$c9,$c8,$c8).
% 46.98/47.19 190 [hyper,161,124] {-} para($c3,$c3,$c8,$c8).
% 46.98/47.19 191 [hyper,161,70] {-} coll($c3,$c9,$c8).
% 46.98/47.19 192 [hyper,161,69] {-} cong($c3,$c9,$c3,$c8).
% 46.98/47.19 193 [hyper,161,11] {-} midp($c3,$c8,$c9).
% 46.98/47.19 210 [hyper,163,128] {-} para($c9,$c9,$c7,$c7).
% 46.98/47.19 220 [hyper,163,70] {-} coll($c2,$c9,$c7).
% 46.98/47.19 221 [hyper,163,69] {-} cong($c2,$c9,$c2,$c7).
% 46.98/47.19 222 [hyper,163,45,161] {-} para($c3,$c2,$c8,$c7).
% 46.98/47.19 223 [hyper,163,45,161] {-} para($c2,$c3,$c7,$c8).
% 46.98/47.19 224 [hyper,163,11] {-} midp($c2,$c7,$c9).
% 46.98/47.19 241 [hyper,165,128] {-} para($c8,$c8,$c7,$c7).
% 46.98/47.19 242 [hyper,165,124] {-} para($c1,$c1,$c7,$c7).
% 46.98/47.19 259 [hyper,165,70] {-} coll($c1,$c8,$c7).
% 46.98/47.19 260 [hyper,165,69] {-} cong($c1,$c8,$c1,$c7).
% 46.98/47.19 261 [hyper,165,11] {-} midp($c1,$c7,$c8).
% 46.98/47.19 311 [hyper,170,1] {-} coll($c8,$c6,$c8).
% 46.98/47.19 324 [hyper,171,114] {-} coll($c8,$c8,$c9).
% 46.98/47.19 338 [hyper,172,114] {-} coll($c9,$c9,$c6).
% 46.98/47.19 352 [hyper,191,114] {-} coll($c8,$c8,$c3).
% 46.98/47.19 353 [hyper,191,2] {-} coll($c9,$c3,$c8).
% 46.98/47.19 354 [hyper,191,1] {-} coll($c3,$c8,$c9).
% 46.98/47.19 367 [hyper,162,8] {-} perp($c3,$c5,$c9,$c8).
% 46.98/47.19 368 [hyper,162,7] {-} perp($c9,$c8,$c5,$c3).
% 46.98/47.19 415 [hyper,193,69] {-} cong($c3,$c8,$c3,$c9).
% 46.98/47.19 416 [hyper,193,64,161] {-} para($c9,$c8,$c8,$c9).
% 46.98/47.19 417 [hyper,193,64,161] {-} para($c8,$c9,$c9,$c8).
% 46.98/47.19 418 [hyper,193,45,165] {-} para($c1,$c3,$c7,$c9).
% 46.98/47.19 419 [hyper,193,45,165] {-} para($c3,$c1,$c9,$c7).
% 46.98/47.19 432 [hyper,220,114] {-} coll($c7,$c7,$c2).
% 46.98/47.19 433 [hyper,220,2] {-} coll($c9,$c2,$c7).
% 46.98/47.19 434 [hyper,220,1] {-} coll($c2,$c7,$c9).
% 46.98/47.19 485 [hyper,224,69] {-} cong($c2,$c7,$c2,$c9).
% 46.98/47.19 486 [hyper,224,64,163] {-} para($c9,$c7,$c7,$c9).
% 46.98/47.19 500 [hyper,259,114] {-} coll($c7,$c7,$c1).
% 46.98/47.19 501 [hyper,259,2] {-} coll($c8,$c1,$c7).
% 46.98/47.19 502 [hyper,259,1] {-} coll($c1,$c7,$c8).
% 46.98/47.19 579 [hyper,261,69] {-} cong($c1,$c7,$c1,$c8).
% 46.98/47.19 580 [hyper,261,64,165] {-} para($c8,$c7,$c7,$c8).
% 46.98/47.19 581 [hyper,261,64,165] {-} para($c7,$c8,$c8,$c7).
% 46.98/47.19 582 [hyper,261,45,224] {-} para($c2,$c1,$c9,$c8).
% 46.98/47.19 609 [hyper,311,114] {-} coll($c8,$c8,$c8).
% 46.98/47.19 623 [hyper,324,114] {-} coll($c9,$c9,$c8).
% 46.98/47.19 637 [hyper,166,8] {-} perp($c1,$c5,$c8,$c7).
% 46.98/47.19 638 [hyper,166,7] {-} perp($c8,$c7,$c5,$c1).
% 46.98/47.19 669 [hyper,338,1] {-} coll($c9,$c6,$c9).
% 46.98/47.19 695 [hyper,352,114] {-} coll($c3,$c3,$c8).
% 46.98/47.19 697 [hyper,352,3,170] {-} coll($c3,$c6,$c8).
% 46.98/47.19 715 [hyper,167,8] {-} perp($c7,$c4,$c7,$c5).
% 46.98/47.19 716 [hyper,167,7] {-} perp($c7,$c5,$c4,$c7).
% 46.98/47.19 733 [hyper,353,1] {-} coll($c9,$c8,$c3).
% 46.98/47.19 746 [hyper,354,114] {-} coll($c9,$c9,$c3).
% 46.98/47.19 747 [hyper,354,2] {-} coll($c8,$c3,$c9).
% 46.98/47.19 774 [hyper,433,114] {-} coll($c7,$c7,$c9).
% 46.98/47.19 790 [hyper,168,4] {-} para($c9,$c7,$c6,$c4).
% 46.98/47.19 807 [hyper,434,114] {-} coll($c9,$c9,$c2).
% 46.98/47.19 824 [hyper,500,1] {-} coll($c7,$c1,$c7).
% 46.98/47.19 837 [hyper,501,114] {-} coll($c7,$c7,$c8).
% 46.98/47.19 838 [hyper,501,1] {-} coll($c8,$c7,$c1).
% 46.98/47.19 851 [hyper,502,114] {-} coll($c8,$c8,$c1).
% 46.98/47.19 949 [hyper,609,3,352] {-} coll($c3,$c8,$c8).
% 46.98/47.19 974 [hyper,623,1] {-} coll($c9,$c8,$c9).
% 46.98/47.19 1091 [hyper,669,114] {-} coll($c9,$c9,$c9).
% 46.98/47.19 1178 [hyper,695,1] {-} coll($c3,$c8,$c3).
% 46.98/47.19 1204 [hyper,697,1] {-} coll($c3,$c8,$c6).
% 46.98/47.19 1411 [hyper,774,114] {-} coll($c9,$c9,$c7).
% 46.98/47.19 1412 [hyper,774,3,500] {-} coll($c1,$c9,$c7).
% 46.98/47.19 1414 [hyper,774,1] {-} coll($c7,$c9,$c7).
% 46.98/47.19 1629 [hyper,837,114] {-} coll($c8,$c8,$c7).
% 46.98/47.19 1631 [hyper,837,3,432] {-} coll($c2,$c8,$c7).
% 46.98/47.19 1647 [hyper,838,114] {-} coll($c1,$c1,$c8).
% 46.98/47.19 1713 [hyper,851,3,609] {-} coll($c8,$c1,$c8).
% 46.98/47.19 1717 [hyper,851,3,609] {-} coll($c1,$c8,$c8).
% 46.98/47.19 1718 [hyper,851,3,352] {-} coll($c1,$c3,$c8).
% 46.98/47.19 1719 [hyper,851,3,324] {-} coll($c1,$c9,$c8).
% 46.98/47.19 1720 [hyper,851,3,170] {-} coll($c1,$c6,$c8).
% 46.98/47.19 1848 [hyper,974,3,733] {-} coll($c3,$c9,$c9).
% 46.98/47.19 1901 [hyper,1091,3,807] {-} coll($c2,$c9,$c9).
% 46.98/47.19 1939 [hyper,1178,3,949] {-} coll($c8,$c3,$c3).
% 46.98/47.19 2017 [hyper,1204,3,354] {-} coll($c6,$c9,$c3).
% 46.98/47.19 2213 [hyper,1411,3,746] {-} coll($c3,$c7,$c9).
% 46.98/47.19 2215 [hyper,1411,3,338] {-} coll($c6,$c7,$c9).
% 46.98/47.19 2217 [hyper,1411,3,746] {-} coll($c7,$c3,$c9).
% 46.98/47.19 2688 [hyper,190,5] {-} para($c8,$c8,$c3,$c3).
% 46.98/47.19 2706 [hyper,1629,3,352] {-} coll($c3,$c7,$c8).
% 46.98/47.19 2710 [hyper,1629,3,352] {-} coll($c7,$c3,$c8).
% 46.98/47.19 2773 [hyper,192,23] {-} cong($c3,$c9,$c8,$c3).
% 46.98/47.19 3067 [hyper,1718,1] {-} coll($c1,$c8,$c3).
% 46.98/47.19 3100 [hyper,1720,1] {-} coll($c1,$c8,$c6).
% 46.98/47.19 3887 [hyper,2213,1] {-} coll($c3,$c9,$c7).
% 46.98/47.19 3917 [hyper,2215,1] {-} coll($c6,$c9,$c7).
% 46.98/47.19 3992 [hyper,2217,1] {-} coll($c7,$c9,$c3).
% 46.98/47.19 4811 [hyper,2706,1] {-} coll($c3,$c8,$c7).
% 46.98/47.19 5173 [hyper,3067,114] {-} coll($c3,$c3,$c1).
% 46.98/47.19 5212 [hyper,3100,3,259] {-} coll($c6,$c7,$c1).
% 46.98/47.19 5317 [hyper,3917,114] {-} coll($c7,$c7,$c6).
% 46.98/47.19 5324 [hyper,3917,3,2017] {-} coll($c7,$c3,$c6).
% 46.98/47.19 5339 [hyper,3992,114] {-} coll($c3,$c3,$c7).
% 46.98/47.19 5342 [hyper,3992,3,1414] {-} coll($c7,$c3,$c7).
% 46.98/47.19 5344 [hyper,3992,3,1414] {-} coll($c3,$c7,$c7).
% 46.98/47.19 6283 [hyper,223,4] {-} para($c2,$c3,$c8,$c7).
% 46.98/47.19 7677 [hyper,242,5] {-} para($c7,$c7,$c1,$c1).
% 46.98/47.19 9218 [hyper,367,9,162] {-} para($c9,$c8,$c9,$c8).
% 46.98/47.19 9219 [hyper,367,9,162] {-} para($c3,$c5,$c3,$c5).
% 46.98/47.19 9231 [hyper,368,9,367] {-} para($c3,$c5,$c5,$c3).
% 46.98/47.19 9232 [hyper,368,8] {-} perp($c5,$c3,$c9,$c8).
% 46.98/47.19 9475 [hyper,415,116] {-} circle($c3,$c8,$c9,$c9).
% 46.98/47.19 9477 [hyper,415,25,192] {-} cong($c3,$c9,$c3,$c9).
% 46.98/47.19 9708 [hyper,417,6,416] {-} para($c8,$c9,$c8,$c9).
% 46.98/47.19 9824 [hyper,418,4] {-} para($c1,$c3,$c9,$c7).
% 46.98/47.19 9940 [hyper,419,6,168] {-} para($c3,$c1,$c4,$c6).
% 46.98/47.19 10187 [hyper,485,25,221] {-} cong($c2,$c9,$c2,$c9).
% 46.98/47.19 10303 [hyper,486,4] {-} para($c9,$c7,$c9,$c7).
% 46.98/47.19 10645 [hyper,579,25,260] {-} cong($c1,$c8,$c1,$c8).
% 46.98/47.19 10860 [hyper,581,6,580] {-} para($c7,$c8,$c7,$c8).
% 46.98/47.19 11087 [hyper,638,9,637] {-} para($c1,$c5,$c5,$c1).
% 46.98/47.19 11093 [hyper,715,9,167] {-} para($c7,$c5,$c7,$c5).
% 46.98/47.19 11094 [hyper,715,9,167] {-} para($c7,$c4,$c7,$c4).
% 46.98/47.19 11097 [hyper,716,8] {-} perp($c4,$c7,$c7,$c5).
% 46.98/47.19 11106 [hyper,790,6,419] {-} para($c3,$c1,$c6,$c4).
% 46.98/47.19 11228 [hyper,2773,24] {-} cong($c8,$c3,$c3,$c9).
% 46.98/47.19 12239 [hyper,9219,67] {-} coll($c3,$c5,$c5).
% 46.98/47.19 12241 [hyper,12239,114] {-} coll($c5,$c5,$c3).
% 46.98/47.19 12250 [hyper,12241,114] {-} coll($c3,$c3,$c5).
% 46.98/47.19 12268 [hyper,12250,3,5339] {-} coll($c7,$c5,$c3).
% 46.98/47.19 12269 [hyper,12250,3,5173] {-} coll($c1,$c5,$c3).
% 46.98/47.19 12274 [hyper,12250,3,695] {-} coll($c8,$c5,$c3).
% 46.98/47.19 12275 [hyper,12250,3,5339] {-} coll($c5,$c7,$c3).
% 46.98/47.19 12294 [hyper,12268,1] {-} coll($c7,$c3,$c5).
% 46.98/47.19 12301 [hyper,12269,1] {-} coll($c1,$c3,$c5).
% 46.98/47.19 12335 [hyper,12274,1] {-} coll($c8,$c3,$c5).
% 46.98/47.19 12342 [hyper,12275,1] {-} coll($c5,$c3,$c7).
% 46.98/47.19 12499 [hyper,12294,3,5342] {-} coll($c7,$c5,$c7).
% 46.98/47.19 12500 [hyper,12294,3,5324] {-} coll($c6,$c5,$c7).
% 46.98/47.19 12519 [hyper,12301,114] {-} coll($c5,$c5,$c1).
% 46.98/47.19 12633 [hyper,12335,3,747] {-} coll($c5,$c9,$c8).
% 46.98/47.19 12653 [hyper,12342,114] {-} coll($c7,$c7,$c5).
% 46.98/47.19 14217 [hyper,9232,56,161] {-} cong($c5,$c9,$c5,$c8).
% 46.98/47.19 14218 [hyper,9232,9,368] {-} para($c5,$c3,$c5,$c3).
% 46.98/47.19 14500 [hyper,9475,54,354] {-} perp($c8,$c9,$c9,$c9).
% 46.98/47.19 14511 [hyper,9477,68,1848] {-} midp($c3,$c9,$c9).
% 46.98/47.19 14517 [hyper,14511,129,9218] {-} midp($c3,$c8,$c8).
% 46.98/47.19 14542 [hyper,14511,64,193] {-} para($c8,$c9,$c9,$c9).
% 46.98/47.19 14547 [hyper,14511,46,419,1412] {-} midp($c1,$c9,$c7).
% 46.98/47.19 14585 [hyper,14517,46,222,1631] {-} midp($c2,$c8,$c7).
% 46.98/47.19 14622 [hyper,14547,65,486,210] {-} midp($c1,$c7,$c9).
% 46.98/47.19 14670 [hyper,14585,65,580,241] {-} midp($c2,$c7,$c8).
% 46.98/47.19 14763 [hyper,14670,46,6283,5344] {-} midp($c3,$c7,$c7).
% 46.98/47.19 15274 [hyper,9940,5] {-} para($c4,$c6,$c3,$c1).
% 46.98/47.19 16117 [hyper,10187,68,1901] {-} midp($c2,$c9,$c9).
% 46.98/47.19 16123 [hyper,16117,129,9218] {-} midp($c2,$c8,$c8).
% 46.98/47.19 16186 [hyper,16117,46,582,1719] {-} midp($c1,$c9,$c8).
% 46.98/47.19 16251 [hyper,16123,64,14670] {-} para($c7,$c8,$c8,$c8).
% 46.98/47.19 16260 [hyper,16123,46,6283,4811] {-} midp($c3,$c8,$c7).
% 46.98/47.19 16334 [hyper,16186,65,416,189] {-} midp($c1,$c8,$c9).
% 46.98/47.19 16417 [hyper,16260,65,580,241] {-} midp($c3,$c7,$c8).
% 46.98/47.19 16429 [hyper,16260,45,165] {-} para($c3,$c1,$c7,$c7).
% 46.98/47.19 16498 [hyper,16334,64,14622] {-} para($c7,$c8,$c9,$c9).
% 46.98/47.19 16584 [hyper,16417,64,14763] {-} para($c7,$c7,$c7,$c8).
% 46.98/47.19 17402 [hyper,10645,68,1717] {-} midp($c1,$c8,$c8).
% 46.98/47.19 17408 [hyper,17402,129,9708] {-} midp($c1,$c9,$c9).
% 46.98/47.19 17493 [hyper,17408,129,10303] {-} midp($c1,$c7,$c7).
% 46.98/47.19 17579 [hyper,17408,46,9824,3887] {-} midp($c3,$c9,$c7).
% 46.98/47.19 17766 [hyper,17493,46,418,2213] {-} midp($c3,$c7,$c9).
% 46.98/47.19 19213 [hyper,11093,129,17493] {-} midp($c1,$c5,$c5).
% 46.98/47.19 19215 [hyper,11093,129,14763] {-} midp($c3,$c5,$c5).
% 46.98/47.19 19357 [hyper,11093,4] {-} para($c7,$c5,$c5,$c7).
% 46.98/47.19 19361 [hyper,19213,124] {-} para($c1,$c1,$c5,$c5).
% 46.98/47.19 19478 [hyper,19213,64,17493] {-} para($c5,$c7,$c5,$c7).
% 46.98/47.19 19487 [hyper,19213,46,11087,12519] {-} midp($c5,$c5,$c1).
% 46.98/47.19 19727 [hyper,19215,46,9231,12241] {-} midp($c5,$c5,$c3).
% 46.98/47.19 19860 [hyper,19487,11] {-} midp($c5,$c1,$c5).
% 46.98/47.19 20136 [hyper,19727,11] {-} midp($c5,$c3,$c5).
% 46.98/47.19 20554 [hyper,11094,129,17493] {-} midp($c1,$c4,$c4).
% 46.98/47.19 20556 [hyper,11094,129,14763] {-} midp($c3,$c4,$c4).
% 46.98/47.19 20561 [hyper,11094,67] {-} coll($c7,$c4,$c4).
% 46.98/47.19 20714 [hyper,20554,70] {-} coll($c1,$c4,$c4).
% 46.98/47.19 21051 [hyper,20561,114] {-} coll($c4,$c4,$c7).
% 46.98/47.19 21057 [hyper,20714,114] {-} coll($c4,$c4,$c1).
% 46.98/47.19 21063 [hyper,21051,114] {-} coll($c7,$c7,$c4).
% 46.98/47.19 21076 [hyper,21057,114] {-} coll($c1,$c1,$c4).
% 46.98/47.19 21137 [hyper,21063,3,5317] {-} coll($c6,$c4,$c7).
% 46.98/47.19 21144 [hyper,21063,3,12653] {-} coll($c4,$c5,$c7).
% 46.98/47.19 21169 [hyper,21076,3,1647] {-} coll($c4,$c8,$c1).
% 46.98/47.19 21410 [hyper,21137,1] {-} coll($c6,$c7,$c4).
% 46.98/47.19 21418 [hyper,21144,1] {-} coll($c4,$c7,$c5).
% 46.98/47.19 22445 [hyper,21410,3,5212] {-} coll($c1,$c4,$c6).
% 46.98/47.19 23635 [hyper,22445,46,20556,9940] {-} midp($c1,$c4,$c6).
% 46.98/47.19 24915 [hyper,23635,64,19213] {-} para($c5,$c4,$c5,$c6).
% 46.98/47.19 24940 [hyper,23635,11] {-} midp($c1,$c6,$c4).
% 46.98/47.19 25106 [hyper,24940,64,19213] {-} para($c5,$c6,$c5,$c4).
% 46.98/47.19 26921 [hyper,11106,5] {-} para($c6,$c4,$c3,$c1).
% 46.98/47.19 27811 [hyper,11228,25,2773] {-} cong($c8,$c3,$c8,$c3).
% 46.98/47.19 30804 [hyper,14217,68,12633] {-} midp($c5,$c9,$c8).
% 46.98/47.19 31006 [hyper,30804,65,416,189] {-} midp($c5,$c8,$c9).
% 46.98/47.19 31246 [hyper,14218,129,19215] {-} midp($c3,$c3,$c3).
% 46.98/47.19 31621 [hyper,31246,64,17766] {-} para($c3,$c7,$c3,$c9).
% 46.98/47.19 31622 [hyper,31246,64,17579] {-} para($c3,$c9,$c3,$c7).
% 46.98/47.19 34524 [hyper,14500,8] {-} perp($c9,$c9,$c8,$c9).
% 46.98/47.19 34564 [hyper,14542,129,31006] {-} midp($c5,$c9,$c9).
% 46.98/47.19 34576 [hyper,34564,129,10303] {-} midp($c5,$c7,$c7).
% 46.98/47.19 34716 [hyper,34576,129,11093] {-} midp($c5,$c5,$c5).
% 46.98/47.19 34717 [hyper,34576,124] {-} para($c5,$c5,$c7,$c7).
% 46.98/47.19 40079 [hyper,16251,6,2688] {-} para($c7,$c8,$c3,$c3).
% 46.98/47.19 40572 [hyper,16429,6,15274] {-} para($c4,$c6,$c7,$c7).
% 46.98/47.19 41205 [hyper,19357,5] {-} para($c5,$c7,$c7,$c5).
% 46.98/47.19 41227 [hyper,19361,6,7677] {-} para($c7,$c7,$c5,$c5).
% 46.98/47.19 41317 [hyper,19478,46,34716,12499] {-} midp($c7,$c5,$c7).
% 46.98/47.19 41318 [hyper,19478,46,20136,5342] {-} midp($c7,$c3,$c7).
% 46.98/47.19 41320 [hyper,19478,46,19860,824] {-} midp($c7,$c1,$c7).
% 46.98/47.19 41512 [hyper,41317,11] {-} midp($c7,$c7,$c5).
% 46.98/47.19 41694 [hyper,41318,46,16584,2710] {-} midp($c7,$c3,$c8).
% 46.98/47.19 41701 [hyper,41318,11] {-} midp($c7,$c7,$c3).
% 46.98/47.19 42083 [hyper,41320,46,10860,1713] {-} midp($c8,$c1,$c8).
% 46.98/47.19 44079 [hyper,41512,64,41318] {-} para($c7,$c3,$c5,$c7).
% 46.98/47.19 44080 [hyper,41512,56,11097] {-} cong($c4,$c7,$c4,$c5).
% 46.98/47.19 46246 [hyper,41701,64,41512] {-} para($c7,$c7,$c5,$c3).
% 46.98/47.19 46253 [hyper,41701,64,41694] {-} para($c7,$c3,$c3,$c8).
% 46.98/47.19 50658 [hyper,42083,11] {-} midp($c8,$c8,$c1).
% 46.98/47.19 82154 [hyper,27811,68,1939] {-} midp($c8,$c3,$c3).
% 46.98/47.19 82159 [hyper,82154,129,9219] {-} midp($c8,$c5,$c5).
% 46.98/47.19 82588 [hyper,82154,64,50658] {-} para($c8,$c3,$c1,$c3).
% 46.98/47.19 84187 [hyper,82159,65,24915,25106] {-} midp($c8,$c4,$c6).
% 46.98/47.19 89904 [hyper,84187,69] {-} cong($c8,$c4,$c8,$c6).
% 46.98/47.19 224683 [hyper,34524,10,16498] {-} perp($c7,$c8,$c8,$c9).
% 46.98/47.19 233977 [hyper,44080,68,21418] {-} midp($c4,$c7,$c5).
% 46.98/47.19 234835 [hyper,233977,65,19357,41227] {-} midp($c4,$c5,$c7).
% 46.98/47.19 235907 [hyper,234835,46,40572,12500] {-} midp($c6,$c5,$c7).
% 46.98/47.19 236879 [hyper,235907,65,41205,34717] {-} midp($c6,$c7,$c5).
% 46.98/47.19 246712 [hyper,46246,65,236879,44079] {-} midp($c6,$c7,$c3).
% 46.98/47.19 250225 [hyper,46253,65,246712,40079] {-} midp($c6,$c8,$c3).
% 46.98/47.19 251770 [hyper,250225,46,26921,21169] {-} midp($c4,$c8,$c1).
% 46.98/47.19 257460 [hyper,82588,129,251770] {-} midp($c4,$c3,$c3).
% 46.98/47.19 257501 [hyper,257460,65,31621,31622] {-} midp($c4,$c7,$c9).
% 46.98/47.19 277109 [hyper,89904,23] {-} cong($c8,$c4,$c6,$c8).
% 46.98/47.19 292350 [hyper,224683,53,257501] {-} cong($c7,$c4,$c8,$c4).
% 46.98/47.19 367392 [hyper,292350,25,277109] {-} cong($c7,$c4,$c6,$c8).
% 46.98/47.19 367393 [binary,367392.1,113.1] {-} $F.
% 46.98/47.19
% 46.98/47.19 % SZS output end Refutation
% 46.98/47.19 ------------ end of proof -------------
% 46.98/47.19
% 46.98/47.19
% 46.98/47.19 Search stopped by max_proofs option.
% 46.98/47.19
% 46.98/47.19
% 46.98/47.19 Search stopped by max_proofs option.
% 46.98/47.19
% 46.98/47.19 ============ end of search ============
% 46.98/47.19
% 46.98/47.19 That finishes the proof of the theorem.
% 46.98/47.19
% 46.98/47.19 Process 7348 finished Fri Jun 17 19:15:30 2022
%------------------------------------------------------------------------------