%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO598+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:44 PM UTC 2025 % Result : Theorem 150.14s 150.34s % Output : Proof 150.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : GEO598+1 : TPTP v9.2.0. Released v7.5.0. % 0.07/0.15 % Command : duper %s % 0.14/0.37 % Computer : n001.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Fri Oct 3 12:17:53 EDT 2025 % 0.14/0.37 % CPUTime : % 150.14/150.34 SZS status Theorem for theBenchmark.p % 150.14/150.34 SZS output start Proof for theBenchmark.p % 150.14/150.34 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 150.14/150.34 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 150.14/150.34 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 150.14/150.34 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 150.14/150.34 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 150.14/150.34 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 150.14/150.34 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 % 150.14/150.34 Clause #13 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A B D C) True % 150.14/150.34 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 Clause #21 (by assumption #[]): Eq % 150.14/150.34 (∀ (A B C D P Q U V E F G H : Iota), % 150.14/150.34 And (eqangle A B C D P Q U V) (eqangle P Q U V E F G H) → eqangle A B C D E F G H) % 150.14/150.34 True % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 Clause #29 (by assumption #[]): Eq % 150.14/150.34 (∀ (A B C D E F G H P Q U V : Iota), % 150.14/150.34 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) % 150.14/150.34 True % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 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 % 150.14/150.34 Clause #43 (by assumption #[]): Eq % 150.14/150.34 (∀ (A B C P Q R : Iota), % 150.14/150.34 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) % 150.14/150.34 True % 150.14/150.34 Clause #46 (by assumption #[]): Eq (∀ (A B O : Iota), cong O A O B → eqangle O A A B A B O B) True % 150.14/150.34 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 % 150.14/150.34 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 150.14/150.34 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 % 150.14/150.34 Clause #94 (by assumption #[]): Eq % 150.14/150.34 (Not % 150.14/150.34 (∀ (A B C D E F G H I NWPNT1 : Iota), % 150.14/150.34 And % 150.14/150.34 (And % 150.14/150.34 (And (And (And (And (And (circle D A B C) (midp E C B)) (midp F A C)) (midp G B A)) (coll H D G)) % 150.14/150.34 (circle D A H NWPNT1)) % 150.14/150.34 (perp I H A C)) % 150.14/150.34 (coll I A C) → % 150.14/150.34 eqangle F G G I I G G E)) % 150.14/150.34 True % 150.14/150.34 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 150.14/150.34 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 150.17/150.36 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 % 150.17/150.36 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) % 150.17/150.36 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 150.17/150.36 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 150.17/150.36 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 % 150.17/150.36 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) % 150.17/150.36 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 150.17/150.36 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 150.17/150.36 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 % 150.17/150.36 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) % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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) % 150.17/150.36 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)) % 150.17/150.36 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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) % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 150.17/150.36 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) % 150.17/150.36 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 150.17/150.36 Or (Eq (cyclic a a_1 a_2 a_3) True) % 150.17/150.36 (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)) % 150.17/150.36 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.36 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 % 150.17/150.39 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) % 150.17/150.39 Clause #180 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a B D C) True % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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) % 150.17/150.39 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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) % 150.17/150.39 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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) % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.17/150.39 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) % 150.17/150.39 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.17/150.39 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)) % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.39 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 % 150.17/150.42 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.17/150.42 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) % 150.17/150.42 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.17/150.42 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)) % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.17/150.42 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 % 150.17/150.42 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.17/150.42 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 % 150.17/150.42 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.17/150.42 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 % 150.17/150.42 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.17/150.42 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 % 150.17/150.42 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.17/150.42 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) % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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 % 150.17/150.42 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) % 150.17/150.42 Clause #360 (by clausification #[43]): ∀ (a : Iota), % 150.17/150.42 Eq % 150.17/150.42 (∀ (B C P Q R : Iota), % 150.17/150.42 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) % 150.17/150.42 True % 150.17/150.42 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 150.17/150.42 Eq % 150.17/150.42 (∀ (C P Q R : Iota), % 150.17/150.42 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) → % 150.17/150.42 cong a a_1 P Q) % 150.17/150.42 True % 150.17/150.42 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota), % 150.17/150.42 Eq % 150.17/150.42 (∀ (P Q R : Iota), % 150.17/150.42 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) → % 150.17/150.42 cong a a_1 P Q) % 150.17/150.42 True % 150.17/150.42 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 150.17/150.42 Eq % 150.17/150.42 (∀ (Q R : Iota), % 150.17/150.42 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)) % 150.17/150.42 (eqangle a_2 a a_2 a_1 R a_3 R Q) → % 150.17/150.42 cong a a_1 a_3 Q) % 150.17/150.42 True % 150.17/150.42 Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.17/150.42 Eq % 150.17/150.42 (∀ (R : Iota), % 150.17/150.42 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)) % 150.17/150.42 (eqangle a_2 a a_2 a_1 R a_3 R a_4) → % 150.23/150.45 cong a a_1 a_3 a_4) % 150.23/150.45 True % 150.23/150.45 Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 Eq % 150.23/150.45 (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)) % 150.23/150.45 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4) → % 150.23/150.45 cong a a_1 a_3 a_4) % 150.23/150.45 True % 150.23/150.45 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 Or % 150.23/150.45 (Eq % 150.23/150.45 (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)) % 150.23/150.45 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4)) % 150.23/150.45 False) % 150.23/150.45 (Eq (cong a a_1 a_3 a_4) True) % 150.23/150.45 Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 Or (Eq (cong a a_1 a_2 a_3) True) % 150.23/150.45 (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) % 150.23/150.45 (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)) % 150.23/150.45 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 Or (Eq (cong a a_1 a_2 a_3) True) % 150.23/150.45 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 150.23/150.45 (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))) % 150.23/150.45 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 Or (Eq (cong a a_1 a_2 a_3) True) % 150.23/150.45 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 150.23/150.45 (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)))) % 150.23/150.45 Clause #385 (by clausification #[46]): ∀ (a : Iota), Eq (∀ (B O : Iota), cong O a O B → eqangle O a a B a B O B) True % 150.23/150.45 Clause #386 (by clausification #[385]): ∀ (a a_1 : Iota), Eq (∀ (O : Iota), cong O a O a_1 → eqangle O a a a_1 a a_1 O a_1) True % 150.23/150.45 Clause #387 (by clausification #[386]): ∀ (a a_1 a_2 : Iota), Eq (cong a a_1 a a_2 → eqangle a a_1 a_1 a_2 a_1 a_2 a a_2) True % 150.23/150.45 Clause #388 (by clausification #[387]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a_1 a a_2) False) (Eq (eqangle a a_1 a_1 a_2 a_1 a_2 a a_2) True) % 150.23/150.45 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 % 150.23/150.45 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 % 150.23/150.45 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 % 150.23/150.45 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 % 150.23/150.45 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.23/150.45 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 % 150.23/150.45 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.23/150.45 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 % 150.23/150.45 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.23/150.45 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 % 150.23/150.45 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.23/150.45 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 % 150.23/150.45 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.23/150.45 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) % 150.23/150.45 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 % 150.23/150.45 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 % 150.23/150.45 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 % 150.23/150.45 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 % 150.27/150.47 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.47 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 % 150.27/150.47 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.27/150.47 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 % 150.27/150.47 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.27/150.47 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 % 150.27/150.47 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.47 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 % 150.27/150.47 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.47 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) % 150.27/150.47 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 % 150.27/150.48 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 % 150.27/150.48 Clause #460 (by clausification #[459]): ∀ (a a_1 a_2 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #461 (by clausification #[460]): ∀ (a a_1 a_2 a_3 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #462 (by clausification #[461]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.48 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) % 150.27/150.48 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.48 Or (Eq (cong a a_1 a_2 a_3) True) % 150.27/150.48 (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)) % 150.27/150.48 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 % 150.27/150.48 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 % 150.27/150.48 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 % 150.27/150.48 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 % 150.27/150.48 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.48 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 % 150.27/150.48 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.50 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) % 150.27/150.50 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 % 150.27/150.50 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 % 150.27/150.50 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 % 150.27/150.50 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 % 150.27/150.50 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) % 150.27/150.50 Clause #533 (by clausification #[21]): ∀ (a : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (B C D P Q U V E F G H : Iota), % 150.27/150.50 And (eqangle a B C D P Q U V) (eqangle P Q U V E F G H) → eqangle a B C D E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #534 (by clausification #[533]): ∀ (a a_1 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (C D P Q U V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 C D P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 C D E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #535 (by clausification #[534]): ∀ (a a_1 a_2 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (D P Q U V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 a_2 D P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 a_2 D E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #536 (by clausification #[535]): ∀ (a a_1 a_2 a_3 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (P Q U V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 a_2 a_3 P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #537 (by clausification #[536]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (Q U V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 a_2 a_3 a_4 Q U V) (eqangle a_4 Q U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #538 (by clausification #[537]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (U V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 a_2 a_3 a_4 a_5 U V) (eqangle a_4 a_5 U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #539 (by clausification #[538]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (V E F G H : Iota), % 150.27/150.50 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V) (eqangle a_4 a_5 a_6 V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #540 (by clausification #[539]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (E F G H : Iota), % 150.27/150.50 And (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 E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 150.27/150.50 True % 150.27/150.50 Clause #541 (by clausification #[540]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (F G H : Iota), % 150.27/150.50 And (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_8 F G H) → eqangle a a_1 a_2 a_3 a_8 F G H) % 150.27/150.50 True % 150.27/150.50 Clause #542 (by clausification #[541]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (G H : Iota), % 150.27/150.50 And (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_8 a_9 G H) → % 150.27/150.50 eqangle a a_1 a_2 a_3 a_8 a_9 G H) % 150.27/150.50 True % 150.27/150.50 Clause #543 (by clausification #[542]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (∀ (H : Iota), % 150.27/150.50 And (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_8 a_9 a_10 H) → % 150.27/150.50 eqangle a a_1 a_2 a_3 a_8 a_9 a_10 H) % 150.27/150.50 True % 150.27/150.50 Clause #544 (by clausification #[543]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 150.27/150.50 Eq % 150.27/150.50 (And (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_8 a_9 a_10 a_11) → % 150.27/150.50 eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 150.27/150.50 True % 150.27/150.50 Clause #545 (by clausification #[544]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 150.27/150.50 Or (Eq (And (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_8 a_9 a_10 a_11)) False) % 150.27/150.50 (Eq (eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 150.27/150.50 Clause #546 (by clausification #[545]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 150.27/150.50 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 150.27/150.53 (Or (Eq (eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) False) (Eq (eqangle a_8 a_9 a_10 a_11 a_4 a_5 a_6 a_7) False)) % 150.27/150.53 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 % 150.27/150.53 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #549 (by clausification #[548]): ∀ (a a_1 a_2 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #550 (by clausification #[549]): ∀ (a a_1 a_2 a_3 : Iota), % 150.27/150.53 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) % 150.27/150.53 True % 150.27/150.53 Clause #551 (by clausification #[550]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.53 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) % 150.27/150.53 (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True) % 150.27/150.53 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.53 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 150.27/150.53 (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)) % 150.27/150.53 Clause #554 (by clausification #[553]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.53 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 150.27/150.53 (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))) % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 Clause #592 (by clausification #[591]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #593 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #594 (by clausification #[593]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #595 (by clausification #[594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.53 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 % 150.27/150.53 Clause #596 (by clausification #[595]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.27/150.53 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) % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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 % 150.27/150.53 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) % 150.34/150.55 Clause #641 (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 % 150.34/150.55 Clause #642 (by clausification #[641]): ∀ (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 % 150.34/150.55 Clause #643 (by clausification #[642]): ∀ (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 % 150.34/150.55 Clause #644 (by clausification #[643]): ∀ (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 % 150.34/150.55 Clause #645 (by clausification #[644]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #646 (by clausification #[645]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #647 (by clausification #[646]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #648 (by clausification #[647]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #649 (by clausification #[648]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.34/150.55 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) % 150.34/150.55 Clause #694 (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 % 150.34/150.55 Clause #695 (by clausification #[694]): ∀ (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 % 150.34/150.55 Clause #696 (by clausification #[695]): ∀ (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 % 150.34/150.55 Clause #697 (by clausification #[696]): ∀ (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 % 150.34/150.55 Clause #698 (by clausification #[697]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #699 (by clausification #[698]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #700 (by clausification #[699]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #701 (by clausification #[700]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #702 (by clausification #[701]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.34/150.55 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) % 150.34/150.55 Clause #703 (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 % 150.34/150.55 Clause #704 (by clausification #[703]): ∀ (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 % 150.34/150.55 Clause #705 (by clausification #[704]): ∀ (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 % 150.34/150.55 Clause #706 (by clausification #[705]): ∀ (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 % 150.34/150.55 Clause #707 (by clausification #[706]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.34/150.55 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 % 150.34/150.55 Clause #708 (by clausification #[707]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.34/150.55 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 % 150.37/150.58 Clause #709 (by clausification #[708]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.37/150.58 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 % 150.37/150.58 Clause #710 (by clausification #[709]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.37/150.58 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 % 150.37/150.58 Clause #711 (by clausification #[710]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.37/150.58 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) % 150.37/150.58 Clause #749 (by clausification #[94]): Eq % 150.37/150.58 (∀ (A B C D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And (And (And (And (And (circle D A B C) (midp E C B)) (midp F A C)) (midp G B A)) (coll H D G)) % 150.37/150.58 (circle D A H NWPNT1)) % 150.37/150.58 (perp I H A C)) % 150.37/150.58 (coll I A C) → % 150.37/150.58 eqangle F G G I I G G E) % 150.37/150.58 False % 150.37/150.58 Clause #750 (by clausification #[749]): ∀ (a : Iota), % 150.37/150.58 Eq % 150.37/150.58 (Not % 150.37/150.58 (∀ (B C D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And (And (And (circle D (skS.0 13 a) B C) (midp E C B)) (midp F (skS.0 13 a) C)) % 150.37/150.58 (midp G B (skS.0 13 a))) % 150.37/150.58 (coll H D G)) % 150.37/150.58 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.58 (perp I H (skS.0 13 a) C)) % 150.37/150.58 (coll I (skS.0 13 a) C) → % 150.37/150.58 eqangle F G G I I G G E)) % 150.37/150.58 True % 150.37/150.58 Clause #751 (by clausification #[750]): ∀ (a : Iota), % 150.37/150.58 Eq % 150.37/150.58 (∀ (B C D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And (And (And (circle D (skS.0 13 a) B C) (midp E C B)) (midp F (skS.0 13 a) C)) % 150.37/150.58 (midp G B (skS.0 13 a))) % 150.37/150.58 (coll H D G)) % 150.37/150.58 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.58 (perp I H (skS.0 13 a) C)) % 150.37/150.58 (coll I (skS.0 13 a) C) → % 150.37/150.58 eqangle F G G I I G G E) % 150.37/150.58 False % 150.37/150.58 Clause #752 (by clausification #[751]): ∀ (a a_1 : Iota), % 150.37/150.58 Eq % 150.37/150.58 (Not % 150.37/150.58 (∀ (C D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And (And (circle D (skS.0 13 a) (skS.0 14 a a_1) C) (midp E C (skS.0 14 a a_1))) % 150.37/150.58 (midp F (skS.0 13 a) C)) % 150.37/150.58 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.58 (coll H D G)) % 150.37/150.58 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.58 (perp I H (skS.0 13 a) C)) % 150.37/150.58 (coll I (skS.0 13 a) C) → % 150.37/150.58 eqangle F G G I I G G E)) % 150.37/150.58 True % 150.37/150.58 Clause #753 (by clausification #[752]): ∀ (a a_1 : Iota), % 150.37/150.58 Eq % 150.37/150.58 (∀ (C D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And (And (circle D (skS.0 13 a) (skS.0 14 a a_1) C) (midp E C (skS.0 14 a a_1))) % 150.37/150.58 (midp F (skS.0 13 a) C)) % 150.37/150.58 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.58 (coll H D G)) % 150.37/150.58 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.58 (perp I H (skS.0 13 a) C)) % 150.37/150.58 (coll I (skS.0 13 a) C) → % 150.37/150.58 eqangle F G G I I G G E) % 150.37/150.58 False % 150.37/150.58 Clause #754 (by clausification #[753]): ∀ (a a_1 a_2 : Iota), % 150.37/150.58 Eq % 150.37/150.58 (Not % 150.37/150.58 (∀ (D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And % 150.37/150.58 (And (circle D (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.58 (midp E (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.58 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.58 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.58 (coll H D G)) % 150.37/150.58 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.58 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.58 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.58 eqangle F G G I I G G E)) % 150.37/150.58 True % 150.37/150.58 Clause #755 (by clausification #[754]): ∀ (a a_1 a_2 : Iota), % 150.37/150.58 Eq % 150.37/150.58 (∀ (D E F G H I NWPNT1 : Iota), % 150.37/150.58 And % 150.37/150.58 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And (circle D (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.60 (midp E (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.60 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.60 (coll H D G)) % 150.37/150.60 (circle D (skS.0 13 a) H NWPNT1)) % 150.37/150.60 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.60 eqangle F G G I I G G E) % 150.37/150.60 False % 150.37/150.60 Clause #756 (by clausification #[755]): ∀ (a a_1 a_2 a_3 : Iota), % 150.37/150.60 Eq % 150.37/150.60 (Not % 150.37/150.60 (∀ (E F G H I NWPNT1 : Iota), % 150.37/150.60 And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.60 (midp E (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.60 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.60 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.60 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.60 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.60 eqangle F G G I I G G E)) % 150.37/150.60 True % 150.37/150.60 Clause #757 (by clausification #[756]): ∀ (a a_1 a_2 a_3 : Iota), % 150.37/150.60 Eq % 150.37/150.60 (∀ (E F G H I NWPNT1 : Iota), % 150.37/150.60 And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.60 (midp E (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.60 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.60 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.60 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.60 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.60 eqangle F G G I I G G E) % 150.37/150.60 False % 150.37/150.60 Clause #758 (by clausification #[757]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.37/150.60 Eq % 150.37/150.60 (Not % 150.37/150.60 (∀ (F G H I NWPNT1 : Iota), % 150.37/150.60 And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.60 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.60 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.60 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.60 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.60 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.60 eqangle F G G I I G G (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.37/150.60 True % 150.37/150.60 Clause #759 (by clausification #[758]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.37/150.60 Eq % 150.37/150.60 (∀ (F G H I NWPNT1 : Iota), % 150.37/150.60 And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And % 150.37/150.60 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.60 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.60 (midp F (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.60 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.60 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.60 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.60 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.60 eqangle F G G I I G G (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.37/150.60 False % 150.37/150.60 Clause #760 (by clausification #[759]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.37/150.60 Eq % 150.37/150.60 (Not % 150.37/150.60 (∀ (G H I NWPNT1 : Iota), % 150.37/150.62 And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.62 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.62 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.62 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.62 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.62 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.62 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) G G I I G G (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.37/150.62 True % 150.37/150.62 Clause #761 (by clausification #[760]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.37/150.62 Eq % 150.37/150.62 (∀ (G H I NWPNT1 : Iota), % 150.37/150.62 And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.62 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.62 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (midp G (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.62 (coll H (skS.0 16 a a_1 a_2 a_3) G)) % 150.37/150.62 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.62 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.62 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) G G I I G G (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.37/150.62 False % 150.37/150.62 Clause #762 (by clausification #[761]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.37/150.62 Eq % 150.37/150.62 (Not % 150.37/150.62 (∀ (H I NWPNT1 : Iota), % 150.37/150.62 And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.62 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.62 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.62 (coll H (skS.0 16 a a_1 a_2 a_3) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.37/150.62 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.62 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.62 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.37/150.62 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) I I (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.37/150.62 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.37/150.62 True % 150.37/150.62 Clause #763 (by clausification #[762]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.37/150.62 Eq % 150.37/150.62 (∀ (H I NWPNT1 : Iota), % 150.37/150.62 And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And % 150.37/150.62 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.37/150.62 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.37/150.62 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.37/150.62 (coll H (skS.0 16 a a_1 a_2 a_3) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.37/150.62 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) H NWPNT1)) % 150.37/150.62 (perp I H (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.37/150.62 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.37/150.62 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.37/150.62 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) I I (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.37/150.62 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.46/150.65 False % 150.46/150.65 Clause #764 (by clausification #[763]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.46/150.65 Eq % 150.46/150.65 (Not % 150.46/150.65 (∀ (I NWPNT1 : Iota), % 150.46/150.65 And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.65 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.65 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.65 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.65 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.65 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) NWPNT1)) % 150.46/150.65 (perp I (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.65 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.46/150.65 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) I I (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.46/150.65 True % 150.46/150.65 Clause #765 (by clausification #[764]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.46/150.65 Eq % 150.46/150.65 (∀ (I NWPNT1 : Iota), % 150.46/150.65 And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.65 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.65 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.65 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.65 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.65 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) NWPNT1)) % 150.46/150.65 (perp I (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.65 (coll I (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.46/150.65 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) I I (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.46/150.65 False % 150.46/150.65 Clause #766 (by clausification #[765]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.46/150.65 Eq % 150.46/150.65 (Not % 150.46/150.65 (∀ (NWPNT1 : Iota), % 150.46/150.65 And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And % 150.46/150.65 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.65 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.65 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.65 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.65 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.65 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) NWPNT1)) % 150.46/150.65 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.46/150.65 (skS.0 15 a a_1 a_2))) % 150.46/150.65 (coll (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.46/150.65 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.46/150.65 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.65 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.46/150.67 True % 150.46/150.67 Clause #767 (by clausification #[766]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.46/150.67 Eq % 150.46/150.67 (∀ (NWPNT1 : Iota), % 150.46/150.67 And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.67 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.67 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.67 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.67 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.67 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) NWPNT1)) % 150.46/150.67 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.46/150.67 (skS.0 15 a a_1 a_2))) % 150.46/150.67 (coll (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.46/150.67 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.46/150.67 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.46/150.67 False % 150.46/150.67 Clause #768 (by clausification #[767]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.46/150.67 Eq % 150.46/150.67 (Not % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.67 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.67 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.67 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.67 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.67 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.46/150.67 (skS.0 22 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 150.46/150.67 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.46/150.67 (skS.0 15 a a_1 a_2))) % 150.46/150.67 (coll (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.46/150.67 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.46/150.67 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4))) % 150.46/150.67 True % 150.46/150.67 Clause #769 (by clausification #[768]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.46/150.67 Eq % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And % 150.46/150.67 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.46/150.67 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.46/150.67 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.46/150.67 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.46/150.67 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.46/150.67 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.46/150.67 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.46/150.67 (skS.0 22 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 150.46/150.67 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.46/150.67 (skS.0 15 a a_1 a_2))) % 150.49/150.70 (coll (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) (skS.0 15 a a_1 a_2)) → % 150.49/150.70 eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.49/150.70 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.49/150.70 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.49/150.70 False % 150.49/150.70 Clause #770 (by clausification #[769]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.49/150.70 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.49/150.70 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.49/150.70 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.49/150.70 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) % 150.49/150.70 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.49/150.70 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.49/150.70 (skS.0 22 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 150.49/150.70 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.49/150.70 (skS.0 15 a a_1 a_2))) % 150.49/150.70 (coll (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.49/150.70 True % 150.49/150.70 Clause #771 (by clausification #[769]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (eqangle (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) % 150.49/150.70 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.49/150.70 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 17 a a_1 a_2 a_3 a_4)) % 150.49/150.70 False % 150.49/150.70 Clause #773 (by clausification #[770]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And % 150.49/150.70 (And (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 14 a a_1) (skS.0 15 a a_1 a_2)) % 150.49/150.70 (midp (skS.0 17 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 150.49/150.70 (midp (skS.0 18 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a) (skS.0 15 a a_1 a_2))) % 150.49/150.70 (midp (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 14 a a_1) (skS.0 13 a))) % 150.49/150.70 (coll (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 16 a a_1 a_2 a_3) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6))) % 150.49/150.70 (circle (skS.0 16 a a_1 a_2 a_3) (skS.0 13 a) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.49/150.70 (skS.0 22 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 150.49/150.70 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.49/150.70 (skS.0 15 a a_1 a_2))) % 150.49/150.70 True % 150.49/150.70 Clause #782 (by clausification #[29]): ∀ (a : Iota), % 150.49/150.70 Eq % 150.49/150.70 (∀ (B C D E F G H P Q U V : Iota), % 150.49/150.70 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) % 150.49/150.70 True % 150.49/150.70 Clause #783 (by clausification #[782]): ∀ (a a_1 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (∀ (C D E F G H P Q U V : Iota), % 150.49/150.70 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) % 150.49/150.70 True % 150.49/150.70 Clause #784 (by clausification #[783]): ∀ (a a_1 a_2 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (∀ (D E F G H P Q U V : Iota), % 150.49/150.70 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) % 150.49/150.70 True % 150.49/150.70 Clause #785 (by clausification #[784]): ∀ (a a_1 a_2 a_3 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (∀ (E F G H P Q U V : Iota), % 150.49/150.70 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) % 150.49/150.70 True % 150.49/150.70 Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.49/150.70 Eq % 150.49/150.70 (∀ (F G H P Q U V : Iota), % 150.49/150.70 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) % 150.49/150.70 True % 150.49/150.70 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (G H P Q U V : Iota), % 150.49/150.72 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 G H) → eqratio a a_1 a_2 a_3 a_4 a_5 G H) % 150.49/150.72 True % 150.49/150.72 Clause #788 (by clausification #[787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (H P Q U V : Iota), % 150.49/150.72 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 H) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 H) % 150.49/150.72 True % 150.49/150.72 Clause #789 (by clausification #[788]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (P Q U V : Iota), % 150.49/150.72 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 a_7) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.49/150.72 True % 150.49/150.72 Clause #790 (by clausification #[789]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (Q U V : Iota), % 150.49/150.72 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) % 150.49/150.72 True % 150.49/150.72 Clause #791 (by clausification #[790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (U V : Iota), % 150.49/150.72 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) → % 150.49/150.72 eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9) % 150.49/150.72 True % 150.49/150.72 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 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (∀ (V : Iota), % 150.49/150.72 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) → % 150.49/150.72 eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10) % 150.49/150.72 True % 150.49/150.72 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), % 150.49/150.72 Eq % 150.49/150.72 (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) → % 150.49/150.72 eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 150.49/150.72 True % 150.49/150.72 Clause #794 (by clausification #[793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 150.49/150.72 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) % 150.49/150.72 (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 150.49/150.72 Clause #795 (by clausification #[794]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 150.49/150.72 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 150.49/150.72 (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)) % 150.49/150.72 Clause #945 (by clausification #[773]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (perp (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 13 a) % 150.49/150.72 (skS.0 15 a a_1 a_2)) % 150.49/150.72 True % 150.49/150.72 Clause #948 (by superposition #[945, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Or (Eq True False) % 150.49/150.72 (Eq % 150.49/150.72 (perp (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.49/150.72 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 150.49/150.72 True) % 150.49/150.72 Clause #1572 (by clausification #[948]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (perp (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 150.49/150.72 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 150.49/150.72 True % 150.49/150.72 Clause #1573 (by superposition #[1572, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Or (Eq True False) % 150.49/150.72 (Eq % 150.49/150.72 (perp (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.49/150.72 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 150.49/150.72 True) % 150.49/150.72 Clause #1594 (by clausification #[1573]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Eq % 150.49/150.72 (perp (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 150.49/150.72 (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 150.49/150.72 True % 150.49/150.72 Clause #1595 (by superposition #[1594, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.49/150.72 Or (Eq True False) % 150.49/150.72 (Eq % 150.49/150.72 (perp (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) % 150.49/150.72 (skS.0 15 a a_1 a_2)) % 150.49/150.72 True) % 150.49/150.72 Clause #1596 (by superposition #[1594, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 150.49/150.72 Or (Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4) True) % 150.49/150.72 (Or (Eq True False) % 150.49/150.72 (Eq (perp (skS.0 20 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 21 a a_1 a_2 a_5 a_6 a_7 a_8 a_9 a_10) a_3 a_4) False)) % 150.55/150.75 Clause #1605 (by clausification #[1595]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.55/150.75 Eq % 150.55/150.75 (perp (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 13 a) % 150.55/150.75 (skS.0 15 a a_1 a_2)) % 150.55/150.75 True % 150.55/150.75 Clause #1606 (by superposition #[1605, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq % 150.55/150.75 (perp (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 15 a a_1 a_2) % 150.55/150.75 (skS.0 13 a)) % 150.55/150.75 True) % 150.55/150.75 Clause #1616 (by clausification #[1606]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 150.55/150.75 Eq % 150.55/150.75 (perp (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 21 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 15 a a_1 a_2) % 150.55/150.75 (skS.0 13 a)) % 150.55/150.75 True % 150.55/150.75 Clause #1687 (by clausification #[1596]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 150.55/150.75 Or (Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4) True) % 150.55/150.75 (Eq (perp (skS.0 20 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 21 a a_1 a_2 a_5 a_6 a_7 a_8 a_9 a_10) a_3 a_4) False) % 150.55/150.75 Clause #1689 (by superposition #[1687, 1616]): ∀ (a a_1 a_2 : Iota), % 150.55/150.75 Or (Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 15 a a_1 a_2) (skS.0 13 a)) True) (Eq False True) % 150.55/150.75 Clause #1690 (by clausification #[1689]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 15 a a_1 a_2) (skS.0 13 a)) True % 150.55/150.75 Clause #1693 (by superposition #[1690, 156]): ∀ (a a_1 a_2 : Iota), % 150.55/150.75 Or (Eq True False) (Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 13 a) (skS.0 15 a a_1 a_2)) True) % 150.55/150.75 Clause #1714 (by clausification #[1693]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 13 a) (skS.0 15 a a_1 a_2)) True % 150.55/150.75 Clause #1718 (by superposition #[1714, 610]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq (eqangle (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4 (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4) True) % 150.55/150.75 Clause #1719 (by clausification #[1718]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Eq (eqangle (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4 (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4) True % 150.55/150.75 Clause #1727 (by superposition #[1719, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq (eqangle (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4 a_3 a_4) True) % 150.55/150.75 Clause #1731 (by clausification #[1727]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Eq (eqangle (skS.0 13 a) (skS.0 15 a a_1 a_2) (skS.0 13 a) (skS.0 15 a a_1 a_2) a_3 a_4 a_3 a_4) True % 150.55/150.75 Clause #1737 (by superposition #[1731, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq (eqangle a a_1 a a_1 (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True) % 150.55/150.75 Clause #1743 (by clausification #[1737]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Eq (eqangle a a_1 a a_1 (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True % 150.55/150.75 Clause #1747 (by superposition #[1743, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq (eqangle a a_1 a_1 a (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True) % 150.55/150.75 Clause #1763 (by clausification #[1747]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Eq (eqangle a a_1 a_1 a (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True % 150.55/150.75 Clause #1770 (by superposition #[1763, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Or (Eq True False) % 150.55/150.75 (Eq (eqangle a a_1 (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) a_1 a (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True) % 150.55/150.75 Clause #1775 (by clausification #[1770]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 150.55/150.75 Eq (eqangle a a_1 (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4) a_1 a (skS.0 13 a_2) (skS.0 15 a_2 a_3 a_4)) True % 150.55/150.75 Clause #1779 (by superposition #[1775, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 150.55/150.75 Clause #1788 (by clausification #[1779]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 150.55/150.75 Clause #1798 (by superposition #[1788, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 150.55/150.75 Clause #1801 (by superposition #[1788, 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) % 150.57/150.77 Clause #1821 (by clausification #[1798]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 150.57/150.77 Clause #1823 (by superposition #[1821, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 150.57/150.77 Clause #1829 (by clausification #[1823]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 150.57/150.77 Clause #1844 (by superposition #[1829, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 150.57/150.77 Clause #1853 (by clausification #[1844]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 150.57/150.77 Clause #1870 (by superposition #[1853, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 150.57/150.77 Clause #1873 (by superposition #[1853, 554]): ∀ (a a_1 a_2 a_3 : Iota), % 150.57/150.77 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) % 150.57/150.77 (Or (Eq True False) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq (coll a a_1 a_2) False))) % 150.57/150.77 Clause #1879 (by clausification #[1870]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 150.57/150.77 Clause #1897 (by superposition #[1879, 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)) % 150.57/150.77 Clause #1905 (by clausification #[1801]): ∀ (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 % 150.57/150.77 Clause #1912 (by superposition #[1905, 397]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a a_1 a_3 a_2) True) % 150.57/150.77 Clause #1914 (by superposition #[1905, 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) % 150.57/150.77 Clause #1918 (by clausification #[1914]): ∀ (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 % 150.57/150.77 Clause #1924 (by superposition #[1918, 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) % 150.57/150.77 Clause #1933 (by clausification #[1924]): ∀ (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 % 150.57/150.77 Clause #1934 (by superposition #[1933, 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)) % 150.57/150.77 Clause #1937 (by superposition #[1933, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_1 a a_2 a_3 a_3 a_2) True) % 150.57/150.77 Clause #1945 (by clausification #[1937]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a a_2 a_3 a_3 a_2) True % 150.57/150.77 Clause #1953 (by superposition #[1945, 496]): ∀ (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_3 a_2) True) % 150.57/150.77 Clause #1958 (by clausification #[1953]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a a_3 a_2) True % 150.57/150.77 Clause #1963 (by superposition #[1958, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.57/150.77 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 150.57/150.77 (Or (Eq True False) (Eq (eqangle a_1 a a_3 a_2 a_4 a_5 a_6 a_7) False)) % 150.57/150.77 Clause #1964 (by clausification #[1897]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 150.57/150.77 Clause #1971 (by superposition #[1964, 1879]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 150.57/150.77 Clause #1972 (by clausification #[1971]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 150.57/150.77 Clause #2036 (by clausification #[1912]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_1 a_3 a_2) True % 150.57/150.77 Clause #2037 (by superposition #[2036, 369]): ∀ (a a_1 : Iota), % 150.57/150.77 Or (Eq (cong a a_1 a a_1) True) % 150.57/150.77 (Or (Eq True False) % 150.57/150.77 (Or (Eq (cyclic a a_1 a_1 a_1) False) (Or (Eq (cyclic a a_1 a_1 a) False) (Eq (cyclic a a_1 a_1 a_1) False)))) % 150.57/150.77 Clause #2040 (by superposition #[2036, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.57/150.77 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 150.57/150.77 (Or (Eq True False) (Eq (eqangle a a_1 a_3 a_2 a_4 a_5 a_6 a_7) False)) % 150.57/150.77 Clause #2045 (by clausification #[1934]): ∀ (a a_1 : Iota), Or (Eq (cyclic a a a_1 a) True) (Eq (coll a_1 a a) False) % 150.57/150.77 Clause #2046 (by forward demodulation #[2045, 1972]): ∀ (a a_1 : Iota), Or (Eq (cyclic a a a_1 a) True) (Eq True False) % 150.57/150.77 Clause #2047 (by clausification #[2046]): ∀ (a a_1 : Iota), Eq (cyclic a a a_1 a) True % 150.57/150.77 Clause #2049 (by superposition #[2047, 184]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (cyclic a a a a_1) True) % 150.57/150.77 Clause #2054 (by clausification #[2049]): ∀ (a a_1 : Iota), Eq (cyclic a a a a_1) True % 150.57/150.80 Clause #2057 (by superposition #[2054, 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)) % 150.57/150.80 Clause #2125 (by clausification #[2057]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (cyclic a a a a_2) False) % 150.57/150.80 Clause #2127 (by superposition #[2125, 2054]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq False True) % 150.57/150.80 Clause #2128 (by clausification #[2127]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 150.57/150.80 Clause #2129 (by superposition #[2128, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 150.57/150.80 Clause #2136 (by clausification #[2129]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 150.57/150.80 Clause #2140 (by superposition #[2136, 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_1 a a_1 a_3) False)) % 150.57/150.80 Clause #2443 (by clausification #[2140]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq (cyclic a_1 a a_1 a_3) False) % 150.57/150.80 Clause #2444 (by superposition #[2443, 2136]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 150.57/150.80 Clause #2445 (by clausification #[2444]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 150.57/150.80 Clause #2449 (by backward demodulation #[2445, 519]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) True) % 150.57/150.80 Clause #2452 (by clausification #[2449]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) True % 150.57/150.80 Clause #2455 (by superposition #[2452, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_1 a a_3 a_2 a_3) True) % 150.57/150.80 Clause #2463 (by clausification #[2455]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a a_3 a_2 a_3) True % 150.57/150.80 Clause #2464 (by superposition #[2463, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_1 a_3 a_2 a_3) True) % 150.57/150.80 Clause #2467 (by superposition #[2463, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.57/150.80 Or (Eq (eqangle a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True) % 150.57/150.80 (Or (Eq True False) (Eq (eqangle a a_7 a_2 a_7 a_3 a_4 a_5 a_6) False)) % 150.57/150.80 Clause #2468 (by clausification #[2464]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_1 a_3 a_2 a_3) True % 150.57/150.80 Clause #2470 (by superposition #[2468, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_1 a_3 a a_2 a_3) True) % 150.57/150.80 Clause #2474 (by clausification #[2470]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a_3 a a_2 a_3) True % 150.57/150.80 Clause #2475 (by superposition #[2474, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_3 a_1 a_2 a_3) True) % 150.57/150.80 Clause #2476 (by superposition #[2474, 397]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_1 a a_3 a_3 a_2) True) % 150.57/150.80 Clause #2478 (by superposition #[2474, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_3 a_1 a_3 a_2) True) % 150.57/150.80 Clause #2481 (by clausification #[2478]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_3 a_1 a_3 a_2) True % 150.57/150.80 Clause #2483 (by superposition #[2481, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_2 a_3 a_1 a_2 a_3) True) % 150.57/150.80 Clause #2487 (by clausification #[2483]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_2 a_3 a_1 a_2 a_3) True % 150.57/150.80 Clause #2489 (by superposition #[2487, 397]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_2 a_1 a_3 a_3 a_2) True) % 150.57/150.80 Clause #2496 (by clausification #[2489]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_2 a_1 a_3 a_3 a_2) True % 150.57/150.80 Clause #2497 (by superposition #[2496, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_1 a_2 a a_3 a_3 a_2) True) % 150.57/150.80 Clause #2501 (by clausification #[2497]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a_2 a a_3 a_3 a_2) True % 150.57/150.80 Clause #2505 (by superposition #[2501, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.57/150.80 Or (Eq (eqangle a a_1 a_1 a_2 a_3 a_4 a_5 a_6) True) % 150.57/150.80 (Or (Eq True False) (Eq (eqangle a a_7 a_7 a_2 a_3 a_4 a_5 a_6) False)) % 150.57/150.80 Clause #2528 (by clausification #[2475]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_3 a_1 a_2 a_3) True % 150.62/150.82 Clause #2531 (by superposition #[2528, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a a_3 a_4 a_5 a_6) True) % 150.62/150.82 (Or (Eq True False) (Eq (eqangle a_7 a_1 a_2 a_7 a_3 a_4 a_5 a_6) False)) % 150.62/150.82 Clause #2536 (by clausification #[2476]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a a_3 a_3 a_2) True % 150.62/150.82 Clause #2539 (by superposition #[2536, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True) % 150.62/150.82 (Or (Eq True False) (Eq (eqangle a a_7 a_7 a_2 a_3 a_4 a_5 a_6) False)) % 150.62/150.82 Clause #2728 (by clausification #[2040]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqangle a a_1 a_3 a_2 a_4 a_5 a_6 a_7) False) % 150.62/150.82 Clause #2774 (by clausification #[2539]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True) (Eq (eqangle a a_7 a_7 a_2 a_3 a_4 a_5 a_6) False) % 150.62/150.82 Clause #2779 (by clausification #[2467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a_1 a_3 a_4 a_5 a_6) True) (Eq (eqangle a a_7 a_2 a_7 a_3 a_4 a_5 a_6) False) % 150.62/150.82 Clause #2813 (by clausification #[2505]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_1 a_2 a_3 a_4 a_5 a_6) True) (Eq (eqangle a a_7 a_7 a_2 a_3 a_4 a_5 a_6) False) % 150.62/150.82 Clause #2816 (by clausification #[2531]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a a_3 a_4 a_5 a_6) True) (Eq (eqangle a_7 a_1 a_2 a_7 a_3 a_4 a_5 a_6) False) % 150.62/150.82 Clause #2835 (by clausification #[1963]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.62/150.82 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqangle a_1 a a_3 a_2 a_4 a_5 a_6 a_7) False) % 150.62/150.82 Clause #2872 (by clausification #[1873]): ∀ (a a_1 a_2 a_3 : Iota), % 150.62/150.82 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq (coll a a_1 a_2) False)) % 150.62/150.82 Clause #2873 (by forward demodulation #[2872, 1972]): ∀ (a a_1 a_2 a_3 : Iota), % 150.62/150.82 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq True False)) % 150.62/150.82 Clause #2874 (by clausification #[2873]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Eq (para a_1 a_3 a_2 a) False) % 150.62/150.82 Clause #2875 (by superposition #[2874, 1788]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a_1 a a_1 a_1 a) True) (Eq False True) % 150.62/150.82 Clause #2944 (by clausification #[2875]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a_1 a_1 a) True % 150.62/150.82 Clause #2947 (by superposition #[2944, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a a_1) True) % 150.62/150.82 Clause #2949 (by clausification #[2947]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a_1) True % 150.62/150.82 Clause #2952 (by superposition #[2949, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_1 a a_1 a_1) True) % 150.62/150.82 Clause #2955 (by clausification #[2952]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a_1 a a_1 a_1) True % 150.62/150.82 Clause #2957 (by superposition #[2955, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a_1 a a) True) % 150.62/150.82 Clause #2960 (by clausification #[2957]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a a_1 a a) True % 150.62/150.82 Clause #2962 (by superposition #[2960, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a a a_1) True) % 150.62/150.82 Clause #2963 (by superposition #[2960, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_1 a a_1) True) % 150.62/150.82 Clause #2965 (by clausification #[2963]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a_1 a a_1) True % 150.62/150.82 Clause #2968 (by superposition #[2965, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a a_1 a a_1) True) % 150.62/150.82 Clause #2970 (by clausification #[2968]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a_1 a a_1) True % 150.62/150.82 Clause #2972 (by superposition #[2970, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.62/150.82 Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_5) False)) % 150.62/150.82 Clause #3085 (by clausification #[2962]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a a a a_1) True % 150.62/150.85 Clause #3176 (by clausification #[2972]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.62/150.85 Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_5) False) % 150.62/150.85 Clause #3187 (by superposition #[3176, 3085]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a_1 a a a a_1) True) (Eq False True) % 150.62/150.85 Clause #3251 (by clausification #[3187]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a a a_1) True % 150.62/150.85 Clause #3253 (by superposition #[3251, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_1 a a) True) % 150.62/150.85 Clause #3254 (by superposition #[3251, 711]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a a_1 a a_1) True) % 150.62/150.85 Clause #3256 (by clausification #[3254]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a_1 a a_1) True % 150.62/150.85 Clause #3258 (by superposition #[3256, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a a a) True) % 150.62/150.85 Clause #3261 (by clausification #[3258]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a a a a) True % 150.62/150.85 Clause #3265 (by superposition #[3261, 3176]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a_1 a a a a) True) (Eq True False) % 150.62/150.85 Clause #3269 (by clausification #[3265]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a a a) True % 150.62/150.85 Clause #3271 (by superposition #[3269, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a a a) True) % 150.62/150.85 Clause #3282 (by clausification #[3271]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a a a) True % 150.62/150.85 Clause #3284 (by superposition #[3282, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_1 a_1) True) % 150.62/150.85 Clause #3291 (by clausification #[3284]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_1 a_1) True % 150.62/150.85 Clause #3295 (by superposition #[3291, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.62/150.85 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) % 150.62/150.85 (Or (Eq True False) (Eq (eqratio a_1 a_1 a_1 a_1 a_2 a_3 a_4 a_5) False)) % 150.62/150.85 Clause #3303 (by clausification #[3253]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a_1 a a) True % 150.62/150.85 Clause #3305 (by superposition #[3303, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True) % 150.62/150.85 Clause #3307 (by clausification #[3305]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True % 150.62/150.85 Clause #3310 (by superposition #[3307, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a a a) True) % 150.62/150.85 Clause #3313 (by clausification #[3310]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a a a) True % 150.62/150.85 Clause #3317 (by superposition #[3313, 711]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a a) True) % 150.62/150.85 Clause #3319 (by clausification #[3317]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a) True % 150.62/150.85 Clause #3321 (by superposition #[3319, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_1 a_1 a_1) True) % 150.62/150.85 Clause #3331 (by clausification #[3321]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_1 a_1 a_1) True % 150.62/150.85 Clause #3333 (by superposition #[3331, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_1 a) True) % 150.62/150.85 Clause #3341 (by clausification #[3333]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a a_1 a) True % 150.62/150.85 Clause #3599 (by clausification #[3295]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 150.62/150.85 Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_1 a_1 a_1 a_1 a_2 a_3 a_4 a_5) False) % 150.62/150.85 Clause #3612 (by superposition #[3599, 3341]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_2 a_1) True) (Eq False True) % 150.62/150.85 Clause #3613 (by clausification #[3612]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_2 a_1) True % 150.62/150.85 Clause #3616 (by superposition #[3613, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a a_2 a) True) % 150.62/150.85 Clause #3631 (by clausification #[3616]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a a_2 a) True % 150.62/150.85 Clause #3633 (by superposition #[3631, 702]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_1 a_2 a_1) True) % 150.62/150.85 Clause #3635 (by clausification #[3633]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_1 a_2 a_1) True % 150.66/150.87 Clause #3641 (by superposition #[3635, 3599]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_2 a_1) True) (Eq True False) % 150.66/150.87 Clause #3643 (by clausification #[3641]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_2 a_1) True % 150.66/150.87 Clause #3646 (by superposition #[3643, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a a a) True) % 150.66/150.87 Clause #3648 (by clausification #[3646]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a a a) True % 150.66/150.87 Clause #3652 (by superposition #[3648, 3599]): ∀ (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) % 150.66/150.87 Clause #3653 (by clausification #[3652]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_1 a_1) True % 150.66/150.87 Clause #3658 (by superposition #[3653, 711]): ∀ (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) % 150.66/150.87 Clause #3660 (by clausification #[3658]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_1 a_1) True % 150.66/150.87 Clause #3663 (by superposition #[3660, 702]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_2 a) True) % 150.66/150.87 Clause #3665 (by clausification #[3663]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a a_2 a) True % 150.66/150.87 Clause #3668 (by superposition #[3665, 3599]): ∀ (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_1) True) (Eq True False) % 150.66/150.87 Clause #3674 (by clausification #[3668]): ∀ (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 % 150.66/150.87 Clause #3679 (by superposition #[3674, 711]): ∀ (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_1) True) % 150.66/150.87 Clause #3681 (by clausification #[3679]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_3 a_1) True % 150.66/150.87 Clause #3683 (by superposition #[3681, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a a_3 a) True) % 150.66/150.87 Clause #3686 (by clausification #[3683]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a a_3 a) True % 150.66/150.87 Clause #3689 (by superposition #[3686, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a_3 a) True) % 150.66/150.87 Clause #3691 (by clausification #[3689]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a_3 a) True % 150.66/150.87 Clause #3696 (by superposition #[3691, 3599]): ∀ (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_1) True) (Eq True False) % 150.66/150.87 Clause #3700 (by clausification #[3696]): ∀ (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 % 150.66/150.87 Clause #3703 (by superposition #[3700, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a a a_3) True) % 150.66/150.87 Clause #3705 (by superposition #[3700, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_3 a_1) True) % 150.66/150.87 Clause #3707 (by clausification #[3705]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_3 a_1) True % 150.66/150.87 Clause #3709 (by superposition #[3707, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a a_3 a) True) % 150.66/150.87 Clause #3712 (by clausification #[3709]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_2 a a a_3 a) True % 150.66/150.87 Clause #3715 (by superposition #[3712, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a a_3) True) % 150.66/150.87 Clause #3724 (by clausification #[3715]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a a_3) True % 150.66/150.87 Clause #3729 (by superposition #[3724, 3599]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_1 a_3) True) (Eq True False) % 150.66/150.87 Clause #3730 (by clausification #[3729]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_1 a_3) True % 150.66/150.87 Clause #3733 (by superposition #[3730, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_1 a_3) True) % 150.66/150.87 Clause #3735 (by clausification #[3733]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_1 a_3) True % 150.66/150.87 Clause #3738 (by superposition #[3735, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a_3 a a) True) % 150.66/150.87 Clause #3742 (by clausification #[3738]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a_3 a a) True % 150.66/150.90 Clause #3744 (by superposition #[3742, 596]): ∀ (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) % 150.66/150.90 Clause #3749 (by clausification #[3744]): ∀ (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 % 150.66/150.90 Clause #3753 (by superposition #[3749, 3176]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a_1 a_1 a_2 a_1 a_1) True) (Eq True False) % 150.66/150.90 Clause #3754 (by clausification #[3753]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_1 a_2 a_1 a_1) True % 150.66/150.90 Clause #3758 (by superposition #[3754, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a a_1 a_1 a_1) True) % 150.66/150.90 Clause #3760 (by clausification #[3758]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_2 a a_1 a_1 a_1) True % 150.66/150.90 Clause #3762 (by superposition #[3760, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a a_2 a) True) % 150.66/150.90 Clause #3771 (by clausification #[3762]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a_2 a) True % 150.66/150.90 Clause #3774 (by superposition #[3771, 702]): ∀ (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) % 150.66/150.90 Clause #3776 (by clausification #[3774]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a_2 a_1 a_1) True % 150.66/150.90 Clause #3778 (by superposition #[3776, 711]): ∀ (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) % 150.66/150.90 Clause #3780 (by clausification #[3778]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a a_2 a_2) True % 150.66/150.90 Clause #3783 (by superposition #[3780, 3599]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_2 a_2) True) (Eq True False) % 150.66/150.90 Clause #3784 (by clausification #[3783]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_1 a_2 a_2) True % 150.66/150.90 Clause #3789 (by superposition #[3784, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_2 a_2) True) % 150.66/150.90 Clause #3791 (by clausification #[3789]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_2 a_2) True % 150.66/150.90 Clause #3794 (by superposition #[3791, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a a a_1 a_1) True) % 150.66/150.90 Clause #3810 (by clausification #[3794]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a a a_1 a_1) True % 150.66/150.90 Clause #3812 (by superposition #[3810, 596]): ∀ (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) % 150.66/150.90 Clause #3815 (by clausification #[3812]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_1 a_1 a a) True % 150.66/150.90 Clause #3817 (by superposition #[3815, 649]): ∀ (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) % 150.66/150.90 Clause #3951 (by clausification #[3817]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_2 a_2) True % 150.66/150.90 Clause #3953 (by superposition #[3951, 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) % 150.66/150.90 Clause #3955 (by clausification #[3953]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a a a_2 a_2) True % 150.66/150.90 Clause #3958 (by superposition #[3955, 702]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_2 a a_1) True) % 150.66/150.90 Clause #3960 (by clausification #[3958]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a a_2 a a_1) True % 150.66/150.90 Clause #3963 (by superposition #[3960, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a a_2) True) % 150.66/150.90 Clause #3965 (by clausification #[3963]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a a_2) True % 150.66/150.90 Clause #3968 (by superposition #[3965, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.66/150.90 Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) % 150.66/150.90 (Or (Eq True False) (Eq (eqratio a_6 a_6 a a_6 a_2 a_3 a_4 a_5) False)) % 150.66/150.90 Clause #4159 (by clausification #[3703]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a_2 a a a_3) True % 150.66/150.90 Clause #4345 (by clausification #[3968]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 150.66/150.90 Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a_6 a_6 a a_6 a_2 a_3 a_4 a_5) False) % 150.66/150.90 Clause #4370 (by superposition #[4345, 4159]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_3 a_4) True) (Eq False True) % 150.66/150.92 Clause #4371 (by clausification #[4370]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_3 a_4) True % 150.66/150.92 Clause #4377 (by superposition #[4371, 3599]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_3 a_4) True) (Eq True False) % 150.66/150.92 Clause #4380 (by clausification #[4377]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_3 a_4) True % 150.66/150.92 Clause #4385 (by superposition #[4380, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_3 a_4) True) % 150.66/150.92 Clause #4387 (by clausification #[4385]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_3 a_4) True % 150.66/150.92 Clause #4391 (by superposition #[4387, 702]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_3 a a_4 a_1) True) % 150.66/150.92 Clause #4396 (by clausification #[4391]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_2 a_3 a a_4 a_1) True % 150.66/150.92 Clause #4400 (by superposition #[4396, 4345]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a) True) (Eq True False) % 150.66/150.92 Clause #4406 (by clausification #[4400]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_4 a) True % 150.66/150.92 Clause #4412 (by superposition #[4406, 3599]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_1) True) (Eq True False) % 150.66/150.92 Clause #4413 (by clausification #[4412]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a_3 a_4 a_1) True % 150.66/150.92 Clause #4418 (by superposition #[4413, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_1) True) % 150.66/150.92 Clause #4420 (by clausification #[4418]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_1) True % 150.66/150.92 Clause #4422 (by superposition #[4420, 596]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a a a_4 a) True) % 150.66/150.92 Clause #4425 (by superposition #[4420, 4345]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_2 a_3 a_2) True) (Eq True False) % 150.66/150.92 Clause #4426 (by clausification #[4425]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_3 a_2) True % 150.66/150.92 Clause #4432 (by superposition #[4426, 3599]): ∀ (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) % 150.66/150.92 Clause #4433 (by clausification #[4432]): ∀ (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 % 150.66/150.92 Clause #4437 (by superposition #[4433, 711]): ∀ (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) % 150.66/150.92 Clause #4440 (by clausification #[4437]): ∀ (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 % 150.66/150.92 Clause #4442 (by superposition #[4440, 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_3 a_2) True) % 150.66/150.92 Clause #4457 (by clausification #[4442]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a_3 a_2) True % 150.66/150.92 Clause #4460 (by superposition #[4457, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a a_3 a_2 a_2) True) % 150.66/150.92 Clause #4462 (by clausification #[4460]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_2 a_2) True % 150.66/150.92 Clause #4467 (by superposition #[4462, 4345]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_2 a_2) True) (Eq True False) % 150.66/150.92 Clause #4468 (by clausification #[4467]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_2 a_2) True % 150.66/150.92 Clause #4471 (by superposition #[4468, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a a_3 a_1 a_1) True) % 150.66/150.92 Clause #4499 (by clausification #[4471]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_1 a_1) True % 150.66/150.92 Clause #4501 (by superposition #[4499, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a a_2 a_3) True) % 150.66/150.92 Clause #4506 (by clausification #[4501]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a_2 a_3) True % 150.66/150.92 Clause #4508 (by superposition #[4506, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.66/150.92 Or (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_6) True) % 150.74/150.95 (Or (Eq True False) (Eq (eqratio a a a_2 a_7 a_3 a_4 a_5 a_6) False)) % 150.74/150.95 Clause #4555 (by clausification #[4422]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a a a_4 a) True % 150.74/150.95 Clause #4558 (by superposition #[4555, 702]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a_3 a_4) True) % 150.74/150.95 Clause #4560 (by clausification #[4558]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a a a_2 a_3 a_4) True % 150.74/150.95 Clause #4566 (by superposition #[4560, 4345]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq True False) % 150.74/150.95 Clause #4567 (by clausification #[4566]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True % 150.74/150.95 Clause #4571 (by superposition #[4567, 711]): ∀ (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 a_3 a_4 a_5) True) % 150.74/150.95 Clause #4630 (by clausification #[4571]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_4 a_5) True % 150.74/150.95 Clause #4764 (by clausification #[4508]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.74/150.95 Or (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_6) True) (Eq (eqratio a a a_2 a_7 a_3 a_4 a_5 a_6) False) % 150.74/150.95 Clause #4776 (by superposition #[4764, 4630]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a_1 a_2 a_2 a a_3 a_4 a_5) True) (Eq False True) % 150.74/150.95 Clause #4779 (by clausification #[4776]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a a_3 a_4 a_5) True % 150.74/150.95 Clause #4784 (by superposition #[4779, 711]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_3 a_3 a_4 a_5) True) % 150.74/150.95 Clause #4792 (by clausification #[4784]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a a_2 a_3 a_3 a_4 a_5) True % 150.74/150.95 Clause #4795 (by superposition #[4792, 649]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_5) True) % 150.74/150.95 Clause #4798 (by superposition #[4792, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.74/150.95 Or (Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_6) True) % 150.74/150.95 (Or (Eq True False) (Eq (eqratio a_7 a_7 a_8 a_9 a_3 a_4 a_5 a_6) False)) % 150.74/150.95 Clause #4816 (by clausification #[4795]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_5) True % 150.74/150.95 Clause #4818 (by superposition #[4816, 596]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_5 a_5) True) % 150.74/150.95 Clause #4823 (by clausification #[4818]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_5 a_5) True % 150.74/150.95 Clause #4827 (by superposition #[4823, 711]): ∀ (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_4 a_5 a_5) True) % 150.74/150.95 Clause #4829 (by clausification #[4827]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_4 a_5 a_5) True % 150.74/150.95 Clause #4832 (by superposition #[4829, 702]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a a_4 a_5) True) % 150.74/150.95 Clause #4836 (by clausification #[4832]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a a_4 a_5) True % 150.74/150.95 Clause #4839 (by superposition #[4836, 649]): ∀ (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_4 a_5 a_1) True) % 150.74/150.95 Clause #4846 (by clausification #[4839]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_1) True % 150.74/150.95 Clause #4848 (by superposition #[4846, 711]): ∀ (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_4 a_5 a_3) True) % 150.74/150.95 Clause #4851 (by clausification #[4848]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_3) True % 150.74/150.95 Clause #4854 (by superposition #[4851, 4764]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_3) True) (Eq True False) % 150.74/150.95 Clause #4855 (by clausification #[4854]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_3) True % 150.74/150.95 Clause #4860 (by superposition #[4855, 711]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_4 a_5 a_2) True) % 150.74/150.95 Clause #4865 (by clausification #[4860]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_4 a_5 a_2) True % 150.74/150.97 Clause #4868 (by superposition #[4865, 702]): ∀ (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_4 a_2 a_5) True) % 150.74/150.97 Clause #4872 (by clausification #[4868]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_2 a_5) True % 150.74/150.97 Clause #4875 (by superposition #[4872, 4764]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_6) True) (Eq True False) % 150.74/150.97 Clause #4876 (by clausification #[4875]): ∀ (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 % 150.74/150.97 Clause #4994 (by clausification #[4798]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 150.74/150.97 Or (Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_6) True) (Eq (eqratio a_7 a_7 a_8 a_9 a_3 a_4 a_5 a_6) False) % 150.74/150.97 Clause #4995 (by superposition #[4994, 4876]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_6) True) (Eq False True) % 150.74/150.97 Clause #4998 (by clausification #[4995]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a a_2 a_3 a_4 a_5 a_6) True % 150.74/150.97 Clause #5000 (by superposition #[4998, 596]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_5 a_6) True) % 150.74/150.97 Clause #5016 (by clausification #[5000]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_5 a_6) True % 150.74/150.97 Clause #5019 (by superposition #[5016, 702]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_5 a_6) True) % 150.74/150.97 Clause #5021 (by clausification #[5019]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_5 a_6) True % 150.74/150.97 Clause #5024 (by superposition #[5021, 711]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_3 a_6) True) % 150.74/150.97 Clause #5027 (by clausification #[5024]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_3 a_6) True % 150.74/150.97 Clause #5029 (by superposition #[5027, 702]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_2) True) % 150.74/150.97 Clause #5031 (by clausification #[5029]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_2) True % 150.74/150.97 Clause #5033 (by superposition #[5031, 649]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a a_5 a_6) True) % 150.74/150.97 Clause #5035 (by clausification #[5033]): ∀ (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 a_5 a_6) True % 150.74/150.97 Clause #5038 (by superposition #[5035, 795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 150.74/150.97 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 150.74/150.97 (Or (Eq True False) (Eq (eqratio a_8 a a_9 a_10 a_4 a_5 a_6 a_7) False)) % 150.74/150.97 Clause #5095 (by clausification #[5038]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 150.74/150.97 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqratio a_8 a a_9 a_10 a_4 a_5 a_6 a_7) False) % 150.74/150.97 Clause #5096 (by superposition #[5095, 4876]): ∀ (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 False True) % 150.74/150.97 Clause #5111 (by clausification #[5096]): ∀ (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 % 150.74/150.97 Clause #5112 (by superposition #[5111, 467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 150.74/150.97 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)) % 150.74/150.97 Clause #5113 (by clausification #[5112]): ∀ (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) % 150.74/150.97 Clause #5641 (by clausification #[2037]): ∀ (a a_1 : Iota), % 150.74/150.97 Or (Eq (cong a a_1 a a_1) True) % 150.74/150.97 (Or (Eq (cyclic a a_1 a_1 a_1) False) (Or (Eq (cyclic a a_1 a_1 a) False) (Eq (cyclic a a_1 a_1 a_1) False))) % 150.74/150.97 Clause #5642 (by eliminate duplicate literals #[5641]): ∀ (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 (cyclic a a_1 a_1 a) False)) % 150.74/150.97 Clause #5643 (by superposition #[5642, 2445]): ∀ (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 False True)) % 150.79/150.99 Clause #5645 (by clausification #[5643]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq (cyclic a a_1 a_1 a) False) % 150.79/150.99 Clause #5646 (by superposition #[5645, 2445]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq False True) % 150.79/150.99 Clause #5647 (by clausification #[5646]): ∀ (a a_1 : Iota), Eq (cong a a_1 a a_1) True % 150.79/150.99 Clause #5656 (by superposition #[5647, 5113]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False) % 150.79/150.99 Clause #5679 (by clausification #[5656]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True % 150.79/150.99 Clause #5681 (by backward demodulation #[5679, 388]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_1 a_2 a_1 a_2 a a_2) True) % 150.79/150.99 Clause #5734 (by clausification #[5681]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_1 a_2 a_1 a_2 a a_2) True % 150.79/150.99 Clause #5738 (by superposition #[5734, 397]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_2 a_1 a a_1) True) % 150.79/150.99 Clause #5830 (by clausification #[5738]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_2 a a_2 a_1 a a_1) True % 150.79/150.99 Clause #5856 (by superposition #[5830, 2835]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a_2 a a_1 a) True) (Eq True False) % 150.79/150.99 Clause #5857 (by clausification #[5856]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_1 a_2 a_2 a a_1 a) True % 150.79/150.99 Clause #5865 (by superposition #[5857, 2728]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqangle a a_1 a_2 a_1 a_2 a a_1 a) True) (Eq True False) % 150.79/150.99 Clause #5870 (by clausification #[5865]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_2 a_1 a_2 a a_1 a) True % 150.79/150.99 Clause #5873 (by superposition #[5870, 496]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_2 a_1 a_1 a) True) % 150.79/150.99 Clause #5876 (by clausification #[5873]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_2 a a_2 a_1 a_1 a) True % 150.79/150.99 Clause #5896 (by superposition #[5876, 2835]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a_2 a a a_1) True) (Eq True False) % 150.79/150.99 Clause #5897 (by clausification #[5896]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_1 a_2 a_2 a a a_1) True % 150.79/150.99 Clause #5902 (by superposition #[5897, 496]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_1 a_2 a a_1) True) % 150.79/150.99 Clause #5918 (by clausification #[5902]): ∀ (a a_1 a_2 : Iota), Eq (eqangle a a_1 a_2 a a_1 a_2 a a_1) True % 150.79/150.99 Clause #5933 (by superposition #[5918, 2816]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a a_1 a_2 a_3 a_1) True) (Eq True False) % 150.79/150.99 Clause #7452 (by clausification #[5933]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_1 a_2 a_3 a_1) True % 150.79/150.99 Clause #7454 (by superposition #[7452, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_3 a a_1 a_3) True) % 150.79/150.99 Clause #7458 (by clausification #[7454]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_3 a a_1 a_3) True % 150.79/150.99 Clause #7469 (by superposition #[7458, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a_3 a_1 a a_3) True) (Eq True False) % 150.79/150.99 Clause #7470 (by clausification #[7469]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a_2 a_3 a_1 a a_3) True % 150.79/150.99 Clause #7478 (by superposition #[7470, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_1 a_3 a_1 a a_3) True) (Eq True False) % 150.79/150.99 Clause #7480 (by clausification #[7478]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a_3 a_1 a a_3) True % 150.79/150.99 Clause #7484 (by superposition #[7480, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_1 a_3 a_1 a a_2) True) % 150.79/150.99 Clause #7488 (by clausification #[7484]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a_3 a_1 a a_2) True % 150.79/150.99 Clause #7505 (by superposition #[7488, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a a_2 a_3 a a_1 a_2) True) (Eq True False) % 150.79/150.99 Clause #7506 (by clausification #[7505]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_2 a_3 a a_1 a_2) True % 150.79/150.99 Clause #7511 (by superposition #[7506, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a a_3 a_1 a_3) True) % 150.79/150.99 Clause #7520 (by clausification #[7511]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a a_3 a_1 a_3) True % 150.79/151.02 Clause #7536 (by superposition #[7520, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a_1 a_3 a a_3) True) (Eq True False) % 150.79/151.02 Clause #7540 (by clausification #[7536]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a_2 a_1 a_3 a a_3) True % 150.79/151.02 Clause #7543 (by superposition #[7540, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_1 a_2 a a a_3) True) % 150.79/151.02 Clause #7723 (by clausification #[7543]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a_2 a a a_3) True % 150.79/151.02 Clause #7727 (by superposition #[7723, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_2 a_1 a a_3) True) % 150.79/151.02 Clause #7730 (by clausification #[7727]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_2 a_1 a a_3) True % 150.79/151.02 Clause #7738 (by superposition #[7730, 2774]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a a_1 a_2 a_2 a a_3) True) (Eq True False) % 150.79/151.02 Clause #7764 (by clausification #[7738]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_2 a_2 a a_3) True % 150.79/151.02 Clause #7769 (by superposition #[7764, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_2 a a_1 a a_3) True) % 150.79/151.02 Clause #7772 (by clausification #[7769]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a a_1 a a_3) True % 150.79/151.02 Clause #7780 (by superposition #[7772, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_2 a_1 a a_1 a_3) True) (Eq True False) % 150.79/151.02 Clause #7781 (by clausification #[7780]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a_1 a a_1 a_3) True % 150.79/151.02 Clause #7783 (by superposition #[7781, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_2 a_1 a a_3 a_3) True) % 150.79/151.02 Clause #7789 (by clausification #[7783]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_2 a_1 a a_3 a_3) True % 150.79/151.02 Clause #7811 (by superposition #[7789, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_1 a a_1 a_3 a_3) True) (Eq True False) % 150.79/151.02 Clause #7812 (by clausification #[7811]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a a_1 a_3 a_3) True % 150.79/151.02 Clause #7820 (by superposition #[7812, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a a_1 a_3 a_3) True) (Eq True False) % 150.79/151.02 Clause #7822 (by clausification #[7820]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a_2 a a_1 a_3 a_3) True % 150.79/151.02 Clause #7826 (by superposition #[7822, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_1 a_1 a_2 a_3 a_3) True) % 150.79/151.02 Clause #7832 (by clausification #[7826]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_1 a_2 a_3 a_3) True % 150.79/151.02 Clause #7834 (by superposition #[7832, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_2 a_3 a a_3 a) True) % 150.79/151.02 Clause #7838 (by clausification #[7834]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a_3 a a_3 a) True % 150.79/151.02 Clause #7844 (by superposition #[7838, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_2 a_3 a_1 a_3 a_1) True) (Eq True False) % 150.79/151.02 Clause #7845 (by clausification #[7844]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a_3 a_1 a_3 a_1) True % 150.79/151.02 Clause #7846 (by superposition #[7845, 397]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a_2 a_3 a_2 a_3 a_2) True) % 150.79/151.02 Clause #7851 (by clausification #[7846]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_3 a_2 a_3 a_2) True % 150.79/151.02 Clause #7854 (by superposition #[7851, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a_2 a_3 a_2 a_1 a_2) True) % 150.79/151.02 Clause #7873 (by clausification #[7854]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_3 a_2 a_1 a_2) True % 150.79/151.02 Clause #7877 (by superposition #[7873, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a a_1 a_2 a_3 a_1 a_2 a_1) True) (Eq True False) % 150.79/151.02 Clause #7878 (by clausification #[7877]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_3 a_1 a_2 a_1) True % 150.79/151.02 Clause #7882 (by superposition #[7878, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a_2 a_2 a_3 a_3 a_2) True) % 150.79/151.02 Clause #7891 (by clausification #[7882]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_2 a_3 a_3 a_2) True % 150.79/151.04 Clause #7898 (by superposition #[7891, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a a_1 a_2 a_1 a_3 a_3 a_1) True) (Eq True False) % 150.79/151.04 Clause #7899 (by clausification #[7898]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_1 a_3 a_3 a_1) True % 150.79/151.04 Clause #7903 (by superposition #[7899, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a_2 a_1 a_3 a_2 a_1) True) % 150.79/151.04 Clause #7907 (by clausification #[7903]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a_1 a_3 a_2 a_1) True % 150.79/151.04 Clause #7917 (by superposition #[7907, 2779]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_1 a_2 a_3 a a_2) True) (Eq True False) % 150.79/151.04 Clause #7932 (by clausification #[7917]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_1 a_2 a_3 a a_2) True % 150.79/151.04 Clause #7933 (by superposition #[7932, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_2 a_3 a_1 a_2) True) % 150.79/151.04 Clause #7937 (by clausification #[7933]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_2 a_3 a_1 a_2) True % 150.79/151.04 Clause #7939 (by superposition #[7937, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_2 a a_1 a_2) True) % 150.79/151.04 Clause #7942 (by clausification #[7939]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a a_1 a_2) True % 150.79/151.04 Clause #7947 (by superposition #[7942, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a a_3) True) (Eq True False) % 150.79/151.04 Clause #7953 (by clausification #[7947]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a a_3) True % 150.79/151.04 Clause #7958 (by superposition #[7953, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_2 a_1 a a_2) True) (Eq True False) % 150.79/151.04 Clause #7960 (by clausification #[7958]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a_1 a a_2) True % 150.79/151.04 Clause #7961 (by superposition #[7960, 397]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_2 a a a_3) True) % 150.79/151.04 Clause #7965 (by clausification #[7961]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a a a_3) True % 150.79/151.04 Clause #7973 (by superposition #[7965, 2816]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a a_2 a_3 a_3 a_3) True) (Eq True False) % 150.79/151.04 Clause #7988 (by clausification #[7973]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_2 a_3 a_3 a_3) True % 150.79/151.04 Clause #7993 (by superposition #[7988, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_2 a a_3 a_3) True) % 150.79/151.04 Clause #7996 (by clausification #[7993]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a a_3 a_3) True % 150.79/151.04 Clause #8013 (by superposition #[7996, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a_2 a_2) True) (Eq True False) % 150.79/151.04 Clause #8014 (by clausification #[8013]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a_2 a_2) True % 150.79/151.04 Clause #8022 (by superposition #[8014, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_2 a_1 a_3 a_3) True) (Eq True False) % 150.79/151.04 Clause #8027 (by clausification #[8022]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a_1 a_3 a_3) True % 150.79/151.04 Clause #8029 (by superposition #[8027, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_2 a_3 a_1 a a_2) True) % 150.79/151.04 Clause #8033 (by clausification #[8029]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a_3 a_1 a a_2) True % 150.79/151.04 Clause #8040 (by superposition #[8033, 2835]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a_1 a_2 a_2 a_3 a a_1 a_2) True) (Eq True False) % 150.79/151.04 Clause #8041 (by clausification #[8040]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_2 a_3 a a_1 a_2) True % 150.79/151.04 Clause #8045 (by superposition #[8041, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a a_3 a_3 a_1 a_3) True) % 150.79/151.04 Clause #8052 (by clausification #[8045]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a a_3 a_3 a_1 a_3) True % 150.79/151.04 Clause #8054 (by superposition #[8052, 441]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a a_2 a_1 a_3 a_2) True) % 150.79/151.04 Clause #8058 (by clausification #[8054]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a a_2 a_1 a_3 a_2) True % 150.97/151.20 Clause #8063 (by superposition #[8058, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a a a_1 a_2 a_1 a_3 a_2) True) (Eq True False) % 150.97/151.20 Clause #8064 (by clausification #[8063]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a a_1 a_2 a_1 a_3 a_2) True % 150.97/151.20 Clause #8068 (by superposition #[8064, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a_1 a_2 a a_2 a_3 a_1) True) % 150.97/151.20 Clause #8072 (by clausification #[8068]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a a_2 a_3 a_1) True % 150.97/151.20 Clause #8079 (by superposition #[8072, 2728]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqangle a a a_1 a_2 a a_1 a_3 a_2) True) (Eq True False) % 150.97/151.20 Clause #8083 (by clausification #[8079]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a_1 a_2 a a_1 a_3 a_2) True % 150.97/151.20 Clause #8085 (by superposition #[8083, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a a a_1 a_1 a_2 a_3 a_2) True) % 150.97/151.20 Clause #8089 (by clausification #[8085]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a a a_1 a_1 a_2 a_3 a_2) True % 150.97/151.20 Clause #8100 (by superposition #[8089, 2813]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqangle a a_1 a_1 a_2 a_2 a_3 a_4 a_3) True) (Eq True False) % 150.97/151.20 Clause #8101 (by clausification #[8100]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_1 a_2 a_2 a_3 a_4 a_3) True % 150.97/151.20 Clause #8106 (by superposition #[8101, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_1 a_2 a_4 a_3) True) % 150.97/151.20 Clause #8109 (by clausification #[8106]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a_2 a_4 a_3) True % 150.97/151.20 Clause #8122 (by superposition #[8109, 2835]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a a_3 a_4 a_2) True) (Eq True False) % 150.97/151.20 Clause #8126 (by clausification #[8122]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_3 a_4 a_2) True % 150.97/151.20 Clause #8134 (by superposition #[8126, 2728]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a a_2 a_4 a_3) True) (Eq True False) % 150.97/151.20 Clause #8136 (by clausification #[8134]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_2 a_4 a_3) True % 150.97/151.20 Clause #8138 (by superposition #[8136, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a a_4 a_1 a_3) True) % 150.97/151.20 Clause #8142 (by clausification #[8138]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_4 a_1 a_3) True % 150.97/151.20 Clause #8150 (by superposition #[8142, 2835]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_1 a_4 a a_2) True) (Eq True False) % 150.97/151.20 Clause #8151 (by clausification #[8150]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a_4 a a_2) True % 150.97/151.20 Clause #8154 (by superposition #[8151, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_2 a a_3 a_4) True) % 150.97/151.20 Clause #8500 (by clausification #[8154]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a_2 a a_3 a_4) True % 150.97/151.20 Clause #8506 (by superposition #[8500, 2835]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a_2 a_4) True) (Eq True False) % 150.97/151.20 Clause #8508 (by clausification #[8506]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqangle a a_1 a_2 a_3 a_3 a_1 a_2 a_4) True % 150.97/151.20 Clause #8509 (by superposition #[8508, 771]): Eq True False % 150.97/151.20 Clause #8517 (by clausification #[8509]): False % 150.97/151.20 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------