%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO568+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:42 PM UTC 2025 % Result : Theorem 271.51s 271.79s % Output : Proof 272.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO568+1 : TPTP v9.2.0. Released v7.5.0. % 0.07/0.13 % Command : duper %s % 0.13/0.35 % Computer : n027.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 12:27:23 EDT 2025 % 0.13/0.35 % CPUTime : % 271.51/271.79 SZS status Theorem for theBenchmark.p % 271.51/271.79 SZS output start Proof for theBenchmark.p % 271.51/271.79 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 271.51/271.79 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 271.51/271.79 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 271.51/271.79 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 271.51/271.79 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 271.51/271.79 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 271.51/271.79 Clause #8 (by assumption #[]): Eq (∀ (A B C D E F : Iota), And (perp A B C D) (perp C D E F) → para A B E F) True % 271.51/271.79 Clause #13 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A B D C) True % 271.51/271.79 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 271.51/271.79 Clause #15 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic B A C D) True % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 Clause #29 (by assumption #[]): Eq % 271.51/271.79 (∀ (A B C D E F G H P Q U V : Iota), % 271.51/271.79 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) % 271.51/271.79 True % 271.51/271.79 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 % 271.51/271.79 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 % 271.51/271.79 Clause #40 (by assumption #[]): Eq (∀ (A B P Q : Iota), cyclic A B P Q → eqangle P A P B Q A Q B) True % 271.51/271.79 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 % 271.51/271.79 Clause #43 (by assumption #[]): Eq % 271.51/271.79 (∀ (A B C P Q R : Iota), % 271.51/271.79 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) % 271.51/271.79 True % 271.51/271.79 Clause #56 (by assumption #[]): Eq (∀ (A B P Q : Iota), And (cong A P B P) (cong A Q B Q) → perp A B P Q) True % 271.51/271.79 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 % 271.51/271.79 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 271.51/271.79 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 % 271.51/271.79 Clause #94 (by assumption #[]): Eq % 271.51/271.79 (Not % 271.51/271.79 (∀ (A B C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.51/271.79 And % 271.51/271.79 (And % 271.51/271.79 (And % 271.51/271.79 (And % 271.51/271.79 (And % 271.51/271.79 (And (And (And (And (midp MIDPNT1 A B) (perp A B MIDPNT1 O)) (midp MIDPNT2 A C)) (perp A C MIDPNT2 O)) % 271.51/271.79 (midp MIDPNT3 B C)) % 271.51/271.79 (perp B C MIDPNT3 O)) % 271.51/271.79 (perp D C A B)) % 271.51/271.79 (coll D A B)) % 271.51/271.79 (perp E B A C)) % 271.51/271.79 (coll E A C) → % 271.51/271.79 perp A O D E)) % 271.51/271.79 True % 271.51/271.79 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 271.56/271.81 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 271.56/271.81 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 % 271.56/271.81 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) % 271.56/271.81 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 271.56/271.81 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 271.56/271.81 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 % 271.56/271.81 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) % 271.56/271.81 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 271.56/271.81 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 271.56/271.81 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 % 271.56/271.81 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) % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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) % 271.56/271.81 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)) % 271.56/271.81 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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) % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.81 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 271.56/271.81 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) % 271.56/271.81 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 271.56/271.81 Or (Eq (cyclic a a_1 a_2 a_3) True) % 271.56/271.81 (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)) % 271.56/271.81 Clause #170 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic B a C D) True % 271.56/271.81 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 % 271.56/271.81 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 % 271.56/271.84 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 % 271.56/271.84 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) % 271.56/271.84 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 271.56/271.84 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 % 271.56/271.84 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 % 271.56/271.84 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 % 271.56/271.84 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) % 271.56/271.84 Clause #180 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a B D C) True % 271.56/271.84 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 % 271.56/271.84 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 % 271.56/271.84 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 % 271.56/271.84 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) % 271.56/271.84 Clause #207 (by clausification #[56]): ∀ (a : Iota), Eq (∀ (B P Q : Iota), And (cong a P B P) (cong a Q B Q) → perp a B P Q) True % 271.56/271.84 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), Eq (∀ (P Q : Iota), And (cong a P a_1 P) (cong a Q a_1 Q) → perp a a_1 P Q) True % 271.56/271.84 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Q : Iota), And (cong a a_1 a_2 a_1) (cong a Q a_2 Q) → perp a a_2 a_1 Q) True % 271.56/271.84 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (cong a a_1 a_2 a_1) (cong a a_3 a_2 a_3) → perp a a_2 a_1 a_3) True % 271.56/271.84 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (cong a a_1 a_2 a_1) (cong a a_3 a_2 a_3)) False) (Eq (perp a a_2 a_1 a_3) True) % 271.56/271.84 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 a_3 : Iota), % 271.56/271.84 Or (Eq (perp a a_1 a_2 a_3) True) (Or (Eq (cong a a_2 a_1 a_2) False) (Eq (cong a a_3 a_1 a_3) False)) % 271.56/271.84 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 271.56/271.84 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), perp a a_1 C D → perp a a_1 D C) True % 271.56/271.84 Clause #263 (by clausification #[262]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), perp a a_1 a_2 D → perp a a_1 D a_2) True % 271.56/271.84 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3 → perp a a_1 a_3 a_2) True % 271.56/271.84 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) False) (Eq (perp a a_1 a_3 a_2) True) % 271.56/271.84 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 271.56/271.84 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), perp a a_1 C D → perp C D a a_1) True % 271.56/271.84 Clause #268 (by clausification #[267]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), perp a a_1 a_2 D → perp a_2 D a a_1) True % 271.56/271.84 Clause #269 (by clausification #[268]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3 → perp a_2 a_3 a a_1) True % 271.56/271.84 Clause #270 (by clausification #[269]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) False) (Eq (perp a_2 a_3 a a_1) True) % 271.56/271.84 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 % 271.56/271.84 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 % 271.56/271.84 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 % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.86 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) % 271.61/271.86 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.86 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)) % 271.61/271.86 Clause #298 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (B C D E F : Iota), And (perp a B C D) (perp C D E F) → para a B E F) True % 271.61/271.86 Clause #299 (by clausification #[298]): ∀ (a a_1 : Iota), Eq (∀ (C D E F : Iota), And (perp a a_1 C D) (perp C D E F) → para a a_1 E F) True % 271.61/271.86 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E F : Iota), And (perp a a_1 a_2 D) (perp a_2 D E F) → para a a_1 E F) True % 271.61/271.86 Clause #301 (by clausification #[300]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 E F) → para a a_1 E F) True % 271.61/271.86 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 F) → para a a_1 a_4 F) True % 271.61/271.86 Clause #303 (by clausification #[302]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5) → para a a_1 a_4 a_5) True % 271.61/271.86 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.86 Or (Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5)) False) (Eq (para a a_1 a_4 a_5) True) % 271.61/271.86 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.86 Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (perp a a_1 a_4 a_5) False) (Eq (perp a_4 a_5 a_2 a_3) False)) % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.86 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 % 271.61/271.86 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.86 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 % 271.61/271.86 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.61/271.86 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 % 271.61/271.86 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.86 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 % 271.61/271.86 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.86 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) % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.86 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 % 271.61/271.88 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 % 271.61/271.88 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 % 271.61/271.88 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) % 271.61/271.88 Clause #360 (by clausification #[43]): ∀ (a : Iota), % 271.61/271.88 Eq % 271.61/271.88 (∀ (B C P Q R : Iota), % 271.61/271.88 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) % 271.61/271.88 True % 271.61/271.88 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 271.61/271.88 Eq % 271.61/271.88 (∀ (C P Q R : Iota), % 271.61/271.88 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) → % 271.61/271.88 cong a a_1 P Q) % 271.61/271.88 True % 271.61/271.88 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota), % 271.61/271.88 Eq % 271.61/271.88 (∀ (P Q R : Iota), % 271.61/271.88 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) → % 271.61/271.88 cong a a_1 P Q) % 271.61/271.88 True % 271.61/271.88 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 271.61/271.88 Eq % 271.61/271.88 (∀ (Q R : Iota), % 271.61/271.88 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)) % 271.61/271.88 (eqangle a_2 a a_2 a_1 R a_3 R Q) → % 271.61/271.88 cong a a_1 a_3 Q) % 271.61/271.88 True % 271.61/271.88 Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.88 Eq % 271.61/271.88 (∀ (R : Iota), % 271.61/271.88 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)) % 271.61/271.88 (eqangle a_2 a a_2 a_1 R a_3 R a_4) → % 271.61/271.88 cong a a_1 a_3 a_4) % 271.61/271.88 True % 271.61/271.88 Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 Eq % 271.61/271.88 (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)) % 271.61/271.88 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4) → % 271.61/271.88 cong a a_1 a_3 a_4) % 271.61/271.88 True % 271.61/271.88 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 Or % 271.61/271.88 (Eq % 271.61/271.88 (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)) % 271.61/271.88 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4)) % 271.61/271.88 False) % 271.61/271.88 (Eq (cong a a_1 a_3 a_4) True) % 271.61/271.88 Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 Or (Eq (cong a a_1 a_2 a_3) True) % 271.61/271.88 (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) % 271.61/271.88 (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)) % 271.61/271.88 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 Or (Eq (cong a a_1 a_2 a_3) True) % 271.61/271.88 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 271.61/271.88 (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))) % 271.61/271.88 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 Or (Eq (cong a a_1 a_2 a_3) True) % 271.61/271.88 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 271.61/271.88 (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)))) % 271.61/271.88 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 % 271.61/271.88 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 % 271.61/271.88 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 % 271.61/271.88 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 % 271.61/271.88 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.88 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 % 271.61/271.88 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.88 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 % 271.61/271.88 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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) % 271.61/271.91 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 % 271.61/271.91 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 % 271.61/271.91 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 % 271.61/271.91 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 % 271.61/271.91 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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) % 271.61/271.91 Clause #458 (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 % 271.61/271.91 Clause #459 (by clausification #[458]): ∀ (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 % 271.61/271.91 Clause #460 (by clausification #[459]): ∀ (a a_1 a_2 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #461 (by clausification #[460]): ∀ (a a_1 a_2 a_3 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #462 (by clausification #[461]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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 % 271.61/271.91 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 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) % 271.61/271.91 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.91 Or (Eq (cong a a_1 a_2 a_3) True) % 271.61/271.91 (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)) % 271.61/271.91 Clause #488 (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 % 271.61/271.91 Clause #489 (by clausification #[488]): ∀ (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 % 271.61/271.93 Clause #490 (by clausification #[489]): ∀ (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 % 271.61/271.93 Clause #491 (by clausification #[490]): ∀ (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 % 271.61/271.93 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.61/271.93 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) % 271.61/271.93 Clause #515 (by clausification #[40]): ∀ (a : Iota), Eq (∀ (B P Q : Iota), cyclic a B P Q → eqangle P a P B Q a Q B) True % 271.61/271.93 Clause #516 (by clausification #[515]): ∀ (a a_1 : Iota), Eq (∀ (P Q : Iota), cyclic a a_1 P Q → eqangle P a P a_1 Q a Q a_1) True % 271.61/271.93 Clause #517 (by clausification #[516]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Q : Iota), cyclic a a_1 a_2 Q → eqangle a_2 a a_2 a_1 Q a Q a_1) True % 271.61/271.93 Clause #518 (by clausification #[517]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → eqangle a_2 a a_2 a_1 a_3 a a_3 a_1) True % 271.61/271.93 Clause #519 (by clausification #[518]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (eqangle a_2 a a_2 a_1 a_3 a a_3 a_1) True) % 271.61/271.93 Clause #547 (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 % 271.61/271.93 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #549 (by clausification #[548]): ∀ (a a_1 a_2 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #550 (by clausification #[549]): ∀ (a a_1 a_2 a_3 : Iota), % 271.61/271.93 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) % 271.61/271.93 True % 271.61/271.93 Clause #551 (by clausification #[550]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.93 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 % 271.61/271.93 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.93 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) % 271.61/271.93 (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True) % 271.61/271.93 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.93 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 271.61/271.93 (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)) % 271.61/271.93 Clause #554 (by clausification #[553]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.61/271.93 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 271.61/271.93 (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))) % 271.61/271.93 Clause #588 (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 % 271.61/271.93 Clause #589 (by clausification #[588]): ∀ (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 % 271.61/271.93 Clause #590 (by clausification #[589]): ∀ (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 % 271.61/271.93 Clause #591 (by clausification #[590]): ∀ (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 % 271.70/271.95 Clause #592 (by clausification #[591]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.70/271.95 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 % 271.70/271.95 Clause #593 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.70/271.95 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 % 271.70/271.95 Clause #594 (by clausification #[593]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.70/271.95 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 % 271.70/271.95 Clause #595 (by clausification #[594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.70/271.95 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 % 271.70/271.95 Clause #596 (by clausification #[595]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.70/271.95 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) % 271.70/271.95 Clause #604 (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 % 271.70/271.95 Clause #605 (by clausification #[604]): ∀ (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 % 271.70/271.95 Clause #606 (by clausification #[605]): ∀ (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 % 271.70/271.95 Clause #607 (by clausification #[606]): ∀ (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 % 271.70/271.95 Clause #608 (by clausification #[607]): ∀ (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 % 271.70/271.95 Clause #609 (by clausification #[608]): ∀ (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 % 271.70/271.95 Clause #610 (by clausification #[609]): ∀ (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) % 271.70/271.95 Clause #611 (by clausification #[94]): Eq % 271.70/271.95 (∀ (A B C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.95 And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And (And (And (And (midp MIDPNT1 A B) (perp A B MIDPNT1 O)) (midp MIDPNT2 A C)) (perp A C MIDPNT2 O)) % 271.70/271.95 (midp MIDPNT3 B C)) % 271.70/271.95 (perp B C MIDPNT3 O)) % 271.70/271.95 (perp D C A B)) % 271.70/271.95 (coll D A B)) % 271.70/271.95 (perp E B A C)) % 271.70/271.95 (coll E A C) → % 271.70/271.95 perp A O D E) % 271.70/271.95 False % 271.70/271.95 Clause #612 (by clausification #[611]): ∀ (a : Iota), % 271.70/271.95 Eq % 271.70/271.95 (Not % 271.70/271.95 (∀ (B C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.95 And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And (And (midp MIDPNT1 (skS.0 5 a) B) (perp (skS.0 5 a) B MIDPNT1 O)) % 271.70/271.95 (midp MIDPNT2 (skS.0 5 a) C)) % 271.70/271.95 (perp (skS.0 5 a) C MIDPNT2 O)) % 271.70/271.95 (midp MIDPNT3 B C)) % 271.70/271.95 (perp B C MIDPNT3 O)) % 271.70/271.95 (perp D C (skS.0 5 a) B)) % 271.70/271.95 (coll D (skS.0 5 a) B)) % 271.70/271.95 (perp E B (skS.0 5 a) C)) % 271.70/271.95 (coll E (skS.0 5 a) C) → % 271.70/271.95 perp (skS.0 5 a) O D E)) % 271.70/271.95 True % 271.70/271.95 Clause #613 (by clausification #[612]): ∀ (a : Iota), % 271.70/271.95 Eq % 271.70/271.95 (∀ (B C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.95 And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And % 271.70/271.95 (And (And (midp MIDPNT1 (skS.0 5 a) B) (perp (skS.0 5 a) B MIDPNT1 O)) % 271.70/271.95 (midp MIDPNT2 (skS.0 5 a) C)) % 271.70/271.95 (perp (skS.0 5 a) C MIDPNT2 O)) % 271.70/271.95 (midp MIDPNT3 B C)) % 271.70/271.95 (perp B C MIDPNT3 O)) % 271.70/271.95 (perp D C (skS.0 5 a) B)) % 271.70/271.95 (coll D (skS.0 5 a) B)) % 271.70/271.95 (perp E B (skS.0 5 a) C)) % 271.70/271.95 (coll E (skS.0 5 a) C) → % 271.70/271.95 perp (skS.0 5 a) O D E) % 271.70/271.95 False % 271.70/271.95 Clause #614 (by clausification #[613]): ∀ (a a_1 : Iota), % 271.70/271.95 Eq % 271.70/271.95 (Not % 271.70/271.95 (∀ (C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.97 And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 O)) % 271.70/271.97 (midp MIDPNT2 (skS.0 5 a) C)) % 271.70/271.97 (perp (skS.0 5 a) C MIDPNT2 O)) % 271.70/271.97 (midp MIDPNT3 (skS.0 6 a a_1) C)) % 271.70/271.97 (perp (skS.0 6 a a_1) C MIDPNT3 O)) % 271.70/271.97 (perp D C (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (perp E (skS.0 6 a a_1) (skS.0 5 a) C)) % 271.70/271.97 (coll E (skS.0 5 a) C) → % 271.70/271.97 perp (skS.0 5 a) O D E)) % 271.70/271.97 True % 271.70/271.97 Clause #615 (by clausification #[614]): ∀ (a a_1 : Iota), % 271.70/271.97 Eq % 271.70/271.97 (∀ (C O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.97 And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 O)) % 271.70/271.97 (midp MIDPNT2 (skS.0 5 a) C)) % 271.70/271.97 (perp (skS.0 5 a) C MIDPNT2 O)) % 271.70/271.97 (midp MIDPNT3 (skS.0 6 a a_1) C)) % 271.70/271.97 (perp (skS.0 6 a a_1) C MIDPNT3 O)) % 271.70/271.97 (perp D C (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (perp E (skS.0 6 a a_1) (skS.0 5 a) C)) % 271.70/271.97 (coll E (skS.0 5 a) C) → % 271.70/271.97 perp (skS.0 5 a) O D E) % 271.70/271.97 False % 271.70/271.97 Clause #616 (by clausification #[615]): ∀ (a a_1 a_2 : Iota), % 271.70/271.97 Eq % 271.70/271.97 (Not % 271.70/271.97 (∀ (O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.97 And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 O)) % 271.70/271.97 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 O)) % 271.70/271.97 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 O)) % 271.70/271.97 (perp D (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.97 perp (skS.0 5 a) O D E)) % 271.70/271.97 True % 271.70/271.97 Clause #617 (by clausification #[616]): ∀ (a a_1 a_2 : Iota), % 271.70/271.97 Eq % 271.70/271.97 (∀ (O D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.97 And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 O)) % 271.70/271.97 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 O)) % 271.70/271.97 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 O)) % 271.70/271.97 (perp D (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.97 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.97 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.97 perp (skS.0 5 a) O D E) % 271.70/271.97 False % 271.70/271.97 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 a_3 : Iota), % 271.70/271.97 Eq % 271.70/271.97 (Not % 271.70/271.97 (∀ (D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.97 And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And % 271.70/271.97 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.70/271.97 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.97 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (perp D (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.99 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) D E)) % 271.70/271.99 True % 271.70/271.99 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 a_3 : Iota), % 271.70/271.99 Eq % 271.70/271.99 (∀ (D E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.99 And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (perp D (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (coll D (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.99 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) D E) % 271.70/271.99 False % 271.70/271.99 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.70/271.99 Eq % 271.70/271.99 (Not % 271.70/271.99 (∀ (E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.99 And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.99 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) E)) % 271.70/271.99 True % 271.70/271.99 Clause #621 (by clausification #[620]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.70/271.99 Eq % 271.70/271.99 (∀ (E MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.70/271.99 And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And % 271.70/271.99 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.70/271.99 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.70/271.99 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.70/271.99 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.70/271.99 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) E) % 271.75/272.01 False % 271.75/272.01 Clause #622 (by clausification #[621]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.75/272.01 Eq % 271.75/272.01 (Not % 271.75/272.01 (∀ (MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.75/272.01 And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.01 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 271.75/272.01 True % 271.75/272.01 Clause #623 (by clausification #[622]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.75/272.01 Eq % 271.75/272.01 (∀ (MIDPNT1 MIDPNT2 MIDPNT3 : Iota), % 271.75/272.01 And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And (midp MIDPNT1 (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 6 a a_1) MIDPNT1 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.01 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 271.75/272.01 False % 271.75/272.01 Clause #624 (by clausification #[623]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.75/272.01 Eq % 271.75/272.01 (Not % 271.75/272.01 (∀ (MIDPNT2 MIDPNT3 : Iota), % 271.75/272.01 And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And % 271.75/272.01 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 271.75/272.01 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.01 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.01 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.01 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.01 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 271.75/272.01 True % 271.75/272.01 Clause #625 (by clausification #[624]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.75/272.01 Eq % 271.75/272.01 (∀ (MIDPNT2 MIDPNT3 : Iota), % 271.75/272.03 And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 271.75/272.03 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp MIDPNT2 (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) MIDPNT2 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.03 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 271.75/272.03 False % 271.75/272.03 Clause #626 (by clausification #[625]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.75/272.03 Eq % 271.75/272.03 (Not % 271.75/272.03 (∀ (MIDPNT3 : Iota), % 271.75/272.03 And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 271.75/272.03 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 271.75/272.03 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.03 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 271.75/272.03 True % 271.75/272.03 Clause #627 (by clausification #[626]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.75/272.03 Eq % 271.75/272.03 (∀ (MIDPNT3 : Iota), % 271.75/272.03 And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And % 271.75/272.03 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 271.75/272.03 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 271.75/272.03 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (midp MIDPNT3 (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) MIDPNT3 (skS.0 8 a a_1 a_2 a_3))) % 271.75/272.03 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.75/272.03 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.75/272.03 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.75/272.03 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 271.80/272.05 False % 271.80/272.05 Clause #628 (by clausification #[627]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 271.80/272.05 Eq % 271.80/272.05 (Not % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.05 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.05 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.80/272.05 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 271.80/272.05 True % 271.80/272.05 Clause #629 (by clausification #[628]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 271.80/272.05 Eq % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.05 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.05 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) → % 271.80/272.05 perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 271.80/272.05 False % 271.80/272.05 Clause #630 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 271.80/272.05 Eq % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And % 271.80/272.05 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.80/272.05 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 271.80/272.05 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.05 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.05 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.07 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.07 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.07 True % 271.80/272.07 Clause #631 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.07 Eq (perp (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) False % 271.80/272.07 Clause #633 (by clausification #[630]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 271.80/272.07 Eq % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And % 271.80/272.07 (And (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 6 a a_1)) % 271.80/272.07 (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.07 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.07 (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.07 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 271.80/272.07 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 271.80/272.07 (skS.0 8 a a_1 a_2 a_3))) % 271.80/272.07 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.07 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 271.80/272.07 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 271.80/272.07 True % 271.80/272.07 Clause #659 (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 % 271.80/272.07 Clause #660 (by clausification #[659]): ∀ (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 % 271.80/272.07 Clause #661 (by clausification #[660]): ∀ (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 % 271.80/272.07 Clause #662 (by clausification #[661]): ∀ (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 % 271.80/272.07 Clause #663 (by clausification #[662]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #664 (by clausification #[663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #665 (by clausification #[664]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #666 (by clausification #[665]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #667 (by clausification #[666]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.07 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) % 271.80/272.07 Clause #714 (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 % 271.80/272.07 Clause #715 (by clausification #[714]): ∀ (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 % 271.80/272.07 Clause #716 (by clausification #[715]): ∀ (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 % 271.80/272.07 Clause #717 (by clausification #[716]): ∀ (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 % 271.80/272.07 Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.07 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 % 271.80/272.07 Clause #720 (by clausification #[719]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #721 (by clausification #[720]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #722 (by clausification #[721]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.09 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) % 271.80/272.09 Clause #732 (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 % 271.80/272.09 Clause #733 (by clausification #[732]): ∀ (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 % 271.80/272.09 Clause #734 (by clausification #[733]): ∀ (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 % 271.80/272.09 Clause #735 (by clausification #[734]): ∀ (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 % 271.80/272.09 Clause #736 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #737 (by clausification #[736]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #738 (by clausification #[737]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #739 (by clausification #[738]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.09 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 % 271.80/272.09 Clause #740 (by clausification #[739]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.09 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) % 271.80/272.09 Clause #780 (by clausification #[29]): ∀ (a : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (B C D E F G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #781 (by clausification #[780]): ∀ (a a_1 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (C D E F G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #782 (by clausification #[781]): ∀ (a a_1 a_2 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (D E F G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #783 (by clausification #[782]): ∀ (a a_1 a_2 a_3 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (E F G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #784 (by clausification #[783]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (F G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #785 (by clausification #[784]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (G H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (H P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (P Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #788 (by clausification #[787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 271.80/272.09 Eq % 271.80/272.09 (∀ (Q U V : Iota), % 271.80/272.09 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) % 271.80/272.09 True % 271.80/272.09 Clause #789 (by clausification #[788]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 271.80/272.12 Eq % 271.80/272.12 (∀ (U V : Iota), % 271.80/272.12 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) → % 271.80/272.12 eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9) % 271.80/272.12 True % 271.80/272.12 Clause #790 (by clausification #[789]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 271.80/272.12 Eq % 271.80/272.12 (∀ (V : Iota), % 271.80/272.12 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) → % 271.80/272.12 eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10) % 271.80/272.12 True % 271.80/272.12 Clause #791 (by clausification #[790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 271.80/272.12 Eq % 271.80/272.12 (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) → % 271.80/272.12 eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 271.80/272.12 True % 271.80/272.12 Clause #792 (by clausification #[791]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 271.80/272.12 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) % 271.80/272.12 (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 271.80/272.12 Clause #793 (by clausification #[792]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 271.80/272.12 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 271.80/272.12 (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)) % 271.80/272.12 Clause #883 (by clausification #[633]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2)) True % 271.80/272.12 Clause #885 (by superposition #[883, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True) % 271.80/272.12 Clause #886 (by superposition #[883, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1)) True) % 271.80/272.12 Clause #916 (by clausification #[886]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1)) True % 271.80/272.12 Clause #917 (by superposition #[916, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) True) % 271.80/272.12 Clause #957 (by clausification #[917]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) True % 271.80/272.12 Clause #958 (by superposition #[957, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) True) % 271.80/272.12 Clause #966 (by clausification #[958]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2)) True % 271.80/272.12 Clause #967 (by superposition #[966, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True) % 271.80/272.12 Clause #974 (by clausification #[967]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True % 271.80/272.12 Clause #975 (by superposition #[974, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) True) % 271.80/272.12 Clause #982 (by clausification #[975]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) True % 271.80/272.12 Clause #983 (by superposition #[982, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Or (Eq True False) (Eq (perp (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1)) True) % 271.80/272.12 Clause #990 (by clausification #[983]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.80/272.12 Eq (perp (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1)) True % 271.80/272.12 Clause #991 (by superposition #[990, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.80/272.12 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4) True) % 271.80/272.12 (Or (Eq True False) (Eq (perp (skS.0 10 a a_1 a_2 a_5 a_6 a_7) (skS.0 6 a a_1) a_3 a_4) False)) % 271.89/272.14 Clause #997 (by clausification #[885]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.89/272.14 Eq (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True % 271.89/272.14 Clause #1582 (by clausification #[991]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.89/272.14 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4) True) % 271.89/272.14 (Eq (perp (skS.0 10 a a_1 a_2 a_5 a_6 a_7) (skS.0 6 a a_1) a_3 a_4) False) % 271.89/272.14 Clause #1584 (by superposition #[1582, 997]): ∀ (a a_1 a_2 : Iota), % 271.89/272.14 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True) (Eq False True) % 271.89/272.14 Clause #1585 (by clausification #[1584]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 5 a)) True % 271.89/272.14 Clause #1587 (by superposition #[1585, 156]): ∀ (a a_1 a_2 : Iota), % 271.89/272.14 Or (Eq True False) (Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2)) True) % 271.89/272.14 Clause #1591 (by clausification #[1587]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2)) True % 271.89/272.14 Clause #1598 (by superposition #[1591, 610]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4) True) % 271.89/272.14 Clause #1612 (by clausification #[1598]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4) True % 271.89/272.14 Clause #1614 (by superposition #[1612, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4 a_3 a_4) True) % 271.89/272.14 Clause #1616 (by clausification #[1614]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4 a_3 a_4) True % 271.89/272.14 Clause #1619 (by superposition #[1616, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) % 271.89/272.14 (Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4)) True) % 271.89/272.14 Clause #1624 (by clausification #[1619]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4)) True % 271.89/272.14 Clause #1626 (by superposition #[1624, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) % 271.89/272.14 (Eq (eqangle a a_1 a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True) % 271.89/272.14 Clause #1635 (by clausification #[1626]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle a a_1 a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True % 271.89/272.14 Clause #1639 (by superposition #[1635, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) % 271.89/272.14 (Eq (eqangle a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True) % 271.89/272.14 Clause #1642 (by clausification #[1639]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True % 271.89/272.14 Clause #1643 (by superposition #[1642, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) % 271.89/272.14 (Eq (eqangle a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True) % 271.89/272.14 Clause #1647 (by clausification #[1643]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle a a_1 (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True % 271.89/272.14 Clause #1651 (by superposition #[1647, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) % 271.89/272.14 (Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) a_1 a (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4)) True) % 271.89/272.14 Clause #1656 (by clausification #[1651]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) a_1 a (skS.0 5 a_2) (skS.0 7 a_2 a_3 a_4)) True % 271.89/272.14 Clause #1659 (by superposition #[1656, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 5 a) (skS.0 7 a a_1 a_2) a_4 a_3) True) % 271.89/272.14 Clause #1664 (by clausification #[1659]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.14 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 5 a) (skS.0 7 a a_1 a_2) a_4 a_3) True % 271.89/272.17 Clause #1667 (by superposition #[1664, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4 a_4 a_3) True) % 271.89/272.17 Clause #1679 (by clausification #[1667]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 5 a) (skS.0 7 a a_1 a_2) a_3 a_4 a_4 a_3) True % 271.89/272.17 Clause #1681 (by superposition #[1679, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Or (Eq True False) (Eq (eqangle (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 a_4 a_3) True) % 271.89/272.17 Clause #1686 (by clausification #[1681]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Eq (eqangle (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 a_4 a_3) True % 271.89/272.17 Clause #1687 (by superposition #[1686, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 a_4 a_3) True) % 271.89/272.17 Clause #1692 (by clausification #[1687]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 a_4 a_3) True % 271.89/272.17 Clause #1699 (by superposition #[1692, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Or (Eq True False) (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 7 a a_1 a_2) (skS.0 5 a) a_4 a_3) True) % 271.89/272.17 Clause #1704 (by clausification #[1699]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 5 a) a_3 a_4 (skS.0 7 a a_1 a_2) (skS.0 5 a) a_4 a_3) True % 271.89/272.17 Clause #1709 (by superposition #[1704, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Or (Eq True False) % 271.89/272.17 (Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True) % 271.89/272.17 Clause #1716 (by clausification #[1709]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 271.89/272.17 Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 5 a_2)) True % 271.89/272.17 Clause #1721 (by superposition #[1716, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 271.89/272.17 Clause #1731 (by clausification #[1721]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 271.89/272.17 Clause #1740 (by superposition #[1731, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 271.89/272.17 Clause #1743 (by superposition #[1731, 610]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_1 a a_2 a_3) True) % 271.89/272.17 Clause #1760 (by clausification #[1740]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 271.89/272.17 Clause #1761 (by superposition #[1760, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 271.89/272.17 Clause #1766 (by clausification #[1761]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 271.89/272.17 Clause #1776 (by superposition #[1766, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 271.89/272.17 Clause #1785 (by clausification #[1776]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 271.89/272.17 Clause #1799 (by superposition #[1785, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 271.89/272.17 Clause #1809 (by clausification #[1799]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 271.89/272.17 Clause #1821 (by superposition #[1809, 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)) % 271.89/272.17 Clause #1823 (by superposition #[1809, 554]): ∀ (a a_1 a_2 a_3 : Iota), % 271.89/272.17 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) % 271.89/272.17 (Or (Eq True False) (Or (Eq (para a_1 a a_2 a_3) False) (Eq (coll a a_1 a_2) False))) % 271.89/272.17 Clause #1843 (by clausification #[1743]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a a_2 a_3) True % 271.89/272.17 Clause #1852 (by superposition #[1843, 496]): ∀ (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) % 271.89/272.17 Clause #1856 (by clausification #[1852]): ∀ (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 % 271.89/272.17 Clause #1862 (by superposition #[1856, 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) % 271.89/272.17 Clause #1869 (by clausification #[1862]): ∀ (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 % 271.89/272.17 Clause #1870 (by superposition #[1869, 162]): ∀ (a a_1 : Iota), Or (Eq (cyclic a a a_1 a) True) (Or (Eq True False) (Eq (coll a_1 a a) False)) % 271.94/272.19 Clause #1906 (by clausification #[1821]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 271.94/272.19 Clause #1912 (by superposition #[1906, 1809]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 271.94/272.19 Clause #1913 (by clausification #[1912]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 271.94/272.19 Clause #1976 (by clausification #[1870]): ∀ (a a_1 : Iota), Or (Eq (cyclic a a a_1 a) True) (Eq (coll a_1 a a) False) % 271.94/272.19 Clause #1977 (by forward demodulation #[1976, 1913]): ∀ (a a_1 : Iota), Or (Eq (cyclic a a a_1 a) True) (Eq True False) % 271.94/272.19 Clause #1978 (by clausification #[1977]): ∀ (a a_1 : Iota), Eq (cyclic a a a_1 a) True % 271.94/272.19 Clause #1980 (by superposition #[1978, 184]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (cyclic a a a a_1) True) % 271.94/272.19 Clause #1985 (by clausification #[1980]): ∀ (a a_1 : Iota), Eq (cyclic a a a a_1) True % 271.94/272.19 Clause #1988 (by superposition #[1985, 290]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Or (Eq True False) (Eq (cyclic a a a a_2) False)) % 271.94/272.19 Clause #2031 (by clausification #[1988]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (cyclic a a a a_2) False) % 271.94/272.19 Clause #2033 (by superposition #[2031, 1985]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq False True) % 271.94/272.19 Clause #2034 (by clausification #[2033]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 271.94/272.19 Clause #2035 (by superposition #[2034, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 271.94/272.19 Clause #2038 (by superposition #[2034, 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)) % 271.94/272.19 Clause #2042 (by clausification #[2035]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 271.94/272.19 Clause #2043 (by superposition #[2042, 174]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_1 a_2) True) % 271.94/272.19 Clause #2066 (by clausification #[2043]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_1 a_2) True % 271.94/272.19 Clause #2069 (by superposition #[2066, 519]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a a_2 a_1 a_2 a) True) % 271.94/272.19 Clause #2232 (by clausification #[2069]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a a a_2 a_1 a_2 a) True % 271.94/272.19 Clause #2233 (by superposition #[2232, 369]): ∀ (a a_1 a_2 : Iota), % 271.94/272.19 Or (Eq (cong a a_1 a a_1) True) % 271.94/272.19 (Or (Eq True False) % 271.94/272.19 (Or (Eq (cyclic a a_1 a_1 a_2) False) (Or (Eq (cyclic a a_1 a_1 a) False) (Eq (cyclic a a_1 a_1 a_1) False)))) % 271.94/272.19 Clause #2301 (by clausification #[2038]): ∀ (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) % 271.94/272.19 Clause #2302 (by superposition #[2301, 2034]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 271.94/272.19 Clause #2310 (by clausification #[2302]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 271.94/272.19 Clause #2814 (by clausification #[1823]): ∀ (a a_1 a_2 a_3 : Iota), % 271.94/272.19 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Or (Eq (para a_1 a a_2 a_3) False) (Eq (coll a a_1 a_2) False)) % 271.94/272.19 Clause #2815 (by forward demodulation #[2814, 1913]): ∀ (a a_1 a_2 a_3 : Iota), % 271.94/272.19 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Or (Eq (para a_1 a a_2 a_3) False) (Eq True False)) % 271.94/272.19 Clause #2816 (by clausification #[2815]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Eq (para a_1 a a_2 a_3) False) % 271.94/272.19 Clause #2817 (by superposition #[2816, 1731]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a a a a a_1) True) (Eq False True) % 271.94/272.19 Clause #2887 (by clausification #[2817]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a_1) True % 271.94/272.19 Clause #2892 (by superposition #[2887, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a a a_1) True) % 271.94/272.19 Clause #2894 (by clausification #[2892]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a a a_1) True % 271.94/272.19 Clause #2896 (by superposition #[2894, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True) % 271.94/272.19 Clause #2900 (by clausification #[2896]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True % 271.94/272.21 Clause #2903 (by superposition #[2900, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True) % 271.94/272.21 Clause #2905 (by clausification #[2903]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True % 271.94/272.21 Clause #2909 (by superposition #[2905, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a a_1 a_1) True) % 271.94/272.21 Clause #2911 (by clausification #[2909]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a_1 a a_1 a_1) True % 271.94/272.21 Clause #2913 (by superposition #[2911, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a_1 a a) True) % 271.94/272.21 Clause #2925 (by clausification #[2913]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a_1 a a) True % 271.94/272.21 Clause #2928 (by superposition #[2925, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_1 a_1 a) True) % 271.94/272.21 Clause #2930 (by clausification #[2928]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a_1 a_1 a) True % 271.94/272.21 Clause #2932 (by superposition #[2930, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a a a_1) True) % 271.94/272.21 Clause #2993 (by clausification #[2932]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a a a_1) True % 271.94/272.21 Clause #2995 (by superposition #[2993, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.94/272.21 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) % 271.94/272.21 (Or (Eq True False) (Eq (eqratio a_1 a a a_1 a_2 a_3 a_4 a_5) False)) % 271.94/272.21 Clause #3091 (by clausification #[2995]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.94/272.21 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_1 a a a_1 a_2 a_3 a_4 a_5) False) % 271.94/272.21 Clause #3099 (by superposition #[3091, 2925]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True) (Eq False True) % 271.94/272.21 Clause #3271 (by clausification #[3099]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True % 271.94/272.21 Clause #3276 (by superposition #[3271, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a_1) True) % 271.94/272.21 Clause #3281 (by clausification #[3276]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a_1) True % 271.94/272.21 Clause #3284 (by superposition #[3281, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a a) True) % 271.94/272.21 Clause #3285 (by superposition #[3281, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a a_1) True) % 271.94/272.21 Clause #3341 (by clausification #[3284]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a) True % 271.94/272.21 Clause #3344 (by superposition #[3341, 3091]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_1 a_1) True) (Eq True False) % 271.94/272.21 Clause #3345 (by clausification #[3344]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_1 a_1) True % 271.94/272.21 Clause #3348 (by superposition #[3345, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a a a) True) % 271.94/272.21 Clause #3360 (by clausification #[3348]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a a) True % 271.94/272.21 Clause #3362 (by superposition #[3360, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.94/272.21 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Or (Eq True False) (Eq (eqratio a a a a a_2 a_3 a_4 a_5) False)) % 271.94/272.21 Clause #3382 (by clausification #[3285]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a a a_1) True % 271.94/272.21 Clause #3515 (by clausification #[3362]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 271.94/272.21 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Eq (eqratio a a a a a_2 a_3 a_4 a_5) False) % 271.94/272.21 Clause #3528 (by superposition #[3515, 3382]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a a_2 a a a_2) True) (Eq False True) % 271.94/272.21 Clause #3529 (by clausification #[3528]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a a a_2) True % 271.94/272.21 Clause #3533 (by superposition #[3529, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a a a_1) True) % 271.94/272.21 Clause #3539 (by clausification #[3533]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a a a_1) True % 271.94/272.21 Clause #3542 (by superposition #[3539, 722]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_2 a_1) True) % 271.94/272.21 Clause #3551 (by clausification #[3542]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_2 a_1) True % 271.94/272.21 Clause #3554 (by superposition #[3551, 667]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_1 a a a) True) % 271.94/272.24 Clause #3561 (by clausification #[3554]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_1 a a a) True % 271.94/272.24 Clause #3564 (by superposition #[3561, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_2 a a a) True) % 271.94/272.24 Clause #3567 (by clausification #[3564]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a a a) True % 271.94/272.24 Clause #3571 (by superposition #[3567, 3091]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_1 a_1) True) (Eq True False) % 271.94/272.24 Clause #3575 (by clausification #[3571]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_1 a_1) True % 271.94/272.24 Clause #3580 (by superposition #[3575, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_1 a_1) True) % 271.94/272.24 Clause #3582 (by clausification #[3580]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_1 a_1) True % 271.94/272.24 Clause #3585 (by superposition #[3582, 722]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_2 a) True) % 271.94/272.24 Clause #3587 (by clausification #[3585]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a a_2 a) True % 271.94/272.24 Clause #3590 (by superposition #[3587, 3515]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a_2 a a_3 a) True) (Eq True False) % 271.94/272.24 Clause #3591 (by clausification #[3590]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a_2 a a_3 a) True % 271.94/272.24 Clause #3593 (by superposition #[3591, 667]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_3 a_1) True) % 271.94/272.24 Clause #3600 (by clausification #[3593]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_3 a_1) True % 271.94/272.24 Clause #3603 (by superposition #[3600, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_1 a_1 a_1) True) % 271.94/272.24 Clause #3605 (by clausification #[3603]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_1 a_1 a_1) True % 271.94/272.24 Clause #3607 (by superposition #[3605, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_3 a a a) True) % 271.94/272.24 Clause #3609 (by clausification #[3607]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a_3 a a a) True % 271.94/272.24 Clause #3612 (by superposition #[3609, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_3 a_1) True) % 271.94/272.24 Clause #3614 (by clausification #[3612]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_3 a_1) True % 271.94/272.24 Clause #3618 (by superposition #[3614, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 271.94/272.24 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) % 271.94/272.24 (Or (Eq True False) (Eq (eqratio a_1 a_6 a_7 a_1 a_2 a_3 a_4 a_5) False)) % 271.94/272.24 Clause #3619 (by superposition #[3614, 3515]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a a_2 a_3 a) True) (Eq True False) % 271.94/272.24 Clause #3620 (by clausification #[3619]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a_3 a) True % 271.94/272.24 Clause #3624 (by superposition #[3620, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a a_3 a) True) % 271.94/272.24 Clause #3629 (by clausification #[3624]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a a_3 a) True % 271.94/272.24 Clause #3631 (by superposition #[3629, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_1 a_3) True) % 271.94/272.24 Clause #3634 (by clausification #[3631]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_1 a_3) True % 271.94/272.24 Clause #3637 (by superposition #[3634, 667]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_3 a_1 a_1) True) % 271.94/272.24 Clause #3641 (by clausification #[3637]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_3 a_1 a_1) True % 271.94/272.24 Clause #3644 (by superposition #[3641, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_3 a_1 a_1 a_1) True) % 271.94/272.24 Clause #3651 (by clausification #[3644]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_2 a_3 a_1 a_1 a_1) True % 271.94/272.24 Clause #3655 (by superposition #[3651, 3091]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a a a) True) (Eq True False) % 271.94/272.24 Clause #3656 (by clausification #[3655]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a a a) True % 272.00/272.26 Clause #3661 (by superposition #[3656, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_1 a_1 a a) True) % 272.00/272.26 Clause #3663 (by clausification #[3661]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_1 a_1 a a) True % 272.00/272.26 Clause #3666 (by superposition #[3663, 667]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_2 a_2) True) % 272.00/272.26 Clause #3688 (by clausification #[3666]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_2 a_2) True % 272.00/272.26 Clause #3690 (by superposition #[3688, 596]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a a_2 a_2) True) % 272.00/272.26 Clause #3692 (by clausification #[3690]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a a a_2 a_2) True % 272.00/272.26 Clause #3696 (by superposition #[3692, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_2 a_2 a_2) True) % 272.00/272.26 Clause #3698 (by clausification #[3696]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a a_2 a_2 a_2) True % 272.00/272.26 Clause #3703 (by superposition #[3698, 3515]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a a a_2 a_2 a_2) True) (Eq True False) % 272.00/272.26 Clause #3704 (by clausification #[3703]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a_2 a_2 a_2) True % 272.00/272.26 Clause #3706 (by superposition #[3704, 667]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_1 a_2) True) % 272.00/272.26 Clause #3721 (by clausification #[3706]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_1 a_2) True % 272.00/272.26 Clause #3723 (by superposition #[3721, 596]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_2 a a_2) True) % 272.00/272.26 Clause #3733 (by clausification #[3723]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_2 a_2 a a_2) True % 272.00/272.26 Clause #3737 (by superposition #[3733, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a a a_2) True) % 272.00/272.26 Clause #3742 (by clausification #[3737]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a a_2) True % 272.00/272.26 Clause #3745 (by superposition #[3742, 722]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a a_2 a_1 a_1) True) % 272.00/272.26 Clause #3747 (by clausification #[3745]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a a_2 a_1 a_1) True % 272.00/272.26 Clause #3749 (by superposition #[3747, 667]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a_1 a a_2) True) % 272.00/272.26 Clause #3751 (by clausification #[3749]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_1 a_1 a a_2) True % 272.00/272.26 Clause #3754 (by superposition #[3751, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a a a_2) True) % 272.00/272.26 Clause #3756 (by clausification #[3754]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a a a a_2) True % 272.00/272.26 Clause #3758 (by superposition #[3756, 596]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a_1 a_1 a_2) True) % 272.00/272.26 Clause #3760 (by clausification #[3758]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_1 a_1 a_1 a_2) True % 272.00/272.26 Clause #3763 (by superposition #[3760, 722]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a a_2 a_2) True) % 272.00/272.26 Clause #3770 (by clausification #[3763]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a a_2 a_2) True % 272.00/272.26 Clause #3773 (by superposition #[3770, 740]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a_1 a_1) True) % 272.00/272.26 Clause #3929 (by clausification #[3773]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a_2 a_1 a_1) True % 272.00/272.26 Clause #4253 (by clausification #[3618]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.00/272.26 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_1 a_6 a_7 a_1 a_2 a_3 a_4 a_5) False) % 272.00/272.26 Clause #4274 (by superposition #[4253, 3929]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_3 a_3) True) (Eq False True) % 272.00/272.26 Clause #4277 (by clausification #[4274]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_3 a_3) True % 272.00/272.26 Clause #4279 (by superposition #[4277, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_2 a_3 a_3) True) % 272.00/272.28 Clause #4284 (by superposition #[4277, 3515]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a a_2 a_3 a_3) True) (Eq True False) % 272.00/272.28 Clause #4289 (by clausification #[4284]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a_3 a_3) True % 272.00/272.28 Clause #4293 (by superposition #[4289, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a a_3 a_3) True) % 272.00/272.28 Clause #4295 (by clausification #[4293]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a a_3 a_3) True % 272.00/272.28 Clause #4298 (by superposition #[4295, 722]): ∀ (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_1 a_3) True) % 272.00/272.28 Clause #4302 (by superposition #[4295, 4253]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_3 a_3) True) (Eq True False) % 272.00/272.28 Clause #4303 (by clausification #[4302]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_3 a_3) True % 272.00/272.28 Clause #4308 (by superposition #[4303, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_3 a_3) True) % 272.00/272.28 Clause #4310 (by clausification #[4308]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_3 a_3) True % 272.00/272.28 Clause #4313 (by superposition #[4310, 667]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_3 a_1 a_1) True) % 272.00/272.28 Clause #4341 (by clausification #[4313]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_3 a_1 a_1) True % 272.00/272.28 Clause #4343 (by superposition #[4341, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_3 a_3 a a) True) % 272.00/272.28 Clause #4349 (by clausification #[4343]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a_3 a_3 a a) True % 272.00/272.28 Clause #4351 (by superposition #[4349, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_1 a_2 a_3 a_1) True) % 272.00/272.28 Clause #4354 (by clausification #[4351]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_1 a_2 a_3 a_1) True % 272.00/272.28 Clause #4357 (by superposition #[4354, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_1 a_1 a_3 a_1) True) % 272.00/272.28 Clause #4360 (by clausification #[4357]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a_1 a_1 a_3 a_1) True % 272.00/272.28 Clause #4363 (by superposition #[4360, 4253]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_2) True) (Eq True False) % 272.00/272.28 Clause #4364 (by clausification #[4363]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_2) True % 272.00/272.28 Clause #4368 (by superposition #[4364, 740]): ∀ (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_2) True) % 272.00/272.28 Clause #4415 (by clausification #[4368]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_3 a_2) True % 272.00/272.28 Clause #4478 (by clausification #[4298]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_1 a_3) True % 272.00/272.28 Clause #4480 (by superposition #[4478, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a a a_3) True) % 272.00/272.28 Clause #4493 (by clausification #[4480]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a a_3) True % 272.00/272.28 Clause #4497 (by superposition #[4493, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_2 a a_3) True) % 272.00/272.28 Clause #4499 (by clausification #[4497]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a a_2 a_2 a a_3) True % 272.00/272.28 Clause #4629 (by clausification #[4279]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a a a_2 a_3 a_3) True % 272.00/272.28 Clause #4632 (by superposition #[4629, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a_3 a a) True) % 272.00/272.28 Clause #4634 (by clausification #[4632]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a a_3 a a) True % 272.00/272.28 Clause #4638 (by superposition #[4634, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_3 a_3 a a) True) % 272.00/272.28 Clause #4640 (by clausification #[4638]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_2 a_3 a_3 a a) True % 272.00/272.28 Clause #4643 (by superposition #[4640, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_1 a_2 a_1 a_3) True) % 272.00/272.28 Clause #4645 (by clausification #[4643]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_1 a_2 a_1 a_3) True % 272.00/272.30 Clause #4647 (by superposition #[4645, 667]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_2 a a_3) True) % 272.00/272.30 Clause #4654 (by clausification #[4647]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a a_2 a a_3) True % 272.00/272.30 Clause #4656 (by superposition #[4654, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.00/272.30 Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) % 272.00/272.30 (Or (Eq True False) (Eq (eqratio a a_6 a a_7 a_2 a_3 a_4 a_5) False)) % 272.00/272.30 Clause #4912 (by clausification #[4656]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.00/272.30 Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a a_6 a a_7 a_2 a_3 a_4 a_5) False) % 272.00/272.30 Clause #4931 (by superposition #[4912, 4499]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_2 a a_3) True) (Eq False True) % 272.00/272.30 Clause #4934 (by clausification #[4931]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_2 a a_3) True % 272.00/272.30 Clause #4937 (by superposition #[4934, 722]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_1 a_1 a_3 a_3) True) % 272.00/272.30 Clause #4942 (by clausification #[4937]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a_1 a_1 a_3 a_3) True % 272.00/272.30 Clause #4944 (by superposition #[4942, 667]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a a) True) % 272.00/272.30 Clause #4948 (by clausification #[4944]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a a) True % 272.00/272.30 Clause #4950 (by superposition #[4948, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_1 a_1) True) % 272.00/272.30 Clause #4959 (by clausification #[4950]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_1 a_1) True % 272.00/272.30 Clause #4964 (by superposition #[4959, 4912]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_2 a_3 a_3) True) (Eq True False) % 272.00/272.30 Clause #4965 (by clausification #[4964]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_2 a_3 a_3) True % 272.00/272.30 Clause #4968 (by superposition #[4965, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.00/272.30 Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) % 272.00/272.30 (Or (Eq True False) (Eq (eqratio a_6 a_6 a_7 a_7 a_2 a_3 a_4 a_5) False)) % 272.00/272.30 Clause #5016 (by clausification #[4968]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.00/272.30 Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_6 a_6 a_7 a_7 a_2 a_3 a_4 a_5) False) % 272.00/272.30 Clause #5023 (by superposition #[5016, 4415]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_2 a_3 a_4) True) (Eq False True) % 272.00/272.30 Clause #5024 (by clausification #[5023]): ∀ (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 % 272.00/272.30 Clause #5031 (by superposition #[5024, 4253]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_4) True) (Eq True False) % 272.00/272.30 Clause #5034 (by clausification #[5031]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_2 a_3 a_4) True % 272.00/272.30 Clause #5039 (by superposition #[5034, 740]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_3 a_4) True) % 272.00/272.30 Clause #5041 (by clausification #[5039]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_2 a_1 a_1 a_3 a_4) True % 272.00/272.30 Clause #5048 (by superposition #[5041, 3515]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a a a_2 a_3) True) (Eq True False) % 272.00/272.30 Clause #5049 (by clausification #[5048]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a a_2 a_3) True % 272.00/272.30 Clause #5053 (by superposition #[5049, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_2 a_3) True) % 272.00/272.30 Clause #5064 (by clausification #[5053]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a_1 a a_2 a_3) True % 272.00/272.30 Clause #5073 (by superposition #[5064, 5016]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq True False) % 272.00/272.30 Clause #5074 (by clausification #[5073]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True % 272.00/272.30 Clause #5078 (by superposition #[5074, 740]): ∀ (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_3 a_4 a_5) True) % 272.05/272.32 Clause #5081 (by superposition #[5074, 4253]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq True False) % 272.05/272.32 Clause #5082 (by clausification #[5081]): ∀ (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 % 272.05/272.32 Clause #5087 (by superposition #[5082, 740]): ∀ (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) % 272.05/272.32 Clause #5089 (by clausification #[5087]): ∀ (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 % 272.05/272.32 Clause #5091 (by superposition #[5089, 596]): ∀ (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 a a_4 a_5) True) % 272.05/272.32 Clause #5213 (by clausification #[5091]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a a a_4 a_5) True % 272.05/272.32 Clause #5215 (by superposition #[5213, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 272.05/272.32 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 272.05/272.32 (Or (Eq True False) (Eq (eqratio a a a_8 a_9 a_4 a_5 a_6 a_7) False)) % 272.05/272.32 Clause #5241 (by clausification #[5078]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_3 a_4 a_5) True % 272.05/272.32 Clause #5315 (by clausification #[5215]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 272.05/272.32 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqratio a a a_8 a_9 a_4 a_5 a_6 a_7) False) % 272.05/272.32 Clause #5326 (by superposition #[5315, 5241]): ∀ (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_4 a_5 a_6) True) (Eq False True) % 272.05/272.32 Clause #5327 (by clausification #[5326]): ∀ (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_4 a_5 a_6) True % 272.05/272.32 Clause #5332 (by superposition #[5327, 740]): ∀ (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_2 a_3 a_4 a_5 a_6) True) % 272.05/272.32 Clause #5338 (by clausification #[5332]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_6) True % 272.05/272.32 Clause #5341 (by superposition #[5338, 5315]): ∀ (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) % 272.05/272.32 Clause #5342 (by clausification #[5341]): ∀ (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 % 272.05/272.32 Clause #5343 (by superposition #[5342, 467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 272.05/272.32 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)) % 272.05/272.32 Clause #5356 (by clausification #[5343]): ∀ (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) % 272.05/272.32 Clause #5953 (by clausification #[2233]): ∀ (a a_1 a_2 : Iota), % 272.05/272.32 Or (Eq (cong a a_1 a a_1) True) % 272.05/272.32 (Or (Eq (cyclic a a_1 a_1 a_2) False) (Or (Eq (cyclic a a_1 a_1 a) False) (Eq (cyclic a a_1 a_1 a_1) False))) % 272.05/272.32 Clause #5954 (by superposition #[5953, 2310]): ∀ (a a_1 : Iota), % 272.05/272.32 Or (Eq (cong a a_1 a a_1) True) % 272.05/272.32 (Or (Eq (cyclic a a_1 a_1 a) False) (Or (Eq (cyclic a a_1 a_1 a_1) False) (Eq False True))) % 272.05/272.32 Clause #5955 (by clausification #[5954]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Or (Eq (cyclic a a_1 a_1 a) False) (Eq (cyclic a a_1 a_1 a_1) False)) % 272.05/272.32 Clause #5956 (by superposition #[5955, 2310]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Or (Eq (cyclic a a_1 a_1 a_1) False) (Eq False True)) % 272.05/272.32 Clause #5957 (by clausification #[5956]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq (cyclic a a_1 a_1 a_1) False) % 272.05/272.32 Clause #5958 (by superposition #[5957, 2310]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq False True) % 272.05/272.32 Clause #5959 (by clausification #[5958]): ∀ (a a_1 : Iota), Eq (cong a a_1 a a_1) True % 272.05/272.32 Clause #5967 (by superposition #[5959, 5356]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False) % 272.05/272.32 Clause #6006 (by clausification #[5967]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True % 272.05/272.32 Clause #6010 (by superposition #[6006, 212]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a a_3 a_1 a_3) False)) % 272.05/272.32 Clause #9821 (by clausification #[6010]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Eq (cong a a_3 a_1 a_3) False) % 272.19/272.48 Clause #9822 (by superposition #[9821, 6006]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Eq False True) % 272.19/272.48 Clause #9823 (by clausification #[9822]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3) True % 272.19/272.48 Clause #9843 (by superposition #[9823, 631]): Eq True False % 272.19/272.48 Clause #9849 (by clausification #[9843]): False % 272.19/272.48 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------