%------------------------------------------------------------------------------
% File : SOS---2.0
% Problem : GEO574+1 : TPTP v8.1.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : sos-script %s
% Computer : n015.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:57 EDT 2022
% Result : Theorem 80.42s 80.63s
% Output : Refutation 80.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GEO574+1 : TPTP v8.1.0. Released v7.5.0.
% 0.11/0.12 % Command : sos-script %s
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sat Jun 18 13:16:43 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.12/0.36 ----- Otter 3.2, August 2001 -----
% 0.12/0.36 The process was started by sandbox2 on n015.cluster.edu,
% 0.12/0.36 Sat Jun 18 13:16:43 2022
% 0.12/0.36 The command was "./sos". The process ID is 4167.
% 0.12/0.36
% 0.12/0.36 set(prolog_style_variables).
% 0.12/0.36 set(auto).
% 0.12/0.36 dependent: set(auto1).
% 0.12/0.36 dependent: set(process_input).
% 0.12/0.36 dependent: clear(print_kept).
% 0.12/0.36 dependent: clear(print_new_demod).
% 0.12/0.36 dependent: clear(print_back_demod).
% 0.12/0.36 dependent: clear(print_back_sub).
% 0.12/0.36 dependent: set(control_memory).
% 0.12/0.36 dependent: assign(max_mem, 12000).
% 0.12/0.36 dependent: assign(pick_given_ratio, 4).
% 0.12/0.36 dependent: assign(stats_level, 1).
% 0.12/0.36 dependent: assign(pick_semantic_ratio, 3).
% 0.12/0.36 dependent: assign(sos_limit, 5000).
% 0.12/0.36 dependent: assign(max_weight, 60).
% 0.12/0.36 clear(print_given).
% 0.12/0.36
% 0.12/0.36 formula_list(usable).
% 0.12/0.36
% 0.12/0.36 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5.
% 0.12/0.36
% 0.12/0.36 This ia a non-Horn set with equality. The strategy will be
% 0.12/0.36 Knuth-Bendix, ordered hyper_res, ur_res, factoring, and
% 0.12/0.36 unit deletion, with positive clauses in sos and nonpositive
% 0.12/0.36 clauses in usable.
% 0.12/0.36
% 0.12/0.36 dependent: set(knuth_bendix).
% 0.12/0.36 dependent: set(para_from).
% 0.12/0.36 dependent: set(para_into).
% 0.12/0.36 dependent: clear(para_from_right).
% 0.12/0.36 dependent: clear(para_into_right).
% 0.12/0.36 dependent: set(para_from_vars).
% 0.12/0.36 dependent: set(eq_units_both_ways).
% 0.12/0.36 dependent: set(dynamic_demod_all).
% 0.12/0.36 dependent: set(dynamic_demod).
% 0.12/0.36 dependent: set(order_eq).
% 0.12/0.36 dependent: set(back_demod).
% 0.12/0.36 dependent: set(lrpo).
% 0.12/0.36 dependent: set(hyper_res).
% 0.12/0.36 dependent: set(unit_deletion).
% 0.12/0.36 dependent: set(factor).
% 0.12/0.36
% 0.12/0.36 ------------> process usable:
% 0.12/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.12/0.36
% 0.12/0.36 ------------> process sos:
% 0.12/0.36 Following clause subsumed by 167 during input processing: 0 [copy,167,flip.1] {-} A=A.
% 0.12/0.36 167 back subsumes 146.
% 0.12/0.36 167 back subsumes 145.
% 0.12/0.36 167 back subsumes 144.
% 0.12/0.36 167 back subsumes 143.
% 0.12/0.36
% 0.12/0.36 ======= end of input processing =======
% 0.18/0.42
% 0.18/0.42
% 0.18/0.42 Failed to model usable list: disabling FINDER
% 0.18/0.42
% 0.18/0.42
% 0.18/0.42
% 0.18/0.42 -------------- Softie stats --------------
% 0.18/0.42
% 0.18/0.42 UPDATE_STOP: 300
% 0.18/0.42 SFINDER_TIME_LIMIT: 2
% 0.18/0.42 SHORT_CLAUSE_CUTOFF: 4
% 0.18/0.42 number of clauses in intial UL: 154
% 0.18/0.42 number of clauses initially in problem: 163
% 0.18/0.42 percentage of clauses intially in UL: 94
% 0.18/0.42 percentage of distinct symbols occuring in initial UL: 90
% 0.18/0.42 percent of all initial clauses that are short: 100
% 0.18/0.42 absolute distinct symbol count: 40
% 0.18/0.42 distinct predicate count: 12
% 0.18/0.42 distinct function count: 20
% 0.18/0.42 distinct constant count: 8
% 0.18/0.42
% 0.18/0.42 ---------- no more Softie stats ----------
% 0.18/0.42
% 0.18/0.42
% 0.18/0.42
% 0.18/0.42 =========== start of search ===========
% 7.11/7.35
% 7.11/7.35
% 7.11/7.35 Changing weight limit from 60 to 58.
% 7.11/7.35
% 7.11/7.35 Resetting weight limit to 58 after 250 givens.
% 7.11/7.35
% 8.15/8.39
% 8.15/8.39
% 8.15/8.39 Changing weight limit from 58 to 57.
% 8.15/8.39
% 8.15/8.39 Resetting weight limit to 57 after 255 givens.
% 8.15/8.39
% 8.60/8.81
% 8.60/8.81
% 8.60/8.81 Changing weight limit from 57 to 56.
% 8.60/8.81
% 8.60/8.81 Resetting weight limit to 56 after 260 givens.
% 8.60/8.81
% 11.08/11.34
% 11.08/11.34
% 11.08/11.34 Changing weight limit from 56 to 55.
% 11.08/11.34
% 11.08/11.34 Resetting weight limit to 55 after 275 givens.
% 11.08/11.34
% 13.11/13.38
% 13.11/13.38
% 13.11/13.38 Changing weight limit from 55 to 54.
% 13.11/13.38
% 13.11/13.38 Resetting weight limit to 54 after 285 givens.
% 13.11/13.38
% 14.42/14.63
% 14.42/14.63
% 14.42/14.63 Changing weight limit from 54 to 52.
% 14.42/14.63
% 14.42/14.63 Resetting weight limit to 52 after 290 givens.
% 14.42/14.63
% 15.70/15.95
% 15.70/15.95
% 15.70/15.95 Changing weight limit from 52 to 51.
% 15.70/15.95
% 15.70/15.95 Resetting weight limit to 51 after 295 givens.
% 15.70/15.95
% 17.88/18.14
% 17.88/18.14
% 17.88/18.14 Changing weight limit from 51 to 50.
% 17.88/18.14
% 17.88/18.14 Modelling stopped after 300 given clauses and 0.00 seconds
% 17.88/18.14
% 17.88/18.14
% 17.88/18.14 Resetting weight limit to 50 after 305 givens.
% 17.88/18.14
% 19.53/19.79
% 19.53/19.79
% 19.53/19.79 Changing weight limit from 50 to 49.
% 19.53/19.79
% 19.53/19.79 Resetting weight limit to 49 after 320 givens.
% 19.53/19.79
% 20.31/20.57
% 20.31/20.57
% 20.31/20.57 Changing weight limit from 49 to 46.
% 20.31/20.57
% 20.31/20.57 Resetting weight limit to 46 after 335 givens.
% 20.31/20.57
% 21.28/21.54
% 21.28/21.54
% 21.28/21.54 Changing weight limit from 46 to 35.
% 21.28/21.54
% 21.28/21.54 Resetting weight limit to 35 after 345 givens.
% 21.28/21.54
% 21.44/21.65
% 21.44/21.65
% 21.44/21.65 Changing weight limit from 35 to 31.
% 21.44/21.65
% 21.44/21.65 Resetting weight limit to 31 after 350 givens.
% 21.44/21.65
% 21.84/22.04
% 21.84/22.04
% 21.84/22.04 Changing weight limit from 31 to 30.
% 21.84/22.04
% 21.84/22.04 Resetting weight limit to 30 after 380 givens.
% 21.84/22.04
% 24.61/24.86
% 24.61/24.86
% 24.61/24.86 Changing weight limit from 30 to 29.
% 24.61/24.86
% 24.61/24.86 Resetting weight limit to 29 after 495 givens.
% 24.61/24.86
% 25.23/25.48
% 25.23/25.48
% 25.23/25.48 Changing weight limit from 29 to 26.
% 25.23/25.48
% 25.23/25.48 Resetting weight limit to 26 after 570 givens.
% 25.23/25.48
% 25.23/25.49
% 25.23/25.49
% 25.23/25.49 Changing weight limit from 26 to 18.
% 25.23/25.49
% 25.23/25.49 Resetting weight limit to 18 after 580 givens.
% 25.23/25.49
% 25.30/25.56
% 25.30/25.56
% 25.30/25.56 Changing weight limit from 18 to 17.
% 25.30/25.56
% 25.30/25.56 Resetting weight limit to 17 after 650 givens.
% 25.30/25.56
% 25.30/25.56
% 25.30/25.56
% 25.30/25.56 Changing weight limit from 17 to 16.
% 25.30/25.56
% 25.30/25.56 Resetting weight limit to 16 after 655 givens.
% 25.30/25.56
% 25.44/25.64
% 25.44/25.64
% 25.44/25.64 Changing weight limit from 16 to 14.
% 25.44/25.64
% 25.44/25.64 Resetting weight limit to 14 after 725 givens.
% 25.44/25.64
% 25.52/25.77
% 25.52/25.77
% 25.52/25.77 Changing weight limit from 14 to 13.
% 25.52/25.77
% 25.52/25.77 Resetting weight limit to 13 after 870 givens.
% 25.52/25.77
% 25.59/25.79
% 25.59/25.79
% 25.59/25.79 Changing weight limit from 13 to 12.
% 25.59/25.79
% 25.59/25.79 Resetting weight limit to 12 after 880 givens.
% 25.59/25.79
% 25.59/25.82
% 25.59/25.82
% 25.59/25.82 Changing weight limit from 12 to 10.
% 25.59/25.82
% 25.59/25.82 Resetting weight limit to 10 after 935 givens.
% 25.59/25.82
% 26.92/27.12
% 26.92/27.12
% 26.92/27.12 Changing weight limit from 10 to 9.
% 26.92/27.12
% 26.92/27.12 Resetting weight limit to 9 after 1575 givens.
% 26.92/27.12
% 39.73/39.96
% 39.73/39.96
% 39.73/39.96 Changing weight limit from 9 to 8.
% 39.73/39.96
% 39.73/39.96 Resetting weight limit to 8 after 7615 givens.
% 39.73/39.96
% 59.81/60.08
% 59.81/60.08
% 59.81/60.08 Changing weight limit from 8 to 9.
% 59.81/60.08
% 59.81/60.08 Resetting weight limit to 9 after 10795 givens.
% 59.81/60.08
% 60.73/60.99
% 60.73/60.99
% 60.73/60.99 Changing weight limit from 9 to 8.
% 60.73/60.99
% 60.73/60.99 Resetting weight limit to 8 after 10940 givens.
% 60.73/60.99
% 63.80/64.08
% 63.80/64.08
% 63.80/64.08 Changing weight limit from 8 to 7.
% 63.80/64.08
% 63.80/64.08 Resetting weight limit to 7 after 13655 givens.
% 63.80/64.08
% 64.01/64.21
% 64.01/64.21
% 64.01/64.21 Changing weight limit from 7 to 5.
% 64.01/64.21
% 64.01/64.21 Resetting weight limit to 5 after 13660 givens.
% 64.01/64.21
% 66.12/66.33
% 66.12/66.33
% 66.12/66.33 Changing weight limit from 5 to 6.
% 66.12/66.33
% 66.12/66.33 Resetting weight limit to 6 after 16435 givens.
% 66.12/66.33
% 66.12/66.33
% 66.12/66.33
% 66.12/66.33 Changing weight limit from 6 to 7.
% 66.12/66.33
% 66.12/66.33 Resetting weight limit to 7 after 16440 givens.
% 66.12/66.33
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34 Changing weight limit from 7 to 8.
% 66.12/66.34
% 66.12/66.34 Resetting weight limit to 8 after 16445 givens.
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34 Changing weight limit from 8 to 9.
% 66.12/66.34
% 66.12/66.34 Resetting weight limit to 9 after 16450 givens.
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34 Changing weight limit from 9 to 10.
% 66.12/66.34
% 66.12/66.34 Resetting weight limit to 10 after 16455 givens.
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34
% 66.12/66.34 Changing weight limit from 10 to 11.
% 66.12/66.34
% 66.12/66.34 Resetting weight limit to 11 after 16460 givens.
% 66.12/66.34
% 66.30/66.54
% 66.30/66.54
% 66.30/66.54 Changing weight limit from 11 to 9.
% 66.30/66.54
% 66.30/66.54 Resetting weight limit to 9 after 16770 givens.
% 66.30/66.54
% 72.28/72.49
% 72.28/72.49
% 72.28/72.49 Changing weight limit from 9 to 8.
% 72.28/72.49
% 72.28/72.49 Resetting weight limit to 8 after 19510 givens.
% 72.28/72.49
% 73.21/73.41
% 73.21/73.41
% 73.21/73.41 Changing weight limit from 8 to 9.
% 73.21/73.41
% 73.21/73.41 Resetting weight limit to 9 after 19555 givens.
% 73.21/73.41
% 73.21/73.42
% 73.21/73.42
% 73.21/73.42 Changing weight limit from 9 to 10.
% 73.21/73.42
% 73.21/73.42 Resetting weight limit to 10 after 19560 givens.
% 73.21/73.42
% 73.21/73.42
% 73.21/73.42
% 73.21/73.42 Changing weight limit from 10 to 11.
% 73.21/73.42
% 73.21/73.42 Resetting weight limit to 11 after 19565 givens.
% 73.21/73.42
% 73.91/74.15
% 73.91/74.15
% 73.91/74.15 Changing weight limit from 11 to 10.
% 73.91/74.15
% 73.91/74.15 Resetting weight limit to 10 after 19705 givens.
% 73.91/74.15
% 74.73/74.96
% 74.73/74.96
% 74.73/74.96 Changing weight limit from 10 to 11.
% 74.73/74.96
% 74.73/74.96 Resetting weight limit to 11 after 19730 givens.
% 74.73/74.96
% 74.73/74.96
% 74.73/74.96
% 74.73/74.96 Changing weight limit from 11 to 12.
% 74.73/74.96
% 74.73/74.96 Resetting weight limit to 12 after 19735 givens.
% 74.73/74.96
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97 Changing weight limit from 12 to 13.
% 74.73/74.97
% 74.73/74.97 Resetting weight limit to 13 after 19740 givens.
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97 Changing weight limit from 13 to 14.
% 74.73/74.97
% 74.73/74.97 Resetting weight limit to 14 after 19745 givens.
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97 Changing weight limit from 14 to 15.
% 74.73/74.97
% 74.73/74.97 Resetting weight limit to 15 after 19750 givens.
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97
% 74.73/74.97 Changing weight limit from 15 to 16.
% 74.73/74.97
% 74.73/74.97 Resetting weight limit to 16 after 19755 givens.
% 74.73/74.97
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98 Changing weight limit from 16 to 17.
% 74.73/74.98
% 74.73/74.98 Resetting weight limit to 17 after 19760 givens.
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98 Changing weight limit from 17 to 18.
% 74.73/74.98
% 74.73/74.98 Resetting weight limit to 18 after 19765 givens.
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98 Changing weight limit from 18 to 19.
% 74.73/74.98
% 74.73/74.98 Resetting weight limit to 19 after 19770 givens.
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98
% 74.73/74.98 Changing weight limit from 19 to 20.
% 74.73/74.98
% 74.73/74.98 Resetting weight limit to 20 after 19775 givens.
% 74.73/74.98
% 74.73/74.99
% 74.73/74.99
% 74.73/74.99 Changing weight limit from 20 to 21.
% 74.73/74.99
% 74.73/74.99 Resetting weight limit to 21 after 19780 givens.
% 74.73/74.99
% 74.73/74.99
% 74.73/74.99
% 74.73/74.99 Changing weight limit from 21 to 22.
% 74.73/74.99
% 74.73/74.99 Resetting weight limit to 22 after 19785 givens.
% 74.73/74.99
% 74.73/74.99
% 74.73/74.99
% 74.73/74.99 Changing weight limit from 22 to 23.
% 74.73/74.99
% 74.73/74.99 Resetting weight limit to 23 after 19790 givens.
% 74.73/74.99
% 74.73/75.00
% 74.73/75.00
% 74.73/75.00 Changing weight limit from 23 to 24.
% 74.73/75.00
% 74.73/75.00 Resetting weight limit to 24 after 19795 givens.
% 74.73/75.00
% 74.73/75.00
% 74.73/75.00
% 74.73/75.00 Changing weight limit from 24 to 25.
% 74.73/75.00
% 74.73/75.00 Resetting weight limit to 25 after 19800 givens.
% 74.73/75.00
% 74.73/75.00
% 74.73/75.00
% 74.73/75.00 Changing weight limit from 25 to 26.
% 74.73/75.00
% 74.73/75.00 Resetting weight limit to 26 after 19805 givens.
% 74.73/75.00
% 74.81/75.01
% 74.81/75.01
% 74.81/75.01 Changing weight limit from 26 to 27.
% 74.81/75.01
% 74.81/75.01 Resetting weight limit to 27 after 19810 givens.
% 74.81/75.01
% 74.81/75.01
% 74.81/75.01
% 74.81/75.01 Changing weight limit from 27 to 28.
% 74.81/75.01
% 74.81/75.01 Resetting weight limit to 28 after 19815 givens.
% 74.81/75.01
% 74.81/75.01
% 74.81/75.01
% 74.81/75.01 Changing weight limit from 28 to 29.
% 74.81/75.01
% 74.81/75.01 Resetting weight limit to 29 after 19820 givens.
% 74.81/75.01
% 74.81/75.02
% 74.81/75.02
% 74.81/75.02 Changing weight limit from 29 to 30.
% 74.81/75.02
% 74.81/75.02 Resetting weight limit to 30 after 19825 givens.
% 74.81/75.02
% 74.81/75.02
% 74.81/75.02
% 74.81/75.02 Changing weight limit from 30 to 31.
% 74.81/75.02
% 74.81/75.02 Resetting weight limit to 31 after 19830 givens.
% 74.81/75.02
% 74.81/75.02
% 74.81/75.02
% 74.81/75.02 Changing weight limit from 31 to 32.
% 74.81/75.02
% 74.81/75.02 Resetting weight limit to 32 after 19835 givens.
% 74.81/75.02
% 74.89/75.15
% 74.89/75.15
% 74.89/75.15 Changing weight limit from 32 to 27.
% 74.89/75.15
% 74.89/75.15 Resetting weight limit to 27 after 20000 givens.
% 74.89/75.15
% 74.99/75.20
% 74.99/75.20
% 74.99/75.20 Changing weight limit from 27 to 24.
% 74.99/75.20
% 74.99/75.20 Resetting weight limit to 24 after 20010 givens.
% 74.99/75.20
% 75.19/75.40
% 75.19/75.40
% 75.19/75.40 Changing weight limit from 24 to 21.
% 75.19/75.40
% 75.19/75.40 Resetting weight limit to 21 after 20035 givens.
% 75.19/75.40
% 75.64/75.89
% 75.64/75.89
% 75.64/75.89 Changing weight limit from 21 to 18.
% 75.64/75.89
% 75.64/75.89 Resetting weight limit to 18 after 20150 givens.
% 75.64/75.89
% 75.64/75.90
% 75.64/75.90
% 75.64/75.90 Changing weight limit from 18 to 15.
% 75.64/75.90
% 75.64/75.90 Resetting weight limit to 15 after 20155 givens.
% 75.64/75.90
% 75.87/76.07
% 75.87/76.07
% 75.87/76.07 Changing weight limit from 15 to 14.
% 75.87/76.07
% 75.87/76.07 Resetting weight limit to 14 after 20215 givens.
% 75.87/76.07
% 76.49/76.70
% 76.49/76.70
% 76.49/76.70 Changing weight limit from 14 to 15.
% 76.49/76.70
% 76.49/76.70 Resetting weight limit to 15 after 20380 givens.
% 76.49/76.70
% 76.51/76.72
% 76.51/76.72
% 76.51/76.72 Changing weight limit from 15 to 16.
% 76.51/76.72
% 76.51/76.72 Resetting weight limit to 16 after 20385 givens.
% 76.51/76.72
% 76.53/76.76
% 76.53/76.76
% 76.53/76.76 Changing weight limit from 16 to 17.
% 76.53/76.76
% 76.53/76.76 Resetting weight limit to 17 after 20390 givens.
% 76.53/76.76
% 76.53/76.78
% 76.53/76.78
% 76.53/76.78 Changing weight limit from 17 to 18.
% 76.53/76.78
% 76.53/76.78 Resetting weight limit to 18 after 20395 givens.
% 76.53/76.78
% 76.53/76.80
% 76.53/76.80
% 76.53/76.80 Changing weight limit from 18 to 19.
% 76.53/76.80
% 76.53/76.80 Resetting weight limit to 19 after 20400 givens.
% 76.53/76.80
% 76.53/76.80
% 76.53/76.80
% 76.53/76.80 Changing weight limit from 19 to 20.
% 76.53/76.80
% 76.53/76.80 Resetting weight limit to 20 after 20405 givens.
% 76.53/76.80
% 76.53/76.81
% 76.53/76.81
% 76.53/76.81 Changing weight limit from 20 to 21.
% 76.53/76.81
% 76.53/76.81 Resetting weight limit to 21 after 20410 givens.
% 76.53/76.81
% 76.53/76.81
% 76.53/76.81
% 76.53/76.81 Changing weight limit from 21 to 22.
% 76.53/76.81
% 76.53/76.81 Resetting weight limit to 22 after 20415 givens.
% 76.53/76.81
% 76.62/76.82
% 76.62/76.82
% 76.62/76.82 Changing weight limit from 22 to 23.
% 76.62/76.82
% 76.62/76.82 Resetting weight limit to 23 after 20420 givens.
% 76.62/76.82
% 76.62/76.82
% 76.62/76.82
% 76.62/76.82 Changing weight limit from 23 to 24.
% 76.62/76.82
% 76.62/76.82 Resetting weight limit to 24 after 20425 givens.
% 76.62/76.82
% 76.62/76.83
% 76.62/76.83
% 76.62/76.83 Changing weight limit from 24 to 25.
% 76.62/76.83
% 76.62/76.83 Resetting weight limit to 25 after 20430 givens.
% 76.62/76.83
% 76.62/76.83
% 76.62/76.83
% 76.62/76.83 Changing weight limit from 25 to 26.
% 76.62/76.83
% 76.62/76.83 Resetting weight limit to 26 after 20435 givens.
% 76.62/76.83
% 76.81/77.05
% 76.81/77.05
% 76.81/77.05 Changing weight limit from 26 to 25.
% 76.81/77.05
% 76.81/77.05 Resetting weight limit to 25 after 20645 givens.
% 76.81/77.05
% 77.11/77.31
% 77.11/77.31
% 77.11/77.31 Changing weight limit from 25 to 24.
% 77.11/77.31
% 77.11/77.31 Resetting weight limit to 24 after 20730 givens.
% 77.11/77.31
% 77.11/77.35
% 77.11/77.35
% 77.11/77.35 Changing weight limit from 24 to 21.
% 77.11/77.35
% 77.11/77.35 Resetting weight limit to 21 after 20740 givens.
% 77.11/77.35
% 78.92/79.12
% 78.92/79.12
% 78.92/79.12 Changing weight limit from 21 to 22.
% 78.92/79.12
% 78.92/79.12 Resetting weight limit to 22 after 21045 givens.
% 78.92/79.12
% 78.92/79.13
% 78.92/79.13
% 78.92/79.13 Changing weight limit from 22 to 23.
% 78.92/79.13
% 78.92/79.13 Resetting weight limit to 23 after 21050 givens.
% 78.92/79.13
% 78.92/79.13
% 78.92/79.13
% 78.92/79.13 Changing weight limit from 23 to 24.
% 78.92/79.13
% 78.92/79.13 Resetting weight limit to 24 after 21055 givens.
% 78.92/79.13
% 78.92/79.14
% 78.92/79.14
% 78.92/79.14 Changing weight limit from 24 to 25.
% 78.92/79.14
% 78.92/79.14 Resetting weight limit to 25 after 21060 givens.
% 78.92/79.14
% 78.99/79.23
% 78.99/79.23
% 78.99/79.23 Changing weight limit from 25 to 26.
% 78.99/79.23
% 78.99/79.23 Resetting weight limit to 26 after 21065 givens.
% 78.99/79.23
% 79.09/79.31
% 79.09/79.31
% 79.09/79.31 Changing weight limit from 26 to 27.
% 79.09/79.31
% 79.09/79.31 Resetting weight limit to 27 after 21070 givens.
% 79.09/79.31
% 79.12/79.33
% 79.12/79.33
% 79.12/79.33 Changing weight limit from 27 to 28.
% 79.12/79.33
% 79.12/79.33 Resetting weight limit to 28 after 21075 givens.
% 79.12/79.33
% 79.13/79.35
% 79.13/79.35
% 79.13/79.35 Changing weight limit from 28 to 29.
% 79.13/79.35
% 79.13/79.35 Resetting weight limit to 29 after 21080 givens.
% 79.13/79.35
% 79.13/79.36
% 79.13/79.36
% 79.13/79.36 Changing weight limit from 29 to 30.
% 79.13/79.36
% 79.13/79.36 Resetting weight limit to 30 after 21085 givens.
% 79.13/79.36
% 79.13/79.38
% 79.13/79.38
% 79.13/79.38 Changing weight limit from 30 to 31.
% 79.13/79.38
% 79.13/79.38 Resetting weight limit to 31 after 21090 givens.
% 79.13/79.38
% 79.13/79.40
% 79.13/79.40
% 79.13/79.40 Changing weight limit from 31 to 32.
% 79.13/79.40
% 79.13/79.40 Resetting weight limit to 32 after 21095 givens.
% 79.13/79.40
% 79.21/79.42
% 79.21/79.42
% 79.21/79.42 Changing weight limit from 32 to 33.
% 79.21/79.42
% 79.21/79.42 Resetting weight limit to 33 after 21100 givens.
% 79.21/79.42
% 79.21/79.43
% 79.21/79.43
% 79.21/79.43 Changing weight limit from 33 to 34.
% 79.21/79.43
% 79.21/79.43 Resetting weight limit to 34 after 21105 givens.
% 79.21/79.43
% 79.21/79.45
% 79.21/79.45
% 79.21/79.45 Changing weight limit from 34 to 35.
% 79.21/79.45
% 79.21/79.45 Resetting weight limit to 35 after 21110 givens.
% 79.21/79.45
% 79.27/79.47
% 79.27/79.47
% 79.27/79.47 Changing weight limit from 35 to 36.
% 79.27/79.47
% 79.27/79.47 Resetting weight limit to 36 after 21115 givens.
% 79.27/79.47
% 79.27/79.49
% 79.27/79.49
% 79.27/79.49 Changing weight limit from 36 to 37.
% 79.27/79.49
% 79.27/79.49 Resetting weight limit to 37 after 21120 givens.
% 79.27/79.49
% 79.27/79.51
% 79.27/79.51
% 79.27/79.51 Changing weight limit from 37 to 38.
% 79.27/79.51
% 79.27/79.51 Resetting weight limit to 38 after 21125 givens.
% 79.27/79.51
% 79.27/79.52
% 79.27/79.52
% 79.27/79.52 Changing weight limit from 38 to 39.
% 79.27/79.52
% 79.27/79.52 Resetting weight limit to 39 after 21130 givens.
% 79.27/79.52
% 79.27/79.54
% 79.27/79.54
% 79.27/79.54 Changing weight limit from 39 to 40.
% 79.27/79.54
% 79.27/79.54 Resetting weight limit to 40 after 21135 givens.
% 79.27/79.54
% 79.27/79.56
% 79.27/79.56
% 79.27/79.56 Changing weight limit from 40 to 41.
% 79.27/79.56
% 79.27/79.56 Resetting weight limit to 41 after 21140 givens.
% 79.27/79.56
% 79.38/79.57
% 79.38/79.57
% 79.38/79.57 Changing weight limit from 41 to 42.
% 79.38/79.57
% 79.38/79.57 Resetting weight limit to 42 after 21145 givens.
% 79.38/79.57
% 79.40/79.59
% 79.40/79.59
% 79.40/79.59 Changing weight limit from 42 to 43.
% 79.40/79.59
% 79.40/79.59 Resetting weight limit to 43 after 21150 givens.
% 79.40/79.59
% 79.40/79.61
% 79.40/79.61
% 79.40/79.61 Changing weight limit from 43 to 44.
% 79.40/79.61
% 79.40/79.61 Resetting weight limit to 44 after 21155 givens.
% 79.40/79.61
% 79.45/79.63
% 79.45/79.63
% 79.45/79.63 Changing weight limit from 44 to 45.
% 79.45/79.63
% 79.45/79.63 Resetting weight limit to 45 after 21160 givens.
% 79.45/79.63
% 79.45/79.65
% 79.45/79.65
% 79.45/79.65 Changing weight limit from 45 to 46.
% 79.45/79.65
% 79.45/79.65 Resetting weight limit to 46 after 21165 givens.
% 79.45/79.65
% 79.45/79.67
% 79.45/79.67
% 79.45/79.67 Changing weight limit from 46 to 47.
% 79.45/79.67
% 79.45/79.67 Resetting weight limit to 47 after 21170 givens.
% 79.45/79.67
% 79.45/79.69
% 79.45/79.69
% 79.45/79.69 Changing weight limit from 47 to 48.
% 79.45/79.69
% 79.45/79.69 Resetting weight limit to 48 after 21175 givens.
% 79.45/79.69
% 79.52/79.71
% 79.52/79.71
% 79.52/79.71 Changing weight limit from 48 to 49.
% 79.52/79.71
% 79.52/79.71 Resetting weight limit to 49 after 21180 givens.
% 79.52/79.71
% 79.52/79.73
% 79.52/79.73
% 79.52/79.73 Changing weight limit from 49 to 50.
% 79.52/79.73
% 79.52/79.73 Resetting weight limit to 50 after 21185 givens.
% 79.52/79.73
% 79.52/79.75
% 79.52/79.75
% 79.52/79.75 Changing weight limit from 50 to 51.
% 79.52/79.75
% 79.52/79.75 Resetting weight limit to 51 after 21190 givens.
% 79.52/79.75
% 79.52/79.77
% 79.52/79.77
% 79.52/79.77 Changing weight limit from 51 to 52.
% 79.52/79.77
% 79.52/79.77 Resetting weight limit to 52 after 21195 givens.
% 79.52/79.77
% 79.60/79.79
% 79.60/79.79
% 79.60/79.79 Changing weight limit from 52 to 53.
% 79.60/79.79
% 79.60/79.79 Resetting weight limit to 53 after 21200 givens.
% 79.60/79.79
% 79.60/79.81
% 79.60/79.81
% 79.60/79.81 Changing weight limit from 53 to 54.
% 79.60/79.81
% 79.60/79.81 Resetting weight limit to 54 after 21205 givens.
% 79.60/79.81
% 79.60/79.83
% 79.60/79.83
% 79.60/79.83 Changing weight limit from 54 to 55.
% 79.60/79.83
% 79.60/79.83 Resetting weight limit to 55 after 21210 givens.
% 79.60/79.83
% 79.60/79.85
% 79.60/79.85
% 79.60/79.85 Changing weight limit from 55 to 56.
% 79.60/79.85
% 79.60/79.85 Resetting weight limit to 56 after 21215 givens.
% 79.60/79.85
% 79.60/79.86
% 79.60/79.86
% 79.60/79.86 Changing weight limit from 56 to 57.
% 79.60/79.86
% 79.60/79.86 Resetting weight limit to 57 after 21220 givens.
% 79.60/79.86
% 79.70/79.89
% 79.70/79.89
% 79.70/79.89 Changing weight limit from 57 to 58.
% 79.70/79.89
% 79.70/79.89 Resetting weight limit to 58 after 21225 givens.
% 79.70/79.89
% 79.70/79.90
% 79.70/79.90
% 79.70/79.90 Changing weight limit from 58 to 59.
% 79.70/79.90
% 79.70/79.90 Resetting weight limit to 59 after 21230 givens.
% 79.70/79.90
% 79.72/79.92
% 79.72/79.92
% 79.72/79.92 Changing weight limit from 59 to 60.
% 79.72/79.92
% 79.72/79.92 Resetting weight limit to 60 after 21235 givens.
% 79.72/79.92
% 80.42/80.63
% 80.42/80.63 -- HEY sandbox2, WE HAVE A PROOF!! --
% 80.42/80.63
% 80.42/80.63 ----> UNIT CONFLICT at 77.74 sec ----> 292775 [binary,292774.1,113.1] {-} $F.
% 80.42/80.63
% 80.42/80.63 Length of proof is 224. Level of proof is 33.
% 80.42/80.63
% 80.42/80.63 ---------------- PROOF ----------------
% 80.42/80.63 % SZS status Theorem
% 80.42/80.63 % SZS output start Refutation
% 80.42/80.63
% 80.42/80.63 1 [] {+} -coll(A,B,C)|coll(A,C,B).
% 80.42/80.63 2 [] {+} -coll(A,B,C)|coll(B,A,C).
% 80.42/80.63 3 [] {+} -coll(A,B,C)| -coll(A,B,D)|coll(C,D,A).
% 80.42/80.63 4 [] {+} -para(A,B,C,D)|para(A,B,D,C).
% 80.42/80.63 5 [] {+} -para(A,B,C,D)|para(C,D,A,B).
% 80.42/80.63 6 [] {+} -para(A,B,C,D)| -para(C,D,E,F)|para(A,B,E,F).
% 80.42/80.63 7 [] {+} -perp(A,B,C,D)|perp(A,B,D,C).
% 80.42/80.63 8 [] {+} -perp(A,B,C,D)|perp(C,D,A,B).
% 80.42/80.63 9 [] {+} -perp(A,B,C,D)| -perp(C,D,E,F)|para(A,B,E,F).
% 80.42/80.63 10 [] {+} -para(A,B,C,D)| -perp(C,D,E,F)|perp(A,B,E,F).
% 80.42/80.63 11 [] {+} -midp(A,B,C)|midp(A,C,B).
% 80.42/80.63 14 [] {+} -cyclic(A,B,C,D)|cyclic(A,B,D,C).
% 80.42/80.63 15 [] {+} -cyclic(A,B,C,D)|cyclic(A,C,B,D).
% 80.42/80.63 16 [] {+} -cyclic(A,B,C,D)|cyclic(B,A,C,D).
% 80.42/80.63 17 [] {+} -cyclic(A,B,C,D)| -cyclic(A,B,C,E)|cyclic(B,C,D,E).
% 80.42/80.63 19 [] {+} -eqangle(A,B,C,D,E,F,G,H)|eqangle(C,D,A,B,G,H,E,F).
% 80.42/80.63 22 [] {+} -eqangle(A,B,C,D,E,F,G,H)| -eqangle(E,F,G,H,I,J,K,L)|eqangle(A,B,C,D,I,J,K,L).
% 80.42/80.63 25 [] {+} -cong(A,B,C,D)| -cong(C,D,E,F)|cong(A,B,E,F).
% 80.42/80.63 29 [] {+} -eqratio(A,B,C,D,E,F,G,H)|eqratio(A,B,E,F,C,D,G,H).
% 80.42/80.63 39 [] {+} -eqangle(A,B,C,D,E,F,C,D)|para(A,B,E,F).
% 80.42/80.63 40 [] {+} -para(A,B,C,D)|eqangle(A,B,E,F,C,D,E,F).
% 80.42/80.63 43 [] {+} -eqangle(A,B,A,C,D,B,D,C)| -coll(A,D,C)|cyclic(B,C,A,D).
% 80.42/80.63 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).
% 80.42/80.63 45 [] {+} -midp(A,B,C)| -midp(D,B,E)|para(A,D,C,E).
% 80.42/80.63 46 [] {+} -midp(A,B,C)| -para(A,D,C,E)| -coll(D,B,E)|midp(D,B,E).
% 80.42/80.63 53 [] {+} -perp(A,B,B,C)| -midp(D,A,C)|cong(A,D,B,D).
% 80.42/80.63 54 [] {+} -circle(A,B,C,D)| -coll(A,B,D)|perp(B,C,C,D).
% 80.42/80.63 56 [] {+} -midp(A,B,C)| -perp(D,A,B,C)|cong(D,B,D,C).
% 80.42/80.63 57 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)|perp(A,C,B,D).
% 80.42/80.63 58 [] {+} -cong(A,B,C,B)| -cong(A,D,C,D)| -cyclic(A,C,B,D)|perp(B,A,A,D).
% 80.42/80.63 64 [] {+} -midp(A,B,C)| -midp(A,D,E)|para(B,D,C,E).
% 80.42/80.63 65 [] {+} -midp(A,B,C)| -para(B,D,C,E)| -para(B,E,C,D)|midp(A,D,E).
% 80.42/80.63 66 [] {+} -para(A,B,C,D)| -coll(E,A,C)| -coll(E,B,D)|eqratio(E,A,A,C,E,B,B,D).
% 80.42/80.63 67 [] {+} -para(A,B,A,C)|coll(A,B,C).
% 80.42/80.63 68 [] {+} -cong(A,B,A,C)| -coll(A,B,C)|midp(A,B,C).
% 80.42/80.63 69 [] {+} -midp(A,B,C)|cong(A,B,A,C).
% 80.42/80.63 75 [] {+} -eqratio(A,B,C,D,E,F,G,H)| -cong(E,F,G,H)|cong(A,B,C,D).
% 80.42/80.63 99 [] {+} -circle(A,B,C,D)|perp($f12(B,C,D,A),B,B,A).
% 80.42/80.63 113 [] {+} -eqangle($c1,$c8,$c8,$c7,$c7,$c8,$c8,$c5).
% 80.42/80.63 114 [factor,3.1.2] {+} -coll(A,B,C)|coll(C,C,A).
% 80.42/80.63 120 [factor,17.1.2] {+} -cyclic(A,B,C,D)|cyclic(B,C,D,D).
% 80.42/80.63 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).
% 80.42/80.63 124 [factor,45.1.2] {+} -midp(A,B,C)|para(A,A,C,C).
% 80.42/80.63 125 [factor,57.1.2] {+} -cong(A,B,C,B)|perp(A,C,B,B).
% 80.42/80.63 126 [factor,58.1.2] {+} -cong(A,B,C,B)| -cyclic(A,C,B,B)|perp(B,A,A,B).
% 80.42/80.63 128 [factor,64.1.2] {+} -midp(A,B,C)|para(B,B,C,C).
% 80.42/80.63 129 [factor,65.2.3] {+} -midp(A,B,C)| -para(B,D,C,D)|midp(A,D,D).
% 80.42/80.63 159 [] {-} circle($c5,$c8,$c7,$c6).
% 80.42/80.63 160 [] {-} perp($c4,$c6,$c8,$c7).
% 80.42/80.63 161 [] {-} coll($c4,$c8,$c7).
% 80.42/80.63 162 [] {-} perp($c3,$c7,$c8,$c6).
% 80.42/80.63 163 [] {-} coll($c3,$c8,$c6).
% 80.42/80.63 164 [] {-} coll($c2,$c6,$c4).
% 80.42/80.63 168 [hyper,159,99] {-} perp($f12($c8,$c7,$c6,$c5),$c8,$c8,$c5).
% 80.42/80.63 185 [hyper,161,114] {-} coll($c7,$c7,$c4).
% 80.42/80.63 186 [hyper,161,2] {-} coll($c8,$c4,$c7).
% 80.42/80.63 187 [hyper,161,1] {-} coll($c4,$c7,$c8).
% 80.42/80.63 200 [hyper,163,114] {-} coll($c6,$c6,$c3).
% 80.42/80.63 201 [hyper,163,2] {-} coll($c8,$c3,$c6).
% 80.42/80.63 215 [hyper,164,114] {-} coll($c4,$c4,$c2).
% 80.42/80.63 216 [hyper,164,2] {-} coll($c6,$c2,$c4).
% 80.42/80.63 217 [hyper,164,1] {-} coll($c2,$c4,$c6).
% 80.42/80.63 230 [hyper,160,8] {-} perp($c8,$c7,$c4,$c6).
% 80.42/80.63 231 [hyper,160,7] {-} perp($c4,$c6,$c7,$c8).
% 80.42/80.63 263 [hyper,185,114] {-} coll($c4,$c4,$c7).
% 80.42/80.63 277 [hyper,186,114] {-} coll($c7,$c7,$c8).
% 80.42/80.63 278 [hyper,186,1] {-} coll($c8,$c7,$c4).
% 80.42/80.63 291 [hyper,187,114] {-} coll($c8,$c8,$c4).
% 80.42/80.63 305 [hyper,162,8] {-} perp($c8,$c6,$c3,$c7).
% 80.42/80.63 306 [hyper,162,7] {-} perp($c3,$c7,$c6,$c8).
% 80.42/80.63 324 [hyper,200,1] {-} coll($c6,$c3,$c6).
% 80.42/80.63 337 [hyper,201,114] {-} coll($c6,$c6,$c8).
% 80.42/80.63 365 [hyper,215,114] {-} coll($c2,$c2,$c4).
% 80.42/80.63 366 [hyper,215,1] {-} coll($c4,$c2,$c4).
% 80.42/80.63 396 [hyper,216,114] {-} coll($c4,$c4,$c6).
% 80.42/80.63 410 [hyper,217,114] {-} coll($c6,$c6,$c2).
% 80.42/80.63 411 [hyper,217,2] {-} coll($c4,$c2,$c6).
% 80.42/80.63 452 [hyper,168,8] {-} perp($c8,$c5,$f12($c8,$c7,$c6,$c5),$c8).
% 80.42/80.63 502 [hyper,263,1] {-} coll($c4,$c7,$c4).
% 80.42/80.63 529 [hyper,277,114] {-} coll($c8,$c8,$c7).
% 80.42/80.63 643 [hyper,278,114] {-} coll($c4,$c4,$c8).
% 80.42/80.63 798 [hyper,324,114] {-} coll($c6,$c6,$c6).
% 80.42/80.63 812 [hyper,337,114] {-} coll($c8,$c8,$c6).
% 80.42/80.63 813 [hyper,337,1] {-} coll($c6,$c8,$c6).
% 80.42/80.63 968 [hyper,365,1] {-} coll($c2,$c4,$c2).
% 80.42/80.63 981 [hyper,366,114] {-} coll($c4,$c4,$c4).
% 80.42/80.63 982 [hyper,366,2] {-} coll($c2,$c4,$c4).
% 80.42/80.63 995 [hyper,396,114] {-} coll($c6,$c6,$c4).
% 80.42/80.63 996 [hyper,396,3,263] {-} coll($c7,$c6,$c4).
% 80.42/80.63 997 [hyper,396,3,263] {-} coll($c6,$c7,$c4).
% 80.42/80.63 1142 [hyper,411,3,366] {-} coll($c6,$c4,$c4).
% 80.42/80.63 1431 [hyper,502,3,187] {-} coll($c8,$c4,$c4).
% 80.42/80.63 1433 [hyper,502,2] {-} coll($c7,$c4,$c4).
% 80.42/80.63 1658 [hyper,643,3,396] {-} coll($c6,$c8,$c4).
% 80.42/80.63 1815 [hyper,798,3,410] {-} coll($c2,$c6,$c6).
% 80.42/80.63 1900 [hyper,812,3,529] {-} coll($c7,$c6,$c8).
% 80.42/80.63 1903 [hyper,812,3,291] {-} coll($c6,$c4,$c8).
% 80.42/80.63 1904 [hyper,812,1] {-} coll($c8,$c6,$c8).
% 80.42/80.63 2130 [hyper,968,3,217] {-} coll($c6,$c2,$c2).
% 80.42/80.63 2131 [hyper,968,3,217] {-} coll($c2,$c6,$c2).
% 80.42/80.63 2132 [hyper,968,2] {-} coll($c4,$c2,$c2).
% 80.42/80.63 2210 [hyper,995,3,337] {-} coll($c8,$c4,$c6).
% 80.42/80.63 2225 [hyper,996,1] {-} coll($c7,$c4,$c6).
% 80.42/80.63 2238 [hyper,997,1] {-} coll($c6,$c4,$c7).
% 80.42/80.63 3528 [hyper,1900,1] {-} coll($c7,$c8,$c6).
% 80.42/80.63 4065 [hyper,2238,114] {-} coll($c7,$c7,$c6).
% 80.42/80.63 5892 [hyper,230,9,160] {-} para($c4,$c6,$c4,$c6).
% 80.42/80.63 5894 [hyper,230,7] {-} perp($c8,$c7,$c6,$c4).
% 80.42/80.63 5912 [hyper,231,8] {-} perp($c7,$c8,$c4,$c6).
% 80.42/80.63 5968 [hyper,306,9,305] {-} para($c8,$c6,$c6,$c8).
% 80.42/80.63 5969 [hyper,306,8] {-} perp($c6,$c8,$c3,$c7).
% 80.42/80.63 6062 [hyper,5892,66,982,1815] {-} eqratio($c2,$c4,$c4,$c4,$c2,$c6,$c6,$c6).
% 80.42/80.63 6064 [hyper,5892,40] {-} eqangle($c4,$c6,A,B,$c4,$c6,A,B).
% 80.42/80.63 6065 [hyper,5892,4] {-} para($c4,$c6,$c6,$c4).
% 80.42/80.63 6177 [hyper,5894,8] {-} perp($c6,$c4,$c8,$c7).
% 80.42/80.63 6656 [hyper,5969,9,306] {-} para($c6,$c8,$c6,$c8).
% 80.42/80.63 6753 [hyper,6065,5] {-} para($c6,$c4,$c4,$c6).
% 80.42/80.63 6770 [hyper,6177,9,5894] {-} para($c6,$c4,$c6,$c4).
% 80.42/80.63 7487 [hyper,6770,40] {-} eqangle($c6,$c4,A,B,$c6,$c4,A,B).
% 80.42/80.63 7761 [hyper,452,9,168] {-} para($c8,$c5,$c8,$c5).
% 80.42/80.63 7795 [hyper,7761,67] {-} coll($c8,$c5,$c5).
% 80.42/80.63 7814 [hyper,7795,114] {-} coll($c5,$c5,$c8).
% 80.42/80.63 7816 [hyper,7795,2] {-} coll($c5,$c8,$c5).
% 80.42/80.63 7829 [hyper,7814,114] {-} coll($c8,$c8,$c5).
% 80.42/80.63 7865 [hyper,7829,3,812] {-} coll($c6,$c5,$c8).
% 80.42/80.63 7866 [hyper,7829,3,529] {-} coll($c7,$c5,$c8).
% 80.42/80.63 7868 [hyper,7829,3,291] {-} coll($c4,$c5,$c8).
% 80.42/80.63 7871 [hyper,7829,3,812] {-} coll($c5,$c6,$c8).
% 80.42/80.63 7926 [hyper,7865,1] {-} coll($c6,$c8,$c5).
% 80.42/80.63 7939 [hyper,7866,1] {-} coll($c7,$c8,$c5).
% 80.42/80.63 8038 [hyper,7871,1] {-} coll($c5,$c8,$c6).
% 80.42/80.63 8157 [hyper,7926,3,1658] {-} coll($c4,$c5,$c6).
% 80.42/80.63 8164 [hyper,7926,3,813] {-} coll($c5,$c6,$c6).
% 80.42/80.63 8184 [hyper,7939,3,3528] {-} coll($c6,$c5,$c7).
% 80.42/80.63 8286 [hyper,8038,114] {-} coll($c6,$c6,$c5).
% 80.42/80.63 8339 [hyper,8038,54,159] {-} perp($c8,$c7,$c7,$c6).
% 80.42/80.63 8341 [hyper,8038,3,7816] {-} coll($c5,$c6,$c5).
% 80.42/80.63 10314 [hyper,8339,9,6177] {-} para($c6,$c4,$c7,$c6).
% 80.42/80.63 10315 [hyper,8339,9,160] {-} para($c4,$c6,$c7,$c6).
% 80.42/80.63 10316 [hyper,8339,8] {-} perp($c7,$c6,$c8,$c7).
% 80.42/80.63 10317 [hyper,8339,7] {-} perp($c8,$c7,$c6,$c7).
% 80.42/80.63 10563 [hyper,10314,4] {-} para($c6,$c4,$c6,$c7).
% 80.42/80.63 10679 [hyper,10315,4] {-} para($c4,$c6,$c6,$c7).
% 80.42/80.63 10697 [hyper,10317,9,10316] {-} para($c7,$c6,$c6,$c7).
% 80.42/80.63 10698 [hyper,10317,8] {-} perp($c6,$c7,$c8,$c7).
% 80.42/80.63 11062 [hyper,10563,5] {-} para($c6,$c7,$c6,$c4).
% 80.42/80.63 11291 [hyper,10679,5] {-} para($c6,$c7,$c4,$c6).
% 80.42/80.63 11520 [hyper,10697,5] {-} para($c6,$c7,$c7,$c6).
% 80.42/80.63 11537 [hyper,10698,9,10317] {-} para($c6,$c7,$c6,$c7).
% 80.42/80.63 17536 [hyper,6062,29] {-} eqratio($c2,$c4,$c2,$c6,$c4,$c4,$c6,$c6).
% 80.42/80.63 17543 [hyper,6064,43,981] {-} cyclic($c6,$c4,$c4,$c4).
% 80.42/80.63 17545 [hyper,6064,43,396] {-} cyclic($c6,$c6,$c4,$c4).
% 80.42/80.63 17547 [hyper,6064,43,215] {-} cyclic($c6,$c2,$c4,$c4).
% 80.42/80.63 17549 [hyper,6064,19] {-} eqangle(A,B,$c4,$c6,A,B,$c4,$c6).
% 80.42/80.63 17564 [hyper,17545,15] {-} cyclic($c6,$c4,$c6,$c4).
% 80.42/80.63 17569 [hyper,17547,16] {-} cyclic($c2,$c6,$c4,$c4).
% 80.42/80.63 17570 [hyper,17547,15] {-} cyclic($c6,$c4,$c2,$c4).
% 80.42/80.63 17601 [hyper,17564,16] {-} cyclic($c4,$c6,$c6,$c4).
% 80.42/80.63 17602 [hyper,17564,14] {-} cyclic($c6,$c4,$c4,$c6).
% 80.42/80.63 17614 [hyper,17569,15] {-} cyclic($c2,$c4,$c6,$c4).
% 80.42/80.63 17619 [hyper,17570,16] {-} cyclic($c4,$c6,$c2,$c4).
% 80.42/80.63 17620 [hyper,17570,14] {-} cyclic($c6,$c4,$c4,$c2).
% 80.42/80.63 17670 [hyper,17601,14] {-} cyclic($c4,$c6,$c4,$c6).
% 80.42/80.63 17671 [hyper,17602,123,17543,6064] {-} cong($c6,$c4,$c6,$c4).
% 80.42/80.63 17708 [hyper,17614,16] {-} cyclic($c4,$c2,$c6,$c4).
% 80.42/80.63 17711 [hyper,17619,14] {-} cyclic($c4,$c6,$c4,$c2).
% 80.42/80.63 17712 [hyper,17620,120] {-} cyclic($c4,$c4,$c2,$c2).
% 80.42/80.63 17721 [hyper,17620,17,17602] {-} cyclic($c4,$c4,$c2,$c6).
% 80.42/80.63 17836 [hyper,17671,126,17545] {-} perp($c4,$c6,$c6,$c4).
% 80.42/80.63 17842 [hyper,17671,68,1142] {-} midp($c6,$c4,$c4).
% 80.42/80.63 17847 [hyper,17842,129,5892] {-} midp($c6,$c6,$c6).
% 80.42/80.63 17850 [hyper,17842,46,11291,2225] {-} midp($c7,$c4,$c6).
% 80.42/80.63 17851 [hyper,17842,46,6753,396] {-} midp($c4,$c4,$c6).
% 80.42/80.63 17857 [hyper,17847,129,11537] {-} midp($c6,$c7,$c7).
% 80.42/80.63 17858 [hyper,17847,129,6656] {-} midp($c6,$c8,$c8).
% 80.42/80.63 17863 [hyper,17847,65,11062,10563] {-} midp($c6,$c7,$c4).
% 80.42/80.63 17869 [hyper,17847,46,6656,1904] {-} midp($c8,$c6,$c8).
% 80.42/80.63 17885 [hyper,17850,56,230] {-} cong($c8,$c4,$c8,$c6).
% 80.42/80.63 17902 [hyper,17851,69] {-} cong($c4,$c4,$c4,$c6).
% 80.42/80.63 17909 [hyper,17857,124] {-} para($c6,$c6,$c7,$c7).
% 80.42/80.63 17927 [hyper,17857,46,11520,4065] {-} midp($c7,$c7,$c6).
% 80.42/80.63 17934 [hyper,17858,129,7761] {-} midp($c6,$c5,$c5).
% 80.42/80.63 17983 [hyper,17863,64,17858] {-} para($c8,$c7,$c8,$c4).
% 80.42/80.63 17987 [hyper,17863,64,17857] {-} para($c7,$c7,$c4,$c7).
% 80.42/80.63 18247 [hyper,17869,46,7761,8341] {-} midp($c5,$c6,$c5).
% 80.42/80.63 18504 [hyper,17934,64,17847] {-} para($c6,$c5,$c6,$c5).
% 80.42/80.63 18509 [hyper,17934,64,17857] {-} para($c5,$c7,$c5,$c7).
% 80.42/80.63 18740 [hyper,18247,69] {-} cong($c5,$c6,$c5,$c5).
% 80.42/80.63 18741 [hyper,18247,11] {-} midp($c5,$c5,$c6).
% 80.42/80.63 18833 [hyper,18741,128] {-} para($c5,$c5,$c6,$c6).
% 80.42/80.63 18918 [hyper,18741,69] {-} cong($c5,$c5,$c5,$c6).
% 80.42/80.63 18920 [hyper,18741,64,18247] {-} para($c5,$c6,$c6,$c5).
% 80.42/80.63 19084 [hyper,17711,120] {-} cyclic($c6,$c4,$c2,$c2).
% 80.42/80.63 19092 [hyper,17711,17,17670] {-} cyclic($c6,$c4,$c2,$c6).
% 80.42/80.63 19181 [hyper,17721,120] {-} cyclic($c4,$c2,$c6,$c6).
% 80.42/80.63 19186 [hyper,17721,17,17712] {-} cyclic($c4,$c2,$c6,$c2).
% 80.42/80.63 19833 [hyper,17836,53,17842] {-} cong($c4,$c6,$c6,$c6).
% 80.42/80.63 19837 [hyper,17836,9,5912] {-} para($c7,$c8,$c6,$c4).
% 80.42/80.63 19840 [hyper,17836,9,6177] {-} para($c4,$c6,$c8,$c7).
% 80.42/80.63 20454 [hyper,17885,68,2210] {-} midp($c8,$c4,$c6).
% 80.42/80.63 20553 [hyper,20454,46,5968,1903] {-} midp($c6,$c4,$c8).
% 80.42/80.63 20788 [hyper,20553,64,17934] {-} para($c5,$c4,$c5,$c8).
% 80.42/80.63 20808 [hyper,20553,11] {-} midp($c6,$c8,$c4).
% 80.42/80.63 20914 [hyper,20808,46,11291,3528] {-} midp($c7,$c8,$c6).
% 80.42/80.63 27914 [hyper,18509,4] {-} para($c5,$c7,$c7,$c5).
% 80.42/80.63 28697 [hyper,18833,6,17909] {-} para($c5,$c5,$c7,$c7).
% 80.42/80.63 28705 [hyper,18918,25,18740] {-} cong($c5,$c6,$c5,$c6).
% 80.42/80.63 29976 [hyper,19084,15] {-} cyclic($c6,$c2,$c4,$c2).
% 80.42/80.63 29996 [hyper,19092,15] {-} cyclic($c6,$c2,$c4,$c6).
% 80.42/80.63 31539 [hyper,19833,25,17902] {-} cong($c4,$c4,$c6,$c6).
% 80.42/80.63 31627 [hyper,19837,46,20914,291] {-} midp($c8,$c8,$c4).
% 80.42/80.63 31628 [hyper,19837,46,17927,278] {-} midp($c8,$c7,$c4).
% 80.42/80.63 31629 [hyper,19837,46,17850,1431] {-} midp($c8,$c4,$c4).
% 80.42/80.63 31716 [hyper,31627,11] {-} midp($c8,$c4,$c8).
% 80.42/80.63 31719 [hyper,31628,129,17987] {-} midp($c8,$c7,$c7).
% 80.42/80.63 31876 [hyper,31629,64,20454] {-} para($c4,$c4,$c6,$c4).
% 80.42/80.63 31974 [hyper,31716,46,17983,1433] {-} midp($c7,$c4,$c4).
% 80.42/80.63 32259 [hyper,31719,64,20454] {-} para($c4,$c7,$c6,$c7).
% 80.42/80.63 35980 [hyper,7487,44,17708,19186,19181] {-} cong($c4,$c2,$c4,$c2).
% 80.42/80.63 53850 [hyper,28705,68,8164] {-} midp($c5,$c6,$c6).
% 80.42/80.63 53860 [hyper,53850,129,18504] {-} midp($c5,$c5,$c5).
% 80.42/80.63 53863 [hyper,53850,129,6770] {-} midp($c5,$c4,$c4).
% 80.42/80.63 54181 [hyper,53850,46,18920,8286] {-} midp($c6,$c6,$c5).
% 80.42/80.63 54537 [hyper,53860,46,20788,7868] {-} midp($c4,$c5,$c8).
% 80.42/80.63 55572 [hyper,53863,45,31974] {-} para($c7,$c5,$c4,$c4).
% 80.42/80.63 59078 [hyper,54537,46,19840,8184] {-} midp($c6,$c5,$c7).
% 80.42/80.63 65511 [hyper,59078,65,27914,28697] {-} midp($c6,$c7,$c5).
% 80.42/80.63 65515 [hyper,59078,46,10314,8157] {-} midp($c4,$c5,$c6).
% 80.42/80.63 68039 [hyper,65515,65,18920,18833] {-} midp($c4,$c6,$c5).
% 80.42/80.63 73408 [hyper,29996,44,29976,17547,6064] {-} cong($c6,$c2,$c6,$c2).
% 80.42/80.63 76788 [hyper,35980,125] {-} perp($c4,$c4,$c2,$c2).
% 80.42/80.63 76790 [hyper,35980,68,2132] {-} midp($c4,$c2,$c2).
% 80.42/80.63 77203 [hyper,76790,64,68039] {-} para($c6,$c2,$c5,$c2).
% 80.42/80.63 119585 [hyper,17536,75,31539] {-} cong($c2,$c4,$c2,$c6).
% 80.42/80.63 120986 [hyper,73408,68,2130] {-} midp($c6,$c2,$c2).
% 80.42/80.63 122578 [hyper,17549,39] {-} para(A,B,A,B).
% 80.42/80.63 127351 [hyper,76788,10,55572] {-} perp($c7,$c5,$c2,$c2).
% 80.42/80.63 128081 [hyper,77203,46,54181,2131] {-} midp($c2,$c6,$c2).
% 80.42/80.63 128098 [hyper,128081,11] {-} midp($c2,$c2,$c6).
% 80.42/80.63 139197 [hyper,119585,68,217] {-} midp($c2,$c4,$c6).
% 80.42/80.63 139358 [hyper,139197,129,32259] {-} midp($c2,$c7,$c7).
% 80.42/80.63 139362 [hyper,139197,129,31876] {-} midp($c2,$c4,$c4).
% 80.42/80.63 139654 [hyper,139358,45,65511] {-} para($c2,$c6,$c7,$c5).
% 80.42/80.63 141786 [hyper,122578,129,139362] {-} midp($c2,A,A).
% 80.42/80.63 141791 [hyper,122578,129,120986] {-} midp($c6,A,A).
% 80.42/80.63 141793 [hyper,122578,67] {-} coll(A,B,B).
% 80.42/80.63 141796 [hyper,141786,69] {-} cong($c2,A,$c2,A).
% 80.42/80.63 141828 [hyper,141786,64,128098] {-} para($c2,A,$c6,A).
% 80.42/80.63 141941 [hyper,141793,114] {-} coll(A,A,B).
% 80.42/80.63 142871 [hyper,141941,3,141941] {-} coll(A,B,C).
% 80.42/80.63 143714 [hyper,142871,46,141791,122578] {-} midp(A,$c6,A).
% 80.42/80.63 143719 [hyper,142871,46,141786,122578] {-} midp(A,$c2,A).
% 80.42/80.63 145661 [hyper,143714,11] {-} midp(A,A,$c6).
% 80.42/80.63 149727 [hyper,143719,69] {-} cong(A,$c2,A,A).
% 80.42/80.63 151294 [hyper,145661,69] {-} cong(A,A,A,$c6).
% 80.42/80.63 151303 [hyper,145661,64,143719] {-} para(A,$c2,$c6,A).
% 80.42/80.63 163455 [hyper,139654,10,127351] {-} perp($c2,$c6,$c2,$c2).
% 80.42/80.63 166722 [hyper,141796,57,141796] {-} perp($c2,$c2,A,B).
% 80.42/80.63 173321 [hyper,151294,25,149727] {-} cong(A,$c2,A,$c6).
% 80.42/80.63 180614 [hyper,166722,9,163455] {-} para($c2,$c6,A,B).
% 80.42/80.63 186612 [hyper,173321,68,142871] {-} midp(A,$c2,$c6).
% 80.42/80.63 186718 [hyper,186612,129,141828] {-} midp(A,B,B).
% 80.42/80.63 188503 [hyper,186718,46,151303,142871] {-} midp($c2,$c6,A).
% 80.42/80.63 221304 [hyper,188503,11] {-} midp($c2,A,$c6).
% 80.42/80.63 261804 [hyper,180614,46,221304,142871] {-} midp($c6,A,B).
% 80.42/80.63 262129 [hyper,261804,64,261804] {-} para(A,B,C,D).
% 80.42/80.63 283148 [hyper,262129,40] {-} eqangle(A,B,C,D,E,F,C,D).
% 80.42/80.63 291599 [hyper,283148,19] {-} eqangle(A,B,C,D,A,B,E,F).
% 80.42/80.63 292774 [hyper,291599,22,283148] {-} eqangle(A,B,C,D,E,F,G,H).
% 80.42/80.63 292775 [binary,292774.1,113.1] {-} $F.
% 80.42/80.63
% 80.42/80.63 % SZS output end Refutation
% 80.42/80.63 ------------ end of proof -------------
% 80.42/80.63
% 80.42/80.63
% 80.42/80.63 Search stopped by max_proofs option.
% 80.42/80.63
% 80.42/80.63
% 80.42/80.63 Search stopped by max_proofs option.
% 80.42/80.63
% 80.42/80.63 ============ end of search ============
% 80.42/80.63
% 80.42/80.63 That finishes the proof of the theorem.
% 80.42/80.63
% 80.42/80.63 Process 4167 finished Sat Jun 18 13:18:03 2022
%------------------------------------------------------------------------------