Duper---1.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : GEO647+1 : TPTP v9.2.0. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n024.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  : 300s
% DateTime : Fri Oct  3 07:48:48 PM UTC 2025

% Result   : Theorem 101.27s 101.46s
% Output   : Proof 101.80s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : GEO647+1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.13  % Command    : duper %s
% 0.13/0.34  % Computer : n024.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit   : 300
% 0.13/0.34  % WCLimit    : 300
% 0.13/0.34  % DateTime   : Fri Oct  3 12:25:08 EDT 2025
% 0.13/0.34  % CPUTime    : 
% 101.27/101.46  SZS status Theorem for theBenchmark.p
% 101.27/101.46  SZS output start Proof for theBenchmark.p
% 101.27/101.46  Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True
% 101.27/101.46  Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True
% 101.27/101.46  Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True
% 101.27/101.46  Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True
% 101.27/101.46  Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True
% 101.27/101.46  Clause #5 (by assumption #[]): Eq (∀ (A B C D E F : Iota), And (para A B C D) (para C D E F) → para A B E F) True
% 101.27/101.46  Clause #13 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A B D C) True
% 101.27/101.46  Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True
% 101.27/101.46  Clause #15 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic B A C D) True
% 101.27/101.46  Clause #16 (by assumption #[]): Eq (∀ (A B C D E : Iota), And (cyclic A B C D) (cyclic A B C E) → cyclic B C D E) True
% 101.27/101.46  Clause #17 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle B A C D P Q U V) True
% 101.27/101.46  Clause #18 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle C D A B U V P Q) True
% 101.27/101.46  Clause #19 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle P Q U V A B C D) True
% 101.27/101.46  Clause #20 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle A B P Q C D U V) True
% 101.27/101.46  Clause #25 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio B A C D P Q U V) True
% 101.27/101.46  Clause #26 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio C D A B U V P Q) True
% 101.27/101.46  Clause #27 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio P Q U V A B C D) True
% 101.27/101.46  Clause #28 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio A B P Q C D U V) True
% 101.27/101.46  Clause #29 (by assumption #[]): Eq
% 101.27/101.46    (∀ (A B C D E F G H P Q U V : Iota),
% 101.27/101.46      And (eqratio A B C D P Q U V) (eqratio P Q U V E F G H) → eqratio A B C D E F G H)
% 101.27/101.46    True
% 101.27/101.46  Clause #38 (by assumption #[]): Eq (∀ (A B C D P Q : Iota), eqangle A B P Q C D P Q → para A B C D) True
% 101.27/101.46  Clause #39 (by assumption #[]): Eq (∀ (A B C D P Q : Iota), para A B C D → eqangle A B P Q C D P Q) True
% 101.27/101.46  Clause #42 (by assumption #[]): Eq (∀ (A B P Q : Iota), And (eqangle P A P B Q A Q B) (coll P Q B) → cyclic A B P Q) True
% 101.27/101.46  Clause #43 (by assumption #[]): Eq
% 101.27/101.46    (∀ (A B C P Q R : Iota),
% 101.27/101.46      And (And (And (cyclic A B C P) (cyclic A B C Q)) (cyclic A B C R)) (eqangle C A C B R P R Q) → cong A B P Q)
% 101.27/101.46    True
% 101.27/101.46  Clause #44 (by assumption #[]): Eq (∀ (A B C E F : Iota), And (midp E A B) (midp F A C) → para E F B C) True
% 101.27/101.46  Clause #65 (by assumption #[]): Eq (∀ (A B C D O : Iota), And (And (para A B C D) (coll O A C)) (coll O B D) → eqratio O A A C O B B D) True
% 101.27/101.46  Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True
% 101.27/101.46  Clause #67 (by assumption #[]): Eq (∀ (A B C : Iota), And (cong A B A C) (coll A B C) → midp A B C) True
% 101.27/101.46  Clause #75 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), And (eqratio A B C D P Q U V) (cong P Q U V) → cong A B C D) True
% 101.27/101.46  Clause #94 (by assumption #[]): Eq
% 101.27/101.46    (Not
% 101.27/101.46      (∀ (A B C D E F G : Iota),
% 101.27/101.46        And (And (And (And (midp D A C) (midp E B A)) (midp F C B)) (para A F G D)) (para A C G F) → para C E G B))
% 101.27/101.46    True
% 101.27/101.46  Clause #99 (by clausification #[67]): ∀ (a : Iota), Eq (∀ (B C : Iota), And (cong a B a C) (coll a B C) → midp a B C) True
% 101.27/101.46  Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), And (cong a a_1 a C) (coll a a_1 C) → midp a a_1 C) True
% 101.27/101.46  Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), Eq (And (cong a a_1 a a_2) (coll a a_1 a_2) → midp a a_1 a_2) True
% 101.27/101.46  Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (cong a a_1 a a_2) (coll a a_1 a_2)) False) (Eq (midp a a_1 a_2) True)
% 101.27/101.49  Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) True) (Or (Eq (cong a a_1 a a_2) False) (Eq (coll a a_1 a_2) False))
% 101.27/101.49  Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True
% 101.27/101.49  Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True
% 101.27/101.49  Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), Eq (para a a_1 a a_2 → coll a a_1 a_2) True
% 101.27/101.49  Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), Or (Eq (para a a_1 a a_2) False) (Eq (coll a a_1 a_2) True)
% 101.27/101.49  Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True
% 101.27/101.49  Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True
% 101.27/101.49  Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2 → coll a_1 a a_2) True
% 101.27/101.49  Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) False) (Eq (coll a_1 a a_2) True)
% 101.27/101.49  Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True
% 101.27/101.49  Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True
% 101.27/101.49  Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2 → coll a a_2 a_1) True
% 101.27/101.49  Clause #119 (by clausification #[118]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) False) (Eq (coll a a_2 a_1) True)
% 101.27/101.49  Clause #120 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (B C D : Iota), And (coll a B C) (coll a B D) → coll C D a) True
% 101.27/101.49  Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), And (coll a a_1 C) (coll a a_1 D) → coll C D a) True
% 101.27/101.49  Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), And (coll a a_1 a_2) (coll a a_1 D) → coll a_2 D a) True
% 101.27/101.49  Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (coll a a_1 a_2) (coll a a_1 a_3) → coll a_2 a_3 a) True
% 101.27/101.49  Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (coll a a_1 a_2) (coll a a_1 a_3)) False) (Eq (coll a_2 a_3 a) True)
% 101.27/101.49  Clause #125 (by clausification #[124]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (coll a a_1 a_2) True) (Or (Eq (coll a_2 a_3 a) False) (Eq (coll a_2 a_3 a_1) False))
% 101.27/101.49  Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True
% 101.27/101.49  Clause #153 (by clausification #[152]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), para a a_1 C D → para a a_1 D C) True
% 101.27/101.49  Clause #154 (by clausification #[153]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), para a a_1 a_2 D → para a a_1 D a_2) True
% 101.27/101.49  Clause #155 (by clausification #[154]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para a a_1 a_2 a_3 → para a a_1 a_3 a_2) True
% 101.27/101.49  Clause #156 (by clausification #[155]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (para a a_1 a_2 a_3) False) (Eq (para a a_1 a_3 a_2) True)
% 101.27/101.49  Clause #157 (by clausification #[42]): ∀ (a : Iota), Eq (∀ (B P Q : Iota), And (eqangle P a P B Q a Q B) (coll P Q B) → cyclic a B P Q) True
% 101.27/101.49  Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), Eq (∀ (P Q : Iota), And (eqangle P a P a_1 Q a Q a_1) (coll P Q a_1) → cyclic a a_1 P Q) True
% 101.27/101.49  Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Q : Iota), And (eqangle a a_1 a a_2 Q a_1 Q a_2) (coll a Q a_2) → cyclic a_1 a_2 a Q) True
% 101.27/101.49  Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) (coll a a_3 a_2) → cyclic a_1 a_2 a a_3) True
% 101.27/101.49  Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.27/101.49    Or (Eq (And (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) (coll a a_3 a_2)) False) (Eq (cyclic a_1 a_2 a a_3) True)
% 101.27/101.49  Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.27/101.49    Or (Eq (cyclic a a_1 a_2 a_3) True)
% 101.27/101.49      (Or (Eq (eqangle a_2 a a_2 a_1 a_3 a a_3 a_1) False) (Eq (coll a_2 a_3 a_1) False))
% 101.27/101.49  Clause #170 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic B a C D) True
% 101.34/101.52  Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a_1 a C D) True
% 101.34/101.52  Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a_1 a a_2 D) True
% 101.34/101.52  Clause #173 (by clausification #[172]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a_1 a a_2 a_3) True
% 101.34/101.52  Clause #174 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a_1 a a_2 a_3) True)
% 101.34/101.52  Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True
% 101.34/101.52  Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a C a_1 D) True
% 101.34/101.52  Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a a_2 a_1 D) True
% 101.34/101.52  Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a a_2 a_1 a_3) True
% 101.34/101.52  Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a a_2 a_1 a_3) True)
% 101.34/101.52  Clause #180 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a B D C) True
% 101.34/101.52  Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a a_1 D C) True
% 101.34/101.52  Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a a_1 D a_2) True
% 101.34/101.52  Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a a_1 a_3 a_2) True
% 101.34/101.52  Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a a_1 a_3 a_2) True)
% 101.34/101.52  Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True
% 101.34/101.52  Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), para a a_1 C D → para C D a a_1) True
% 101.34/101.52  Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), para a a_1 a_2 D → para a_2 D a a_1) True
% 101.34/101.52  Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para a a_1 a_2 a_3 → para a_2 a_3 a a_1) True
% 101.34/101.52  Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (para a a_1 a_2 a_3) False) (Eq (para a_2 a_3 a a_1) True)
% 101.34/101.52  Clause #220 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (B C D E F : Iota), And (para a B C D) (para C D E F) → para a B E F) True
% 101.34/101.52  Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), Eq (∀ (C D E F : Iota), And (para a a_1 C D) (para C D E F) → para a a_1 E F) True
% 101.34/101.52  Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E F : Iota), And (para a a_1 a_2 D) (para a_2 D E F) → para a a_1 E F) True
% 101.34/101.52  Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E F : Iota), And (para a a_1 a_2 a_3) (para a_2 a_3 E F) → para a a_1 E F) True
% 101.34/101.52  Clause #224 (by clausification #[223]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (F : Iota), And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 F) → para a a_1 a_4 F) True
% 101.34/101.52  Clause #225 (by clausification #[224]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 a_5) → para a a_1 a_4 a_5) True
% 101.34/101.52  Clause #226 (by clausification #[225]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.52    Or (Eq (And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 a_5)) False) (Eq (para a a_1 a_4 a_5) True)
% 101.34/101.52  Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.52    Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (para a a_1 a_4 a_5) False) (Eq (para a_4 a_5 a_2 a_3) False))
% 101.34/101.52  Clause #284 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (B C D E : Iota), And (cyclic a B C D) (cyclic a B C E) → cyclic B C D E) True
% 101.34/101.52  Clause #285 (by clausification #[284]): ∀ (a a_1 : Iota), Eq (∀ (C D E : Iota), And (cyclic a a_1 C D) (cyclic a a_1 C E) → cyclic a_1 C D E) True
% 101.34/101.52  Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E : Iota), And (cyclic a a_1 a_2 D) (cyclic a a_1 a_2 E) → cyclic a_1 a_2 D E) True
% 101.34/101.54  Clause #287 (by clausification #[286]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E : Iota), And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 E) → cyclic a_1 a_2 a_3 E) True
% 101.34/101.54  Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4) → cyclic a_1 a_2 a_3 a_4) True
% 101.34/101.54  Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.54    Or (Eq (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) False) (Eq (cyclic a_1 a_2 a_3 a_4) True)
% 101.34/101.54  Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.54    Or (Eq (cyclic a a_1 a_2 a_3) True) (Or (Eq (cyclic a_4 a a_1 a_2) False) (Eq (cyclic a_4 a a_1 a_3) False))
% 101.34/101.54  Clause #291 (by clausification #[44]): ∀ (a : Iota), Eq (∀ (B C E F : Iota), And (midp E a B) (midp F a C) → para E F B C) True
% 101.34/101.54  Clause #292 (by clausification #[291]): ∀ (a a_1 : Iota), Eq (∀ (C E F : Iota), And (midp E a a_1) (midp F a C) → para E F a_1 C) True
% 101.34/101.54  Clause #293 (by clausification #[292]): ∀ (a a_1 a_2 : Iota), Eq (∀ (E F : Iota), And (midp E a a_1) (midp F a a_2) → para E F a_1 a_2) True
% 101.34/101.54  Clause #294 (by clausification #[293]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (F : Iota), And (midp a a_1 a_2) (midp F a_1 a_3) → para a F a_2 a_3) True
% 101.34/101.54  Clause #295 (by clausification #[294]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (And (midp a a_1 a_2) (midp a_3 a_1 a_4) → para a a_3 a_2 a_4) True
% 101.34/101.54  Clause #296 (by clausification #[295]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (And (midp a a_1 a_2) (midp a_3 a_1 a_4)) False) (Eq (para a a_3 a_2 a_4) True)
% 101.34/101.54  Clause #297 (by clausification #[296]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.54    Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (midp a a_4 a_2) False) (Eq (midp a_1 a_4 a_3) False))
% 101.34/101.54  Clause #344 (by clausification #[17]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle B a C D P Q U V) True
% 101.34/101.54  Clause #345 (by clausification #[344]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle a_1 a C D P Q U V) True
% 101.34/101.54  Clause #346 (by clausification #[345]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a_1 a a_2 D P Q U V) True
% 101.34/101.54  Clause #347 (by clausification #[346]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a_1 a a_2 a_3 P Q U V) True
% 101.34/101.54  Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.54    Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a_1 a a_2 a_3 a_4 Q U V) True
% 101.34/101.54  Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.54    Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a_1 a a_2 a_3 a_4 a_5 U V) True
% 101.34/101.54  Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.34/101.54    Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_1 a a_2 a_3 a_4 a_5 a_6 V) True
% 101.34/101.54  Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.34/101.54    Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True
% 101.34/101.54  Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.34/101.54    Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True)
% 101.34/101.54  Clause #353 (by clausification #[38]): ∀ (a : Iota), Eq (∀ (B C D P Q : Iota), eqangle a B P Q C D P Q → para a B C D) True
% 101.34/101.54  Clause #354 (by clausification #[353]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q : Iota), eqangle a a_1 P Q C D P Q → para a a_1 C D) True
% 101.34/101.54  Clause #355 (by clausification #[354]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q : Iota), eqangle a a_1 P Q a_2 D P Q → para a a_1 a_2 D) True
% 101.34/101.54  Clause #356 (by clausification #[355]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q : Iota), eqangle a a_1 P Q a_2 a_3 P Q → para a a_1 a_2 a_3) True
% 101.34/101.54  Clause #357 (by clausification #[356]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (Q : Iota), eqangle a a_1 a_2 Q a_3 a_4 a_2 Q → para a a_1 a_3 a_4) True
% 101.34/101.54  Clause #358 (by clausification #[357]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_2 a_3 → para a a_1 a_4 a_5) True
% 101.34/101.56  Clause #359 (by clausification #[358]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_2 a_3) False) (Eq (para a a_1 a_4 a_5) True)
% 101.34/101.56  Clause #360 (by clausification #[43]): ∀ (a : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (∀ (B C P Q R : Iota),
% 101.34/101.56        And (And (And (cyclic a B C P) (cyclic a B C Q)) (cyclic a B C R)) (eqangle C a C B R P R Q) → cong a B P Q)
% 101.34/101.56      True
% 101.34/101.56  Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (∀ (C P Q R : Iota),
% 101.34/101.56        And (And (And (cyclic a a_1 C P) (cyclic a a_1 C Q)) (cyclic a a_1 C R)) (eqangle C a C a_1 R P R Q) →
% 101.34/101.56          cong a a_1 P Q)
% 101.34/101.56      True
% 101.34/101.56  Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (∀ (P Q R : Iota),
% 101.34/101.56        And (And (And (cyclic a a_1 a_2 P) (cyclic a a_1 a_2 Q)) (cyclic a a_1 a_2 R)) (eqangle a_2 a a_2 a_1 R P R Q) →
% 101.34/101.56          cong a a_1 P Q)
% 101.34/101.56      True
% 101.34/101.56  Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (∀ (Q R : Iota),
% 101.34/101.56        And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 Q)) (cyclic a a_1 a_2 R))
% 101.34/101.56            (eqangle a_2 a a_2 a_1 R a_3 R Q) →
% 101.34/101.56          cong a a_1 a_3 Q)
% 101.34/101.56      True
% 101.34/101.56  Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (∀ (R : Iota),
% 101.34/101.56        And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 R))
% 101.34/101.56            (eqangle a_2 a a_2 a_1 R a_3 R a_4) →
% 101.34/101.56          cong a a_1 a_3 a_4)
% 101.34/101.56      True
% 101.34/101.56  Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.56    Eq
% 101.34/101.56      (And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 a_5))
% 101.34/101.56          (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4) →
% 101.34/101.56        cong a a_1 a_3 a_4)
% 101.34/101.56      True
% 101.34/101.56  Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.56    Or
% 101.34/101.56      (Eq
% 101.34/101.56        (And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 a_5))
% 101.34/101.56          (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4))
% 101.34/101.56        False)
% 101.34/101.56      (Eq (cong a a_1 a_3 a_4) True)
% 101.34/101.57  Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.57    Or (Eq (cong a a_1 a_2 a_3) True)
% 101.34/101.57      (Or (Eq (And (And (cyclic a a_1 a_4 a_2) (cyclic a a_1 a_4 a_3)) (cyclic a a_1 a_4 a_5)) False)
% 101.34/101.57        (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False))
% 101.34/101.57  Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.57    Or (Eq (cong a a_1 a_2 a_3) True)
% 101.34/101.57      (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)
% 101.34/101.57        (Or (Eq (And (cyclic a a_1 a_4 a_2) (cyclic a a_1 a_4 a_3)) False) (Eq (cyclic a a_1 a_4 a_5) False)))
% 101.34/101.57  Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.57    Or (Eq (cong a a_1 a_2 a_3) True)
% 101.34/101.57      (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)
% 101.34/101.57        (Or (Eq (cyclic a a_1 a_4 a_5) False) (Or (Eq (cyclic a a_1 a_4 a_2) False) (Eq (cyclic a a_1 a_4 a_3) False))))
% 101.34/101.57  Clause #389 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle C D a B U V P Q) True
% 101.34/101.57  Clause #390 (by clausification #[389]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle C D a a_1 U V P Q) True
% 101.34/101.57  Clause #391 (by clausification #[390]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a_2 D a a_1 U V P Q) True
% 101.34/101.57  Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a_2 a_3 a a_1 U V P Q) True
% 101.34/101.57  Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.34/101.57    Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a_2 a_3 a a_1 U V a_4 Q) True
% 101.34/101.57  Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.34/101.57    Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a_2 a_3 a a_1 U V a_4 a_5) True
% 101.34/101.57  Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.34/101.57    Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_2 a_3 a a_1 a_6 V a_4 a_5) True
% 101.34/101.57  Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.59    Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True
% 101.41/101.59  Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.59    Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True)
% 101.41/101.59  Clause #433 (by clausification #[19]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle P Q U V a B C D) True
% 101.41/101.59  Clause #434 (by clausification #[433]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle P Q U V a a_1 C D) True
% 101.41/101.59  Clause #435 (by clausification #[434]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle P Q U V a a_1 a_2 D) True
% 101.41/101.59  Clause #436 (by clausification #[435]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle P Q U V a a_1 a_2 a_3) True
% 101.41/101.59  Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.59    Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a_4 Q U V a a_1 a_2 a_3) True
% 101.41/101.59  Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.41/101.59    Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a_4 a_5 U V a a_1 a_2 a_3) True
% 101.41/101.59  Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.59    Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_4 a_5 a_6 V a a_1 a_2 a_3) True
% 101.41/101.59  Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.59    Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True
% 101.41/101.59  Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.59    Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True)
% 101.41/101.59  Clause #458 (by clausification #[94]): Eq
% 101.41/101.59    (∀ (A B C D E F G : Iota),
% 101.41/101.59      And (And (And (And (midp D A C) (midp E B A)) (midp F C B)) (para A F G D)) (para A C G F) → para C E G B)
% 101.41/101.59    False
% 101.41/101.59  Clause #459 (by clausification #[458]): ∀ (a : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (Not
% 101.41/101.59        (∀ (B C D E F G : Iota),
% 101.41/101.59          And (And (And (And (midp D (skS.0 4 a) C) (midp E B (skS.0 4 a))) (midp F C B)) (para (skS.0 4 a) F G D))
% 101.41/101.59              (para (skS.0 4 a) C G F) →
% 101.41/101.59            para C E G B))
% 101.41/101.59      True
% 101.41/101.59  Clause #460 (by clausification #[459]): ∀ (a : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (∀ (B C D E F G : Iota),
% 101.41/101.59        And (And (And (And (midp D (skS.0 4 a) C) (midp E B (skS.0 4 a))) (midp F C B)) (para (skS.0 4 a) F G D))
% 101.41/101.59            (para (skS.0 4 a) C G F) →
% 101.41/101.59          para C E G B)
% 101.41/101.59      False
% 101.41/101.59  Clause #461 (by clausification #[460]): ∀ (a a_1 : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (Not
% 101.41/101.59        (∀ (C D E F G : Iota),
% 101.41/101.59          And
% 101.41/101.59              (And (And (And (midp D (skS.0 4 a) C) (midp E (skS.0 5 a a_1) (skS.0 4 a))) (midp F C (skS.0 5 a a_1)))
% 101.41/101.59                (para (skS.0 4 a) F G D))
% 101.41/101.59              (para (skS.0 4 a) C G F) →
% 101.41/101.59            para C E G (skS.0 5 a a_1)))
% 101.41/101.59      True
% 101.41/101.59  Clause #462 (by clausification #[461]): ∀ (a a_1 : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (∀ (C D E F G : Iota),
% 101.41/101.59        And
% 101.41/101.59            (And (And (And (midp D (skS.0 4 a) C) (midp E (skS.0 5 a a_1) (skS.0 4 a))) (midp F C (skS.0 5 a a_1)))
% 101.41/101.59              (para (skS.0 4 a) F G D))
% 101.41/101.59            (para (skS.0 4 a) C G F) →
% 101.41/101.59          para C E G (skS.0 5 a a_1))
% 101.41/101.59      False
% 101.41/101.59  Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (Not
% 101.41/101.59        (∀ (D E F G : Iota),
% 101.41/101.59          And
% 101.41/101.59              (And
% 101.41/101.59                (And (And (midp D (skS.0 4 a) (skS.0 6 a a_1 a_2)) (midp E (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.59                  (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.59                (para (skS.0 4 a) F G D))
% 101.41/101.59              (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.59            para (skS.0 6 a a_1 a_2) E G (skS.0 5 a a_1)))
% 101.41/101.59      True
% 101.41/101.59  Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 : Iota),
% 101.41/101.59    Eq
% 101.41/101.59      (∀ (D E F G : Iota),
% 101.41/101.59        And
% 101.41/101.59            (And
% 101.41/101.59              (And (And (midp D (skS.0 4 a) (skS.0 6 a a_1 a_2)) (midp E (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.59                (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.59              (para (skS.0 4 a) F G D))
% 101.41/101.59            (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.62          para (skS.0 6 a a_1 a_2) E G (skS.0 5 a a_1))
% 101.41/101.62      False
% 101.41/101.62  Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (Not
% 101.41/101.62        (∀ (E F G : Iota),
% 101.41/101.62          And
% 101.41/101.62              (And
% 101.41/101.62                (And
% 101.41/101.62                  (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                    (midp E (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                  (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62                (para (skS.0 4 a) F G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62              (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.62            para (skS.0 6 a a_1 a_2) E G (skS.0 5 a a_1)))
% 101.41/101.62      True
% 101.41/101.62  Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (∀ (E F G : Iota),
% 101.41/101.62        And
% 101.41/101.62            (And
% 101.41/101.62              (And
% 101.41/101.62                (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2)) (midp E (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62              (para (skS.0 4 a) F G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62            (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.62          para (skS.0 6 a a_1 a_2) E G (skS.0 5 a a_1))
% 101.41/101.62      False
% 101.41/101.62  Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (Not
% 101.41/101.62        (∀ (F G : Iota),
% 101.41/101.62          And
% 101.41/101.62              (And
% 101.41/101.62                (And
% 101.41/101.62                  (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                    (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                  (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62                (para (skS.0 4 a) F G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62              (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.62            para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) G (skS.0 5 a a_1)))
% 101.41/101.62      True
% 101.41/101.62  Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (∀ (F G : Iota),
% 101.41/101.62        And
% 101.41/101.62            (And
% 101.41/101.62              (And
% 101.41/101.62                (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                  (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62              (para (skS.0 4 a) F G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62            (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G F) →
% 101.41/101.62          para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) G (skS.0 5 a a_1))
% 101.41/101.62      False
% 101.41/101.62  Clause #469 (by clausification #[468]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (Not
% 101.41/101.62        (∀ (G : Iota),
% 101.41/101.62          And
% 101.41/101.62              (And
% 101.41/101.62                (And
% 101.41/101.62                  (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                    (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                  (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62                (para (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62              (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) →
% 101.41/101.62            para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) G (skS.0 5 a a_1)))
% 101.41/101.62      True
% 101.41/101.62  Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (∀ (G : Iota),
% 101.41/101.62        And
% 101.41/101.62            (And
% 101.41/101.62              (And
% 101.41/101.62                (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                  (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62              (para (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) G (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.62            (para (skS.0 4 a) (skS.0 6 a a_1 a_2) G (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) →
% 101.41/101.62          para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) G (skS.0 5 a a_1))
% 101.41/101.62      False
% 101.41/101.62  Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.62    Eq
% 101.41/101.62      (Not
% 101.41/101.62        (And
% 101.41/101.62            (And
% 101.41/101.62              (And
% 101.41/101.62                (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.62                  (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.62                (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.62              (para (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)
% 101.41/101.64                (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.64            (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) →
% 101.41/101.64          para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1)))
% 101.41/101.64      True
% 101.41/101.64  Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Eq
% 101.41/101.64      (And
% 101.41/101.64          (And
% 101.41/101.64            (And
% 101.41/101.64              (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.64                (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.64              (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.64            (para (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)
% 101.41/101.64              (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.64          (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) →
% 101.41/101.64        para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1))
% 101.41/101.64      False
% 101.41/101.64  Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Eq
% 101.41/101.64      (And
% 101.41/101.64        (And
% 101.41/101.64          (And
% 101.41/101.64            (And (midp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.64              (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)))
% 101.41/101.64            (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)))
% 101.41/101.64          (para (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3)))
% 101.41/101.64        (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)))
% 101.41/101.64      True
% 101.41/101.64  Clause #474 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Eq (para (skS.0 6 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1)) False
% 101.41/101.64  Clause #475 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) True
% 101.41/101.64  Clause #479 (by superposition #[475, 189]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Or (Eq True False)
% 101.41/101.64      (Eq (para (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a) (skS.0 6 a a_1 a_2))
% 101.41/101.64        True)
% 101.41/101.64  Clause #480 (by superposition #[475, 227]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 101.41/101.64    Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True)
% 101.41/101.64      (Or (Eq True False) (Eq (para (skS.0 10 a a_1 a_2 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False))
% 101.41/101.64  Clause #482 (by clausification #[75]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), And (eqratio a B C D P Q U V) (cong P Q U V) → cong a B C D) True
% 101.41/101.64  Clause #483 (by clausification #[482]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), And (eqratio a a_1 C D P Q U V) (cong P Q U V) → cong a a_1 C D) True
% 101.41/101.64  Clause #484 (by clausification #[483]): ∀ (a a_1 a_2 : Iota),
% 101.41/101.64    Eq (∀ (D P Q U V : Iota), And (eqratio a a_1 a_2 D P Q U V) (cong P Q U V) → cong a a_1 a_2 D) True
% 101.41/101.64  Clause #485 (by clausification #[484]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.41/101.64    Eq (∀ (P Q U V : Iota), And (eqratio a a_1 a_2 a_3 P Q U V) (cong P Q U V) → cong a a_1 a_2 a_3) True
% 101.41/101.64  Clause #486 (by clausification #[485]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.64    Eq (∀ (Q U V : Iota), And (eqratio a a_1 a_2 a_3 a_4 Q U V) (cong a_4 Q U V) → cong a a_1 a_2 a_3) True
% 101.41/101.64  Clause #487 (by clausification #[486]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.41/101.64    Eq (∀ (U V : Iota), And (eqratio a a_1 a_2 a_3 a_4 a_5 U V) (cong a_4 a_5 U V) → cong a a_1 a_2 a_3) True
% 101.41/101.64  Clause #488 (by clausification #[487]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.64    Eq (∀ (V : Iota), And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V) (cong a_4 a_5 a_6 V) → cong a a_1 a_2 a_3) True
% 101.41/101.64  Clause #489 (by clausification #[488]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.64    Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (cong a_4 a_5 a_6 a_7) → cong a a_1 a_2 a_3) True
% 101.41/101.64  Clause #490 (by clausification #[489]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.67    Or (Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (cong a_4 a_5 a_6 a_7)) False) (Eq (cong a a_1 a_2 a_3) True)
% 101.41/101.67  Clause #491 (by clausification #[490]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.67    Or (Eq (cong a a_1 a_2 a_3) True)
% 101.41/101.67      (Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (cong a_4 a_5 a_6 a_7) False))
% 101.41/101.67  Clause #502 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle a B P Q C D U V) True
% 101.41/101.67  Clause #503 (by clausification #[502]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle a a_1 P Q C D U V) True
% 101.41/101.67  Clause #504 (by clausification #[503]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a a_1 P Q a_2 D U V) True
% 101.41/101.67  Clause #505 (by clausification #[504]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a a_1 P Q a_2 a_3 U V) True
% 101.41/101.67  Clause #506 (by clausification #[505]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.67    Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a a_1 a_4 Q a_2 a_3 U V) True
% 101.41/101.67  Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.41/101.67    Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a a_1 a_4 a_5 a_2 a_3 U V) True
% 101.41/101.67  Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.41/101.67    Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a a_1 a_4 a_5 a_2 a_3 a_6 V) True
% 101.41/101.67  Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.67    Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True
% 101.41/101.67  Clause #510 (by clausification #[509]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.41/101.67    Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True)
% 101.41/101.67  Clause #583 (by clausification #[65]): ∀ (a : Iota), Eq (∀ (B C D O : Iota), And (And (para a B C D) (coll O a C)) (coll O B D) → eqratio O a a C O B B D) True
% 101.41/101.67  Clause #584 (by clausification #[583]): ∀ (a a_1 : Iota),
% 101.41/101.67    Eq (∀ (C D O : Iota), And (And (para a a_1 C D) (coll O a C)) (coll O a_1 D) → eqratio O a a C O a_1 a_1 D) True
% 101.41/101.67  Clause #585 (by clausification #[584]): ∀ (a a_1 a_2 : Iota),
% 101.41/101.67    Eq (∀ (D O : Iota), And (And (para a a_1 a_2 D) (coll O a a_2)) (coll O a_1 D) → eqratio O a a a_2 O a_1 a_1 D) True
% 101.41/101.67  Clause #586 (by clausification #[585]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.41/101.67    Eq (∀ (O : Iota), And (And (para a a_1 a_2 a_3) (coll O a a_2)) (coll O a_1 a_3) → eqratio O a a a_2 O a_1 a_1 a_3)
% 101.41/101.67      True
% 101.41/101.67  Clause #587 (by clausification #[586]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.67    Eq (And (And (para a a_1 a_2 a_3) (coll a_4 a a_2)) (coll a_4 a_1 a_3) → eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True
% 101.41/101.67  Clause #588 (by clausification #[587]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.67    Or (Eq (And (And (para a a_1 a_2 a_3) (coll a_4 a a_2)) (coll a_4 a_1 a_3)) False)
% 101.41/101.67      (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True)
% 101.41/101.67  Clause #589 (by clausification #[588]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.67    Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True)
% 101.41/101.67      (Or (Eq (And (para a_1 a_3 a_2 a_4) (coll a a_1 a_2)) False) (Eq (coll a a_3 a_4) False))
% 101.41/101.67  Clause #590 (by clausification #[589]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.41/101.67    Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True)
% 101.41/101.67      (Or (Eq (coll a a_3 a_4) False) (Or (Eq (para a_1 a_3 a_2 a_4) False) (Eq (coll a a_1 a_2) False)))
% 101.41/101.67  Clause #605 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio B a C D P Q U V) True
% 101.41/101.67  Clause #606 (by clausification #[605]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio a_1 a C D P Q U V) True
% 101.41/101.67  Clause #607 (by clausification #[606]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a_1 a a_2 D P Q U V) True
% 101.41/101.67  Clause #608 (by clausification #[607]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a_1 a a_2 a_3 P Q U V) True
% 101.41/101.67  Clause #609 (by clausification #[608]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.51/101.69    Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_1 a a_2 a_3 a_4 Q U V) True
% 101.51/101.69  Clause #610 (by clausification #[609]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.51/101.69    Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_1 a a_2 a_3 a_4 a_5 U V) True
% 101.51/101.69  Clause #611 (by clausification #[610]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.51/101.69    Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_1 a a_2 a_3 a_4 a_5 a_6 V) True
% 101.51/101.69  Clause #612 (by clausification #[611]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.51/101.69    Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True
% 101.51/101.69  Clause #613 (by clausification #[612]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.51/101.69    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True)
% 101.51/101.69  Clause #621 (by clausification #[39]): ∀ (a : Iota), Eq (∀ (B C D P Q : Iota), para a B C D → eqangle a B P Q C D P Q) True
% 101.51/101.69  Clause #622 (by clausification #[621]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q : Iota), para a a_1 C D → eqangle a a_1 P Q C D P Q) True
% 101.51/101.69  Clause #623 (by clausification #[622]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q : Iota), para a a_1 a_2 D → eqangle a a_1 P Q a_2 D P Q) True
% 101.51/101.69  Clause #624 (by clausification #[623]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q : Iota), para a a_1 a_2 a_3 → eqangle a a_1 P Q a_2 a_3 P Q) True
% 101.51/101.69  Clause #625 (by clausification #[624]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (Q : Iota), para a a_1 a_2 a_3 → eqangle a a_1 a_4 Q a_2 a_3 a_4 Q) True
% 101.51/101.69  Clause #626 (by clausification #[625]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (para a a_1 a_2 a_3 → eqangle a a_1 a_4 a_5 a_2 a_3 a_4 a_5) True
% 101.51/101.69  Clause #627 (by clausification #[626]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (para a a_1 a_2 a_3) False) (Eq (eqangle a a_1 a_4 a_5 a_2 a_3 a_4 a_5) True)
% 101.51/101.69  Clause #655 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio C D a B U V P Q) True
% 101.51/101.69  Clause #656 (by clausification #[655]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio C D a a_1 U V P Q) True
% 101.51/101.69  Clause #657 (by clausification #[656]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a_2 D a a_1 U V P Q) True
% 101.51/101.69  Clause #658 (by clausification #[657]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a_2 a_3 a a_1 U V P Q) True
% 101.51/101.69  Clause #659 (by clausification #[658]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.51/101.69    Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_2 a_3 a a_1 U V a_4 Q) True
% 101.51/101.69  Clause #660 (by clausification #[659]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.51/101.69    Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_2 a_3 a a_1 U V a_4 a_5) True
% 101.51/101.69  Clause #661 (by clausification #[660]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.51/101.69    Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_2 a_3 a a_1 a_6 V a_4 a_5) True
% 101.51/101.69  Clause #662 (by clausification #[661]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.51/101.69    Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True
% 101.51/101.69  Clause #663 (by clausification #[662]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.51/101.69    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True)
% 101.51/101.69  Clause #711 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio P Q U V a B C D) True
% 101.51/101.69  Clause #712 (by clausification #[711]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio P Q U V a a_1 C D) True
% 101.51/101.69  Clause #713 (by clausification #[712]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio P Q U V a a_1 a_2 D) True
% 101.51/101.69  Clause #714 (by clausification #[713]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio P Q U V a a_1 a_2 a_3) True
% 101.51/101.69  Clause #715 (by clausification #[714]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.54/101.72    Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_4 Q U V a a_1 a_2 a_3) True
% 101.54/101.72  Clause #716 (by clausification #[715]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.54/101.72    Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_4 a_5 U V a a_1 a_2 a_3) True
% 101.54/101.72  Clause #717 (by clausification #[716]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.54/101.72    Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_4 a_5 a_6 V a a_1 a_2 a_3) True
% 101.54/101.72  Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.54/101.72    Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True
% 101.54/101.72  Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.54/101.72    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True)
% 101.54/101.72  Clause #728 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio a B P Q C D U V) True
% 101.54/101.72  Clause #729 (by clausification #[728]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio a a_1 P Q C D U V) True
% 101.54/101.72  Clause #730 (by clausification #[729]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a a_1 P Q a_2 D U V) True
% 101.54/101.72  Clause #731 (by clausification #[730]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a a_1 P Q a_2 a_3 U V) True
% 101.54/101.72  Clause #732 (by clausification #[731]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.54/101.72    Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a a_1 a_4 Q a_2 a_3 U V) True
% 101.54/101.72  Clause #733 (by clausification #[732]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.54/101.72    Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a a_1 a_4 a_5 a_2 a_3 U V) True
% 101.54/101.72  Clause #734 (by clausification #[733]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.54/101.72    Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a a_1 a_4 a_5 a_2 a_3 a_6 V) True
% 101.54/101.72  Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.54/101.72    Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True
% 101.54/101.72  Clause #736 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.54/101.72    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True)
% 101.54/101.72  Clause #774 (by clausification #[29]): ∀ (a : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (B C D E F G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a B C D P Q U V) (eqratio P Q U V E F G H) → eqratio a B C D E F G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #775 (by clausification #[774]): ∀ (a a_1 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (C D E F G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 C D P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 C D E F G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #776 (by clausification #[775]): ∀ (a a_1 a_2 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (D E F G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 D P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 a_2 D E F G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #777 (by clausification #[776]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (E F G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 a_2 a_3 E F G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #778 (by clausification #[777]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (F G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 F G H) → eqratio a a_1 a_2 a_3 a_4 F G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #779 (by clausification #[778]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (G H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 G H) → eqratio a a_1 a_2 a_3 a_4 a_5 G H)
% 101.54/101.72      True
% 101.54/101.72  Clause #780 (by clausification #[779]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (H P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 H) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 H)
% 101.54/101.72      True
% 101.54/101.72  Clause #781 (by clausification #[780]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.54/101.72    Eq
% 101.54/101.72      (∀ (P Q U V : Iota),
% 101.54/101.72        And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 a_7) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 101.58/101.74      True
% 101.58/101.74  Clause #782 (by clausification #[781]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 101.58/101.74    Eq
% 101.58/101.74      (∀ (Q U V : Iota),
% 101.58/101.74        And (eqratio a a_1 a_2 a_3 a_4 Q U V) (eqratio a_4 Q U V a_5 a_6 a_7 a_8) → eqratio a a_1 a_2 a_3 a_5 a_6 a_7 a_8)
% 101.58/101.74      True
% 101.58/101.74  Clause #783 (by clausification #[782]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 101.58/101.74    Eq
% 101.58/101.74      (∀ (U V : Iota),
% 101.58/101.74        And (eqratio a a_1 a_2 a_3 a_4 a_5 U V) (eqratio a_4 a_5 U V a_6 a_7 a_8 a_9) →
% 101.58/101.74          eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9)
% 101.58/101.74      True
% 101.58/101.74  Clause #784 (by clausification #[783]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 101.58/101.74    Eq
% 101.58/101.74      (∀ (V : Iota),
% 101.58/101.74        And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V) (eqratio a_4 a_5 a_6 V a_7 a_8 a_9 a_10) →
% 101.58/101.74          eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10)
% 101.58/101.74      True
% 101.58/101.74  Clause #785 (by clausification #[784]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 101.58/101.74    Eq
% 101.58/101.74      (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqratio a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) →
% 101.58/101.74        eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11)
% 101.58/101.74      True
% 101.58/101.74  Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 101.58/101.74    Or (Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqratio a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) False)
% 101.58/101.74      (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True)
% 101.58/101.74  Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 101.58/101.74    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True)
% 101.58/101.74      (Or (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) False) (Eq (eqratio a_8 a_9 a_10 a_11 a_4 a_5 a_6 a_7) False))
% 101.58/101.74  Clause #849 (by clausification #[479]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.58/101.74    Eq (para (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True
% 101.58/101.74  Clause #851 (by superposition #[849, 156]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.58/101.74    Or (Eq True False)
% 101.58/101.74      (Eq (para (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 4 a))
% 101.58/101.74        True)
% 101.58/101.74  Clause #856 (by clausification #[851]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.58/101.74    Eq (para (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True
% 101.58/101.74  Clause #904 (by clausification #[480]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 101.58/101.74    Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True)
% 101.58/101.74      (Eq (para (skS.0 10 a a_1 a_2 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False)
% 101.58/101.74  Clause #906 (by superposition #[904, 856]): ∀ (a a_1 a_2 : Iota),
% 101.58/101.74    Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) (Eq False True)
% 101.58/101.74  Clause #907 (by clausification #[906]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True
% 101.58/101.74  Clause #913 (by superposition #[907, 627]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4) True)
% 101.58/101.74  Clause #1050 (by clausification #[913]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4) True
% 101.58/101.74  Clause #1052 (by superposition #[1050, 510]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_3 a_4) True)
% 101.58/101.74  Clause #1054 (by clausification #[1052]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_3 a_4) True
% 101.58/101.74  Clause #1057 (by superposition #[1054, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Or (Eq True False)
% 101.58/101.74      (Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True)
% 101.58/101.74  Clause #1063 (by clausification #[1057]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True
% 101.58/101.74  Clause #1065 (by superposition #[1063, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.74    Or (Eq True False)
% 101.58/101.74      (Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True)
% 101.58/101.77  Clause #1070 (by clausification #[1065]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True
% 101.58/101.77  Clause #1073 (by superposition #[1070, 510]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False)
% 101.58/101.77      (Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True)
% 101.58/101.77  Clause #1077 (by clausification #[1073]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True
% 101.58/101.77  Clause #1078 (by superposition #[1077, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False)
% 101.58/101.77      (Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True)
% 101.58/101.77  Clause #1082 (by clausification #[1078]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True
% 101.58/101.77  Clause #1086 (by superposition #[1082, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False)
% 101.58/101.77      (Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True)
% 101.58/101.77  Clause #1091 (by clausification #[1086]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True
% 101.58/101.77  Clause #1094 (by superposition #[1091, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_4 a_3) True)
% 101.58/101.77  Clause #1104 (by clausification #[1094]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_4 a_3) True
% 101.58/101.77  Clause #1107 (by superposition #[1104, 510]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_4 a_3) True)
% 101.58/101.77  Clause #1110 (by clausification #[1107]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_4 a_3) True
% 101.58/101.77  Clause #1112 (by superposition #[1110, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False) (Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True)
% 101.58/101.77  Clause #1117 (by clausification #[1112]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True
% 101.58/101.77  Clause #1118 (by superposition #[1117, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True)
% 101.58/101.77  Clause #1123 (by clausification #[1118]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True
% 101.58/101.77  Clause #1130 (by superposition #[1123, 510]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 4 a) (skS.0 6 a a_1 a_2) a_4 a_3) True)
% 101.58/101.77  Clause #1135 (by clausification #[1130]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 4 a) (skS.0 6 a a_1 a_2) a_4 a_3) True
% 101.58/101.77  Clause #1140 (by superposition #[1135, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Or (Eq True False)
% 101.58/101.77      (Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True)
% 101.58/101.77  Clause #1148 (by clausification #[1140]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 101.58/101.77    Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True
% 101.58/101.77  Clause #1153 (by superposition #[1148, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True)
% 101.58/101.77  Clause #1161 (by clausification #[1153]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True
% 101.58/101.77  Clause #1164 (by superposition #[1161, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True)
% 101.58/101.77  Clause #1180 (by clausification #[1164]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True
% 101.58/101.77  Clause #1181 (by superposition #[1180, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True)
% 101.58/101.80  Clause #1185 (by superposition #[1180, 627]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True)
% 101.58/101.80  Clause #1188 (by clausification #[1181]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True
% 101.58/101.80  Clause #1190 (by superposition #[1188, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True)
% 101.58/101.80  Clause #1194 (by superposition #[1188, 590]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.58/101.80    Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_3) True)
% 101.58/101.80      (Or (Eq True False) (Or (Eq (para a_1 a_3 a_2 a_3) False) (Eq (coll a a_1 a_2) False)))
% 101.58/101.80  Clause #1204 (by clausification #[1190]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True
% 101.58/101.80  Clause #1206 (by superposition #[1204, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True)
% 101.58/101.80  Clause #1215 (by clausification #[1206]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True
% 101.58/101.80  Clause #1217 (by superposition #[1215, 125]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Or (Eq True False) (Eq (coll a_2 a_2 a_1) False))
% 101.58/101.80  Clause #1225 (by clausification #[1185]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True
% 101.58/101.80  Clause #1227 (by superposition #[1225, 162]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Or (Eq True False) (Eq (coll a_2 a_2 a_1) False))
% 101.58/101.80  Clause #1232 (by superposition #[1225, 510]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_1 a_2 a_3 a_2 a_3) True)
% 101.58/101.80  Clause #1237 (by clausification #[1232]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_2 a_3 a_2 a_3) True
% 101.58/101.80  Clause #1241 (by superposition #[1237, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_1 a a_2 a_3 a_2 a_3) True)
% 101.58/101.80  Clause #1249 (by clausification #[1241]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a a_2 a_3 a_2 a_3) True
% 101.58/101.80  Clause #1255 (by superposition #[1249, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_1 a_2 a_3 a_3 a_2) True)
% 101.58/101.80  Clause #1263 (by clausification #[1255]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_2 a_3 a_3 a_2) True
% 101.58/101.80  Clause #1268 (by superposition #[1263, 369]): ∀ (a a_1 a_2 : Iota),
% 101.58/101.80    Or (Eq (cong a a a_1 a_1) True)
% 101.58/101.80      (Or (Eq True False)
% 101.58/101.80        (Or (Eq (cyclic a a a_2 a_1) False) (Or (Eq (cyclic a a a_2 a_1) False) (Eq (cyclic a a a_2 a_1) False))))
% 101.58/101.80  Clause #1317 (by clausification #[1217]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False)
% 101.58/101.80  Clause #1320 (by superposition #[1317, 1215]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True)
% 101.58/101.80  Clause #1321 (by clausification #[1320]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True
% 101.58/101.80  Clause #1323 (by backward demodulation #[1321, 103]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) True) (Or (Eq (cong a a_1 a a_2) False) (Eq True False))
% 101.58/101.80  Clause #1345 (by clausification #[1323]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) True) (Eq (cong a a_1 a a_2) False)
% 101.58/101.80  Clause #1346 (by clausification #[1227]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq (coll a_2 a_2 a_1) False)
% 101.58/101.80  Clause #1347 (by forward demodulation #[1346, 1321]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq True False)
% 101.58/101.80  Clause #1348 (by clausification #[1347]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_2) True
% 101.58/101.80  Clause #1350 (by superposition #[1348, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_2 a_1) True)
% 101.58/101.80  Clause #1359 (by clausification #[1350]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_1) True
% 101.58/101.80  Clause #1361 (by superposition #[1359, 184]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_1 a_2) True)
% 101.58/101.80  Clause #1366 (by clausification #[1361]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_1 a_2) True
% 101.58/101.80  Clause #1367 (by superposition #[1366, 174]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True)
% 101.58/101.80  Clause #1372 (by clausification #[1367]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True
% 101.58/101.80  Clause #1373 (by superposition #[1372, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a a_1 a_2) True)
% 101.58/101.80  Clause #1378 (by clausification #[1373]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True
% 101.58/101.82  Clause #1380 (by superposition #[1378, 290]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cyclic a a a_1 a_3) False))
% 101.58/101.82  Clause #1677 (by clausification #[1380]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq (cyclic a a a_1 a_3) False)
% 101.58/101.82  Clause #1681 (by superposition #[1677, 1378]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True)
% 101.58/101.82  Clause #1682 (by clausification #[1681]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True
% 101.58/101.82  Clause #2474 (by clausification #[1194]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.58/101.82    Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_3) True) (Or (Eq (para a_1 a_3 a_2 a_3) False) (Eq (coll a a_1 a_2) False))
% 101.58/101.82  Clause #2475 (by forward demodulation #[2474, 1321]): ∀ (a a_1 a_2 a_3 : Iota),
% 101.58/101.82    Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_3) True) (Or (Eq (para a_1 a_3 a_2 a_3) False) (Eq True False))
% 101.58/101.82  Clause #2476 (by clausification #[2475]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_3) True) (Eq (para a_1 a_3 a_2 a_3) False)
% 101.58/101.82  Clause #2478 (by superposition #[2476, 1180]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a a_2 a_2 a_2) True) (Eq False True)
% 101.58/101.82  Clause #2479 (by clausification #[2478]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_2 a_2 a_2) True
% 101.58/101.82  Clause #2484 (by superposition #[2479, 736]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a_2) True)
% 101.58/101.82  Clause #2486 (by clausification #[2484]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a_2) True
% 101.58/101.82  Clause #2488 (by superposition #[2486, 613]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a a_2 a_2) True)
% 101.58/101.82  Clause #2495 (by clausification #[2488]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a a_2 a_2) True
% 101.58/101.82  Clause #2498 (by superposition #[2495, 719]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_2 a_2 a_1) True)
% 101.58/101.82  Clause #2500 (by clausification #[2498]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a a_2 a_2 a_1) True
% 101.58/101.82  Clause #2503 (by superposition #[2500, 736]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a_1 a_2) True)
% 101.58/101.82  Clause #2504 (by superposition #[2500, 787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.58/101.82    Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True)
% 101.58/101.82      (Or (Eq True False) (Eq (eqratio a a_6 a_6 a_1 a_2 a_3 a_4 a_5) False))
% 101.58/101.82  Clause #2505 (by clausification #[2503]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_1 a_2) True
% 101.58/101.82  Clause #2507 (by superposition #[2505, 719]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a_2 a_2 a_1) True)
% 101.58/101.82  Clause #2509 (by clausification #[2507]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a_2 a_2 a_1) True
% 101.58/101.82  Clause #2511 (by superposition #[2509, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_2) True)
% 101.58/101.82  Clause #2514 (by clausification #[2511]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_2) True
% 101.58/101.82  Clause #2516 (by superposition #[2514, 613]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_1 a_2 a_2) True)
% 101.58/101.82  Clause #2518 (by clausification #[2516]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_2 a_1 a_2 a_2) True
% 101.58/101.82  Clause #2520 (by superposition #[2518, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a_2 a_1) True)
% 101.58/101.82  Clause #2530 (by clausification #[2520]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_2 a_1) True
% 101.58/101.82  Clause #2579 (by clausification #[2504]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.58/101.82    Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a a_6 a_6 a_1 a_2 a_3 a_4 a_5) False)
% 101.58/101.82  Clause #2586 (by superposition #[2579, 2514]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a a_2 a_2) True) (Eq False True)
% 101.58/101.82  Clause #2589 (by superposition #[2579, 2530]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_2 a_2 a_1) True) (Eq False True)
% 101.58/101.82  Clause #2606 (by clausification #[2589]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_2 a_2 a_1) True
% 101.67/101.84  Clause #2609 (by superposition #[2606, 719]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a_1 a_1) True)
% 101.67/101.84  Clause #2656 (by clausification #[2609]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_1 a_1) True
% 101.67/101.84  Clause #2658 (by superposition #[2656, 787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.67/101.84    Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True)
% 101.67/101.84      (Or (Eq True False) (Eq (eqratio a_6 a_6 a_1 a_1 a_2 a_3 a_4 a_5) False))
% 101.67/101.84  Clause #2661 (by clausification #[2586]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a_2 a a_2 a_2) True
% 101.67/101.84  Clause #2698 (by clausification #[2658]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 101.67/101.84    Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_6 a_6 a_1 a_1 a_2 a_3 a_4 a_5) False)
% 101.67/101.84  Clause #2713 (by superposition #[2698, 2661]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_2 a_2) True) (Eq False True)
% 101.67/101.84  Clause #2714 (by clausification #[2713]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_2 a_2) True
% 101.67/101.84  Clause #2719 (by superposition #[2714, 2579]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_2 a_2) True) (Eq True False)
% 101.67/101.84  Clause #2723 (by clausification #[2719]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_3 a_2 a_2) True
% 101.67/101.84  Clause #2726 (by superposition #[2723, 719]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_2 a_3 a_3) True)
% 101.67/101.84  Clause #2753 (by clausification #[2726]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a a_2 a_2 a_3 a_3) True
% 101.67/101.84  Clause #2755 (by superposition #[2753, 613]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_3) True)
% 101.67/101.84  Clause #2758 (by clausification #[2755]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_3) True
% 101.67/101.84  Clause #2762 (by superposition #[2758, 736]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_3 a_3) True)
% 101.67/101.84  Clause #2767 (by clausification #[2762]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_3 a_3) True
% 101.67/101.85  Clause #2770 (by superposition #[2767, 719]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a a_3 a_3) True)
% 101.67/101.85  Clause #2774 (by clausification #[2770]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_2 a a_3 a_3) True
% 101.67/101.85  Clause #2778 (by superposition #[2774, 2698]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_4) True) (Eq True False)
% 101.67/101.85  Clause #2779 (by clausification #[2778]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_4 a_4) True
% 101.67/101.85  Clause #2785 (by superposition #[2779, 2579]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_4) True) (Eq True False)
% 101.67/101.85  Clause #2786 (by clausification #[2785]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_4) True
% 101.67/101.85  Clause #2788 (by superposition #[2786, 663]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a_2 a_3 a_4) True)
% 101.67/101.85  Clause #2803 (by clausification #[2788]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_2 a_3 a_4) True
% 101.67/101.85  Clause #2806 (by superposition #[2803, 2698]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_2 a_3 a_4) True) (Eq True False)
% 101.67/101.85  Clause #2807 (by clausification #[2806]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_3 a_4) True
% 101.67/101.85  Clause #2811 (by superposition #[2807, 736]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_2 a_3 a_4) True)
% 101.67/101.85  Clause #2819 (by clausification #[2811]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_1 a a_2 a_3 a_4) True
% 101.67/101.85  Clause #2825 (by superposition #[2819, 2698]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq True False)
% 101.67/101.85  Clause #2826 (by clausification #[2825]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True
% 101.67/101.85  Clause #2828 (by superposition #[2826, 663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_3 a_4 a_5) True)
% 101.67/101.85  Clause #2880 (by clausification #[2828]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a a a_2 a_3 a_4 a_5) True
% 101.67/101.87  Clause #2882 (by superposition #[2880, 613]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True)
% 101.67/101.87  Clause #2884 (by clausification #[2882]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True
% 101.67/101.87  Clause #2888 (by superposition #[2884, 736]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_5) True)
% 101.67/101.87  Clause #2892 (by clausification #[2888]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_5) True
% 101.67/101.87  Clause #2894 (by superposition #[2892, 663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_3 a_3) True)
% 101.67/101.87  Clause #2895 (by superposition #[2892, 719]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_3 a a_4 a_5) True)
% 101.67/101.87  Clause #2897 (by clausification #[2895]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a a_4 a_5) True
% 101.67/101.87  Clause #2899 (by superposition #[2897, 663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_2) True)
% 101.67/101.87  Clause #2901 (by clausification #[2899]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_2) True
% 101.67/101.87  Clause #2908 (by clausification #[2894]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_3 a_3) True
% 101.67/101.87  Clause #2910 (by superposition #[2908, 787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 101.67/101.87    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True)
% 101.67/101.87      (Or (Eq True False) (Eq (eqratio a_8 a_9 a_3 a_3 a_4 a_5 a_6 a_7) False))
% 101.67/101.87  Clause #3025 (by clausification #[2910]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 101.67/101.87    Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqratio a_8 a_9 a_3 a_3 a_4 a_5 a_6 a_7) False)
% 101.67/101.87  Clause #3034 (by superposition #[3025, 2901]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_3) True) (Eq False True)
% 101.67/101.87  Clause #3038 (by clausification #[3034]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_3) True
% 101.67/101.87  Clause #3042 (by superposition #[3038, 736]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_5) True)
% 101.67/101.87  Clause #3045 (by clausification #[3042]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_5) True
% 101.67/101.87  Clause #3047 (by superposition #[3045, 719]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True)
% 101.67/101.87  Clause #3050 (by clausification #[3047]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True
% 101.67/101.87  Clause #3054 (by superposition #[3050, 3025]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq True False)
% 101.67/101.87  Clause #3058 (by clausification #[3054]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True
% 101.67/101.87  Clause #3059 (by superposition #[3058, 491]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 101.67/101.87    Or (Eq (cong a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a_4 a_5 a_6 a_7) False))
% 101.67/101.87  Clause #3068 (by clausification #[3059]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq (cong a_4 a_5 a_6 a_7) False)
% 101.67/101.87  Clause #3218 (by clausification #[1268]): ∀ (a a_1 a_2 : Iota),
% 101.67/101.87    Or (Eq (cong a a a_1 a_1) True)
% 101.67/101.87      (Or (Eq (cyclic a a a_2 a_1) False) (Or (Eq (cyclic a a a_2 a_1) False) (Eq (cyclic a a a_2 a_1) False)))
% 101.67/101.87  Clause #3219 (by eliminate duplicate literals #[3218]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq (cyclic a a a_2 a_1) False)
% 101.67/101.87  Clause #3220 (by superposition #[3219, 1682]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq False True)
% 101.67/101.87  Clause #3221 (by clausification #[3220]): ∀ (a a_1 : Iota), Eq (cong a a a_1 a_1) True
% 101.67/101.87  Clause #3228 (by superposition #[3221, 3068]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False)
% 101.67/101.87  Clause #3258 (by clausification #[3228]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True
% 101.80/101.97  Clause #3265 (by superposition #[3258, 1345]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) True) (Eq True False)
% 101.80/101.97  Clause #3268 (by clausification #[3265]): ∀ (a a_1 a_2 : Iota), Eq (midp a a_1 a_2) True
% 101.80/101.97  Clause #3286 (by superposition #[3268, 297]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (midp a_1 a_4 a_3) False))
% 101.80/101.97  Clause #7617 (by clausification #[3286]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (para a a_1 a_2 a_3) True) (Eq (midp a_1 a_4 a_3) False)
% 101.80/101.97  Clause #7618 (by superposition #[7617, 3268]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (para a a_1 a_2 a_3) True) (Eq False True)
% 101.80/101.97  Clause #7619 (by clausification #[7618]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para a a_1 a_2 a_3) True
% 101.80/101.97  Clause #7633 (by superposition #[7619, 474]): Eq True False
% 101.80/101.97  Clause #7635 (by clausification #[7633]): False
% 101.80/101.97  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------