%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO643+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:48:47 PM UTC 2025 % Result : Theorem 20.86s 21.06s % Output : Proof 21.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO643+1 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n025.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:36:08 EDT 2025 % 0.13/0.35 % CPUTime : % 20.86/21.06 SZS status Theorem for theBenchmark.p % 20.86/21.06 SZS output start Proof for theBenchmark.p % 20.86/21.06 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 20.86/21.06 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 20.86/21.06 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 20.86/21.06 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 20.86/21.06 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 20.86/21.06 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 20.86/21.06 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 20.86/21.06 Clause #8 (by assumption #[]): Eq (∀ (A B C D E F : Iota), And (perp A B C D) (perp C D E F) → para A B E F) True % 20.86/21.06 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 20.86/21.06 Clause #16 (by assumption #[]): Eq (∀ (A B C D E : Iota), And (cyclic A B C D) (cyclic A B C E) → cyclic B C D E) True % 20.86/21.06 Clause #17 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle B A C D P Q U V) True % 20.86/21.06 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 % 20.86/21.06 Clause #19 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle P Q U V A B C D) True % 20.86/21.06 Clause #20 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle A B P Q C D U V) True % 20.86/21.06 Clause #38 (by assumption #[]): Eq (∀ (A B C D P Q : Iota), eqangle A B P Q C D P Q → para A B C D) True % 20.86/21.06 Clause #39 (by assumption #[]): Eq (∀ (A B C D P Q : Iota), para A B C D → eqangle A B P Q C D P Q) True % 20.86/21.06 Clause #42 (by assumption #[]): Eq (∀ (A B P Q : Iota), And (eqangle P A P B Q A Q B) (coll P Q B) → cyclic A B P Q) True % 20.86/21.06 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 20.86/21.06 Clause #86 (by assumption #[]): Eq (∀ (A B C O : Iota), Exists fun P => circle O A B C → perp P A A O) True % 20.86/21.06 Clause #94 (by assumption #[]): Eq % 20.86/21.06 (Not % 20.86/21.06 (∀ (A B C D E F G H I J : Iota), % 20.86/21.06 And % 20.86/21.06 (And % 20.86/21.06 (And (And (And (And (And (coll C A B) (coll E A D)) (coll F B E)) (coll F C D)) (circle G D E F)) % 20.86/21.06 (circle H A C D)) % 20.86/21.06 (circle I B C F)) % 20.86/21.06 (circle J B A E) → % 20.86/21.06 cyclic I J H G)) % 20.86/21.06 True % 20.86/21.06 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 20.86/21.06 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 20.86/21.06 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 % 20.86/21.06 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) % 20.86/21.06 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 20.86/21.06 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 20.86/21.06 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 % 20.86/21.06 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) % 20.86/21.06 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 20.86/21.06 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 20.86/21.06 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 % 20.86/21.06 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) % 20.86/21.06 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 % 20.86/21.06 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 % 20.86/21.06 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 % 20.86/21.09 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 % 20.86/21.09 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) % 20.86/21.09 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)) % 20.86/21.09 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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) % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 20.86/21.09 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) % 20.86/21.09 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 20.86/21.09 Or (Eq (cyclic a a_1 a_2 a_3) True) % 20.86/21.09 (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)) % 20.86/21.09 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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) % 20.86/21.09 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 20.86/21.09 Clause #186 (by clausification #[185]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), para a a_1 C D → para C D a a_1) True % 20.86/21.09 Clause #187 (by clausification #[186]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), para a a_1 a_2 D → para a_2 D a a_1) True % 20.86/21.09 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para a a_1 a_2 a_3 → para a_2 a_3 a a_1) True % 20.86/21.09 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (para a a_1 a_2 a_3) False) (Eq (para a_2 a_3 a a_1) True) % 20.86/21.09 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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 % 20.86/21.09 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) % 20.86/21.09 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 20.94/21.11 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), perp a a_1 C D → perp C D a a_1) True % 20.94/21.11 Clause #268 (by clausification #[267]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), perp a a_1 a_2 D → perp a_2 D a a_1) True % 20.94/21.11 Clause #269 (by clausification #[268]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3 → perp a_2 a_3 a a_1) True % 20.94/21.11 Clause #270 (by clausification #[269]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) False) (Eq (perp a_2 a_3 a a_1) True) % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.11 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) % 20.94/21.11 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.11 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)) % 20.94/21.11 Clause #298 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (B C D E F : Iota), And (perp a B C D) (perp C D E F) → para a B E F) True % 20.94/21.11 Clause #299 (by clausification #[298]): ∀ (a a_1 : Iota), Eq (∀ (C D E F : Iota), And (perp a a_1 C D) (perp C D E F) → para a a_1 E F) True % 20.94/21.11 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E F : Iota), And (perp a a_1 a_2 D) (perp a_2 D E F) → para a a_1 E F) True % 20.94/21.11 Clause #301 (by clausification #[300]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 E F) → para a a_1 E F) True % 20.94/21.11 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 F) → para a a_1 a_4 F) True % 20.94/21.11 Clause #303 (by clausification #[302]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5) → para a a_1 a_4 a_5) True % 20.94/21.11 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.11 Or (Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5)) False) (Eq (para a a_1 a_4 a_5) True) % 20.94/21.11 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.11 Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (perp a a_1 a_4 a_5) False) (Eq (perp a_4 a_5 a_2 a_3) False)) % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 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 % 20.94/21.11 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.11 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 % 20.94/21.11 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.11 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 % 20.94/21.11 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.94/21.11 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 % 20.94/21.14 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.14 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 % 20.94/21.14 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.14 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) % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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) % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 Clause #375 (by clausification #[374]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.14 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) % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.14 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.14 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 % 20.94/21.14 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.14 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 % 20.94/21.14 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.94/21.14 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 % 20.94/21.14 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.14 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 % 20.94/21.14 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.14 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) % 20.94/21.14 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 % 20.94/21.14 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.16 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) % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.16 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 % 20.94/21.16 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 20.94/21.16 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) % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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 % 20.94/21.16 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) % 20.94/21.16 Clause #630 (by clausification #[94]): Eq % 20.94/21.16 (∀ (A B C D E F G H I J : Iota), % 20.94/21.16 And % 20.94/21.16 (And % 20.94/21.16 (And (And (And (And (And (coll C A B) (coll E A D)) (coll F B E)) (coll F C D)) (circle G D E F)) % 20.94/21.16 (circle H A C D)) % 20.94/21.16 (circle I B C F)) % 20.94/21.16 (circle J B A E) → % 21.00/21.19 cyclic I J H G) % 21.00/21.19 False % 21.00/21.19 Clause #631 (by clausification #[630]): ∀ (a : Iota), % 21.00/21.19 Eq % 21.00/21.19 (Not % 21.00/21.19 (∀ (B C D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (And (And (coll C (skS.0 5 a) B) (coll E (skS.0 5 a) D)) (coll F B E)) (coll F C D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) C D)) % 21.00/21.19 (circle I B C F)) % 21.00/21.19 (circle J B (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G)) % 21.00/21.19 True % 21.00/21.19 Clause #632 (by clausification #[631]): ∀ (a : Iota), % 21.00/21.19 Eq % 21.00/21.19 (∀ (B C D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (And (And (coll C (skS.0 5 a) B) (coll E (skS.0 5 a) D)) (coll F B E)) (coll F C D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) C D)) % 21.00/21.19 (circle I B C F)) % 21.00/21.19 (circle J B (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G) % 21.00/21.19 False % 21.00/21.19 Clause #633 (by clausification #[632]): ∀ (a a_1 : Iota), % 21.00/21.19 Eq % 21.00/21.19 (Not % 21.00/21.19 (∀ (C D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (coll C (skS.0 5 a) (skS.0 6 a a_1)) (coll E (skS.0 5 a) D)) (coll F (skS.0 6 a a_1) E)) % 21.00/21.19 (coll F C D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) C D)) % 21.00/21.19 (circle I (skS.0 6 a a_1) C F)) % 21.00/21.19 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G)) % 21.00/21.19 True % 21.00/21.19 Clause #634 (by clausification #[633]): ∀ (a a_1 : Iota), % 21.00/21.19 Eq % 21.00/21.19 (∀ (C D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (And (coll C (skS.0 5 a) (skS.0 6 a a_1)) (coll E (skS.0 5 a) D)) (coll F (skS.0 6 a a_1) E)) % 21.00/21.19 (coll F C D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) C D)) % 21.00/21.19 (circle I (skS.0 6 a a_1) C F)) % 21.00/21.19 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G) % 21.00/21.19 False % 21.00/21.19 Clause #635 (by clausification #[634]): ∀ (a a_1 a_2 : Iota), % 21.00/21.19 Eq % 21.00/21.19 (Not % 21.00/21.19 (∀ (D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) (coll E (skS.0 5 a) D)) % 21.00/21.19 (coll F (skS.0 6 a a_1) E)) % 21.00/21.19 (coll F (skS.0 7 a a_1 a_2) D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) D)) % 21.00/21.19 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.19 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G)) % 21.00/21.19 True % 21.00/21.19 Clause #636 (by clausification #[635]): ∀ (a a_1 a_2 : Iota), % 21.00/21.19 Eq % 21.00/21.19 (∀ (D E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) (coll E (skS.0 5 a) D)) % 21.00/21.19 (coll F (skS.0 6 a a_1) E)) % 21.00/21.19 (coll F (skS.0 7 a a_1 a_2) D)) % 21.00/21.19 (circle G D E F)) % 21.00/21.19 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) D)) % 21.00/21.19 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.19 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.19 cyclic I J H G) % 21.00/21.19 False % 21.00/21.19 Clause #637 (by clausification #[636]): ∀ (a a_1 a_2 a_3 : Iota), % 21.00/21.19 Eq % 21.00/21.19 (Not % 21.00/21.19 (∀ (E F G H I J : Iota), % 21.00/21.19 And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And % 21.00/21.19 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.19 (coll E (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.19 (coll F (skS.0 6 a a_1) E)) % 21.00/21.19 (coll F (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.19 (circle G (skS.0 8 a a_1 a_2 a_3) E F)) % 21.00/21.19 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.19 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.19 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.21 cyclic I J H G)) % 21.00/21.21 True % 21.00/21.21 Clause #638 (by clausification #[637]): ∀ (a a_1 a_2 a_3 : Iota), % 21.00/21.21 Eq % 21.00/21.21 (∀ (E F G H I J : Iota), % 21.00/21.21 And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.21 (coll E (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (coll F (skS.0 6 a a_1) E)) % 21.00/21.21 (coll F (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle G (skS.0 8 a a_1 a_2 a_3) E F)) % 21.00/21.21 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.21 (circle J (skS.0 6 a a_1) (skS.0 5 a) E) → % 21.00/21.21 cyclic I J H G) % 21.00/21.21 False % 21.00/21.21 Clause #639 (by clausification #[638]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.00/21.21 Eq % 21.00/21.21 (Not % 21.00/21.21 (∀ (F G H I J : Iota), % 21.00/21.21 And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.21 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (coll F (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.21 (coll F (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle G (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) F)) % 21.00/21.21 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.21 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.21 cyclic I J H G)) % 21.00/21.21 True % 21.00/21.21 Clause #640 (by clausification #[639]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 21.00/21.21 Eq % 21.00/21.21 (∀ (F G H I J : Iota), % 21.00/21.21 And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.21 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (coll F (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.21 (coll F (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle G (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) F)) % 21.00/21.21 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) F)) % 21.00/21.21 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.21 cyclic I J H G) % 21.00/21.21 False % 21.00/21.21 Clause #641 (by clausification #[640]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.00/21.21 Eq % 21.00/21.21 (Not % 21.00/21.21 (∀ (G H I J : Iota), % 21.00/21.21 And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.21 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.21 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle G (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.21 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.21 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.21 cyclic I J H G)) % 21.00/21.21 True % 21.00/21.21 Clause #642 (by clausification #[641]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 21.00/21.21 Eq % 21.00/21.21 (∀ (G H I J : Iota), % 21.00/21.21 And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And % 21.00/21.21 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.21 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.21 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle G (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.24 cyclic I J H G) % 21.00/21.24 False % 21.00/21.24 Clause #643 (by clausification #[642]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.00/21.24 Eq % 21.00/21.24 (Not % 21.00/21.24 (∀ (H I J : Iota), % 21.00/21.24 And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.24 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.00/21.24 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.24 cyclic I J H (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 21.00/21.24 True % 21.00/21.24 Clause #644 (by clausification #[643]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 21.00/21.24 Eq % 21.00/21.24 (∀ (H I J : Iota), % 21.00/21.24 And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.24 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.00/21.24 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle H (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.24 cyclic I J H (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 21.00/21.24 False % 21.00/21.24 Clause #645 (by clausification #[644]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.00/21.24 Eq % 21.00/21.24 (Not % 21.00/21.24 (∀ (I J : Iota), % 21.00/21.24 And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And % 21.00/21.24 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.00/21.24 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.00/21.24 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.00/21.24 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) % 21.00/21.24 (skS.0 8 a a_1 a_2 a_3))) % 21.00/21.24 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.00/21.24 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.00/21.24 cyclic I J (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 21.00/21.24 True % 21.00/21.24 Clause #646 (by clausification #[645]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.00/21.24 Eq % 21.00/21.24 (∀ (I J : Iota), % 21.08/21.26 And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.08/21.26 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.08/21.26 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle I (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.08/21.26 cyclic I J (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 21.08/21.26 False % 21.08/21.26 Clause #647 (by clausification #[646]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.08/21.26 Eq % 21.08/21.26 (Not % 21.08/21.26 (∀ (J : Iota), % 21.08/21.26 And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.08/21.26 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.08/21.26 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) % 21.08/21.26 (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.08/21.26 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.08/21.26 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) J (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.08/21.26 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 21.08/21.26 True % 21.08/21.26 Clause #648 (by clausification #[647]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.08/21.26 Eq % 21.08/21.26 (∀ (J : Iota), % 21.08/21.26 And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.08/21.26 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.08/21.26 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.08/21.26 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.08/21.26 (circle J (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.08/21.26 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) J (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.08/21.26 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 21.08/21.26 False % 21.08/21.26 Clause #649 (by clausification #[648]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.08/21.26 Eq % 21.08/21.26 (Not % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And % 21.08/21.26 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.08/21.26 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.08/21.26 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 6 a a_1) (skS.0 5 a) % 21.11/21.29 (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.11/21.29 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 21.11/21.29 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 21.11/21.29 True % 21.11/21.29 Clause #650 (by clausification #[649]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.11/21.29 Eq % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.11/21.29 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 6 a a_1) (skS.0 5 a) % 21.11/21.29 (skS.0 9 a a_1 a_2 a_3 a_4)) → % 21.11/21.29 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 21.11/21.29 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 21.11/21.29 False % 21.11/21.29 Clause #651 (by clausification #[650]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.11/21.29 Eq % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.11/21.29 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.11/21.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.29 (circle (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.29 True % 21.11/21.29 Clause #652 (by clausification #[650]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.11/21.29 Eq % 21.11/21.29 (cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 21.11/21.29 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 21.11/21.29 False % 21.11/21.29 Clause #654 (by clausification #[651]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.29 Eq % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And % 21.11/21.29 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.11/21.29 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.29 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.31 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.31 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.11/21.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.31 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.31 (circle (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) % 21.11/21.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.31 True % 21.11/21.31 Clause #859 (by clausification #[654]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.11/21.31 Eq % 21.11/21.31 (And % 21.11/21.31 (And % 21.11/21.31 (And % 21.11/21.31 (And % 21.11/21.31 (And (coll (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1)) % 21.11/21.31 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.31 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 21.11/21.31 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.31 (circle (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4) % 21.11/21.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 21.11/21.31 (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3))) % 21.11/21.31 True % 21.11/21.31 Clause #1082 (by clausification #[859]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.11/21.31 Eq (circle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) True % 21.11/21.31 Clause #1086 (by superposition #[1082, 375]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Or (Eq True False) % 21.11/21.31 (Eq % 21.11/21.31 (perp % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.11/21.31 True) % 21.11/21.31 Clause #1090 (by clausification #[1086]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Eq % 21.11/21.31 (perp (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.11/21.31 True % 21.11/21.31 Clause #1093 (by superposition #[1090, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Or (Eq True False) % 21.11/21.31 (Eq % 21.11/21.31 (perp (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a)) % 21.11/21.31 True) % 21.11/21.31 Clause #1108 (by clausification #[1093]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Eq % 21.11/21.31 (perp (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a)) % 21.11/21.31 True % 21.11/21.31 Clause #1109 (by superposition #[1108, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Or (Eq True False) % 21.11/21.31 (Eq % 21.11/21.31 (perp (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8)) % 21.11/21.31 True) % 21.11/21.31 Clause #1119 (by clausification #[1109]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Eq % 21.11/21.31 (perp (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8)) % 21.11/21.31 True % 21.11/21.31 Clause #1120 (by superposition #[1119, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Or (Eq True False) % 21.11/21.31 (Eq % 21.11/21.31 (perp (skS.0 5 a) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.11/21.31 True) % 21.11/21.31 Clause #1130 (by clausification #[1120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.11/21.31 Eq % 21.11/21.31 (perp (skS.0 5 a) % 21.11/21.31 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.11/21.31 (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.11/21.31 True % 21.11/21.31 Clause #1131 (by superposition #[1130, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Or (Eq True False) % 21.16/21.34 (Eq % 21.16/21.34 (perp (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.16/21.34 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a)) % 21.16/21.34 True) % 21.16/21.34 Clause #1142 (by clausification #[1131]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Eq % 21.16/21.34 (perp (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.16/21.34 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a)) % 21.16/21.34 True % 21.16/21.34 Clause #1143 (by superposition #[1142, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Or (Eq True False) % 21.16/21.34 (Eq % 21.16/21.34 (perp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8)) % 21.16/21.34 True) % 21.16/21.34 Clause #1153 (by clausification #[1143]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Eq % 21.16/21.34 (perp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8)) % 21.16/21.34 True % 21.16/21.34 Clause #1155 (by superposition #[1153, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Or (Eq True False) % 21.16/21.34 (Eq % 21.16/21.34 (perp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.16/21.34 (skS.0 5 a)) % 21.16/21.34 True) % 21.16/21.34 Clause #1170 (by clausification #[1155]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 21.16/21.34 Eq % 21.16/21.34 (perp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_8) % 21.16/21.34 (skS.0 5 a)) % 21.16/21.34 True % 21.16/21.34 Clause #1171 (by superposition #[1170, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 21.16/21.34 Or (Eq (para (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) a_8 a_9) True) % 21.16/21.34 (Or (Eq True False) % 21.16/21.34 (Eq % 21.16/21.34 (perp % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) % 21.16/21.34 a_10) % 21.16/21.34 (skS.0 5 a) a_8 a_9) % 21.16/21.34 False)) % 21.16/21.34 Clause #1193 (by clausification #[1171]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 21.16/21.34 Or (Eq (para (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) a_8 a_9) True) % 21.16/21.34 (Eq % 21.16/21.34 (perp % 21.16/21.34 (skS.0 0 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3) a_10) % 21.16/21.34 (skS.0 5 a) a_8 a_9) % 21.16/21.34 False) % 21.16/21.34 Clause #1201 (by superposition #[1193, 1090]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.34 Or % 21.16/21.34 (Eq (para (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.16/21.34 True) % 21.16/21.34 (Eq False True) % 21.16/21.34 Clause #1202 (by clausification #[1201]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.34 Eq (para (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 21.16/21.34 True % 21.16/21.34 Clause #1205 (by superposition #[1202, 189]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.34 Or (Eq True False) % 21.16/21.34 (Eq (para (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a)) % 21.16/21.34 True) % 21.16/21.34 Clause #1211 (by clausification #[1205]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 21.16/21.34 Eq (para (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a)) % 21.16/21.34 True % 21.16/21.34 Clause #1217 (by superposition #[1211, 610]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.34 Or (Eq True False) % 21.16/21.34 (Eq % 21.16/21.34 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.34 (skS.0 5 a) a_8 a_9) % 21.16/21.34 True) % 21.16/21.34 Clause #1347 (by clausification #[1217]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.34 Eq % 21.16/21.34 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.34 (skS.0 5 a) a_8 a_9) % 21.16/21.34 True % 21.16/21.34 Clause #1349 (by superposition #[1347, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.36 a_8 a_9 a_8 a_9) % 21.16/21.36 True) % 21.16/21.36 Clause #1351 (by clausification #[1349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.36 a_8 a_9 a_8 a_9) % 21.16/21.36 True % 21.16/21.36 Clause #1354 (by superposition #[1351, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle a a_1 a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2)) % 21.16/21.36 True) % 21.16/21.36 Clause #1359 (by clausification #[1354]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle a a_1 a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2)) % 21.16/21.36 True % 21.16/21.36 Clause #1361 (by superposition #[1359, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle a a_1 a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True) % 21.16/21.36 Clause #1367 (by clausification #[1361]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle a a_1 a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True % 21.16/21.36 Clause #1371 (by superposition #[1367, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) a a_1 (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True) % 21.16/21.36 Clause #1374 (by clausification #[1371]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) a a_1 (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True % 21.16/21.36 Clause #1375 (by superposition #[1374, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) a_1 a (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True) % 21.16/21.36 Clause #1379 (by clausification #[1375]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle a a_1 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2) a_1 a (skS.0 5 a_2) % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.36 True % 21.16/21.36 Clause #1383 (by superposition #[1379, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_1 a % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2)) % 21.16/21.36 True) % 21.16/21.36 Clause #1388 (by clausification #[1383]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_1 a % 21.16/21.36 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 5 a_2)) % 21.16/21.36 True % 21.16/21.36 Clause #1391 (by superposition #[1388, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.36 (skS.0 5 a) a_9 a_8) % 21.16/21.36 True) % 21.16/21.36 Clause #1396 (by clausification #[1391]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Eq % 21.16/21.36 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.36 (skS.0 5 a) a_9 a_8) % 21.16/21.36 True % 21.16/21.36 Clause #1399 (by superposition #[1396, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.36 Or (Eq True False) % 21.16/21.36 (Eq % 21.16/21.36 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.36 a_8 a_9 a_9 a_8) % 21.16/21.36 True) % 21.16/21.36 Clause #1403 (by clausification #[1399]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Eq % 21.16/21.39 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) % 21.16/21.39 a_8 a_9 a_9 a_8) % 21.16/21.39 True % 21.16/21.39 Clause #1405 (by superposition #[1403, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Or (Eq True False) % 21.16/21.39 (Eq % 21.16/21.39 (eqangle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.39 a_8 a_9 a_9 a_8) % 21.16/21.39 True) % 21.16/21.39 Clause #1410 (by clausification #[1405]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Eq % 21.16/21.39 (eqangle (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.39 a_8 a_9 a_9 a_8) % 21.16/21.39 True % 21.16/21.39 Clause #1411 (by superposition #[1410, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Or (Eq True False) % 21.16/21.39 (Eq % 21.16/21.39 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.39 a_8 a_9 a_9 a_8) % 21.16/21.39 True) % 21.16/21.39 Clause #1416 (by clausification #[1411]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Eq % 21.16/21.39 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 21.16/21.39 a_8 a_9 a_9 a_8) % 21.16/21.39 True % 21.16/21.39 Clause #1423 (by superposition #[1416, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Or (Eq True False) % 21.16/21.39 (Eq % 21.16/21.39 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 5 a) % 21.16/21.39 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_9 a_8) % 21.16/21.39 True) % 21.16/21.39 Clause #1428 (by clausification #[1423]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Eq % 21.16/21.39 (eqangle (skS.0 5 a) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8 a_9 (skS.0 5 a) % 21.16/21.39 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_9 a_8) % 21.16/21.39 True % 21.16/21.39 Clause #1433 (by superposition #[1428, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Or (Eq True False) % 21.16/21.39 (Eq % 21.16/21.39 (eqangle a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_1 a (skS.0 5 a_2) % 21.16/21.39 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.39 True) % 21.16/21.39 Clause #1440 (by clausification #[1433]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 21.16/21.39 Eq % 21.16/21.39 (eqangle a a_1 (skS.0 5 a_2) (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_1 a (skS.0 5 a_2) % 21.16/21.39 (skS.0 12 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 21.16/21.39 True % 21.16/21.39 Clause #1445 (by superposition #[1440, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 21.16/21.39 Clause #1454 (by clausification #[1445]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 21.16/21.39 Clause #1457 (by superposition #[1454, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 21.16/21.39 Clause #1460 (by superposition #[1454, 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) % 21.16/21.39 Clause #1472 (by clausification #[1457]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 21.16/21.39 Clause #1473 (by superposition #[1472, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 21.16/21.39 Clause #1478 (by clausification #[1473]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 21.16/21.39 Clause #1481 (by superposition #[1478, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 21.16/21.39 Clause #1491 (by clausification #[1481]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 21.16/21.39 Clause #1494 (by superposition #[1491, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 21.16/21.39 Clause #1505 (by clausification #[1494]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 21.16/21.39 Clause #1507 (by superposition #[1505, 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)) % 21.16/21.39 Clause #1517 (by clausification #[1460]): ∀ (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 % 21.16/21.39 Clause #1526 (by superposition #[1517, 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) % 21.16/21.39 Clause #1530 (by clausification #[1526]): ∀ (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 % 21.16/21.39 Clause #1534 (by superposition #[1530, 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) % 21.24/21.41 Clause #1578 (by clausification #[1534]): ∀ (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 % 21.24/21.41 Clause #1579 (by superposition #[1578, 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)) % 21.24/21.41 Clause #1607 (by clausification #[1507]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 21.24/21.41 Clause #1609 (by superposition #[1607, 1505]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 21.24/21.41 Clause #1610 (by clausification #[1609]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 21.24/21.41 Clause #1689 (by clausification #[1579]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (coll a_1 a_2 a) False) % 21.24/21.41 Clause #1690 (by forward demodulation #[1689, 1610]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq True False) % 21.24/21.41 Clause #1691 (by clausification #[1690]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 21.24/21.41 Clause #1692 (by superposition #[1691, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 21.24/21.41 Clause #1700 (by clausification #[1692]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 21.24/21.41 Clause #1704 (by superposition #[1700, 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)) % 21.24/21.41 Clause #2080 (by clausification #[1704]): ∀ (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) % 21.24/21.41 Clause #2082 (by superposition #[2080, 1700]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 21.24/21.41 Clause #2085 (by clausification #[2082]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 21.24/21.41 Clause #2092 (by superposition #[2085, 652]): Eq True False % 21.24/21.41 Clause #2094 (by clausification #[2092]): False % 21.24/21.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------