%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO638+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:47 PM UTC 2025 % Result : Theorem 216.87s 217.06s % Output : Proof 217.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GEO638+1 : TPTP v9.2.0. Released v7.5.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 11:50:38 EDT 2025 % 0.13/0.35 % CPUTime : % 216.87/217.06 SZS status Theorem for theBenchmark.p % 216.87/217.06 SZS output start Proof for theBenchmark.p % 216.87/217.06 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 216.87/217.06 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 216.87/217.06 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 216.87/217.06 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 216.87/217.06 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 216.87/217.06 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 216.87/217.06 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 % 216.87/217.06 Clause #11 (by assumption #[]): Eq (∀ (A B C O : Iota), And (cong O A O B) (cong O A O C) → circle O A B C) True % 216.87/217.06 Clause #13 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A B D C) True % 216.87/217.06 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 216.87/217.06 Clause #15 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic B A C D) True % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 Clause #29 (by assumption #[]): Eq % 216.87/217.06 (∀ (A B C D E F G H P Q U V : Iota), % 216.87/217.06 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) % 216.87/217.06 True % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 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 % 216.87/217.06 Clause #43 (by assumption #[]): Eq % 216.87/217.06 (∀ (A B C P Q R : Iota), % 216.87/217.06 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) % 216.87/217.06 True % 216.87/217.06 Clause #53 (by assumption #[]): Eq (∀ (A B C O : Iota), And (circle O A B C) (coll O A C) → perp A B B C) True % 216.87/217.06 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 % 216.87/217.06 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 216.87/217.06 Clause #74 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), And (eqangle A B C D P Q U V) (perp P Q U V) → perp A B C D) True % 216.87/217.06 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 % 216.87/217.06 Clause #94 (by assumption #[]): Eq % 216.87/217.06 (Not % 216.87/217.06 (∀ (A B E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 216.87/217.06 And % 216.87/217.06 (And % 216.87/217.06 (And % 216.87/217.06 (And % 216.87/217.06 (And (And (And (And (midp E A B) (circle E A NWPNT1 NWPNT2)) (circle E A G NWPNT3)) (perp E G G D)) % 216.87/217.06 (para A D C B)) % 216.87/217.06 (coll C G D)) % 216.87/217.06 (midp F C D)) % 216.87/217.06 (perp H F A B)) % 216.87/217.06 (coll H A B) → % 216.87/217.06 perp C H D H)) % 216.87/217.06 True % 216.87/217.06 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 216.90/217.08 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 216.90/217.08 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 % 216.90/217.08 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) % 216.90/217.08 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 216.90/217.08 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 216.90/217.08 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 % 216.90/217.08 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) % 216.90/217.08 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 216.90/217.08 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 216.90/217.08 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 % 216.90/217.08 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) % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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) % 216.90/217.08 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)) % 216.90/217.08 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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) % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 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 % 216.90/217.08 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 216.90/217.08 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) % 216.90/217.08 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 216.90/217.08 Or (Eq (cyclic a a_1 a_2 a_3) True) % 216.90/217.08 (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)) % 216.90/217.08 Clause #170 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic B a C D) True % 216.90/217.08 Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a_1 a C D) True % 216.90/217.08 Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a_1 a a_2 D) True % 216.90/217.11 Clause #173 (by clausification #[172]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a_1 a a_2 a_3) True % 216.90/217.11 Clause #174 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a_1 a a_2 a_3) True) % 216.90/217.11 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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) % 216.90/217.11 Clause #180 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a B D C) True % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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) % 216.90/217.11 Clause #249 (by clausification #[53]): ∀ (a : Iota), Eq (∀ (B C O : Iota), And (circle O a B C) (coll O a C) → perp a B B C) True % 216.90/217.11 Clause #250 (by clausification #[249]): ∀ (a a_1 : Iota), Eq (∀ (C O : Iota), And (circle O a a_1 C) (coll O a C) → perp a a_1 a_1 C) True % 216.90/217.11 Clause #251 (by clausification #[250]): ∀ (a a_1 a_2 : Iota), Eq (∀ (O : Iota), And (circle O a a_1 a_2) (coll O a a_2) → perp a a_1 a_1 a_2) True % 216.90/217.11 Clause #252 (by clausification #[251]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (circle a a_1 a_2 a_3) (coll a a_1 a_3) → perp a_1 a_2 a_2 a_3) True % 216.90/217.11 Clause #253 (by clausification #[252]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (circle a a_1 a_2 a_3) (coll a a_1 a_3)) False) (Eq (perp a_1 a_2 a_2 a_3) True) % 216.90/217.11 Clause #254 (by clausification #[253]): ∀ (a a_1 a_2 a_3 : Iota), % 216.90/217.11 Or (Eq (perp a a_1 a_1 a_2) True) (Or (Eq (circle a_3 a a_1 a_2) False) (Eq (coll a_3 a a_2) False)) % 216.90/217.11 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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) % 216.90/217.11 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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 % 216.90/217.11 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) % 216.90/217.11 Clause #271 (by clausification #[11]): ∀ (a : Iota), Eq (∀ (B C O : Iota), And (cong O a O B) (cong O a O C) → circle O a B C) True % 216.90/217.11 Clause #272 (by clausification #[271]): ∀ (a a_1 : Iota), Eq (∀ (C O : Iota), And (cong O a O a_1) (cong O a O C) → circle O a a_1 C) True % 216.90/217.11 Clause #273 (by clausification #[272]): ∀ (a a_1 a_2 : Iota), Eq (∀ (O : Iota), And (cong O a O a_1) (cong O a O a_2) → circle O a a_1 a_2) True % 216.94/217.13 Clause #274 (by clausification #[273]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (cong a a_1 a a_2) (cong a a_1 a a_3) → circle a a_1 a_2 a_3) True % 216.94/217.13 Clause #275 (by clausification #[274]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (cong a a_1 a a_2) (cong a a_1 a a_3)) False) (Eq (circle a a_1 a_2 a_3) True) % 216.94/217.13 Clause #276 (by clausification #[275]): ∀ (a a_1 a_2 a_3 : Iota), % 216.94/217.13 Or (Eq (circle a a_1 a_2 a_3) True) (Or (Eq (cong a a_1 a a_2) False) (Eq (cong a a_1 a a_3) False)) % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.94/217.13 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) % 216.94/217.13 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.94/217.13 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)) % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.94/217.13 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) % 216.94/217.13 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.94/217.13 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)) % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 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 % 216.94/217.13 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.94/217.13 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 % 216.94/217.13 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.94/217.13 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 % 216.94/217.13 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 216.94/217.13 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 % 216.96/217.15 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.15 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 % 216.96/217.15 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.15 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) % 216.96/217.15 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 % 216.96/217.15 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 % 216.96/217.15 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 % 216.96/217.15 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 % 216.96/217.15 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 % 216.96/217.15 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 % 216.96/217.15 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) % 216.96/217.15 Clause #360 (by clausification #[43]): ∀ (a : Iota), % 216.96/217.15 Eq % 216.96/217.15 (∀ (B C P Q R : Iota), % 216.96/217.15 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) % 216.96/217.15 True % 216.96/217.15 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 216.96/217.15 Eq % 216.96/217.15 (∀ (C P Q R : Iota), % 216.96/217.15 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) → % 216.96/217.15 cong a a_1 P Q) % 216.96/217.15 True % 216.96/217.15 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota), % 216.96/217.15 Eq % 216.96/217.15 (∀ (P Q R : Iota), % 216.96/217.15 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) → % 216.96/217.15 cong a a_1 P Q) % 216.96/217.15 True % 216.96/217.15 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 216.96/217.15 Eq % 216.96/217.15 (∀ (Q R : Iota), % 216.96/217.15 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)) % 216.96/217.15 (eqangle a_2 a a_2 a_1 R a_3 R Q) → % 216.96/217.15 cong a a_1 a_3 Q) % 216.96/217.15 True % 216.96/217.15 Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.15 Eq % 216.96/217.15 (∀ (R : Iota), % 216.96/217.15 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)) % 216.96/217.15 (eqangle a_2 a a_2 a_1 R a_3 R a_4) → % 216.96/217.15 cong a a_1 a_3 a_4) % 216.96/217.15 True % 216.96/217.15 Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.15 Eq % 216.96/217.15 (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)) % 216.96/217.15 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4) → % 216.96/217.15 cong a a_1 a_3 a_4) % 216.96/217.15 True % 216.96/217.15 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.15 Or % 216.96/217.15 (Eq % 216.96/217.15 (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)) % 216.96/217.15 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4)) % 216.96/217.15 False) % 216.96/217.15 (Eq (cong a a_1 a_3 a_4) True) % 216.96/217.15 Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.15 Or (Eq (cong a a_1 a_2 a_3) True) % 216.96/217.15 (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) % 216.96/217.15 (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)) % 216.96/217.15 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.15 Or (Eq (cong a a_1 a_2 a_3) True) % 216.96/217.15 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 216.96/217.15 (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))) % 216.96/217.15 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.15 Or (Eq (cong a a_1 a_2 a_3) True) % 216.96/217.15 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 216.96/217.15 (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)))) % 216.96/217.15 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 % 216.96/217.18 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 % 216.96/217.18 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 % 216.96/217.18 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 % 216.96/217.18 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.18 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) % 216.96/217.18 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 % 216.96/217.18 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 % 216.96/217.18 Clause #460 (by clausification #[459]): ∀ (a a_1 a_2 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #461 (by clausification #[460]): ∀ (a a_1 a_2 a_3 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #462 (by clausification #[461]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.18 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 % 216.96/217.18 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.18 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) % 216.96/217.18 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.18 Or (Eq (cong a a_1 a_2 a_3) True) % 216.96/217.18 (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)) % 216.96/217.18 Clause #468 (by clausification #[74]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), And (eqangle a B C D P Q U V) (perp P Q U V) → perp a B C D) True % 216.96/217.18 Clause #469 (by clausification #[468]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), And (eqangle a a_1 C D P Q U V) (perp P Q U V) → perp a a_1 C D) True % 216.96/217.18 Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 : Iota), % 216.96/217.18 Eq (∀ (D P Q U V : Iota), And (eqangle a a_1 a_2 D P Q U V) (perp P Q U V) → perp a a_1 a_2 D) True % 216.96/217.18 Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 : Iota), % 216.96/217.18 Eq (∀ (P Q U V : Iota), And (eqangle a a_1 a_2 a_3 P Q U V) (perp P Q U V) → perp a a_1 a_2 a_3) True % 216.96/217.18 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.18 Eq (∀ (Q U V : Iota), And (eqangle a a_1 a_2 a_3 a_4 Q U V) (perp a_4 Q U V) → perp a a_1 a_2 a_3) True % 216.96/217.20 Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.20 Eq (∀ (U V : Iota), And (eqangle a a_1 a_2 a_3 a_4 a_5 U V) (perp a_4 a_5 U V) → perp a a_1 a_2 a_3) True % 216.96/217.20 Clause #474 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 216.96/217.20 Eq (∀ (V : Iota), And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V) (perp a_4 a_5 a_6 V) → perp a a_1 a_2 a_3) True % 216.96/217.20 Clause #475 (by clausification #[474]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.20 Eq (And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (perp a_4 a_5 a_6 a_7) → perp a a_1 a_2 a_3) True % 216.96/217.20 Clause #476 (by clausification #[475]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.20 Or (Eq (And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (perp a_4 a_5 a_6 a_7)) False) (Eq (perp a a_1 a_2 a_3) True) % 216.96/217.20 Clause #477 (by clausification #[476]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.20 Or (Eq (perp a a_1 a_2 a_3) True) % 216.96/217.20 (Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (perp a_4 a_5 a_6 a_7) False)) % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 216.96/217.20 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) % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 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 % 216.96/217.20 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) % 216.96/217.20 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 % 216.96/217.20 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #549 (by clausification #[548]): ∀ (a a_1 a_2 : Iota), % 216.96/217.20 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 % 216.96/217.20 Clause #550 (by clausification #[549]): ∀ (a a_1 a_2 a_3 : Iota), % 216.96/217.20 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) % 216.96/217.20 True % 216.96/217.20 Clause #551 (by clausification #[550]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 216.96/217.20 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 % 217.03/217.22 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.22 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) % 217.03/217.22 (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True) % 217.03/217.22 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.22 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 217.03/217.22 (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)) % 217.03/217.22 Clause #554 (by clausification #[553]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.22 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 217.03/217.22 (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))) % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 Clause #592 (by clausification #[591]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.22 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 % 217.03/217.22 Clause #593 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.03/217.22 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 % 217.03/217.22 Clause #594 (by clausification #[593]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.03/217.22 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 % 217.03/217.22 Clause #595 (by clausification #[594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.22 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 % 217.03/217.22 Clause #596 (by clausification #[595]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.22 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) % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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) % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 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 % 217.03/217.22 Clause #645 (by clausification #[644]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.22 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 % 217.03/217.22 Clause #646 (by clausification #[645]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #647 (by clausification #[646]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #648 (by clausification #[647]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #649 (by clausification #[648]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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) % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 Clause #698 (by clausification #[697]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #699 (by clausification #[698]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #700 (by clausification #[699]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #701 (by clausification #[700]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #702 (by clausification #[701]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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) % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 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 % 217.03/217.25 Clause #707 (by clausification #[706]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #708 (by clausification #[707]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #709 (by clausification #[708]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #710 (by clausification #[709]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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 % 217.03/217.25 Clause #711 (by clausification #[710]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.03/217.25 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) % 217.03/217.25 Clause #712 (by clausification #[94]): Eq % 217.03/217.25 (∀ (A B E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.25 And % 217.03/217.25 (And % 217.03/217.25 (And % 217.03/217.25 (And % 217.03/217.25 (And (And (And (And (midp E A B) (circle E A NWPNT1 NWPNT2)) (circle E A G NWPNT3)) (perp E G G D)) % 217.03/217.25 (para A D C B)) % 217.03/217.25 (coll C G D)) % 217.03/217.25 (midp F C D)) % 217.03/217.25 (perp H F A B)) % 217.03/217.27 (coll H A B) → % 217.03/217.27 perp C H D H) % 217.03/217.27 False % 217.03/217.27 Clause #713 (by clausification #[712]): ∀ (a : Iota), % 217.03/217.27 Eq % 217.03/217.27 (Not % 217.03/217.27 (∀ (B E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (And (midp E (skS.0 10 a) B) (circle E (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle E (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp E G G D)) % 217.03/217.27 (para (skS.0 10 a) D C B)) % 217.03/217.27 (coll C G D)) % 217.03/217.27 (midp F C D)) % 217.03/217.27 (perp H F (skS.0 10 a) B)) % 217.03/217.27 (coll H (skS.0 10 a) B) → % 217.03/217.27 perp C H D H)) % 217.03/217.27 True % 217.03/217.27 Clause #714 (by clausification #[713]): ∀ (a : Iota), % 217.03/217.27 Eq % 217.03/217.27 (∀ (B E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (And (midp E (skS.0 10 a) B) (circle E (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle E (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp E G G D)) % 217.03/217.27 (para (skS.0 10 a) D C B)) % 217.03/217.27 (coll C G D)) % 217.03/217.27 (midp F C D)) % 217.03/217.27 (perp H F (skS.0 10 a) B)) % 217.03/217.27 (coll H (skS.0 10 a) B) → % 217.03/217.27 perp C H D H) % 217.03/217.27 False % 217.03/217.27 Clause #715 (by clausification #[714]): ∀ (a a_1 : Iota), % 217.03/217.27 Eq % 217.03/217.27 (Not % 217.03/217.27 (∀ (E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (And (midp E (skS.0 10 a) (skS.0 11 a a_1)) (circle E (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle E (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp E G G D)) % 217.03/217.27 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.03/217.27 (coll C G D)) % 217.03/217.27 (midp F C D)) % 217.03/217.27 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.03/217.27 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.03/217.27 perp C H D H)) % 217.03/217.27 True % 217.03/217.27 Clause #716 (by clausification #[715]): ∀ (a a_1 : Iota), % 217.03/217.27 Eq % 217.03/217.27 (∀ (E G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (And (midp E (skS.0 10 a) (skS.0 11 a a_1)) (circle E (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle E (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp E G G D)) % 217.03/217.27 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.03/217.27 (coll C G D)) % 217.03/217.27 (midp F C D)) % 217.03/217.27 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.03/217.27 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.03/217.27 perp C H D H) % 217.03/217.27 False % 217.03/217.27 Clause #717 (by clausification #[716]): ∀ (a a_1 a_2 : Iota), % 217.03/217.27 Eq % 217.03/217.27 (Not % 217.03/217.27 (∀ (G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.03/217.27 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp (skS.0 12 a a_1 a_2) G G D)) % 217.03/217.27 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.03/217.27 (coll C G D)) % 217.03/217.27 (midp F C D)) % 217.03/217.27 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.03/217.27 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.03/217.27 perp C H D H)) % 217.03/217.27 True % 217.03/217.27 Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 : Iota), % 217.03/217.27 Eq % 217.03/217.27 (∀ (G D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.03/217.27 And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And % 217.03/217.27 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.03/217.27 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.03/217.27 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) G NWPNT3)) % 217.03/217.27 (perp (skS.0 12 a a_1 a_2) G G D)) % 217.09/217.29 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.09/217.29 (coll C G D)) % 217.09/217.29 (midp F C D)) % 217.09/217.29 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.29 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.29 perp C H D H) % 217.09/217.29 False % 217.09/217.29 Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 : Iota), % 217.09/217.29 Eq % 217.09/217.29 (Not % 217.09/217.29 (∀ (D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.29 And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.29 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) D)) % 217.09/217.29 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.09/217.29 (coll C (skS.0 13 a a_1 a_2 a_3) D)) % 217.09/217.29 (midp F C D)) % 217.09/217.29 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.29 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.29 perp C H D H)) % 217.09/217.29 True % 217.09/217.29 Clause #720 (by clausification #[719]): ∀ (a a_1 a_2 a_3 : Iota), % 217.09/217.29 Eq % 217.09/217.29 (∀ (D C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.29 And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.29 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) D)) % 217.09/217.29 (para (skS.0 10 a) D C (skS.0 11 a a_1))) % 217.09/217.29 (coll C (skS.0 13 a a_1 a_2 a_3) D)) % 217.09/217.29 (midp F C D)) % 217.09/217.29 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.29 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.29 perp C H D H) % 217.09/217.29 False % 217.09/217.29 Clause #721 (by clausification #[720]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.09/217.29 Eq % 217.09/217.29 (Not % 217.09/217.29 (∀ (C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.29 And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.29 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.29 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.29 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) C (skS.0 11 a a_1))) % 217.09/217.29 (coll C (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.29 (midp F C (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.29 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.29 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.29 perp C H (skS.0 14 a a_1 a_2 a_3 a_4) H)) % 217.09/217.29 True % 217.09/217.29 Clause #722 (by clausification #[721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.09/217.29 Eq % 217.09/217.29 (∀ (C F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.29 And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And % 217.09/217.29 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.29 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.29 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.29 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.29 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) C (skS.0 11 a a_1))) % 217.09/217.29 (coll C (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.29 (midp F C (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.31 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.31 perp C H (skS.0 14 a a_1 a_2 a_3 a_4) H) % 217.09/217.31 False % 217.09/217.31 Clause #723 (by clausification #[722]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.09/217.31 Eq % 217.09/217.31 (Not % 217.09/217.31 (∀ (F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.31 And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.31 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.31 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.31 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (midp F (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.31 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.31 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) H (skS.0 14 a a_1 a_2 a_3 a_4) H)) % 217.09/217.31 True % 217.09/217.31 Clause #724 (by clausification #[723]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.09/217.31 Eq % 217.09/217.31 (∀ (F H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.31 And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.31 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.31 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.31 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (midp F (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (perp H F (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.31 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.31 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) H (skS.0 14 a a_1 a_2 a_3 a_4) H) % 217.09/217.31 False % 217.09/217.31 Clause #725 (by clausification #[724]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.09/217.31 Eq % 217.09/217.31 (Not % 217.09/217.31 (∀ (H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.31 And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.31 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.31 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.31 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.31 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.31 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 217.09/217.31 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.31 (perp H (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.31 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.31 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) H (skS.0 14 a a_1 a_2 a_3 a_4) H)) % 217.09/217.31 True % 217.09/217.31 Clause #726 (by clausification #[725]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.09/217.31 Eq % 217.09/217.31 (∀ (H NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.31 And % 217.09/217.31 (And % 217.09/217.31 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.33 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.33 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.33 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (perp H (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a) (skS.0 11 a a_1))) % 217.09/217.33 (coll H (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.33 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) H (skS.0 14 a a_1 a_2 a_3 a_4) H) % 217.09/217.33 False % 217.09/217.33 Clause #727 (by clausification #[726]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.09/217.33 Eq % 217.09/217.33 (Not % 217.09/217.33 (∀ (NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.33 And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.33 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.33 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.33 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 217.09/217.33 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.09/217.33 (skS.0 11 a a_1))) % 217.09/217.33 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.33 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.09/217.33 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 217.09/217.33 True % 217.09/217.33 Clause #728 (by clausification #[727]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.09/217.33 Eq % 217.09/217.33 (∀ (NWPNT1 NWPNT2 NWPNT3 : Iota), % 217.09/217.33 And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And % 217.09/217.33 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) NWPNT1 NWPNT2)) % 217.09/217.33 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.33 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.33 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.33 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.33 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.09/217.33 (skS.0 11 a a_1))) % 217.09/217.33 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.33 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.09/217.33 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 217.09/217.33 False % 217.09/217.33 Clause #729 (by clausification #[728]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 217.09/217.35 Eq % 217.09/217.35 (Not % 217.09/217.35 (∀ (NWPNT2 NWPNT3 : Iota), % 217.09/217.35 And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.09/217.35 NWPNT2)) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.35 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.35 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.35 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 217.09/217.35 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.09/217.35 (skS.0 11 a a_1))) % 217.09/217.35 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.35 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.09/217.35 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 217.09/217.35 True % 217.09/217.35 Clause #730 (by clausification #[729]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 217.09/217.35 Eq % 217.09/217.35 (∀ (NWPNT2 NWPNT3 : Iota), % 217.09/217.35 And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) NWPNT2)) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.35 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.35 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.35 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.09/217.35 (skS.0 11 a a_1))) % 217.09/217.35 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.09/217.35 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.09/217.35 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 217.09/217.35 False % 217.09/217.35 Clause #731 (by clausification #[730]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 217.09/217.35 Eq % 217.09/217.35 (Not % 217.09/217.35 (∀ (NWPNT3 : Iota), % 217.09/217.35 And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And % 217.09/217.35 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.09/217.35 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.09/217.35 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.09/217.35 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.09/217.35 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.09/217.35 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.09/217.35 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 217.17/217.37 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.17/217.37 (skS.0 11 a a_1))) % 217.17/217.37 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.17/217.37 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.17/217.37 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 217.17/217.37 True % 217.17/217.37 Clause #732 (by clausification #[731]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 217.17/217.37 Eq % 217.17/217.37 (∀ (NWPNT3 : Iota), % 217.17/217.37 And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.17/217.37 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.17/217.37 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.17/217.37 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) NWPNT3)) % 217.17/217.37 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.17/217.37 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.17/217.37 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.17/217.37 (skS.0 11 a a_1))) % 217.17/217.37 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.17/217.37 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.17/217.37 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 217.17/217.37 False % 217.17/217.37 Clause #733 (by clausification #[732]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 217.17/217.37 Eq % 217.17/217.37 (Not % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.17/217.37 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.17/217.37 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.17/217.37 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) % 217.17/217.37 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 217.17/217.37 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.17/217.37 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.17/217.37 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.17/217.37 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.17/217.37 (skS.0 11 a a_1))) % 217.17/217.37 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.17/217.37 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.17/217.37 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 217.17/217.37 True % 217.17/217.37 Clause #734 (by clausification #[733]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 217.17/217.37 Eq % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And % 217.17/217.37 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.17/217.37 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.17/217.37 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.20/217.39 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 217.20/217.39 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.20/217.39 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.20/217.39 (skS.0 11 a a_1))) % 217.20/217.39 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) → % 217.20/217.39 perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.20/217.39 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 217.20/217.39 False % 217.20/217.39 Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 217.20/217.39 Eq % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.20/217.39 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.20/217.39 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.20/217.39 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 217.20/217.39 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.20/217.39 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.20/217.39 (skS.0 11 a a_1))) % 217.20/217.39 (coll (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1))) % 217.20/217.39 True % 217.20/217.39 Clause #736 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.39 Eq % 217.20/217.39 (perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 14 a a_1 a_2 a_3 a_4) % 217.20/217.39 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 217.20/217.39 False % 217.20/217.39 Clause #738 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 217.20/217.39 Eq % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And % 217.20/217.39 (And (midp (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 11 a a_1)) % 217.20/217.39 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 217.20/217.39 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 217.20/217.39 (circle (skS.0 12 a a_1 a_2) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 217.20/217.39 (perp (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 13 a a_1 a_2 a_3) % 217.20/217.39 (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (para (skS.0 10 a) (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1))) % 217.20/217.39 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 13 a a_1 a_2 a_3) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (midp (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 14 a a_1 a_2 a_3 a_4))) % 217.20/217.39 (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) % 217.20/217.39 (skS.0 11 a a_1))) % 217.20/217.39 True % 217.20/217.39 Clause #784 (by clausification #[29]): ∀ (a : Iota), % 217.20/217.39 Eq % 217.20/217.39 (∀ (B C D E F G H P Q U V : Iota), % 217.20/217.39 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) % 217.20/217.39 True % 217.20/217.39 Clause #785 (by clausification #[784]): ∀ (a a_1 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (C D E F G H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (D E F G H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (E F G H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #788 (by clausification #[787]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (F G H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #789 (by clausification #[788]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (G H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #790 (by clausification #[789]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (H P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #791 (by clausification #[790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (P Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #792 (by clausification #[791]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (Q U V : Iota), % 217.20/217.41 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) % 217.20/217.41 True % 217.20/217.41 Clause #793 (by clausification #[792]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (U V : Iota), % 217.20/217.41 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) → % 217.20/217.41 eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9) % 217.20/217.41 True % 217.20/217.41 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 : Iota), % 217.20/217.41 Eq % 217.20/217.41 (∀ (V : Iota), % 217.20/217.41 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) → % 217.20/217.41 eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10) % 217.20/217.41 True % 217.20/217.41 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), % 217.20/217.41 Eq % 217.20/217.41 (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) → % 217.20/217.41 eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 217.20/217.41 True % 217.20/217.41 Clause #796 (by clausification #[795]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 217.20/217.41 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) % 217.20/217.41 (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 217.20/217.41 Clause #797 (by clausification #[796]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 217.20/217.41 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 217.20/217.41 (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)) % 217.20/217.41 Clause #887 (by clausification #[738]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.41 Eq (perp (skS.0 17 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 a_4 a_5 a_6) (skS.0 10 a) (skS.0 11 a a_1)) % 217.20/217.41 True % 217.20/217.41 Clause #890 (by superposition #[887, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.41 Or (Eq True False) % 217.20/217.41 (Eq % 217.20/217.41 (perp (skS.0 10 a) (skS.0 11 a a_1) (skS.0 17 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 a_4 a_5 a_6)) % 217.20/217.41 True) % 217.20/217.41 Clause #1466 (by clausification #[890]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.41 Eq (perp (skS.0 10 a) (skS.0 11 a a_1) (skS.0 17 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 a_4 a_5 a_6)) % 217.20/217.41 True % 217.20/217.41 Clause #1467 (by superposition #[1466, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.20/217.41 Or (Eq True False) % 217.20/217.41 (Eq % 217.20/217.41 (perp (skS.0 10 a) (skS.0 11 a a_1) (skS.0 16 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 a_5 a_6 a_7)) % 217.20/217.41 True) % 217.20/217.41 Clause #1478 (by clausification #[1467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.26/217.44 Eq (perp (skS.0 10 a) (skS.0 11 a a_1) (skS.0 16 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 a_5 a_6 a_7)) % 217.26/217.44 True % 217.26/217.44 Clause #1479 (by superposition #[1478, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.26/217.44 Or (Eq True False) % 217.26/217.44 (Eq % 217.26/217.44 (perp (skS.0 16 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 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) % 217.26/217.44 True) % 217.26/217.44 Clause #1480 (by superposition #[1478, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 217.26/217.44 Or (Eq (para (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3) True) % 217.26/217.44 (Or (Eq True False) % 217.26/217.44 (Eq (perp (skS.0 16 a a_1 a_4 a_5 a_6 a_7 a_8) (skS.0 17 a a_1 a_4 a_5 a_6 a_7 a_8 a_9) a_2 a_3) False)) % 217.26/217.44 Clause #1489 (by clausification #[1479]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.26/217.44 Eq (perp (skS.0 16 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 a_5 a_6 a_7) (skS.0 10 a) (skS.0 11 a a_1)) % 217.26/217.44 True % 217.26/217.44 Clause #1490 (by superposition #[1489, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.26/217.44 Or (Eq True False) % 217.26/217.44 (Eq % 217.26/217.44 (perp (skS.0 16 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 a_5 a_6 a_7) (skS.0 11 a a_1) (skS.0 10 a)) % 217.26/217.44 True) % 217.26/217.44 Clause #1500 (by clausification #[1490]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.26/217.44 Eq (perp (skS.0 16 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 a_5 a_6 a_7) (skS.0 11 a a_1) (skS.0 10 a)) % 217.26/217.44 True % 217.26/217.44 Clause #1564 (by clausification #[1480]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 217.26/217.44 Or (Eq (para (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3) True) % 217.26/217.44 (Eq (perp (skS.0 16 a a_1 a_4 a_5 a_6 a_7 a_8) (skS.0 17 a a_1 a_4 a_5 a_6 a_7 a_8 a_9) a_2 a_3) False) % 217.26/217.44 Clause #1566 (by superposition #[1564, 1500]): ∀ (a a_1 : Iota), Or (Eq (para (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a)) True) (Eq False True) % 217.26/217.44 Clause #1567 (by clausification #[1566]): ∀ (a a_1 : Iota), Eq (para (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a)) True % 217.26/217.44 Clause #1571 (by superposition #[1567, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1)) True) % 217.26/217.44 Clause #1590 (by clausification #[1571]): ∀ (a a_1 : Iota), Eq (para (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1)) True % 217.26/217.44 Clause #1594 (by superposition #[1590, 610]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Or (Eq True False) (Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3 (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3) True) % 217.26/217.44 Clause #1595 (by clausification #[1594]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3 (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3) True % 217.26/217.44 Clause #1603 (by superposition #[1595, 496]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Or (Eq True False) (Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3 a_2 a_3) True) % 217.26/217.44 Clause #1607 (by clausification #[1603]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) a_2 a_3 a_2 a_3) True % 217.26/217.44 Clause #1613 (by superposition #[1607, 441]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Or (Eq True False) (Eq (eqangle a a_1 a a_1 (skS.0 10 a_2) (skS.0 11 a_2 a_3) (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True) % 217.26/217.44 Clause #1620 (by clausification #[1613]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Eq (eqangle a a_1 a a_1 (skS.0 10 a_2) (skS.0 11 a_2 a_3) (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True % 217.26/217.44 Clause #1624 (by superposition #[1620, 352]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Or (Eq True False) (Eq (eqangle a a_1 a_1 a (skS.0 10 a_2) (skS.0 11 a_2 a_3) (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True) % 217.26/217.44 Clause #1631 (by clausification #[1624]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Eq (eqangle a a_1 a_1 a (skS.0 10 a_2) (skS.0 11 a_2 a_3) (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True % 217.26/217.44 Clause #1638 (by superposition #[1631, 496]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Or (Eq True False) (Eq (eqangle a a_1 (skS.0 10 a_2) (skS.0 11 a_2 a_3) a_1 a (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True) % 217.26/217.44 Clause #1643 (by clausification #[1638]): ∀ (a a_1 a_2 a_3 : Iota), % 217.26/217.44 Eq (eqangle a a_1 (skS.0 10 a_2) (skS.0 11 a_2 a_3) a_1 a (skS.0 10 a_2) (skS.0 11 a_2 a_3)) True % 217.26/217.44 Clause #1647 (by superposition #[1643, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 217.28/217.46 Clause #1656 (by clausification #[1647]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 217.28/217.46 Clause #1665 (by superposition #[1656, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 217.28/217.46 Clause #1689 (by clausification #[1665]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 217.28/217.46 Clause #1690 (by superposition #[1689, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 217.28/217.46 Clause #1694 (by superposition #[1689, 610]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True) % 217.28/217.46 Clause #1695 (by clausification #[1690]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 217.28/217.46 Clause #1706 (by superposition #[1695, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 217.28/217.46 Clause #1715 (by clausification #[1706]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 217.28/217.46 Clause #1729 (by superposition #[1715, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 217.28/217.46 Clause #1738 (by clausification #[1729]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 217.28/217.46 Clause #1753 (by superposition #[1738, 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)) % 217.28/217.46 Clause #1755 (by superposition #[1738, 554]): ∀ (a a_1 a_2 a_3 : Iota), % 217.28/217.46 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) % 217.28/217.46 (Or (Eq True False) (Or (Eq (para a_1 a a_2 a_3) False) (Eq (coll a a_1 a_2) False))) % 217.28/217.46 Clause #1782 (by clausification #[1694]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True % 217.28/217.46 Clause #1784 (by superposition #[1782, 162]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Or (Eq True False) (Eq (coll a_2 a_2 a_1) False)) % 217.28/217.46 Clause #1788 (by superposition #[1782, 369]): ∀ (a a_1 a_2 : Iota), % 217.28/217.46 Or (Eq (cong a a_1 a a_1) True) % 217.28/217.46 (Or (Eq True False) % 217.28/217.46 (Or (Eq (cyclic a a_1 a_2 a_2) False) (Or (Eq (cyclic a a_1 a_2 a) False) (Eq (cyclic a a_1 a_2 a_1) False)))) % 217.28/217.46 Clause #1880 (by clausification #[1753]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 217.28/217.46 Clause #1886 (by superposition #[1880, 1738]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 217.28/217.46 Clause #1887 (by clausification #[1886]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 217.28/217.46 Clause #1910 (by backward demodulation #[1887, 254]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_1 a_2) True) (Or (Eq (circle a_3 a a_1 a_2) False) (Eq True False)) % 217.28/217.46 Clause #1936 (by clausification #[1784]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 217.28/217.46 Clause #1937 (by forward demodulation #[1936, 1887]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq True False) % 217.28/217.46 Clause #1938 (by clausification #[1937]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_2) True % 217.28/217.46 Clause #1940 (by superposition #[1938, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_2 a_1) True) % 217.28/217.46 Clause #1946 (by clausification #[1940]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_1) True % 217.28/217.46 Clause #1948 (by superposition #[1946, 184]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_1 a_2) True) % 217.28/217.46 Clause #1953 (by clausification #[1948]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_1 a_2) True % 217.28/217.46 Clause #1954 (by superposition #[1953, 174]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 217.28/217.46 Clause #1959 (by clausification #[1954]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 217.28/217.46 Clause #1962 (by superposition #[1959, 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)) % 217.28/217.46 Clause #2259 (by clausification #[1962]): ∀ (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) % 217.28/217.46 Clause #2263 (by superposition #[2259, 1959]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 217.28/217.46 Clause #2264 (by clausification #[2263]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 217.28/217.46 Clause #2268 (by backward demodulation #[2264, 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) % 217.28/217.49 Clause #2272 (by clausification #[2268]): ∀ (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 % 217.28/217.49 Clause #2275 (by superposition #[2272, 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) % 217.28/217.49 Clause #2278 (by clausification #[2275]): ∀ (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 % 217.28/217.49 Clause #2280 (by superposition #[2278, 477]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_1) True) (Or (Eq True False) (Eq (perp a a_3 a_2 a_3) False)) % 217.28/217.49 Clause #2360 (by clausification #[2280]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_1) True) (Eq (perp a a_3 a_2 a_3) False) % 217.28/217.49 Clause #2442 (by clausification #[1910]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_1 a_2) True) (Eq (circle a_3 a a_1 a_2) False) % 217.28/217.49 Clause #2818 (by clausification #[1755]): ∀ (a a_1 a_2 a_3 : Iota), % 217.28/217.49 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Or (Eq (para a_1 a a_2 a_3) False) (Eq (coll a a_1 a_2) False)) % 217.28/217.49 Clause #2819 (by forward demodulation #[2818, 1887]): ∀ (a a_1 a_2 a_3 : Iota), % 217.28/217.49 Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Or (Eq (para a_1 a a_2 a_3) False) (Eq True False)) % 217.28/217.49 Clause #2820 (by clausification #[2819]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a a a_3) True) (Eq (para a_1 a a_2 a_3) False) % 217.28/217.49 Clause #2821 (by superposition #[2820, 1656]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a a a a a_1) True) (Eq False True) % 217.28/217.49 Clause #2822 (by superposition #[2820, 1689]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a a a a) True) (Eq False True) % 217.28/217.49 Clause #2827 (by clausification #[2822]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a a a) True % 217.28/217.49 Clause #2832 (by superposition #[2827, 711]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a_1 a a) True) % 217.28/217.49 Clause #2834 (by clausification #[2832]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a_1 a a) True % 217.28/217.49 Clause #2836 (by superposition #[2834, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a a_1 a_1) True) % 217.28/217.49 Clause #2855 (by clausification #[2821]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a_1) True % 217.28/217.49 Clause #2860 (by superposition #[2855, 711]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a a a_1) True) % 217.28/217.49 Clause #2862 (by clausification #[2860]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a a a_1) True % 217.28/217.49 Clause #2864 (by superposition #[2862, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True) % 217.28/217.49 Clause #2867 (by clausification #[2864]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True % 217.28/217.49 Clause #2870 (by superposition #[2867, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True) % 217.28/217.49 Clause #2877 (by clausification #[2870]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True % 217.28/217.49 Clause #2880 (by superposition #[2877, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a_1 a) True) % 217.28/217.49 Clause #2980 (by clausification #[2836]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a a_1 a_1) True % 217.28/217.49 Clause #2982 (by superposition #[2980, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a a_1 a_1) True) % 217.28/217.49 Clause #2983 (by superposition #[2980, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_1 a_1 a_1) True) % 217.28/217.49 Clause #2985 (by clausification #[2983]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a_1 a a_1 a_1 a_1) True % 217.28/217.49 Clause #2987 (by superposition #[2985, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a a_1 a) True) % 217.28/217.49 Clause #3004 (by clausification #[2987]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a_1 a a a_1 a) True % 217.28/217.49 Clause #3007 (by clausification #[2982]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a_1 a_1) True % 217.28/217.49 Clause #3009 (by superposition #[3007, 797]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.49 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) False)) % 217.28/217.49 Clause #3040 (by clausification #[2880]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a_1 a) True % 217.28/217.51 Clause #3124 (by clausification #[3009]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.51 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) False) % 217.28/217.51 Clause #3132 (by superposition #[3124, 3004]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a_1 a a a a_1 a) True) (Eq False True) % 217.28/217.51 Clause #3172 (by clausification #[3132]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a_1 a) True % 217.28/217.51 Clause #3175 (by superposition #[3172, 711]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_1 a) True) % 217.28/217.51 Clause #3177 (by clausification #[3175]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a a_1 a) True % 217.28/217.51 Clause #3179 (by superposition #[3177, 702]): ∀ (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) % 217.28/217.51 Clause #3187 (by clausification #[3179]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_1 a_1 a_1) True % 217.28/217.51 Clause #3189 (by superposition #[3187, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a a) True) % 217.28/217.51 Clause #3191 (by clausification #[3189]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a) True % 217.28/217.51 Clause #3194 (by superposition #[3191, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a a_1 a_1 a) True) % 217.28/217.51 Clause #3231 (by clausification #[3194]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a_1 a_1 a) True % 217.28/217.51 Clause #3233 (by superposition #[3231, 797]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.51 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Or (Eq True False) (Eq (eqratio a a_5 a_5 a a_1 a_2 a_3 a_4) False)) % 217.28/217.51 Clause #3288 (by clausification #[3233]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.51 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Eq (eqratio a a_5 a_5 a a_1 a_2 a_3 a_4) False) % 217.28/217.51 Clause #3292 (by superposition #[3288, 3040]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a a a a_1 a) True) (Eq False True) % 217.28/217.51 Clause #3313 (by clausification #[3292]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a a_1 a) True % 217.28/217.51 Clause #3315 (by superposition #[3313, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a a) True) % 217.28/217.51 Clause #3316 (by superposition #[3313, 702]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a a a) True) % 217.28/217.51 Clause #3318 (by clausification #[3316]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a a) True % 217.28/217.51 Clause #3320 (by superposition #[3318, 649]): ∀ (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) % 217.28/217.51 Clause #3323 (by clausification #[3320]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_1 a_1 a_1) True % 217.28/217.51 Clause #3325 (by superposition #[3323, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a a a) True) % 217.28/217.51 Clause #3327 (by clausification #[3325]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a a a) True % 217.28/217.51 Clause #3329 (by superposition #[3327, 649]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a a a a) True) % 217.28/217.51 Clause #3344 (by clausification #[3329]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a a a) True % 217.28/217.51 Clause #3346 (by superposition #[3344, 797]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.51 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 a a a_2 a_3 a_4 a_5) False)) % 217.28/217.51 Clause #3347 (by clausification #[3315]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a a a) True % 217.28/217.51 Clause #3367 (by clausification #[3346]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 217.28/217.51 Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a a a a a_2 a_3 a_4 a_5) False) % 217.28/217.51 Clause #3381 (by superposition #[3367, 3347]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a_1 a_2 a a a) True) (Eq False True) % 217.28/217.51 Clause #3382 (by clausification #[3381]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a a a) True % 217.28/217.51 Clause #3386 (by superposition #[3382, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a a) True) % 217.28/217.51 Clause #3392 (by clausification #[3386]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a_2 a a) True % 217.28/217.51 Clause #3396 (by superposition #[3392, 3367]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a_1 a a_2 a a) True) (Eq True False) % 217.35/217.53 Clause #3397 (by clausification #[3396]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a a_2 a a) True % 217.35/217.53 Clause #3399 (by superposition #[3397, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a a a_2) True) % 217.35/217.53 Clause #3402 (by clausification #[3399]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a a a a_2) True % 217.35/217.53 Clause #3405 (by superposition #[3402, 3367]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a_1 a a a a_2) True) (Eq True False) % 217.35/217.53 Clause #3406 (by clausification #[3405]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a a a a_2) True % 217.35/217.53 Clause #3408 (by superposition #[3406, 649]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_2 a a) True) % 217.35/217.53 Clause #3428 (by clausification #[3408]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a a_2 a a) True % 217.35/217.53 Clause #3430 (by superposition #[3428, 596]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_1 a_1) True) % 217.35/217.53 Clause #3435 (by clausification #[3430]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a_2 a_1 a_1) True % 217.35/217.53 Clause #3439 (by superposition #[3435, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_1 a_1) True) % 217.35/217.53 Clause #3441 (by clausification #[3439]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_1 a_1 a_1) True % 217.35/217.53 Clause #3444 (by superposition #[3441, 702]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a a_2) True) % 217.35/217.53 Clause #3448 (by clausification #[3444]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a a a_2) True % 217.35/217.53 Clause #3452 (by superposition #[3448, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a a a_3) True) (Eq True False) % 217.35/217.53 Clause #3458 (by clausification #[3452]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a a a_3) True % 217.35/217.53 Clause #3462 (by superposition #[3458, 711]): ∀ (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) % 217.35/217.53 Clause #3464 (by clausification #[3462]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a a_3) True % 217.35/217.53 Clause #3467 (by superposition #[3464, 702]): ∀ (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) % 217.35/217.53 Clause #3470 (by clausification #[3467]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_2 a a a_3 a) True % 217.35/217.53 Clause #3473 (by superposition #[3470, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_3 a a a) True) % 217.35/217.53 Clause #3478 (by clausification #[3473]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_2 a_3 a a a) True % 217.35/217.53 Clause #3481 (by superposition #[3478, 711]): ∀ (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) % 217.35/217.53 Clause #3483 (by clausification #[3481]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a_3 a a) True % 217.35/217.53 Clause #3485 (by superposition #[3483, 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) % 217.35/217.53 Clause #3488 (by clausification #[3485]): ∀ (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 % 217.35/217.53 Clause #3491 (by superposition #[3488, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a a_3 a) True) % 217.35/217.53 Clause #3493 (by clausification #[3491]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a a_2 a a_3 a) True % 217.35/217.53 Clause #3499 (by superposition #[3493, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a a_3 a) True) (Eq True False) % 217.35/217.53 Clause #3505 (by clausification #[3499]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a a_3 a) True % 217.35/217.53 Clause #3507 (by superposition #[3505, 711]): ∀ (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) % 217.35/217.53 Clause #3509 (by clausification #[3507]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a_3 a) True % 217.35/217.53 Clause #3513 (by superposition #[3509, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a a_2 a_3 a) True) (Eq True False) % 217.35/217.53 Clause #3514 (by clausification #[3513]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a a_2 a_3 a) True % 217.35/217.53 Clause #3517 (by superposition #[3514, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a a a_3) True) % 217.35/217.56 Clause #3520 (by clausification #[3517]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a a a_3) True % 217.35/217.56 Clause #3522 (by superposition #[3520, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a_3 a_1 a_1) True) % 217.35/217.56 Clause #3526 (by clausification #[3522]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a_3 a_1 a_1) True % 217.35/217.56 Clause #3530 (by superposition #[3526, 3288]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a a_1 a_2 a_1 a_1) True) (Eq True False) % 217.35/217.56 Clause #3531 (by clausification #[3530]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a_2 a_1 a_1) True % 217.35/217.56 Clause #3537 (by superposition #[3531, 3367]): ∀ (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) % 217.35/217.56 Clause #3538 (by clausification #[3537]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_2 a_2) True % 217.35/217.56 Clause #3541 (by superposition #[3538, 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) % 217.35/217.56 Clause #3543 (by clausification #[3541]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_1 a_1) True % 217.35/217.56 Clause #3545 (by superposition #[3543, 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) % 217.35/217.56 Clause #3551 (by clausification #[3545]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a a a_2 a_3) True % 217.35/217.56 Clause #3555 (by superposition #[3551, 3124]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a a a a_1 a_2) True) (Eq True False) % 217.35/217.56 Clause #3556 (by clausification #[3555]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a a_1 a_2) True % 217.35/217.56 Clause #3560 (by superposition #[3556, 711]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a_1 a_2) True) % 217.35/217.56 Clause #3562 (by clausification #[3560]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a a_1 a_2) True % 217.35/217.56 Clause #3568 (by superposition #[3562, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a a_2 a_3) True) (Eq True False) % 217.35/217.56 Clause #3573 (by clausification #[3568]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a a_2 a_3) True % 217.35/217.56 Clause #3577 (by superposition #[3573, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a_2 a_1 a_3) True) % 217.35/217.56 Clause #3579 (by clausification #[3577]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a a_2 a_1 a_3) True % 217.35/217.56 Clause #3581 (by superposition #[3579, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a_2 a_1 a_3) True) % 217.35/217.56 Clause #3585 (by clausification #[3581]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_2 a_1 a_3) True % 217.35/217.56 Clause #3588 (by superposition #[3585, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a a_2 a_2 a_2) True) % 217.35/217.56 Clause #3590 (by clausification #[3588]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_3 a a_2 a_2 a_2) True % 217.35/217.56 Clause #3593 (by superposition #[3590, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_2 a_3 a_2 a_2) True) % 217.35/217.56 Clause #3600 (by clausification #[3593]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_2 a_2 a_3 a_2 a_2) True % 217.35/217.56 Clause #3602 (by superposition #[3600, 596]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_2 a_3 a_2 a_2) True) % 217.35/217.56 Clause #3604 (by clausification #[3602]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_2 a_2 a_3 a_2 a_2) True % 217.35/217.56 Clause #3607 (by superposition #[3604, 702]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_3 a_3 a) True) % 217.35/217.56 Clause #3609 (by clausification #[3607]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a a_2 a_3 a_3 a) True % 217.35/217.56 Clause #3615 (by superposition #[3609, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_3 a) True) (Eq True False) % 217.35/217.56 Clause #3621 (by clausification #[3615]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_3 a) True % 217.35/217.56 Clause #3625 (by superposition #[3621, 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_2 a) True) % 217.35/217.56 Clause #3627 (by clausification #[3625]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_2 a) True % 217.39/217.58 Clause #3630 (by superposition #[3627, 702]): ∀ (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_2) True) % 217.39/217.58 Clause #3635 (by clausification #[3630]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a a_3 a_2) True % 217.39/217.58 Clause #3640 (by superposition #[3635, 3288]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a a a a_1 a_2) True) (Eq True False) % 217.39/217.58 Clause #3642 (by clausification #[3640]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a a a_1 a_2) True % 217.39/217.58 Clause #3647 (by superposition #[3642, 3367]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a_1 a a a_2 a_3) True) (Eq True False) % 217.39/217.58 Clause #3648 (by clausification #[3647]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a_1 a a a_2 a_3) True % 217.39/217.58 Clause #3652 (by superposition #[3648, 711]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a a a a_1 a_2 a_3) True) % 217.39/217.58 Clause #3654 (by clausification #[3652]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a a_1 a_2 a_3) True % 217.39/217.58 Clause #3656 (by superposition #[3654, 649]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a_2 a a_3) True) % 217.39/217.58 Clause #3686 (by clausification #[3656]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a_1 a_2 a a_3) True % 217.39/217.58 Clause #3690 (by superposition #[3686, 3367]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a a_4) True) (Eq True False) % 217.39/217.58 Clause #3691 (by clausification #[3690]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a a_4) True % 217.39/217.58 Clause #3695 (by superposition #[3691, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a a_3 a a_4) True) % 217.39/217.58 Clause #3697 (by clausification #[3695]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a a_4) True % 217.39/217.58 Clause #3700 (by superposition #[3697, 702]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a a_3 a_4) True) % 217.39/217.58 Clause #3705 (by clausification #[3700]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_2 a a a_3 a_4) True % 217.39/217.58 Clause #3708 (by superposition #[3705, 649]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_3 a_4 a a) True) % 217.39/217.58 Clause #3710 (by clausification #[3708]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_2 a_3 a_4 a a) True % 217.39/217.58 Clause #3712 (by superposition #[3710, 596]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_1 a_1) True) % 217.39/217.58 Clause #3713 (by superposition #[3710, 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 a_4 a a) True) % 217.39/217.58 Clause #3717 (by clausification #[3713]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a a_4 a a) True % 217.39/217.58 Clause #3719 (by superposition #[3717, 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_1 a_4 a_1 a_1) True) % 217.39/217.58 Clause #3726 (by clausification #[3719]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_4 a_1 a_1) True % 217.39/217.58 Clause #3729 (by superposition #[3726, 702]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a a_3 a_4) True) % 217.39/217.58 Clause #3731 (by clausification #[3729]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a a_2 a a_3 a_4) True % 217.39/217.58 Clause #3735 (by superposition #[3731, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a a_3 a_4) True) % 217.39/217.58 Clause #4445 (by clausification #[3735]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a a a a_3 a_4) True % 217.39/217.58 Clause #4447 (by superposition #[4445, 596]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_3 a_4) True) % 217.39/217.58 Clause #4449 (by clausification #[4447]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a_1 a_3 a_4) True % 217.39/217.58 Clause #4452 (by superposition #[4449, 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) True) % 217.39/217.58 Clause #4454 (by clausification #[4452]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_2 a_3 a a_4 a) True % 217.39/217.58 Clause #4457 (by superposition #[4454, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a_3 a_4 a) True) % 217.39/217.60 Clause #4466 (by clausification #[4457]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a a_2 a_3 a_4 a) True % 217.39/217.60 Clause #4468 (by superposition #[4466, 702]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_3 a_3 a_4 a_3) True) % 217.39/217.60 Clause #4470 (by clausification #[4468]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_3 a_3 a_4 a_3) True % 217.39/217.60 Clause #4473 (by superposition #[4470, 797]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 217.39/217.60 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 217.39/217.60 (Or (Eq True False) (Eq (eqratio a_3 a_3 a_8 a_3 a_4 a_5 a_6 a_7) False)) % 217.39/217.60 Clause #4591 (by clausification #[3712]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a_2 a_3 a_4 a_1 a_1) True % 217.39/217.60 Clause #4594 (by superposition #[4591, 3288]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a a_1 a_2 a_3 a_3) True) (Eq True False) % 217.39/217.60 Clause #4595 (by clausification #[4594]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a_1 a_2 a_3 a_3) True % 217.39/217.60 Clause #4601 (by superposition #[4595, 3367]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_4) True) (Eq True False) % 217.39/217.60 Clause #4602 (by clausification #[4601]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a_1 a_2 a_3 a_4 a_4) True % 217.39/217.60 Clause #4606 (by superposition #[4602, 711]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a a_3 a_4 a_4) True) % 217.39/217.60 Clause #4609 (by clausification #[4606]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_2 a a_3 a_4 a_4) True % 217.39/217.60 Clause #4611 (by superposition #[4609, 649]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_2 a_4) True) % 217.39/217.60 Clause #4965 (by clausification #[4611]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_2 a_4) True % 217.39/217.60 Clause #5527 (by clausification #[4473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 217.39/217.60 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqratio a_3 a_3 a_8 a_3 a_4 a_5 a_6 a_7) False) % 217.39/217.60 Clause #5567 (by superposition #[5527, 4965]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_4 a_3 a_5) True) (Eq False True) % 217.39/217.60 Clause #5568 (by clausification #[5567]): ∀ (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_3 a_5) True % 217.39/217.60 Clause #5573 (by superposition #[5568, 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_2 a_3 a_4 a_4 a_5) True) % 217.39/217.60 Clause #5581 (by clausification #[5573]): ∀ (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_4 a_5) True % 217.39/217.60 Clause #5588 (by superposition #[5581, 5527]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_5 a_6) True) (Eq True False) % 217.39/217.60 Clause #5589 (by clausification #[5588]): ∀ (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 % 217.39/217.60 Clause #5594 (by superposition #[5589, 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) % 217.39/217.60 Clause #5598 (by clausification #[5594]): ∀ (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 % 217.39/217.60 Clause #5601 (by superposition #[5598, 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) % 217.39/217.60 Clause #5606 (by clausification #[5601]): ∀ (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 % 217.39/217.60 Clause #5611 (by superposition #[5606, 5527]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq True False) % 217.39/217.60 Clause #5612 (by clausification #[5611]): ∀ (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 % 217.39/217.60 Clause #5613 (by superposition #[5612, 467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 217.39/217.60 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)) % 217.39/217.60 Clause #5685 (by clausification #[5613]): ∀ (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) % 217.58/217.76 Clause #6275 (by clausification #[1788]): ∀ (a a_1 a_2 : Iota), % 217.58/217.76 Or (Eq (cong a a_1 a a_1) True) % 217.58/217.76 (Or (Eq (cyclic a a_1 a_2 a_2) False) (Or (Eq (cyclic a a_1 a_2 a) False) (Eq (cyclic a a_1 a_2 a_1) False))) % 217.58/217.76 Clause #6276 (by superposition #[6275, 2264]): ∀ (a a_1 a_2 : Iota), % 217.58/217.76 Or (Eq (cong a a_1 a a_1) True) % 217.58/217.76 (Or (Eq (cyclic a a_1 a_2 a) False) (Or (Eq (cyclic a a_1 a_2 a_1) False) (Eq False True))) % 217.58/217.76 Clause #6277 (by clausification #[6276]): ∀ (a a_1 a_2 : Iota), % 217.58/217.76 Or (Eq (cong a a_1 a a_1) True) (Or (Eq (cyclic a a_1 a_2 a) False) (Eq (cyclic a a_1 a_2 a_1) False)) % 217.58/217.76 Clause #6278 (by superposition #[6277, 2264]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a_1 a a_1) True) (Or (Eq (cyclic a a_1 a_2 a_1) False) (Eq False True)) % 217.58/217.76 Clause #6279 (by clausification #[6278]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq (cyclic a a_1 a_2 a_1) False) % 217.58/217.76 Clause #6280 (by superposition #[6279, 2264]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq False True) % 217.58/217.76 Clause #6281 (by clausification #[6280]): ∀ (a a_1 : Iota), Eq (cong a a_1 a a_1) True % 217.58/217.76 Clause #6289 (by superposition #[6281, 5685]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False) % 217.58/217.76 Clause #6328 (by clausification #[6289]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True % 217.58/217.76 Clause #6333 (by superposition #[6328, 276]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (circle a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a a_1 a a_3) False)) % 217.58/217.76 Clause #9342 (by clausification #[6333]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (circle a a_1 a_2 a_3) True) (Eq (cong a a_1 a a_3) False) % 217.58/217.76 Clause #9343 (by superposition #[9342, 6328]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (circle a a_1 a_2 a_3) True) (Eq False True) % 217.58/217.76 Clause #9344 (by clausification #[9343]): ∀ (a a_1 a_2 a_3 : Iota), Eq (circle a a_1 a_2 a_3) True % 217.58/217.76 Clause #9347 (by superposition #[9344, 2442]): ∀ (a a_1 a_2 : Iota), Or (Eq (perp a a_1 a_1 a_2) True) (Eq True False) % 217.58/217.76 Clause #9348 (by clausification #[9347]): ∀ (a a_1 a_2 : Iota), Eq (perp a a_1 a_1 a_2) True % 217.58/217.76 Clause #9355 (by superposition #[9348, 2360]): ∀ (a a_1 a_2 : Iota), Or (Eq (perp a a_1 a_2 a_1) True) (Eq True False) % 217.58/217.76 Clause #9356 (by clausification #[9355]): ∀ (a a_1 a_2 : Iota), Eq (perp a a_1 a_2 a_1) True % 217.58/217.76 Clause #9357 (by superposition #[9356, 736]): Eq True False % 217.58/217.76 Clause #9361 (by clausification #[9357]): False % 217.58/217.76 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------