%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO587+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:01 EDT 2022
% Result : Theorem 82.65s 82.85s
% Output : Refutation 82.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : GEO587+1 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.12 % Command : sos-script %s
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Sat Jun 18 02:30:42 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.18/0.36 ----- Otter 3.2, August 2001 -----
% 0.18/0.36 The process was started by sandbox2 on n017.cluster.edu,
% 0.18/0.36 Sat Jun 18 02:30:42 2022
% 0.18/0.36 The command was "./sos". The process ID is 15773.
% 0.18/0.36
% 0.18/0.36 set(prolog_style_variables).
% 0.18/0.36 set(auto).
% 0.18/0.36 dependent: set(auto1).
% 0.18/0.36 dependent: set(process_input).
% 0.18/0.36 dependent: clear(print_kept).
% 0.18/0.36 dependent: clear(print_new_demod).
% 0.18/0.36 dependent: clear(print_back_demod).
% 0.18/0.36 dependent: clear(print_back_sub).
% 0.18/0.36 dependent: set(control_memory).
% 0.18/0.36 dependent: assign(max_mem, 12000).
% 0.18/0.36 dependent: assign(pick_given_ratio, 4).
% 0.18/0.36 dependent: assign(stats_level, 1).
% 0.18/0.36 dependent: assign(pick_semantic_ratio, 3).
% 0.18/0.36 dependent: assign(sos_limit, 5000).
% 0.18/0.36 dependent: assign(max_weight, 60).
% 0.18/0.36 clear(print_given).
% 0.18/0.36
% 0.18/0.36 formula_list(usable).
% 0.18/0.36
% 0.18/0.36 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.18/0.36
% 0.18/0.36 This ia a non-Horn set with equality. The strategy will be
% 0.18/0.36 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.18/0.36 unit deletion, with positive clauses in sos and nonpositive
% 0.18/0.36 clauses in usable.
% 0.18/0.36
% 0.18/0.36 dependent: set(knuth_bendix).
% 0.18/0.36 dependent: set(para_from).
% 0.18/0.36 dependent: set(para_into).
% 0.18/0.36 dependent: clear(para_from_right).
% 0.18/0.36 dependent: clear(para_into_right).
% 0.18/0.36 dependent: set(para_from_vars).
% 0.18/0.36 dependent: set(eq_units_both_ways).
% 0.18/0.36 dependent: set(dynamic_demod_all).
% 0.18/0.36 dependent: set(dynamic_demod).
% 0.18/0.36 dependent: set(order_eq).
% 0.18/0.36 dependent: set(back_demod).
% 0.18/0.36 dependent: set(lrpo).
% 0.18/0.36 dependent: set(hyper_res).
% 0.18/0.36 dependent: set(unit_deletion).
% 0.18/0.36 dependent: set(factor).
% 0.18/0.36
% 0.18/0.36 ------------> process usable:
% 0.18/0.36 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.18/0.36
% 0.18/0.36 ------------> process sos:
% 0.18/0.36 Following clause subsumed by 166 during input processing: 0 [copy,166,flip.1] {-} A=A.
% 0.18/0.36 166 back subsumes 146.
% 0.18/0.36 166 back subsumes 145.
% 0.18/0.36 166 back subsumes 144.
% 0.18/0.36 166 back subsumes 143.
% 0.18/0.36
% 0.18/0.36 ======= end of input processing =======
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43 Failed to model usable list: disabling FINDER
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43 -------------- Softie stats --------------
% 0.18/0.43
% 0.18/0.43 UPDATE_STOP: 300
% 0.18/0.43 SFINDER_TIME_LIMIT: 2
% 0.18/0.43 SHORT_CLAUSE_CUTOFF: 4
% 0.18/0.43 number of clauses in intial UL: 154
% 0.18/0.43 number of clauses initially in problem: 162
% 0.18/0.43 percentage of clauses intially in UL: 95
% 0.18/0.43 percentage of distinct symbols occuring in initial UL: 85
% 0.18/0.43 percent of all initial clauses that are short: 100
% 0.18/0.43 absolute distinct symbol count: 41
% 0.18/0.43 distinct predicate count: 12
% 0.18/0.43 distinct function count: 20
% 0.18/0.43 distinct constant count: 9
% 0.18/0.43
% 0.18/0.43 ---------- no more Softie stats ----------
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43 =========== start of search ===========
% 4.87/5.07
% 4.87/5.07
% 4.87/5.07 Changing weight limit from 60 to 57.
% 4.87/5.07
% 4.87/5.07 Resetting weight limit to 57 after 225 givens.
% 4.87/5.07
% 5.55/5.78
% 5.55/5.78
% 5.55/5.78 Changing weight limit from 57 to 56.
% 5.55/5.78
% 5.55/5.78 Resetting weight limit to 56 after 230 givens.
% 5.55/5.78
% 6.87/7.14
% 6.87/7.14
% 6.87/7.14 Changing weight limit from 56 to 55.
% 6.87/7.14
% 6.87/7.14 Resetting weight limit to 55 after 240 givens.
% 6.87/7.14
% 8.26/8.47
% 8.26/8.47
% 8.26/8.47 Changing weight limit from 55 to 52.
% 8.26/8.47
% 8.26/8.47 Resetting weight limit to 52 after 250 givens.
% 8.26/8.47
% 9.49/9.67
% 9.49/9.67
% 9.49/9.67 Changing weight limit from 52 to 51.
% 9.49/9.67
% 9.49/9.67 Resetting weight limit to 51 after 255 givens.
% 9.49/9.67
% 11.56/11.76
% 11.56/11.76
% 11.56/11.76 Changing weight limit from 51 to 50.
% 11.56/11.76
% 11.56/11.76 Resetting weight limit to 50 after 275 givens.
% 11.56/11.76
% 13.21/13.42
% 13.21/13.42
% 13.21/13.42 Changing weight limit from 50 to 49.
% 13.21/13.42
% 13.21/13.42 Modelling stopped after 300 given clauses and 0.00 seconds
% 13.21/13.42
% 13.21/13.42
% 13.21/13.42 Resetting weight limit to 49 after 305 givens.
% 13.21/13.42
% 13.67/13.90
% 13.67/13.90
% 13.67/13.90 Changing weight limit from 49 to 47.
% 13.67/13.90
% 13.67/13.90 Resetting weight limit to 47 after 315 givens.
% 13.67/13.90
% 14.13/14.31
% 14.13/14.31
% 14.13/14.31 Changing weight limit from 47 to 46.
% 14.13/14.31
% 14.13/14.31 Resetting weight limit to 46 after 320 givens.
% 14.13/14.31
% 14.30/14.51
% 14.30/14.51
% 14.30/14.51 Changing weight limit from 46 to 45.
% 14.30/14.51
% 14.30/14.51 Resetting weight limit to 45 after 325 givens.
% 14.30/14.51
% 14.60/14.83
% 14.60/14.83
% 14.60/14.83 Changing weight limit from 45 to 37.
% 14.60/14.83
% 14.60/14.83 Resetting weight limit to 37 after 330 givens.
% 14.60/14.83
% 15.04/15.23
% 15.04/15.23
% 15.04/15.23 Changing weight limit from 37 to 36.
% 15.04/15.23
% 15.04/15.23 Resetting weight limit to 36 after 340 givens.
% 15.04/15.23
% 15.49/15.72
% 15.49/15.72
% 15.49/15.72 Changing weight limit from 36 to 35.
% 15.49/15.72
% 15.49/15.72 Resetting weight limit to 35 after 350 givens.
% 15.49/15.72
% 15.80/15.99
% 15.80/15.99
% 15.80/15.99 Changing weight limit from 35 to 34.
% 15.80/15.99
% 15.80/15.99 Resetting weight limit to 34 after 355 givens.
% 15.80/15.99
% 16.10/16.31
% 16.10/16.31
% 16.10/16.31 Changing weight limit from 34 to 30.
% 16.10/16.31
% 16.10/16.31 Resetting weight limit to 30 after 360 givens.
% 16.10/16.31
% 19.63/19.82
% 19.63/19.82
% 19.63/19.82 Changing weight limit from 30 to 29.
% 19.63/19.82
% 19.63/19.82 Resetting weight limit to 29 after 520 givens.
% 19.63/19.82
% 20.77/21.04
% 20.77/21.04
% 20.77/21.04 Changing weight limit from 29 to 23.
% 20.77/21.04
% 20.77/21.04 Resetting weight limit to 23 after 900 givens.
% 20.77/21.04
% 20.98/21.18
% 20.98/21.18
% 20.98/21.18 Changing weight limit from 23 to 22.
% 20.98/21.18
% 20.98/21.18 Resetting weight limit to 22 after 920 givens.
% 20.98/21.18
% 21.22/21.43
% 21.22/21.43
% 21.22/21.43 Changing weight limit from 22 to 21.
% 21.22/21.43
% 21.22/21.43 Resetting weight limit to 21 after 930 givens.
% 21.22/21.43
% 21.27/21.49
% 21.27/21.49
% 21.27/21.49 Changing weight limit from 21 to 17.
% 21.27/21.49
% 21.27/21.49 Resetting weight limit to 17 after 935 givens.
% 21.27/21.49
% 21.40/21.61
% 21.40/21.61
% 21.40/21.61 Changing weight limit from 17 to 16.
% 21.40/21.61
% 21.40/21.61 Resetting weight limit to 16 after 940 givens.
% 21.40/21.61
% 21.57/21.79
% 21.57/21.79
% 21.57/21.79 Changing weight limit from 16 to 15.
% 21.57/21.79
% 21.57/21.79 Resetting weight limit to 15 after 945 givens.
% 21.57/21.79
% 21.78/21.98
% 21.78/21.98
% 21.78/21.98 Changing weight limit from 15 to 10.
% 21.78/21.98
% 21.78/21.98 Resetting weight limit to 10 after 950 givens.
% 21.78/21.98
% 23.52/23.73
% 23.52/23.73
% 23.52/23.73 Changing weight limit from 10 to 9.
% 23.52/23.73
% 23.52/23.73 Resetting weight limit to 9 after 1210 givens.
% 23.52/23.73
% 30.48/30.67
% 30.48/30.67
% 30.48/30.67 Changing weight limit from 9 to 8.
% 30.48/30.67
% 30.48/30.67 Resetting weight limit to 8 after 5945 givens.
% 30.48/30.67
% 40.21/40.40
% 40.21/40.40
% 40.21/40.40 Changing weight limit from 8 to 7.
% 40.21/40.40
% 40.21/40.40 Resetting weight limit to 7 after 7315 givens.
% 40.21/40.40
% 40.25/40.42
% 40.25/40.42
% 40.25/40.42 Changing weight limit from 7 to 5.
% 40.25/40.42
% 40.25/40.42 Resetting weight limit to 5 after 7320 givens.
% 40.25/40.42
% 58.77/58.96
% 58.77/58.96
% 58.77/58.96 Changing weight limit from 5 to 6.
% 58.77/58.96
% 58.77/58.96 Resetting weight limit to 6 after 16725 givens.
% 58.77/58.96
% 58.77/58.97
% 58.77/58.97
% 58.77/58.97 Changing weight limit from 6 to 7.
% 58.77/58.97
% 58.77/58.97 Resetting weight limit to 7 after 16730 givens.
% 58.77/58.97
% 58.77/58.98
% 58.77/58.98
% 58.77/58.98 Changing weight limit from 7 to 8.
% 58.77/58.98
% 58.77/58.98 Resetting weight limit to 8 after 16735 givens.
% 58.77/58.98
% 58.77/59.01
% 58.77/59.01
% 58.77/59.01 Changing weight limit from 8 to 9.
% 58.77/59.01
% 58.77/59.01 Resetting weight limit to 9 after 16780 givens.
% 58.77/59.01
% 58.77/59.01
% 58.77/59.01
% 58.77/59.01 Changing weight limit from 9 to 10.
% 58.77/59.01
% 58.77/59.01 Resetting weight limit to 10 after 16785 givens.
% 58.77/59.01
% 58.99/59.18
% 58.99/59.18
% 58.99/59.18 Changing weight limit from 10 to 9.
% 58.99/59.18
% 58.99/59.18 Resetting weight limit to 9 after 16845 givens.
% 58.99/59.18
% 59.65/59.88
% 59.65/59.88
% 59.65/59.88 Changing weight limit from 9 to 8.
% 59.65/59.88
% 59.65/59.88 Resetting weight limit to 8 after 17210 givens.
% 59.65/59.88
% 62.99/63.18
% 62.99/63.18
% 62.99/63.18 Changing weight limit from 8 to 9.
% 62.99/63.18
% 62.99/63.18 Resetting weight limit to 9 after 19225 givens.
% 62.99/63.18
% 63.20/63.39
% 63.20/63.39
% 63.20/63.39 Changing weight limit from 9 to 10.
% 63.20/63.39
% 63.20/63.39 Resetting weight limit to 10 after 19460 givens.
% 63.20/63.39
% 63.20/63.39
% 63.20/63.39
% 63.20/63.39 Changing weight limit from 10 to 11.
% 63.20/63.39
% 63.20/63.39 Resetting weight limit to 11 after 19465 givens.
% 63.20/63.39
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40 Changing weight limit from 11 to 12.
% 63.20/63.40
% 63.20/63.40 Resetting weight limit to 12 after 19470 givens.
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40 Changing weight limit from 12 to 13.
% 63.20/63.40
% 63.20/63.40 Resetting weight limit to 13 after 19475 givens.
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40 Changing weight limit from 13 to 14.
% 63.20/63.40
% 63.20/63.40 Resetting weight limit to 14 after 19480 givens.
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40
% 63.20/63.40 Changing weight limit from 14 to 15.
% 63.20/63.40
% 63.20/63.40 Resetting weight limit to 15 after 19485 givens.
% 63.20/63.40
% 63.20/63.41
% 63.20/63.41
% 63.20/63.41 Changing weight limit from 15 to 16.
% 63.20/63.41
% 63.20/63.41 Resetting weight limit to 16 after 19490 givens.
% 63.20/63.41
% 63.20/63.41
% 63.20/63.41
% 63.20/63.41 Changing weight limit from 16 to 17.
% 63.20/63.41
% 63.20/63.41 Resetting weight limit to 17 after 19495 givens.
% 63.20/63.41
% 63.20/63.41
% 63.20/63.41
% 63.20/63.41 Changing weight limit from 17 to 18.
% 63.20/63.41
% 63.20/63.41 Resetting weight limit to 18 after 19500 givens.
% 63.20/63.41
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42 Changing weight limit from 18 to 19.
% 63.20/63.42
% 63.20/63.42 Resetting weight limit to 19 after 19505 givens.
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42 Changing weight limit from 19 to 20.
% 63.20/63.42
% 63.20/63.42 Resetting weight limit to 20 after 19510 givens.
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42 Changing weight limit from 20 to 21.
% 63.20/63.42
% 63.20/63.42 Resetting weight limit to 21 after 19515 givens.
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42
% 63.20/63.42 Changing weight limit from 21 to 22.
% 63.20/63.42
% 63.20/63.42 Resetting weight limit to 22 after 19520 givens.
% 63.20/63.42
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43 Changing weight limit from 22 to 23.
% 63.20/63.43
% 63.20/63.43 Resetting weight limit to 23 after 19525 givens.
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43 Changing weight limit from 23 to 24.
% 63.20/63.43
% 63.20/63.43 Resetting weight limit to 24 after 19530 givens.
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43 Changing weight limit from 24 to 25.
% 63.20/63.43
% 63.20/63.43 Resetting weight limit to 25 after 19535 givens.
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43
% 63.20/63.43 Changing weight limit from 25 to 26.
% 63.20/63.43
% 63.20/63.43 Resetting weight limit to 26 after 19540 givens.
% 63.20/63.43
% 63.20/63.44
% 63.20/63.44
% 63.20/63.44 Changing weight limit from 26 to 27.
% 63.20/63.44
% 63.20/63.44 Resetting weight limit to 27 after 19545 givens.
% 63.20/63.44
% 63.20/63.44
% 63.20/63.44
% 63.20/63.44 Changing weight limit from 27 to 28.
% 63.20/63.44
% 63.20/63.44 Resetting weight limit to 28 after 19550 givens.
% 63.20/63.44
% 63.20/63.45
% 63.20/63.45
% 63.20/63.45 Changing weight limit from 28 to 29.
% 63.20/63.45
% 63.20/63.45 Resetting weight limit to 29 after 19555 givens.
% 63.20/63.45
% 63.79/63.99
% 63.79/63.99
% 63.79/63.99 Changing weight limit from 29 to 18.
% 63.79/63.99
% 63.79/63.99 Resetting weight limit to 18 after 20065 givens.
% 63.79/63.99
% 63.91/64.10
% 63.91/64.10
% 63.91/64.10 Changing weight limit from 18 to 14.
% 63.91/64.10
% 63.91/64.10 Resetting weight limit to 14 after 20070 givens.
% 63.91/64.10
% 68.70/68.93
% 68.70/68.93
% 68.70/68.93 Changing weight limit from 14 to 13.
% 68.70/68.93
% 68.70/68.93 Resetting weight limit to 13 after 20460 givens.
% 68.70/68.93
% 68.99/69.19
% 68.99/69.19
% 68.99/69.19 Changing weight limit from 13 to 12.
% 68.99/69.19
% 68.99/69.19 Resetting weight limit to 12 after 20495 givens.
% 68.99/69.19
% 69.05/69.25
% 69.05/69.25
% 69.05/69.25 Changing weight limit from 12 to 11.
% 69.05/69.25
% 69.05/69.25 Resetting weight limit to 11 after 20505 givens.
% 69.05/69.25
% 69.29/69.51
% 69.29/69.51
% 69.29/69.51 Changing weight limit from 11 to 10.
% 69.29/69.51
% 69.29/69.51 Resetting weight limit to 10 after 20645 givens.
% 69.29/69.51
% 69.83/70.07
% 69.83/70.07
% 69.83/70.07 Changing weight limit from 10 to 9.
% 69.83/70.07
% 69.83/70.07 Resetting weight limit to 9 after 20760 givens.
% 69.83/70.07
% 77.56/77.77
% 77.56/77.77
% 77.56/77.77 Changing weight limit from 9 to 8.
% 77.56/77.77
% 77.56/77.77 Resetting weight limit to 8 after 23180 givens.
% 77.56/77.77
% 82.65/82.85
% 82.65/82.85 -- HEY sandbox2, WE HAVE A PROOF!! --
% 82.65/82.85
% 82.65/82.85 ----> UNIT CONFLICT at 79.69 sec ----> 271659 [binary,271658.1,113.1] {-} $F.
% 82.65/82.85
% 82.65/82.85 Length of proof is 313. Level of proof is 25.
% 82.65/82.85
% 82.65/82.85 ---------------- PROOF ----------------
% 82.65/82.85 % SZS status Theorem
% 82.65/82.85 % SZS output start Refutation
% 82.65/82.85
% 82.65/82.85 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 82.65/82.85 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 82.65/82.85 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 82.65/82.85 4 [] {+} -para(A,B,C,D)|para(A,B,D,C).
% 82.65/82.85 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 82.65/82.85 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 82.65/82.85 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 82.65/82.85 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 82.65/82.85 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 82.65/82.85 10 [] {+} -para(A,B,C,D)| -perp(C,D,E,F)|perp(A,B,E,F).
% 82.65/82.85 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 82.65/82.85 12 [] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|circle(A,B,C,D).
% 82.65/82.85 13 [] {+} -cong(A,B,A,C)| -cong(A,B,A,D)| -cong(A,B,A,E)|cyclic(B,C,D,E).
% 82.65/82.85 14 [] {+} -cyclic(A,B,C,D)|cyclic(A,B,D,C).
% 82.65/82.85 15 [] {+} -cyclic(A,B,C,D)|cyclic(A,C,B,D).
% 82.65/82.85 16 [] {+} -cyclic(A,B,C,D)|cyclic(B,A,C,D).
% 82.65/82.85 17 [] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)|cyclic(B,C,D,E).
% 82.65/82.85 23 [] {+} -cong(A,B,C,D)|cong(A,B,D,C).
% 82.65/82.85 24 [] {+} -cong(A,B,C,D)|cong(C,D,A,B).
% 82.65/82.85 25 [] {+} -cong(A,B,C,D)| -cong(C,D,E,F)|cong(A,B,E,F).
% 82.65/82.85 40 [] {+} -para(A,B,C,D)|eqangle(A,B,E,F,C,D,E,F).
% 82.65/82.85 43 [] {+} -eqangle(A,B,A,C,D,B,D,C)| -coll(A,D,C)|cyclic(B,C,A,D).
% 82.65/82.85 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).
% 82.65/82.85 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 82.65/82.85 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 82.65/82.85 54 [] {+} -circle(A,B,C,D)| -coll(A,B,D)|perp(B,C,C,D).
% 82.65/82.85 58 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)| -cyclic(A,C,B,D)|perp(B,A,A,D).
% 82.65/82.85 64 [] {+} -midp(A,B,C)| -midp(A,D,E)|para(B,D,C,E).
% 82.65/82.85 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 82.65/82.85 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 82.65/82.85 69 [] {+} -midp(A,B,C)|cong(A,B,A,C).
% 82.65/82.85 70 [] {+} -midp(A,B,C)|coll(A,B,C).
% 82.65/82.85 86 [] {+} -midp(A,B,C)| -midp(D,E,F)|midp($f6(B,C,E,F,A,D),B,F).
% 82.65/82.85 113 [] {+} -cong($c1,$c2,$c1,$c3).
% 82.65/82.85 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 82.65/82.85 117 [factor,13.1.2] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|cyclic(B,C,C,D).
% 82.65/82.85 118 [factor,13.1.3] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|cyclic(B,C,D,C).
% 82.65/82.85 119 [factor,13.2.3] {+} -cong(A,B,A,C)| -cong(A,B,A,D)|cyclic(B,C,D,D).
% 82.65/82.85 120 [factor,17.1.2] {+} -cyclic(A,B,C,D)|cyclic(B,C,D,D).
% 82.65/82.85 121 [factor,44.1.2] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)| -eqangle(C,A,C,B,E,D,E,D)|cong(A,B,D,D).
% 82.65/82.85 122 [factor,44.1.3] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)| -eqangle(C,A,C,B,D,D,D,E)|cong(A,B,D,E).
% 82.65/82.85 124 [factor,45.1.2] {+} -midp(A,B,C)|para(A,A,C,C).
% 82.65/82.85 128 [factor,64.1.2] {+} -midp(A,B,C)|para(B,B,C,C).
% 82.65/82.85 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 82.65/82.85 154 [factor,117.1.2] {+} -cong(A,B,A,C)|cyclic(B,C,C,C).
% 82.65/82.85 159 [] {-} perp($c9,$c8,$c7,$c6).
% 82.65/82.85 160 [] {-} midp($c5,$c7,$c9).
% 82.65/82.85 161 [] {-} midp($c4,$c8,$c7).
% 82.65/82.85 162 [] {-} midp($c3,$c6,$c8).
% 82.65/82.85 163 [] {-} midp($c2,$c9,$c6).
% 82.65/82.85 164 [] {-} coll($c1,$c5,$c3).
% 82.65/82.85 165 [] {-} coll($c1,$c4,$c2).
% 82.65/82.85 167 [hyper,159,8] {-} perp($c7,$c6,$c9,$c8).
% 82.65/82.85 168 [hyper,159,7] {-} perp($c9,$c8,$c6,$c7).
% 82.65/82.85 189 [hyper,160,128] {-} para($c7,$c7,$c9,$c9).
% 82.65/82.85 190 [hyper,160,124] {-} para($c5,$c5,$c9,$c9).
% 82.65/82.85 191 [hyper,160,70] {-} coll($c5,$c7,$c9).
% 82.65/82.85 192 [hyper,160,69] {-} cong($c5,$c7,$c5,$c9).
% 82.65/82.85 193 [hyper,160,11] {-} midp($c5,$c9,$c7).
% 82.65/82.85 220 [hyper,161,70] {-} coll($c4,$c8,$c7).
% 82.65/82.85 221 [hyper,161,69] {-} cong($c4,$c8,$c4,$c7).
% 82.65/82.85 222 [hyper,161,11] {-} midp($c4,$c7,$c8).
% 82.65/82.85 257 [hyper,162,70] {-} coll($c3,$c6,$c8).
% 82.65/82.85 258 [hyper,162,69] {-} cong($c3,$c6,$c3,$c8).
% 82.65/82.85 259 [hyper,162,11] {-} midp($c3,$c8,$c6).
% 82.65/82.85 276 [hyper,163,128] {-} para($c9,$c9,$c6,$c6).
% 82.65/82.85 277 [hyper,163,124] {-} para($c2,$c2,$c6,$c6).
% 82.65/82.85 295 [hyper,163,86,160] {-} midp($f6($c9,$c6,$c7,$c9,$c2,$c5),$c9,$c9).
% 82.65/82.85 302 [hyper,163,70] {-} coll($c2,$c9,$c6).
% 82.65/82.85 303 [hyper,163,69] {-} cong($c2,$c9,$c2,$c6).
% 82.65/82.85 304 [hyper,163,11] {-} midp($c2,$c6,$c9).
% 82.65/82.85 317 [hyper,164,114] {-} coll($c3,$c3,$c1).
% 82.65/82.85 318 [hyper,164,2] {-} coll($c5,$c1,$c3).
% 82.65/82.85 319 [hyper,164,1] {-} coll($c1,$c3,$c5).
% 82.65/82.85 332 [hyper,165,114] {-} coll($c2,$c2,$c1).
% 82.65/82.85 333 [hyper,165,2] {-} coll($c4,$c1,$c2).
% 82.65/82.85 334 [hyper,165,1] {-} coll($c1,$c2,$c4).
% 82.65/82.85 347 [hyper,191,114] {-} coll($c9,$c9,$c5).
% 82.65/82.85 348 [hyper,191,2] {-} coll($c7,$c5,$c9).
% 82.65/82.85 349 [hyper,191,1] {-} coll($c5,$c9,$c7).
% 82.65/82.85 400 [hyper,193,69] {-} cong($c5,$c9,$c5,$c7).
% 82.65/82.85 401 [hyper,193,64,160] {-} para($c7,$c9,$c9,$c7).
% 82.65/82.85 402 [hyper,193,64,160] {-} para($c9,$c7,$c7,$c9).
% 82.65/82.85 403 [hyper,193,45,163] {-} para($c2,$c5,$c6,$c7).
% 82.65/82.85 404 [hyper,193,45,163] {-} para($c5,$c2,$c7,$c6).
% 82.65/82.85 417 [hyper,167,9,159] {-} para($c9,$c8,$c9,$c8).
% 82.65/82.85 436 [hyper,220,114] {-} coll($c7,$c7,$c4).
% 82.65/82.85 437 [hyper,220,2] {-} coll($c8,$c4,$c7).
% 82.65/82.85 438 [hyper,220,1] {-} coll($c4,$c7,$c8).
% 82.65/82.85 455 [hyper,222,128] {-} para($c7,$c7,$c8,$c8).
% 82.65/82.85 497 [hyper,222,69] {-} cong($c4,$c7,$c4,$c8).
% 82.65/82.85 498 [hyper,222,64,161] {-} para($c8,$c7,$c7,$c8).
% 82.65/82.85 499 [hyper,222,64,161] {-} para($c7,$c8,$c8,$c7).
% 82.65/82.85 500 [hyper,222,45,160] {-} para($c5,$c4,$c9,$c8).
% 82.65/82.85 501 [hyper,222,45,160] {-} para($c4,$c5,$c8,$c9).
% 82.65/82.85 514 [hyper,257,114] {-} coll($c8,$c8,$c3).
% 82.65/82.85 515 [hyper,257,2] {-} coll($c6,$c3,$c8).
% 82.65/82.85 516 [hyper,257,1] {-} coll($c3,$c8,$c6).
% 82.65/82.85 583 [hyper,259,69] {-} cong($c3,$c8,$c3,$c6).
% 82.65/82.85 586 [hyper,259,45,161] {-} para($c4,$c3,$c7,$c6).
% 82.65/82.85 587 [hyper,259,45,161] {-} para($c3,$c4,$c6,$c7).
% 82.65/82.85 600 [hyper,168,9,167] {-} para($c7,$c6,$c6,$c7).
% 82.65/82.85 618 [hyper,302,114] {-} coll($c6,$c6,$c2).
% 82.65/82.85 619 [hyper,302,2] {-} coll($c9,$c2,$c6).
% 82.65/82.85 620 [hyper,302,1] {-} coll($c2,$c6,$c9).
% 82.65/82.85 695 [hyper,304,69] {-} cong($c2,$c6,$c2,$c9).
% 82.65/82.85 698 [hyper,304,45,162] {-} para($c3,$c2,$c8,$c9).
% 82.65/82.85 699 [hyper,304,45,162] {-} para($c2,$c3,$c9,$c8).
% 82.65/82.85 712 [hyper,317,114] {-} coll($c1,$c1,$c3).
% 82.65/82.85 713 [hyper,317,1] {-} coll($c3,$c1,$c3).
% 82.65/82.85 726 [hyper,318,114] {-} coll($c3,$c3,$c5).
% 82.65/82.85 727 [hyper,318,1] {-} coll($c5,$c3,$c1).
% 82.65/82.85 840 [hyper,319,114] {-} coll($c5,$c5,$c1).
% 82.65/82.85 854 [hyper,332,114] {-} coll($c1,$c1,$c2).
% 82.65/82.85 855 [hyper,332,1] {-} coll($c2,$c1,$c2).
% 82.65/82.85 868 [hyper,333,114] {-} coll($c2,$c2,$c4).
% 82.65/82.85 869 [hyper,333,1] {-} coll($c4,$c2,$c1).
% 82.65/82.85 883 [hyper,334,2] {-} coll($c2,$c1,$c4).
% 82.65/82.85 996 [hyper,347,114] {-} coll($c5,$c5,$c9).
% 82.65/82.85 997 [hyper,347,1] {-} coll($c9,$c5,$c9).
% 82.65/82.85 1010 [hyper,348,114] {-} coll($c9,$c9,$c7).
% 82.65/82.85 1024 [hyper,349,114] {-} coll($c7,$c7,$c5).
% 82.65/82.85 1038 [hyper,436,114] {-} coll($c4,$c4,$c7).
% 82.65/82.85 1152 [hyper,437,114] {-} coll($c7,$c7,$c8).
% 82.65/82.85 1153 [hyper,437,1] {-} coll($c8,$c7,$c4).
% 82.65/82.85 1166 [hyper,438,114] {-} coll($c8,$c8,$c4).
% 82.65/82.85 1180 [hyper,514,114] {-} coll($c3,$c3,$c8).
% 82.65/82.85 1181 [hyper,514,1] {-} coll($c8,$c3,$c8).
% 82.65/82.85 1194 [hyper,515,114] {-} coll($c8,$c8,$c6).
% 82.65/82.85 1308 [hyper,516,114] {-} coll($c6,$c6,$c3).
% 82.65/82.85 1322 [hyper,618,114] {-} coll($c2,$c2,$c6).
% 82.65/82.85 1336 [hyper,619,114] {-} coll($c6,$c6,$c9).
% 82.65/82.85 1337 [hyper,619,1] {-} coll($c9,$c6,$c2).
% 82.65/82.85 1350 [hyper,620,114] {-} coll($c9,$c9,$c2).
% 82.65/82.85 1444 [hyper,712,1] {-} coll($c1,$c3,$c1).
% 82.65/82.85 1457 [hyper,713,114] {-} coll($c3,$c3,$c3).
% 82.65/82.85 1485 [hyper,727,114] {-} coll($c1,$c1,$c5).
% 82.65/82.85 1606 [hyper,854,3,712] {-} coll($c2,$c3,$c1).
% 82.65/82.85 1620 [hyper,855,114] {-} coll($c2,$c2,$c2).
% 82.65/82.85 1714 [hyper,868,114] {-} coll($c4,$c4,$c2).
% 82.65/82.85 1728 [hyper,869,114] {-} coll($c1,$c1,$c4).
% 82.65/82.85 1848 [hyper,996,3,840] {-} coll($c1,$c9,$c5).
% 82.65/82.85 1863 [hyper,997,114] {-} coll($c9,$c9,$c9).
% 82.65/82.85 1864 [hyper,997,2] {-} coll($c5,$c9,$c9).
% 82.65/82.85 1877 [hyper,1010,114] {-} coll($c7,$c7,$c9).
% 82.65/82.85 1963 [hyper,1024,1] {-} coll($c7,$c5,$c7).
% 82.65/82.85 2074 [hyper,1152,114] {-} coll($c8,$c8,$c7).
% 82.65/82.85 2077 [hyper,1152,1] {-} coll($c7,$c8,$c7).
% 82.65/82.85 2090 [hyper,1153,114] {-} coll($c4,$c4,$c8).
% 82.65/82.85 2104 [hyper,1166,3,514] {-} coll($c3,$c4,$c8).
% 82.65/82.85 2106 [hyper,1166,1] {-} coll($c8,$c4,$c8).
% 82.65/82.85 2190 [hyper,1180,3,726] {-} coll($c8,$c5,$c3).
% 82.65/82.85 2191 [hyper,1180,3,317] {-} coll($c8,$c1,$c3).
% 82.65/82.85 2205 [hyper,1181,114] {-} coll($c8,$c8,$c8).
% 82.65/82.85 2206 [hyper,1181,2] {-} coll($c3,$c8,$c8).
% 82.65/82.85 2219 [hyper,1194,114] {-} coll($c6,$c6,$c8).
% 82.65/82.85 2305 [hyper,1308,3,618] {-} coll($c2,$c3,$c6).
% 82.65/82.85 2306 [hyper,1308,3,618] {-} coll($c3,$c2,$c6).
% 82.65/82.85 2404 [hyper,1336,114] {-} coll($c9,$c9,$c6).
% 82.65/82.85 2405 [hyper,1336,3,1308] {-} coll($c3,$c9,$c6).
% 82.65/82.85 2420 [hyper,1337,114] {-} coll($c2,$c2,$c9).
% 82.65/82.85 2421 [hyper,1337,2] {-} coll($c6,$c9,$c2).
% 82.65/82.85 2435 [hyper,1350,3,347] {-} coll($c5,$c2,$c9).
% 82.65/82.85 2436 [hyper,1350,3,1010] {-} coll($c2,$c7,$c9).
% 82.65/82.85 2437 [hyper,1350,3,347] {-} coll($c2,$c5,$c9).
% 82.65/82.85 2504 [hyper,1444,114] {-} coll($c1,$c1,$c1).
% 82.65/82.85 2506 [hyper,1444,3,319] {-} coll($c1,$c5,$c1).
% 82.65/82.85 2520 [hyper,1457,3,1180] {-} coll($c8,$c3,$c3).
% 82.65/82.85 2613 [hyper,1485,3,854] {-} coll($c5,$c2,$c1).
% 82.65/82.85 2718 [hyper,1606,1] {-} coll($c2,$c1,$c3).
% 82.65/82.85 2788 [hyper,1620,3,1322] {-} coll($c6,$c2,$c2).
% 82.65/82.85 2813 [hyper,1714,3,1038] {-} coll($c7,$c2,$c4).
% 82.65/82.85 2882 [hyper,1728,3,1485] {-} coll($c5,$c4,$c1).
% 82.65/82.85 2883 [hyper,1728,3,712] {-} coll($c3,$c4,$c1).
% 82.65/82.85 3048 [hyper,1848,1] {-} coll($c1,$c5,$c9).
% 82.65/82.85 3089 [hyper,1863,3,1350] {-} coll($c2,$c9,$c9).
% 82.65/82.85 3149 [hyper,1877,3,1152] {-} coll($c8,$c9,$c7).
% 82.65/82.85 3150 [hyper,1877,3,436] {-} coll($c4,$c9,$c7).
% 82.65/82.85 3258 [hyper,1963,2] {-} coll($c5,$c7,$c7).
% 82.65/82.85 3345 [hyper,192,154] {-} cyclic($c7,$c9,$c9,$c9).
% 82.65/82.85 3402 [hyper,2074,3,514] {-} coll($c3,$c7,$c8).
% 82.65/82.85 3538 [hyper,2090,3,1714] {-} coll($c2,$c8,$c4).
% 82.65/82.85 3540 [hyper,2090,3,1714] {-} coll($c8,$c2,$c4).
% 82.65/82.85 3646 [hyper,2104,1] {-} coll($c3,$c8,$c4).
% 82.65/82.85 3673 [hyper,2106,2] {-} coll($c4,$c8,$c8).
% 82.65/82.85 3810 [hyper,2190,1] {-} coll($c8,$c3,$c5).
% 82.65/82.85 3823 [hyper,2191,1] {-} coll($c8,$c3,$c1).
% 82.65/82.85 3954 [hyper,2219,3,1336] {-} coll($c9,$c8,$c6).
% 82.65/82.85 4151 [hyper,2305,1] {-} coll($c2,$c6,$c3).
% 82.65/82.85 4164 [hyper,2306,1] {-} coll($c3,$c6,$c2).
% 82.65/82.85 4449 [hyper,2404,3,1010] {-} coll($c6,$c7,$c9).
% 82.65/82.85 4463 [hyper,2405,1] {-} coll($c3,$c6,$c9).
% 82.65/82.85 4543 [hyper,2420,3,868] {-} coll($c4,$c9,$c2).
% 82.65/82.85 4584 [hyper,2435,1] {-} coll($c5,$c9,$c2).
% 82.65/82.85 4644 [hyper,2436,1] {-} coll($c2,$c9,$c7).
% 82.65/82.85 4658 [hyper,2437,1] {-} coll($c2,$c9,$c5).
% 82.65/82.85 4931 [hyper,2613,1] {-} coll($c5,$c1,$c2).
% 82.65/82.85 5147 [hyper,2718,3,883] {-} coll($c4,$c3,$c2).
% 82.65/82.85 5246 [hyper,2813,1] {-} coll($c7,$c4,$c2).
% 82.65/82.85 5329 [hyper,2882,1] {-} coll($c5,$c1,$c4).
% 82.65/82.85 5514 [hyper,3048,114] {-} coll($c9,$c9,$c1).
% 82.65/82.85 5518 [hyper,3048,3,2506] {-} coll($c9,$c1,$c1).
% 82.65/82.85 5661 [hyper,3149,1] {-} coll($c8,$c7,$c9).
% 82.65/82.85 5717 [hyper,3150,1] {-} coll($c4,$c7,$c9).
% 82.65/82.85 6546 [hyper,3538,1] {-} coll($c2,$c4,$c8).
% 82.65/82.85 6599 [hyper,3646,3,2206] {-} coll($c8,$c4,$c3).
% 82.65/82.85 6728 [hyper,3823,3,3810] {-} coll($c5,$c1,$c8).
% 82.65/82.85 6771 [hyper,3954,1] {-} coll($c9,$c6,$c8).
% 82.65/82.85 6933 [hyper,4151,3,620] {-} coll($c9,$c3,$c2).
% 82.65/82.85 7149 [hyper,4449,1] {-} coll($c6,$c9,$c7).
% 82.65/82.85 7191 [hyper,4463,3,4164] {-} coll($c9,$c2,$c3).
% 82.65/82.85 7224 [hyper,4543,1] {-} coll($c4,$c2,$c9).
% 82.65/82.85 7301 [hyper,4584,2] {-} coll($c9,$c5,$c2).
% 82.65/82.85 7332 [hyper,4658,3,4644] {-} coll($c7,$c5,$c2).
% 82.65/82.85 7751 [hyper,5147,1] {-} coll($c4,$c2,$c3).
% 82.65/82.85 7951 [hyper,5329,3,4931] {-} coll($c2,$c4,$c5).
% 82.65/82.85 8327 [hyper,5661,3,1153] {-} coll($c4,$c9,$c8).
% 82.65/82.85 8363 [hyper,5717,2] {-} coll($c7,$c4,$c9).
% 82.65/82.85 9855 [hyper,258,23] {-} cong($c3,$c6,$c8,$c3).
% 82.65/82.85 10210 [hyper,6728,3,4931] {-} coll($c8,$c2,$c5).
% 82.65/82.85 10339 [hyper,6771,3,1337] {-} coll($c2,$c8,$c9).
% 82.65/82.85 11094 [hyper,276,6,190] {-} para($c5,$c5,$c6,$c6).
% 82.65/82.85 11095 [hyper,276,6,189] {-} para($c7,$c7,$c6,$c6).
% 82.65/82.85 11230 [hyper,277,5] {-} para($c6,$c6,$c2,$c2).
% 82.65/82.85 11388 [hyper,7149,3,2421] {-} coll($c2,$c7,$c6).
% 82.65/82.85 12956 [hyper,295,128] {-} para($c9,$c9,$c9,$c9).
% 82.65/82.85 13174 [hyper,7751,3,7224] {-} coll($c9,$c3,$c4).
% 82.65/82.85 13260 [hyper,7951,3,6546] {-} coll($c8,$c5,$c2).
% 82.65/82.85 13372 [hyper,303,23] {-} cong($c2,$c9,$c6,$c2).
% 82.65/82.85 17332 [hyper,400,25,192] {-} cong($c5,$c7,$c5,$c7).
% 82.65/82.85 17333 [hyper,400,25,192] {-} cong($c5,$c9,$c5,$c9).
% 82.65/82.85 17678 [hyper,402,6,401] {-} para($c9,$c7,$c9,$c7).
% 82.65/82.85 18037 [hyper,403,5] {-} para($c6,$c7,$c2,$c5).
% 82.65/82.85 18213 [hyper,404,4] {-} para($c5,$c2,$c6,$c7).
% 82.65/82.85 18387 [hyper,417,40] {-} eqangle($c9,$c8,A,B,$c9,$c8,A,B).
% 82.65/82.85 18923 [hyper,497,25,221] {-} cong($c4,$c8,$c4,$c8).
% 82.65/82.85 19100 [hyper,498,4] {-} para($c8,$c7,$c8,$c7).
% 82.65/82.85 19447 [hyper,500,5] {-} para($c9,$c8,$c5,$c4).
% 82.65/82.85 19448 [hyper,500,4] {-} para($c5,$c4,$c8,$c9).
% 82.65/82.85 19622 [hyper,501,4] {-} para($c4,$c5,$c9,$c8).
% 82.65/82.85 19976 [hyper,583,25,258] {-} cong($c3,$c8,$c3,$c8).
% 82.65/82.85 20500 [hyper,586,4] {-} para($c4,$c3,$c6,$c7).
% 82.65/82.85 20673 [hyper,587,5] {-} para($c6,$c7,$c3,$c4).
% 82.65/82.85 21204 [hyper,695,25,303] {-} cong($c2,$c9,$c2,$c9).
% 82.65/82.85 21726 [hyper,698,5] {-} para($c8,$c9,$c3,$c2).
% 82.65/82.85 21902 [hyper,699,5] {-} para($c9,$c8,$c2,$c3).
% 82.65/82.85 22084 [hyper,3345,16] {-} cyclic($c9,$c7,$c9,$c9).
% 82.65/82.85 23498 [hyper,9855,24] {-} cong($c8,$c3,$c3,$c6).
% 82.65/82.85 24364 [hyper,11230,6,11095] {-} para($c7,$c7,$c2,$c2).
% 82.65/82.85 24365 [hyper,11230,6,11094] {-} para($c5,$c5,$c2,$c2).
% 82.65/82.85 24713 [hyper,12956,40] {-} eqangle($c9,$c9,A,B,$c9,$c9,A,B).
% 82.65/82.85 24720 [hyper,13372,24] {-} cong($c6,$c2,$c2,$c9).
% 82.65/82.85 24906 [hyper,17332,68,3258] {-} midp($c5,$c7,$c7).
% 82.65/82.85 24910 [hyper,17332,12,192] {-} circle($c5,$c7,$c7,$c9).
% 82.65/82.85 24949 [hyper,24906,64,193] {-} para($c7,$c9,$c7,$c7).
% 82.65/82.85 24950 [hyper,24906,64,160] {-} para($c7,$c7,$c7,$c9).
% 82.65/82.85 24953 [hyper,24906,46,404,11388] {-} midp($c2,$c7,$c6).
% 82.65/82.85 25046 [hyper,24953,65,600,11095] {-} midp($c2,$c6,$c7).
% 82.65/82.85 25105 [hyper,25046,45,162] {-} para($c3,$c2,$c8,$c7).
% 82.65/82.85 25112 [hyper,17333,118,400] {-} cyclic($c9,$c7,$c9,$c7).
% 82.65/82.85 25117 [hyper,17333,68,1864] {-} midp($c5,$c9,$c9).
% 82.65/82.85 25124 [hyper,25117,129,417] {-} midp($c5,$c8,$c8).
% 82.65/82.85 25178 [hyper,25117,46,500,8327] {-} midp($c4,$c9,$c8).
% 82.65/82.85 25236 [hyper,25124,64,160] {-} para($c8,$c7,$c8,$c9).
% 82.65/82.85 25239 [hyper,25124,45,161] {-} para($c4,$c5,$c7,$c8).
% 82.65/82.85 25304 [hyper,25178,11] {-} midp($c4,$c8,$c9).
% 82.65/82.85 25368 [hyper,25304,69] {-} cong($c4,$c8,$c4,$c9).
% 82.65/82.85 25369 [hyper,25304,64,222] {-} para($c7,$c8,$c8,$c9).
% 82.65/82.85 25902 [hyper,18037,6,403] {-} para($c2,$c5,$c2,$c5).
% 82.65/82.85 25903 [hyper,18037,4] {-} para($c6,$c7,$c5,$c2).
% 82.65/82.85 26428 [hyper,18213,6,18037] {-} para($c5,$c2,$c2,$c5).
% 82.65/82.85 26969 [hyper,18923,68,3673] {-} midp($c4,$c8,$c8).
% 82.65/82.85 27039 [hyper,26969,64,25304] {-} para($c8,$c8,$c9,$c8).
% 82.65/82.85 28435 [hyper,19448,5] {-} para($c8,$c9,$c5,$c4).
% 82.65/82.85 29539 [hyper,19976,68,2206] {-} midp($c3,$c8,$c8).
% 82.65/82.85 29664 [hyper,29539,46,698,10339] {-} midp($c2,$c8,$c9).
% 82.65/82.85 29926 [hyper,29664,45,26969] {-} para($c2,$c4,$c9,$c8).
% 82.65/82.85 30905 [hyper,20500,6,18037] {-} para($c4,$c3,$c2,$c5).
% 82.65/82.85 31082 [hyper,20673,6,18213] {-} para($c5,$c2,$c3,$c4).
% 82.65/82.85 32139 [hyper,21204,68,3089] {-} midp($c2,$c9,$c9).
% 82.65/82.85 32145 [hyper,32139,129,17678] {-} midp($c2,$c7,$c7).
% 82.65/82.85 32146 [hyper,32139,129,417] {-} midp($c2,$c8,$c8).
% 82.65/82.85 33898 [hyper,21726,6,19448] {-} para($c5,$c4,$c3,$c2).
% 82.65/82.85 33900 [hyper,21726,6,698] {-} para($c3,$c2,$c3,$c2).
% 82.65/82.85 33902 [hyper,21726,4] {-} para($c8,$c9,$c2,$c3).
% 82.65/82.85 34254 [hyper,21902,6,19622] {-} para($c4,$c5,$c2,$c3).
% 82.65/82.85 37201 [hyper,23498,25,9855] {-} cong($c8,$c3,$c8,$c3).
% 82.65/82.85 38587 [hyper,24720,25,13372] {-} cong($c6,$c2,$c6,$c2).
% 82.65/82.85 38967 [hyper,24910,54,191] {-} perp($c7,$c7,$c7,$c9).
% 82.65/82.85 39505 [hyper,24949,6,24364] {-} para($c7,$c9,$c2,$c2).
% 82.65/82.85 39690 [hyper,24950,65,32145,24949] {-} midp($c2,$c7,$c9).
% 82.65/82.85 40413 [hyper,39690,46,699,3402] {-} midp($c3,$c7,$c8).
% 82.65/82.85 41590 [hyper,40413,65,499,455] {-} midp($c3,$c8,$c7).
% 82.65/82.85 44049 [hyper,25105,5] {-} para($c8,$c7,$c3,$c2).
% 82.65/82.85 44229 [hyper,25239,5] {-} para($c7,$c8,$c4,$c5).
% 82.65/82.85 44298 [hyper,25368,119,18923] {-} cyclic($c8,$c8,$c9,$c9).
% 82.65/82.85 44302 [hyper,25368,118,18923] {-} cyclic($c8,$c8,$c9,$c8).
% 82.65/82.85 44309 [hyper,25368,117,221] {-} cyclic($c8,$c9,$c9,$c7).
% 82.65/82.85 44332 [hyper,25369,6,21726] {-} para($c7,$c8,$c3,$c2).
% 82.65/82.85 44674 [hyper,27039,6,21902] {-} para($c8,$c8,$c2,$c3).
% 82.65/82.85 47386 [hyper,29926,6,19447] {-} para($c2,$c4,$c5,$c4).
% 82.65/82.85 51652 [hyper,37201,68,2520] {-} midp($c8,$c3,$c3).
% 82.65/82.85 51654 [hyper,51652,129,33900] {-} midp($c8,$c2,$c2).
% 82.65/82.85 51818 [hyper,51652,46,21726,6933] {-} midp($c9,$c3,$c2).
% 82.65/82.85 51988 [hyper,51654,46,33902,7191] {-} midp($c9,$c2,$c3).
% 82.65/82.85 53063 [hyper,38587,68,2788] {-} midp($c6,$c2,$c2).
% 82.65/82.85 53066 [hyper,53063,129,25902] {-} midp($c6,$c5,$c5).
% 82.65/82.85 53611 [hyper,53066,46,25903,7332] {-} midp($c7,$c5,$c2).
% 82.65/82.85 56642 [hyper,39505,46,53611,7301] {-} midp($c9,$c5,$c2).
% 82.65/82.85 56857 [hyper,56642,65,26428,24365] {-} midp($c9,$c2,$c5).
% 82.65/82.85 56859 [hyper,56642,46,21902,2190] {-} midp($c8,$c5,$c3).
% 82.65/82.85 57071 [hyper,56857,46,19447,3540] {-} midp($c8,$c2,$c4).
% 82.65/82.85 57286 [hyper,56859,65,33898,31082] {-} midp($c8,$c4,$c2).
% 82.65/82.85 57289 [hyper,56859,11] {-} midp($c8,$c3,$c5).
% 82.65/82.85 57953 [hyper,57289,46,28435,13174] {-} midp($c9,$c3,$c4).
% 82.65/82.85 60653 [hyper,18387,43,5514] {-} cyclic($c8,$c1,$c9,$c9).
% 82.65/82.85 60667 [hyper,44302,121,44298,18387] {-} cong($c8,$c8,$c8,$c8).
% 82.65/82.85 61419 [hyper,44674,46,57286,6599] {-} midp($c8,$c4,$c3).
% 82.65/82.85 61646 [hyper,61419,46,44049,5246] {-} midp($c7,$c4,$c2).
% 82.65/82.85 62109 [hyper,61646,65,34254,30905] {-} midp($c7,$c5,$c3).
% 82.65/82.85 62111 [hyper,61646,11] {-} midp($c7,$c2,$c4).
% 82.65/82.85 63540 [hyper,62109,46,44332,13260] {-} midp($c8,$c5,$c2).
% 82.65/82.85 63785 [hyper,62111,46,44229,10210] {-} midp($c8,$c2,$c5).
% 82.65/82.85 80497 [hyper,24713,122,22084,25112] {-} cong($c9,$c7,$c9,$c7).
% 82.65/82.85 80507 [hyper,24713,43,5514] {-} cyclic($c9,$c1,$c9,$c9).
% 82.65/82.85 80867 [hyper,60653,15] {-} cyclic($c8,$c9,$c1,$c9).
% 82.65/82.85 80888 [hyper,60667,68,2205] {-} midp($c8,$c8,$c8).
% 82.65/82.85 81190 [hyper,80888,64,57071] {-} para($c2,$c8,$c4,$c8).
% 82.65/82.85 81200 [hyper,80888,64,63785] {-} para($c8,$c2,$c8,$c5).
% 82.65/82.85 81201 [hyper,80888,64,63540] {-} para($c8,$c5,$c8,$c2).
% 82.65/82.85 81246 [hyper,80888,46,19100,2077] {-} midp($c7,$c8,$c7).
% 82.65/82.85 90777 [hyper,81246,45,41590] {-} para($c7,$c3,$c7,$c7).
% 82.65/82.85 115146 [hyper,80507,15] {-} cyclic($c9,$c9,$c1,$c9).
% 82.65/82.85 115187 [hyper,80867,14] {-} cyclic($c8,$c9,$c9,$c1).
% 82.65/82.85 121381 [hyper,81201,65,32146,81200] {-} midp($c2,$c2,$c5).
% 82.65/82.85 121393 [hyper,121381,129,47386] {-} midp($c2,$c4,$c4).
% 82.65/82.85 121699 [hyper,121393,46,81190,2106] {-} midp($c8,$c4,$c8).
% 82.65/82.85 122062 [hyper,121699,46,25236,8363] {-} midp($c7,$c4,$c9).
% 82.65/82.85 126919 [hyper,90777,10,38967] {-} perp($c7,$c3,$c7,$c9).
% 82.65/82.85 131760 [hyper,115187,120] {-} cyclic($c9,$c9,$c1,$c1).
% 82.65/82.85 131764 [hyper,115187,17,44309] {-} cyclic($c9,$c9,$c7,$c1).
% 82.65/82.85 157705 [hyper,131760,17,115146] {-} cyclic($c9,$c1,$c9,$c1).
% 82.65/82.85 174741 [hyper,157705,122,80507,24713] {-} cong($c9,$c1,$c9,$c1).
% 82.65/82.85 208136 [hyper,174741,68,5518] {-} midp($c9,$c1,$c1).
% 82.65/82.85 208137 [hyper,174741,58,80497,131764] {-} perp($c7,$c9,$c9,$c1).
% 82.65/82.85 210274 [hyper,208136,64,57953] {-} para($c3,$c1,$c4,$c1).
% 82.65/82.85 210344 [hyper,208136,64,51988] {-} para($c1,$c2,$c1,$c3).
% 82.65/82.85 210345 [hyper,208136,64,51818] {-} para($c1,$c3,$c1,$c2).
% 82.65/82.85 216440 [hyper,208137,9,126919] {-} para($c7,$c3,$c9,$c1).
% 82.65/82.85 250605 [hyper,216440,46,122062,2883] {-} midp($c3,$c4,$c1).
% 82.65/82.85 251711 [hyper,250605,11] {-} midp($c3,$c1,$c4).
% 82.65/82.85 268402 [hyper,251711,46,210274,2504] {-} midp($c1,$c1,$c1).
% 82.65/82.85 271479 [hyper,268402,65,210344,210345] {-} midp($c1,$c2,$c3).
% 82.65/82.85 271658 [hyper,271479,69] {-} cong($c1,$c2,$c1,$c3).
% 82.65/82.85 271659 [binary,271658.1,113.1] {-} $F.
% 82.65/82.85
% 82.65/82.85 % SZS output end Refutation
% 82.65/82.85 ------------ end of proof -------------
% 82.65/82.85
% 82.65/82.85
% 82.65/82.85 Search stopped by max_proofs option.
% 82.65/82.85
% 82.65/82.85
% 82.65/82.85 Search stopped by max_proofs option.
% 82.65/82.85
% 82.65/82.85 ============ end of search ============
% 82.65/82.85
% 82.65/82.85 That finishes the proof of the theorem.
% 82.65/82.85
% 82.65/82.85 Process 15773 finished Sat Jun 18 02:32:04 2022
%------------------------------------------------------------------------------