%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO550+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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:40 PM UTC 2025 % Result : Theorem 192.43s 192.61s % Output : Proof 193.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : GEO550+1 : TPTP v9.2.0. Released v7.5.0. % 0.08/0.13 % Command : duper %s % 0.13/0.34 % Computer : n023.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:26:38 EDT 2025 % 0.13/0.34 % CPUTime : % 192.43/192.61 SZS status Theorem for theBenchmark.p % 192.43/192.61 SZS output start Proof for theBenchmark.p % 192.43/192.61 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 192.43/192.61 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 192.43/192.61 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 192.43/192.61 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 192.43/192.61 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 192.43/192.61 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 192.43/192.61 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 192.43/192.61 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 % 192.43/192.61 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 % 192.43/192.61 Clause #18 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle C D A B U V P Q) True % 192.43/192.61 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 % 192.43/192.61 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 % 192.43/192.61 Clause #21 (by assumption #[]): Eq % 192.43/192.61 (∀ (A B C D P Q U V E F G H : Iota), % 192.43/192.61 And (eqangle A B C D P Q U V) (eqangle P Q U V E F G H) → eqangle A B C D E F G H) % 192.43/192.61 True % 192.43/192.61 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 % 192.43/192.61 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 % 192.43/192.61 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 % 192.43/192.61 Clause #48 (by assumption #[]): Eq (∀ (A B C O X : Iota), And (circle O A B C) (perp O A A X) → eqangle A X A B C A C B) True % 192.43/192.61 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 192.43/192.61 Clause #86 (by assumption #[]): Eq (∀ (A B C O : Iota), Exists fun P => circle O A B C → perp P A A O) True % 192.43/192.61 Clause #94 (by assumption #[]): Eq % 192.43/192.61 (Not % 192.43/192.61 (∀ (A B C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.43/192.61 And % 192.43/192.61 (And % 192.43/192.61 (And (And (And (And (And (coll P C D) (coll P A B)) (coll E B C)) (coll E A D)) (circle O1 C D E)) % 192.43/192.61 (circle O E B A)) % 192.43/192.61 (circle O1 C Q NWPNT1)) % 192.43/192.61 (circle O A Q NWPNT2) → % 192.43/192.61 cyclic P D Q A)) % 192.43/192.61 True % 192.43/192.61 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 192.43/192.61 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 192.43/192.61 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 % 192.43/192.61 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) % 192.43/192.61 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 192.43/192.61 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 192.43/192.61 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 % 192.43/192.61 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) % 192.43/192.61 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 192.43/192.61 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 192.43/192.61 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 % 192.43/192.61 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) % 192.43/192.61 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 % 192.43/192.61 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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) % 192.43/192.64 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)) % 192.43/192.64 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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) % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 192.43/192.64 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) % 192.43/192.64 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 192.43/192.64 Or (Eq (cyclic a a_1 a_2 a_3) True) % 192.43/192.64 (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)) % 192.43/192.64 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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) % 192.43/192.64 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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) % 192.43/192.64 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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 % 192.43/192.64 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) % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.43/192.66 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) % 192.43/192.66 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.43/192.66 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)) % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.43/192.66 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 % 192.43/192.66 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.43/192.66 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 % 192.43/192.66 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.43/192.66 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 % 192.43/192.66 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.43/192.66 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 % 192.43/192.66 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.43/192.66 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) % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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 % 192.43/192.66 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) % 192.43/192.66 Clause #370 (by clausification #[86]): ∀ (a : Iota), Eq (∀ (B C O : Iota), Exists fun P => circle O a B C → perp P a a O) True % 192.43/192.66 Clause #371 (by clausification #[370]): ∀ (a a_1 : Iota), Eq (∀ (C O : Iota), Exists fun P => circle O a a_1 C → perp P a a O) True % 192.43/192.66 Clause #372 (by clausification #[371]): ∀ (a a_1 a_2 : Iota), Eq (∀ (O : Iota), Exists fun P => circle O a a_1 a_2 → perp P a a O) True % 192.50/192.69 Clause #373 (by clausification #[372]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Exists fun P => circle a a_1 a_2 a_3 → perp P a_1 a_1 a) True % 192.50/192.69 Clause #374 (by clausification #[373]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (circle a a_1 a_2 a_3 → perp (skS.0 0 a a_1 a_2 a_3 a_4) a_1 a_1 a) True % 192.50/192.69 Clause #375 (by clausification #[374]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.69 Or (Eq (circle a a_1 a_2 a_3) False) (Eq (perp (skS.0 0 a a_1 a_2 a_3 a_4) a_1 a_1 a) True) % 192.50/192.69 Clause #389 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle C D a B U V P Q) True % 192.50/192.69 Clause #390 (by clausification #[389]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle C D a a_1 U V P Q) True % 192.50/192.69 Clause #391 (by clausification #[390]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a_2 D a a_1 U V P Q) True % 192.50/192.69 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a_2 a_3 a a_1 U V P Q) True % 192.50/192.69 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.69 Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a_2 a_3 a a_1 U V a_4 Q) True % 192.50/192.69 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.50/192.69 Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a_2 a_3 a a_1 U V a_4 a_5) True % 192.50/192.69 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.50/192.69 Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_2 a_3 a a_1 a_6 V a_4 a_5) True % 192.50/192.69 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.69 Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True % 192.50/192.69 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.69 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True) % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.69 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.69 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 % 192.50/192.69 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.50/192.69 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 % 192.50/192.69 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.50/192.69 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 % 192.50/192.69 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.69 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 % 192.50/192.69 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.69 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) % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.69 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 % 192.50/192.71 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.71 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 % 192.50/192.71 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.50/192.71 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 % 192.50/192.71 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.50/192.71 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 % 192.50/192.71 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.71 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 % 192.50/192.71 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.71 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) % 192.50/192.71 Clause #533 (by clausification #[21]): ∀ (a : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (B C D P Q U V E F G H : Iota), % 192.50/192.71 And (eqangle a B C D P Q U V) (eqangle P Q U V E F G H) → eqangle a B C D E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #534 (by clausification #[533]): ∀ (a a_1 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (C D P Q U V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 C D P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 C D E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #535 (by clausification #[534]): ∀ (a a_1 a_2 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (D P Q U V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 D P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 a_2 D E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #536 (by clausification #[535]): ∀ (a a_1 a_2 a_3 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (P Q U V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 P Q U V) (eqangle P Q U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #537 (by clausification #[536]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (Q U V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 Q U V) (eqangle a_4 Q U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #538 (by clausification #[537]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (U V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 U V) (eqangle a_4 a_5 U V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #539 (by clausification #[538]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (V E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V) (eqangle a_4 a_5 a_6 V E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #540 (by clausification #[539]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (E F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 E F G H) → eqangle a a_1 a_2 a_3 E F G H) % 192.50/192.71 True % 192.50/192.71 Clause #541 (by clausification #[540]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (F G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 a_8 F G H) → eqangle a a_1 a_2 a_3 a_8 F G H) % 192.50/192.71 True % 192.50/192.71 Clause #542 (by clausification #[541]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (G H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 a_8 a_9 G H) → % 192.50/192.71 eqangle a a_1 a_2 a_3 a_8 a_9 G H) % 192.50/192.71 True % 192.50/192.71 Clause #543 (by clausification #[542]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (∀ (H : Iota), % 192.50/192.71 And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 a_8 a_9 a_10 H) → % 192.50/192.71 eqangle a a_1 a_2 a_3 a_8 a_9 a_10 H) % 192.50/192.71 True % 192.50/192.71 Clause #544 (by clausification #[543]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 192.50/192.71 Eq % 192.50/192.71 (And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) → % 192.50/192.71 eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 192.50/192.71 True % 192.50/192.71 Clause #545 (by clausification #[544]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 192.50/192.71 Or (Eq (And (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqangle a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) False) % 192.50/192.71 (Eq (eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 192.50/192.74 Clause #546 (by clausification #[545]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 192.50/192.74 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 192.50/192.74 (Or (Eq (eqangle a a_1 a_2 a_3 a_8 a_9 a_10 a_11) False) (Eq (eqangle a_8 a_9 a_10 a_11 a_4 a_5 a_6 a_7) False)) % 192.50/192.74 Clause #574 (by clausification #[48]): ∀ (a : Iota), Eq (∀ (B C O X : Iota), And (circle O a B C) (perp O a a X) → eqangle a X a B C a C B) True % 192.50/192.74 Clause #575 (by clausification #[574]): ∀ (a a_1 : Iota), Eq (∀ (C O X : Iota), And (circle O a a_1 C) (perp O a a X) → eqangle a X a a_1 C a C a_1) True % 192.50/192.74 Clause #576 (by clausification #[575]): ∀ (a a_1 a_2 : Iota), % 192.50/192.74 Eq (∀ (O X : Iota), And (circle O a a_1 a_2) (perp O a a X) → eqangle a X a a_1 a_2 a a_2 a_1) True % 192.50/192.74 Clause #577 (by clausification #[576]): ∀ (a a_1 a_2 a_3 : Iota), % 192.50/192.74 Eq (∀ (X : Iota), And (circle a a_1 a_2 a_3) (perp a a_1 a_1 X) → eqangle a_1 X a_1 a_2 a_3 a_1 a_3 a_2) True % 192.50/192.74 Clause #578 (by clausification #[577]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.74 Eq (And (circle a a_1 a_2 a_3) (perp a a_1 a_1 a_4) → eqangle a_1 a_4 a_1 a_2 a_3 a_1 a_3 a_2) True % 192.50/192.74 Clause #579 (by clausification #[578]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.74 Or (Eq (And (circle a a_1 a_2 a_3) (perp a a_1 a_1 a_4)) False) (Eq (eqangle a_1 a_4 a_1 a_2 a_3 a_1 a_3 a_2) True) % 192.50/192.74 Clause #580 (by clausification #[579]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.74 Or (Eq (eqangle a a_1 a a_2 a_3 a a_3 a_2) True) (Or (Eq (circle a_4 a a_2 a_3) False) (Eq (perp a_4 a a a_1) False)) % 192.50/192.74 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 % 192.50/192.74 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 % 192.50/192.74 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 % 192.50/192.74 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 % 192.50/192.74 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 % 192.50/192.74 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 % 192.50/192.74 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) % 192.50/192.74 Clause #712 (by clausification #[94]): Eq % 192.50/192.74 (∀ (A B C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.74 And % 192.50/192.74 (And % 192.50/192.74 (And (And (And (And (And (coll P C D) (coll P A B)) (coll E B C)) (coll E A D)) (circle O1 C D E)) % 192.50/192.74 (circle O E B A)) % 192.50/192.74 (circle O1 C Q NWPNT1)) % 192.50/192.74 (circle O A Q NWPNT2) → % 192.50/192.74 cyclic P D Q A) % 192.50/192.74 False % 192.50/192.74 Clause #713 (by clausification #[712]): ∀ (a : Iota), % 192.50/192.74 Eq % 192.50/192.74 (Not % 192.50/192.74 (∀ (B C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.74 And % 192.50/192.74 (And % 192.50/192.74 (And % 192.50/192.74 (And (And (And (And (coll P C D) (coll P (skS.0 10 a) B)) (coll E B C)) (coll E (skS.0 10 a) D)) % 192.50/192.74 (circle O1 C D E)) % 192.50/192.74 (circle O E B (skS.0 10 a))) % 192.50/192.74 (circle O1 C Q NWPNT1)) % 192.50/192.74 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.74 cyclic P D Q (skS.0 10 a))) % 192.50/192.74 True % 192.50/192.74 Clause #714 (by clausification #[713]): ∀ (a : Iota), % 192.50/192.74 Eq % 192.50/192.74 (∀ (B C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.74 And % 192.50/192.74 (And % 192.50/192.74 (And % 192.50/192.74 (And (And (And (And (coll P C D) (coll P (skS.0 10 a) B)) (coll E B C)) (coll E (skS.0 10 a) D)) % 192.50/192.74 (circle O1 C D E)) % 192.50/192.74 (circle O E B (skS.0 10 a))) % 192.50/192.74 (circle O1 C Q NWPNT1)) % 192.50/192.74 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.74 cyclic P D Q (skS.0 10 a)) % 192.50/192.74 False % 192.50/192.74 Clause #715 (by clausification #[714]): ∀ (a a_1 : Iota), % 192.50/192.74 Eq % 192.50/192.74 (Not % 192.50/192.74 (∀ (C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.74 And % 192.50/192.74 (And % 192.50/192.74 (And % 192.50/192.74 (And % 192.50/192.74 (And (And (And (coll P C D) (coll P (skS.0 10 a) (skS.0 11 a a_1))) (coll E (skS.0 11 a a_1) C)) % 192.50/192.76 (coll E (skS.0 10 a) D)) % 192.50/192.76 (circle O1 C D E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 C Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P D Q (skS.0 10 a))) % 192.50/192.76 True % 192.50/192.76 Clause #716 (by clausification #[715]): ∀ (a a_1 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (∀ (C D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And (And (And (coll P C D) (coll P (skS.0 10 a) (skS.0 11 a a_1))) (coll E (skS.0 11 a a_1) C)) % 192.50/192.76 (coll E (skS.0 10 a) D)) % 192.50/192.76 (circle O1 C D E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 C Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P D Q (skS.0 10 a)) % 192.50/192.76 False % 192.50/192.76 Clause #717 (by clausification #[716]): ∀ (a a_1 a_2 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (Not % 192.50/192.76 (∀ (D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And (And (coll P (skS.0 12 a a_1 a_2) D) (coll P (skS.0 10 a) (skS.0 11 a a_1))) % 192.50/192.76 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.50/192.76 (coll E (skS.0 10 a) D)) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) D E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P D Q (skS.0 10 a))) % 192.50/192.76 True % 192.50/192.76 Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (∀ (D P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And (And (coll P (skS.0 12 a a_1 a_2) D) (coll P (skS.0 10 a) (skS.0 11 a a_1))) % 192.50/192.76 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.50/192.76 (coll E (skS.0 10 a) D)) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) D E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P D Q (skS.0 10 a)) % 192.50/192.76 False % 192.50/192.76 Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (Not % 192.50/192.76 (∀ (P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And (coll P (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.50/192.76 (coll P (skS.0 10 a) (skS.0 11 a a_1))) % 192.50/192.76 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.50/192.76 (coll E (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a))) % 192.50/192.76 True % 192.50/192.76 Clause #720 (by clausification #[719]): ∀ (a a_1 a_2 a_3 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (∀ (P E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And (coll P (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) (coll P (skS.0 10 a) (skS.0 11 a a_1))) % 192.50/192.76 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.50/192.76 (coll E (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) E)) % 192.50/192.76 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.50/192.76 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.50/192.76 (circle O (skS.0 10 a) Q NWPNT2) → % 192.50/192.76 cyclic P (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a)) % 192.50/192.76 False % 192.50/192.76 Clause #721 (by clausification #[720]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.50/192.76 Eq % 192.50/192.76 (Not % 192.50/192.76 (∀ (E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.50/192.76 And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.50/192.76 (And % 192.60/192.78 (And % 192.60/192.78 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.60/192.78 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.60/192.78 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.60/192.78 (coll E (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) E)) % 192.60/192.78 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.60/192.78 (circle O (skS.0 10 a) Q NWPNT2) → % 192.60/192.78 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a))) % 192.60/192.78 True % 192.60/192.78 Clause #722 (by clausification #[721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 192.60/192.78 Eq % 192.60/192.78 (∀ (E O1 O Q NWPNT1 NWPNT2 : Iota), % 192.60/192.78 And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.60/192.78 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.60/192.78 (coll E (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.60/192.78 (coll E (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) E)) % 192.60/192.78 (circle O E (skS.0 11 a a_1) (skS.0 10 a))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.60/192.78 (circle O (skS.0 10 a) Q NWPNT2) → % 192.60/192.78 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a)) % 192.60/192.78 False % 192.60/192.78 Clause #723 (by clausification #[722]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.60/192.78 Eq % 192.60/192.78 (Not % 192.60/192.78 (∀ (O1 O Q NWPNT1 NWPNT2 : Iota), % 192.60/192.78 And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.60/192.78 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.60/192.78 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.60/192.78 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.60/192.78 (circle O (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.60/192.78 (circle O (skS.0 10 a) Q NWPNT2) → % 192.60/192.78 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a))) % 192.60/192.78 True % 192.60/192.78 Clause #724 (by clausification #[723]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.60/192.78 Eq % 192.60/192.78 (∀ (O1 O Q NWPNT1 NWPNT2 : Iota), % 192.60/192.78 And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.60/192.78 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.60/192.78 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.60/192.78 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.60/192.78 (circle O (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a))) % 192.60/192.78 (circle O1 (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.60/192.78 (circle O (skS.0 10 a) Q NWPNT2) → % 192.60/192.78 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a)) % 192.60/192.78 False % 192.60/192.78 Clause #725 (by clausification #[724]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.60/192.78 Eq % 192.60/192.78 (Not % 192.60/192.78 (∀ (O Q NWPNT1 NWPNT2 : Iota), % 192.60/192.78 And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And % 192.60/192.78 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.60/192.78 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.62/192.80 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.62/192.80 (circle O (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.62/192.80 (circle O (skS.0 10 a) Q NWPNT2) → % 192.62/192.80 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a))) % 192.62/192.80 True % 192.62/192.80 Clause #726 (by clausification #[725]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 192.62/192.80 Eq % 192.62/192.80 (∀ (O Q NWPNT1 NWPNT2 : Iota), % 192.62/192.80 And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.62/192.80 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.62/192.80 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.62/192.80 (circle O (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.62/192.80 (circle O (skS.0 10 a) Q NWPNT2) → % 192.62/192.80 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a)) % 192.62/192.80 False % 192.62/192.80 Clause #727 (by clausification #[726]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.62/192.80 Eq % 192.62/192.80 (Not % 192.62/192.80 (∀ (Q NWPNT1 NWPNT2 : Iota), % 192.62/192.80 And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.62/192.80 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.62/192.80 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.62/192.80 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.62/192.80 (skS.0 10 a))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.62/192.80 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) Q NWPNT2) → % 192.62/192.80 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a))) % 192.62/192.80 True % 192.62/192.80 Clause #728 (by clausification #[727]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.62/192.80 Eq % 192.62/192.80 (∀ (Q NWPNT1 NWPNT2 : Iota), % 192.62/192.80 And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And % 192.62/192.80 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.62/192.80 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.62/192.80 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.62/192.80 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.62/192.80 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.62/192.80 (skS.0 10 a))) % 192.62/192.80 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) Q NWPNT1)) % 192.62/192.80 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) Q NWPNT2) → % 192.65/192.82 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) Q (skS.0 10 a)) % 192.65/192.82 False % 192.65/192.82 Clause #729 (by clausification #[728]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.82 Eq % 192.65/192.82 (Not % 192.65/192.82 (∀ (NWPNT1 NWPNT2 : Iota), % 192.65/192.82 And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.82 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.82 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.82 (skS.0 10 a))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) % 192.65/192.82 (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) NWPNT1)) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.82 NWPNT2) → % 192.65/192.82 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.82 (skS.0 10 a))) % 192.65/192.82 True % 192.65/192.82 Clause #730 (by clausification #[729]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.82 Eq % 192.65/192.82 (∀ (NWPNT1 NWPNT2 : Iota), % 192.65/192.82 And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.82 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.82 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.82 (skS.0 10 a))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) % 192.65/192.82 (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) NWPNT1)) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.82 NWPNT2) → % 192.65/192.82 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.82 (skS.0 10 a)) % 192.65/192.82 False % 192.65/192.82 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), % 192.65/192.82 Eq % 192.65/192.82 (Not % 192.65/192.82 (∀ (NWPNT2 : Iota), % 192.65/192.82 And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And % 192.65/192.82 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.82 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.82 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.82 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.82 (skS.0 10 a))) % 192.65/192.82 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) % 192.65/192.82 (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.82 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.84 NWPNT2) → % 192.65/192.84 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.84 (skS.0 10 a))) % 192.65/192.84 True % 192.65/192.84 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), % 192.65/192.84 Eq % 192.65/192.84 (∀ (NWPNT2 : Iota), % 192.65/192.84 And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.84 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.84 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.84 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.84 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.84 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.84 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.84 (skS.0 10 a))) % 192.65/192.84 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) % 192.65/192.84 (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.84 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.84 NWPNT2) → % 192.65/192.84 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.84 (skS.0 10 a)) % 192.65/192.84 False % 192.65/192.84 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), % 192.65/192.84 Eq % 192.65/192.84 (Not % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And % 192.65/192.84 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.84 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.85 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.85 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.85 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.85 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.85 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.85 (skS.0 10 a))) % 192.65/192.85 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) % 192.65/192.85 (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.85 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.85 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) → % 192.65/192.85 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.85 (skS.0 10 a))) % 192.65/192.85 True % 192.65/192.85 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), % 192.65/192.85 Eq % 192.65/192.85 (And % 192.65/192.85 (And % 192.65/192.85 (And % 192.65/192.85 (And % 192.65/192.85 (And % 192.65/192.85 (And % 192.65/192.85 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.85 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.85 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.85 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.85 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.85 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.85 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.85 (skS.0 10 a))) % 192.65/192.85 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.87 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) → % 192.65/192.87 cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 10 a)) % 192.65/192.87 False % 192.65/192.87 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), % 192.65/192.87 Eq % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.87 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.87 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.87 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.87 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.87 (skS.0 10 a))) % 192.65/192.87 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.87 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 20 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 192.65/192.87 True % 192.65/192.87 Clause #736 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.87 Eq % 192.65/192.87 (cyclic (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 13 a a_1 a_2 a_3) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 10 a)) % 192.65/192.87 False % 192.65/192.87 Clause #738 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 192.65/192.87 Eq % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.87 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.87 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.87 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.87 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.65/192.87 (skS.0 10 a))) % 192.65/192.87 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 18 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 192.65/192.87 (skS.0 19 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 192.65/192.87 True % 192.65/192.87 Clause #861 (by clausification #[738]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.65/192.87 Eq % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And % 192.65/192.87 (And (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3)) % 192.65/192.87 (coll (skS.0 14 a a_1 a_2 a_3 a_4) (skS.0 10 a) (skS.0 11 a a_1))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 12 a a_1 a_2))) % 192.65/192.87 (coll (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 13 a a_1 a_2 a_3))) % 192.65/192.87 (circle (skS.0 16 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2) (skS.0 13 a a_1 a_2 a_3) % 192.65/192.87 (skS.0 15 a a_1 a_2 a_3 a_4 a_5))) % 192.65/192.87 (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a))) % 192.65/192.87 True % 192.65/192.87 Clause #1086 (by clausification #[861]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.65/192.87 Eq (circle (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a)) % 192.65/192.87 True % 192.65/192.87 Clause #1090 (by superposition #[1086, 375]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.87 Or (Eq True False) % 192.65/192.87 (Eq % 192.65/192.87 (perp % 192.65/192.87 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (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)) % 192.65/192.89 True) % 192.65/192.89 Clause #1092 (by superposition #[1086, 580]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Or % 192.65/192.89 (Eq % 192.65/192.89 (eqangle (skS.0 15 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 11 a a_1) (skS.0 10 a) % 192.65/192.89 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1)) % 192.65/192.89 True) % 192.65/192.89 (Or (Eq True False) % 192.65/192.89 (Eq % 192.65/192.89 (perp (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_7 a_8) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 a_6) % 192.65/192.89 False)) % 192.65/192.89 Clause #1095 (by clausification #[1090]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Eq % 192.65/192.89 (perp % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (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)) % 192.65/192.89 True % 192.65/192.89 Clause #1098 (by superposition #[1095, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Or (Eq True False) % 192.65/192.89 (Eq % 192.65/192.89 (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) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.65/192.89 True) % 192.65/192.89 Clause #1113 (by clausification #[1098]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Eq % 192.65/192.89 (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) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.65/192.89 True % 192.65/192.89 Clause #1114 (by superposition #[1113, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Or (Eq True False) % 192.65/192.89 (Eq % 192.65/192.89 (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 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8)) % 192.65/192.89 True) % 192.65/192.89 Clause #1124 (by clausification #[1114]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Eq % 192.65/192.89 (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 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8)) % 192.65/192.89 True % 192.65/192.89 Clause #1125 (by superposition #[1124, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Or (Eq True False) % 192.65/192.89 (Eq % 192.65/192.89 (perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (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)) % 192.65/192.89 True) % 192.65/192.89 Clause #1136 (by clausification #[1125]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Eq % 192.65/192.89 (perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (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)) % 192.65/192.89 True % 192.65/192.89 Clause #1137 (by superposition #[1136, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Or (Eq True False) % 192.65/192.89 (Eq % 192.65/192.89 (perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.65/192.89 True) % 192.65/192.89 Clause #1147 (by clausification #[1137]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.65/192.89 Eq % 192.65/192.89 (perp (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.65/192.89 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.65/192.89 a_8) % 192.65/192.89 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.65/192.89 True % 192.65/192.89 Clause #1148 (by superposition #[1147, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or (Eq True False) % 192.73/192.92 (Eq % 192.73/192.92 (perp (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8)) % 192.73/192.92 True) % 192.73/192.92 Clause #1158 (by clausification #[1148]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Eq % 192.73/192.92 (perp (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8)) % 192.73/192.92 True % 192.73/192.92 Clause #1237 (by clausification #[1092]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or % 192.73/192.92 (Eq % 192.73/192.92 (eqangle (skS.0 15 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 11 a a_1) (skS.0 10 a) % 192.73/192.92 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1)) % 192.73/192.92 True) % 192.73/192.92 (Eq % 192.73/192.92 (perp (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_7 a_8) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 a_6) % 192.73/192.92 False) % 192.73/192.92 Clause #1238 (by superposition #[1237, 1158]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or % 192.73/192.92 (Eq % 192.73/192.92 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.73/192.92 (skS.0 11 a a_1)) % 192.73/192.92 True) % 192.73/192.92 (Eq False True) % 192.73/192.92 Clause #1242 (by clausification #[1238]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Eq % 192.73/192.92 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.73/192.92 (skS.0 11 a a_1)) % 192.73/192.92 True % 192.73/192.92 Clause #1248 (by superposition #[1242, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or (Eq True False) % 192.73/192.92 (Eq % 192.73/192.92 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 (skS.0 11 a a_1)) % 192.73/192.92 True) % 192.73/192.92 Clause #1376 (by clausification #[1248]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Eq % 192.73/192.92 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 (skS.0 11 a a_1)) % 192.73/192.92 True % 192.73/192.92 Clause #1378 (by superposition #[1376, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or (Eq True False) % 192.73/192.92 (Eq % 192.73/192.92 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.92 True) % 192.73/192.92 Clause #1384 (by clausification #[1378]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Eq % 192.73/192.92 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 a_8) % 192.73/192.92 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.92 True % 192.73/192.92 Clause #1386 (by superposition #[1384, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.92 Or (Eq True False) % 192.73/192.92 (Eq % 192.73/192.92 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.92 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.92 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True) % 192.73/192.94 Clause #1390 (by clausification #[1386]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Eq % 192.73/192.94 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True % 192.73/192.94 Clause #1393 (by superposition #[1390, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Or (Eq True False) % 192.73/192.94 (Eq % 192.73/192.94 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True) % 192.73/192.94 Clause #1398 (by clausification #[1393]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Eq % 192.73/192.94 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True % 192.73/192.94 Clause #1400 (by superposition #[1398, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Or (Eq True False) % 192.73/192.94 (Eq % 192.73/192.94 (eqangle (skS.0 11 a a_1) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True) % 192.73/192.94 Clause #1406 (by clausification #[1400]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Eq % 192.73/192.94 (eqangle (skS.0 11 a a_1) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8)) % 192.73/192.94 True % 192.73/192.94 Clause #1408 (by superposition #[1406, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Or (Eq True False) % 192.73/192.94 (Eq % 192.73/192.94 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8) % 192.73/192.94 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.73/192.94 True) % 192.73/192.94 Clause #1412 (by clausification #[1408]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Eq % 192.73/192.94 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8) % 192.73/192.94 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.73/192.94 True % 192.73/192.94 Clause #1416 (by superposition #[1412, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Or (Eq True False) % 192.73/192.94 (Eq % 192.73/192.94 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8) % 192.73/192.94 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.73/192.94 True) % 192.73/192.94 Clause #1419 (by clausification #[1416]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.94 Eq % 192.73/192.94 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.94 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.94 a_8) % 192.73/192.94 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.73/192.94 True % 192.73/192.94 Clause #1421 (by superposition #[1419, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Or (Eq True False) % 192.73/192.97 (Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) % 192.73/192.97 (skS.0 10 a)) % 192.73/192.97 True) % 192.73/192.97 Clause #1425 (by clausification #[1421]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) % 192.73/192.97 (skS.0 10 a)) % 192.73/192.97 True % 192.73/192.97 Clause #1427 (by superposition #[1425, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Or (Eq True False) % 192.73/192.97 (Eq % 192.73/192.97 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True) % 192.73/192.97 Clause #1431 (by clausification #[1427]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Eq % 192.73/192.97 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True % 192.73/192.97 Clause #1432 (by superposition #[1431, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Or (Eq True False) % 192.73/192.97 (Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True) % 192.73/192.97 Clause #1437 (by clausification #[1432]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True % 192.73/192.97 Clause #1441 (by superposition #[1437, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Or (Eq True False) % 192.73/192.97 (Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True) % 192.73/192.97 Clause #1444 (by clausification #[1441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.73/192.97 True % 192.73/192.97 Clause #1446 (by superposition #[1444, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Or (Eq True False) % 192.73/192.97 (Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.73/192.97 a_8) % 192.73/192.97 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.73/192.97 (skS.0 10 a)) % 192.73/192.97 True) % 192.73/192.97 Clause #1450 (by clausification #[1446]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.73/192.97 Eq % 192.73/192.97 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.73/192.97 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/192.99 (skS.0 10 a)) % 192.80/192.99 True % 192.80/192.99 Clause #1452 (by superposition #[1450, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Or (Eq True False) % 192.80/192.99 (Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True) % 192.80/192.99 Clause #1456 (by clausification #[1452]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True % 192.80/192.99 Clause #1459 (by superposition #[1456, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Or (Eq True False) % 192.80/192.99 (Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True) % 192.80/192.99 Clause #1462 (by clausification #[1459]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True % 192.80/192.99 Clause #1463 (by superposition #[1462, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Or (Eq True False) % 192.80/192.99 (Eq % 192.80/192.99 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True) % 192.80/192.99 Clause #1468 (by clausification #[1463]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Eq % 192.80/192.99 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/192.99 True % 192.80/192.99 Clause #1471 (by superposition #[1468, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Or (Eq True False) % 192.80/192.99 (Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.80/192.99 (skS.0 10 a)) % 192.80/192.99 True) % 192.80/192.99 Clause #1475 (by clausification #[1471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.80/192.99 (skS.0 10 a)) % 192.80/192.99 True % 192.80/192.99 Clause #1480 (by superposition #[1475, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/192.99 Or (Eq True False) % 192.80/192.99 (Eq % 192.80/192.99 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/192.99 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/192.99 a_8) % 192.80/192.99 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 10 a)) % 192.80/193.01 True) % 192.80/193.01 Clause #1483 (by clausification #[1480]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Eq % 192.80/193.01 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8) % 192.80/193.01 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 10 a)) % 192.80/193.01 True % 192.80/193.01 Clause #1485 (by superposition #[1483, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Or (Eq True False) % 192.80/193.01 (Eq % 192.80/193.01 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8) % 192.80/193.01 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.01 True) % 192.80/193.01 Clause #1489 (by clausification #[1485]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Eq % 192.80/193.01 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8) % 192.80/193.01 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.01 True % 192.80/193.01 Clause #1491 (by superposition #[1489, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Or (Eq True False) % 192.80/193.01 (Eq % 192.80/193.01 (eqangle (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8)) % 192.80/193.01 True) % 192.80/193.01 Clause #1497 (by clausification #[1491]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Eq % 192.80/193.01 (eqangle (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8)) % 192.80/193.01 True % 192.80/193.01 Clause #1498 (by superposition #[1497, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Or (Eq True False) % 192.80/193.01 (Eq % 192.80/193.01 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8)) % 192.80/193.01 True) % 192.80/193.01 Clause #1505 (by clausification #[1498]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Eq % 192.80/193.01 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8)) % 192.80/193.01 True % 192.80/193.01 Clause #1509 (by superposition #[1505, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.01 Or (Eq True False) % 192.80/193.01 (Eq % 192.80/193.01 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.01 a_8)) % 192.80/193.01 True) % 192.80/193.01 Clause #1511 (by superposition #[1505, 546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 192.80/193.01 Or (Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_8 a_9) True) % 192.80/193.01 (Or (Eq True False) % 192.80/193.01 (Eq % 192.80/193.01 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.01 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.80/193.01 (skS.0 10 a) a_12) % 192.80/193.04 a_6 a_7 a_8 a_9) % 192.80/193.04 False)) % 192.80/193.04 Clause #1512 (by clausification #[1509]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Eq % 192.80/193.04 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8)) % 192.80/193.04 True % 192.80/193.04 Clause #1514 (by superposition #[1512, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Or (Eq True False) % 192.80/193.04 (Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.04 True) % 192.80/193.04 Clause #1518 (by clausification #[1514]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.04 True % 192.80/193.04 Clause #1520 (by superposition #[1518, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Or (Eq True False) % 192.80/193.04 (Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.04 (skS.0 11 a a_1)) % 192.80/193.04 True) % 192.80/193.04 Clause #1524 (by clausification #[1520]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.04 (skS.0 11 a a_1)) % 192.80/193.04 True % 192.80/193.04 Clause #1527 (by superposition #[1524, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Or (Eq True False) % 192.80/193.04 (Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) % 192.80/193.04 (skS.0 11 a a_1)) % 192.80/193.04 True) % 192.80/193.04 Clause #1530 (by clausification #[1527]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Eq % 192.80/193.04 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) % 192.80/193.04 (skS.0 11 a a_1)) % 192.80/193.04 True % 192.80/193.04 Clause #1531 (by superposition #[1530, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Or (Eq True False) % 192.80/193.04 (Eq % 192.80/193.04 (eqangle % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1)) % 192.80/193.04 True) % 192.80/193.04 Clause #1536 (by clausification #[1531]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Eq % 192.80/193.04 (eqangle % 192.80/193.04 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.04 a_8) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.04 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1)) % 192.80/193.04 True % 192.80/193.04 Clause #1538 (by superposition #[1536, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.04 Or (Eq True False) % 192.80/193.06 (Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True) % 192.80/193.06 Clause #1542 (by clausification #[1538]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True % 192.80/193.06 Clause #1546 (by superposition #[1542, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Or (Eq True False) % 192.80/193.06 (Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True) % 192.80/193.06 Clause #1549 (by clausification #[1546]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True % 192.80/193.06 Clause #1551 (by superposition #[1549, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Or (Eq True False) % 192.80/193.06 (Eq % 192.80/193.06 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True) % 192.80/193.06 Clause #1555 (by clausification #[1551]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Eq % 192.80/193.06 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.80/193.06 True % 192.80/193.06 Clause #1557 (by superposition #[1555, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Or (Eq True False) % 192.80/193.06 (Eq % 192.80/193.06 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/193.06 True) % 192.80/193.06 Clause #1561 (by clausification #[1557]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Eq % 192.80/193.06 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/193.06 True % 192.80/193.06 Clause #1562 (by superposition #[1561, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Or (Eq True False) % 192.80/193.06 (Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.80/193.06 a_8) % 192.80/193.06 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.80/193.06 True) % 192.80/193.06 Clause #1567 (by clausification #[1562]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.80/193.06 Eq % 192.80/193.06 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) % 192.80/193.06 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.92/193.09 True % 192.92/193.09 Clause #1571 (by superposition #[1567, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Or (Eq True False) % 192.92/193.09 (Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.92/193.09 True) % 192.92/193.09 Clause #1574 (by clausification #[1571]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.92/193.09 True % 192.92/193.09 Clause #1576 (by superposition #[1574, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Or (Eq True False) % 192.92/193.09 (Eq % 192.92/193.09 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.92/193.09 True) % 192.92/193.09 Clause #1580 (by clausification #[1576]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Eq % 192.92/193.09 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.92/193.09 True % 192.92/193.09 Clause #1582 (by superposition #[1580, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Or (Eq True False) % 192.92/193.09 (Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.92/193.09 True) % 192.92/193.09 Clause #1586 (by clausification #[1582]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.92/193.09 True % 192.92/193.09 Clause #1590 (by superposition #[1586, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Or (Eq True False) % 192.92/193.09 (Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.92/193.09 (skS.0 11 a a_1)) % 192.92/193.09 True) % 192.92/193.09 Clause #1593 (by clausification #[1590]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Eq % 192.92/193.09 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.92/193.09 True % 192.92/193.09 Clause #1594 (by superposition #[1593, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.92/193.09 Or (Eq True False) % 192.92/193.09 (Eq % 192.92/193.09 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.92/193.09 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.92/193.09 a_8) % 192.92/193.09 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.92/193.09 (skS.0 11 a a_1)) % 192.94/193.12 True) % 192.94/193.12 Clause #1599 (by clausification #[1594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Eq % 192.94/193.12 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1)) % 192.94/193.12 True % 192.94/193.12 Clause #1600 (by superposition #[1599, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Or (Eq True False) % 192.94/193.12 (Eq % 192.94/193.12 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True) % 192.94/193.12 Clause #1604 (by clausification #[1600]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Eq % 192.94/193.12 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True % 192.94/193.12 Clause #1608 (by superposition #[1604, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Or (Eq True False) % 192.94/193.12 (Eq % 192.94/193.12 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True) % 192.94/193.12 Clause #1611 (by clausification #[1608]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Eq % 192.94/193.12 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True % 192.94/193.12 Clause #1613 (by superposition #[1611, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Or (Eq True False) % 192.94/193.12 (Eq % 192.94/193.12 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True) % 192.94/193.12 Clause #1617 (by clausification #[1613]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Eq % 192.94/193.12 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True % 192.94/193.12 Clause #1618 (by superposition #[1617, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Or (Eq True False) % 192.94/193.12 (Eq % 192.94/193.12 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True) % 192.94/193.12 Clause #1622 (by clausification #[1618]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Eq % 192.94/193.12 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.94/193.12 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.94/193.12 a_8) % 192.94/193.12 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.94/193.12 True % 192.94/193.12 Clause #1626 (by superposition #[1622, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.94/193.12 Or (Eq True False) % 192.94/193.12 (Eq % 192.94/193.12 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.14 True) % 192.96/193.14 Clause #1630 (by clausification #[1626]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Eq % 192.96/193.14 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.14 True % 192.96/193.14 Clause #1632 (by superposition #[1630, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Or (Eq True False) % 192.96/193.14 (Eq % 192.96/193.14 (eqangle % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.14 True) % 192.96/193.14 Clause #1636 (by clausification #[1632]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Eq % 192.96/193.14 (eqangle % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.96/193.14 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.14 True % 192.96/193.14 Clause #1637 (by superposition #[1636, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Or (Eq True False) % 192.96/193.14 (Eq % 192.96/193.14 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.14 (skS.0 11 a a_1)) % 192.96/193.14 True) % 192.96/193.14 Clause #1641 (by clausification #[1637]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Eq % 192.96/193.14 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.14 (skS.0 11 a a_1)) % 192.96/193.14 True % 192.96/193.14 Clause #1644 (by superposition #[1641, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Or (Eq True False) % 192.96/193.14 (Eq % 192.96/193.14 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.14 (skS.0 11 a a_1)) % 192.96/193.14 True) % 192.96/193.14 Clause #1647 (by clausification #[1644]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Eq % 192.96/193.14 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.14 (skS.0 11 a a_1)) % 192.96/193.14 True % 192.96/193.14 Clause #1648 (by superposition #[1647, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Or (Eq True False) % 192.96/193.14 (Eq % 192.96/193.14 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.14 a_8) % 192.96/193.14 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.14 True) % 192.96/193.14 Clause #1831 (by clausification #[1648]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 192.96/193.14 Eq % 192.96/193.14 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.14 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) (skS.0 10 a) % 192.96/193.17 a_8) % 192.96/193.17 (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.17 True % 192.96/193.17 Clause #2591 (by clausification #[1511]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 192.96/193.17 Or (Eq (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_8 a_9) True) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.17 (skS.0 0 (skS.0 17 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 11 a a_1) % 192.96/193.17 (skS.0 10 a) a_12) % 192.96/193.17 a_6 a_7 a_8 a_9) % 192.96/193.17 False) % 192.96/193.17 Clause #2610 (by superposition #[2591, 1831]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.17 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.17 True) % 192.96/193.17 (Eq False True) % 192.96/193.17 Clause #2612 (by clausification #[2610]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.17 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.17 True % 192.96/193.17 Clause #2617 (by superposition #[2612, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.17 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.17 True) % 192.96/193.17 Clause #2621 (by clausification #[2617]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) % 192.96/193.17 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5)) % 192.96/193.17 True % 192.96/193.17 Clause #2623 (by superposition #[2621, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.17 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.96/193.17 True) % 192.96/193.17 Clause #2629 (by clausification #[2623]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) % 192.96/193.17 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) % 192.96/193.17 True % 192.96/193.17 Clause #2631 (by superposition #[2629, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) % 192.96/193.17 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.17 True) % 192.96/193.17 Clause #2635 (by clausification #[2631]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) % 192.96/193.17 (skS.0 11 a a_1) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.17 True % 192.96/193.17 Clause #2638 (by superposition #[2635, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.17 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.17 True) % 192.96/193.17 Clause #2642 (by clausification #[2638]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 11 a a_1) % 192.96/193.17 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 11 a a_1)) % 192.96/193.17 True % 192.96/193.17 Clause #2644 (by superposition #[2642, 359]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq (para (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) True) % 192.96/193.17 Clause #2650 (by clausification #[2644]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 192.96/193.17 Eq (para (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a)) True % 192.96/193.17 Clause #2656 (by superposition #[2650, 610]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.17 Or (Eq True False) % 192.96/193.17 (Eq % 192.96/193.17 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 % 192.96/193.19 a_7) % 192.96/193.19 True) % 192.96/193.19 Clause #2760 (by clausification #[2656]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 % 192.96/193.19 a_7) % 192.96/193.19 True % 192.96/193.19 Clause #2762 (by superposition #[2760, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_6 % 192.96/193.19 a_7) % 192.96/193.19 True) % 192.96/193.19 Clause #2764 (by clausification #[2762]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_6 % 192.96/193.19 a_7) % 192.96/193.19 True % 192.96/193.19 Clause #2767 (by superposition #[2764, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle a a_1 a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) % 192.96/193.19 (skS.0 10 a_2)) % 192.96/193.19 True) % 192.96/193.19 Clause #2772 (by clausification #[2767]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle a a_1 a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) % 192.96/193.19 (skS.0 10 a_2)) % 192.96/193.19 True % 192.96/193.19 Clause #2774 (by superposition #[2772, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle a a_1 a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True) % 192.96/193.19 Clause #2780 (by clausification #[2774]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle a a_1 a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True % 192.96/193.19 Clause #2784 (by superposition #[2780, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) a a_1 (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True) % 192.96/193.19 Clause #2787 (by clausification #[2784]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) a a_1 (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True % 192.96/193.19 Clause #2788 (by superposition #[2787, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) a_1 a (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True) % 192.96/193.19 Clause #2794 (by clausification #[2788]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle a a_1 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a_2) a_1 a (skS.0 10 a_2) % 192.96/193.19 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.19 True % 192.96/193.19 Clause #2798 (by superposition #[2794, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) a_1 a (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) % 192.96/193.19 (skS.0 10 a_2)) % 192.96/193.19 True) % 192.96/193.19 Clause #2804 (by clausification #[2798]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) a_1 a (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) % 192.96/193.19 (skS.0 10 a_2)) % 192.96/193.19 True % 192.96/193.19 Clause #2807 (by superposition #[2804, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_7 % 192.96/193.19 a_6) % 192.96/193.19 True) % 192.96/193.19 Clause #2812 (by clausification #[2807]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_7 % 192.96/193.19 a_6) % 192.96/193.19 True % 192.96/193.19 Clause #2815 (by superposition #[2812, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Or (Eq True False) % 192.96/193.19 (Eq % 192.96/193.19 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_7 % 192.96/193.19 a_6) % 192.96/193.19 True) % 192.96/193.19 Clause #2821 (by clausification #[2815]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.19 Eq % 192.96/193.21 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) a_6 a_7 a_7 % 192.96/193.21 a_6) % 192.96/193.21 True % 192.96/193.21 Clause #2823 (by superposition #[2821, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Or (Eq True False) % 192.96/193.21 (Eq % 192.96/193.21 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 a_7 % 192.96/193.21 a_6) % 192.96/193.21 True) % 192.96/193.21 Clause #2828 (by clausification #[2823]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Eq % 192.96/193.21 (eqangle (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 a_7 % 192.96/193.21 a_6) % 192.96/193.21 True % 192.96/193.21 Clause #2829 (by superposition #[2828, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Or (Eq True False) % 192.96/193.21 (Eq % 192.96/193.21 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 a_7 % 192.96/193.21 a_6) % 192.96/193.21 True) % 192.96/193.21 Clause #2834 (by clausification #[2829]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Eq % 192.96/193.21 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 a_7 % 192.96/193.21 a_6) % 192.96/193.21 True % 192.96/193.21 Clause #2841 (by superposition #[2834, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Or (Eq True False) % 192.96/193.21 (Eq % 192.96/193.21 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_7 % 192.96/193.21 a_6) % 192.96/193.21 True) % 192.96/193.21 Clause #2846 (by clausification #[2841]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Eq % 192.96/193.21 (eqangle (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_6 a_7 (skS.0 10 a) (skS.0 15 a a_1 a_2 a_3 a_4 a_5) a_7 % 192.96/193.21 a_6) % 192.96/193.21 True % 192.96/193.21 Clause #2851 (by superposition #[2846, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Or (Eq True False) % 192.96/193.21 (Eq % 192.96/193.21 (eqangle a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) a_1 a (skS.0 10 a_2) % 192.96/193.21 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.21 True) % 192.96/193.21 Clause #2860 (by clausification #[2851]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 192.96/193.21 Eq % 192.96/193.21 (eqangle a a_1 (skS.0 10 a_2) (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7) a_1 a (skS.0 10 a_2) % 192.96/193.21 (skS.0 15 a_2 a_3 a_4 a_5 a_6 a_7)) % 192.96/193.21 True % 192.96/193.21 Clause #2865 (by superposition #[2860, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 192.96/193.21 Clause #2874 (by clausification #[2865]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 192.96/193.21 Clause #2877 (by superposition #[2874, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 192.96/193.21 Clause #2880 (by superposition #[2874, 610]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a_1 a a_2 a_3) True) % 192.96/193.21 Clause #2897 (by clausification #[2877]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 192.96/193.21 Clause #2898 (by superposition #[2897, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 192.96/193.21 Clause #2903 (by clausification #[2898]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 192.96/193.21 Clause #2906 (by superposition #[2903, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 192.96/193.21 Clause #2922 (by clausification #[2906]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 192.96/193.21 Clause #2924 (by superposition #[2922, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 192.96/193.21 Clause #2941 (by clausification #[2924]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 192.96/193.21 Clause #2943 (by superposition #[2941, 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)) % 192.96/193.21 Clause #2959 (by clausification #[2880]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a a_2 a_3) True % 192.96/193.21 Clause #2968 (by superposition #[2959, 496]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_1 a a_2 a_3 a_2 a_3) True) % 192.96/193.21 Clause #2981 (by clausification #[2968]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a a_2 a_3 a_2 a_3) True % 192.96/193.21 Clause #2985 (by superposition #[2981, 352]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a a_1 a_2 a_3 a_2 a_3) True) % 192.96/193.21 Clause #3032 (by clausification #[2985]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_2 a_3 a_2 a_3) True % 192.96/193.21 Clause #3033 (by superposition #[3032, 162]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Or (Eq True False) (Eq (coll a_1 a_2 a) False)) % 193.05/193.28 Clause #3061 (by clausification #[2943]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 193.05/193.28 Clause #3064 (by superposition #[3061, 2941]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 193.05/193.28 Clause #3066 (by clausification #[3064]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 193.05/193.28 Clause #3154 (by clausification #[3033]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (coll a_1 a_2 a) False) % 193.05/193.28 Clause #3155 (by forward demodulation #[3154, 3066]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq True False) % 193.05/193.28 Clause #3156 (by clausification #[3155]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 193.05/193.28 Clause #3157 (by superposition #[3156, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 193.05/193.28 Clause #3163 (by clausification #[3157]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 193.05/193.28 Clause #3167 (by superposition #[3163, 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)) % 193.05/193.28 Clause #3557 (by clausification #[3167]): ∀ (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) % 193.05/193.28 Clause #3559 (by superposition #[3557, 3163]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 193.05/193.28 Clause #3563 (by clausification #[3559]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 193.05/193.28 Clause #3572 (by superposition #[3563, 736]): Eq True False % 193.05/193.28 Clause #3574 (by clausification #[3572]): False % 193.05/193.28 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------