%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO543+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:48:40 PM UTC 2025 % Result : Theorem 12.19s 12.38s % Output : Proof 12.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO543+1 : TPTP v9.2.0. Released v7.5.0. % 0.07/0.14 % Command : duper %s % 0.15/0.35 % Computer : n016.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 11:33:38 EDT 2025 % 0.15/0.35 % CPUTime : % 12.19/12.38 SZS status Theorem for theBenchmark.p % 12.19/12.38 SZS output start Proof for theBenchmark.p % 12.19/12.38 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 12.19/12.38 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 12.19/12.38 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 12.19/12.38 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 12.19/12.38 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 12.19/12.38 Clause #10 (by assumption #[]): Eq (∀ (A B M : Iota), midp M B A → midp M A B) True % 12.19/12.38 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 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 % 12.19/12.38 Clause #63 (by assumption #[]): Eq (∀ (A B C D M : Iota), And (midp M A B) (midp M C D) → para A C B D) True % 12.19/12.38 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 12.19/12.38 Clause #94 (by assumption #[]): Eq % 12.19/12.38 (Not % 12.19/12.38 (∀ (A B C D E F H A1 P Q : Iota), % 12.19/12.38 And % 12.19/12.38 (And % 12.19/12.38 (And % 12.19/12.38 (And % 12.19/12.38 (And % 12.19/12.38 (And (And (And (And (And (perp D A B C) (coll D B C)) (perp E B A C)) (coll E A C)) (perp F C A B)) % 12.19/12.38 (coll F A B)) % 12.19/12.38 (coll H B E)) % 12.19/12.38 (coll H C F)) % 12.19/12.38 (midp A1 C B)) % 12.19/12.38 (midp P E B)) % 12.19/12.38 (midp Q F C) → % 12.19/12.38 cyclic P Q H D)) % 12.19/12.38 True % 12.19/12.38 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 12.19/12.38 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 12.19/12.38 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 % 12.19/12.38 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) % 12.19/12.38 Clause #108 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (B M : Iota), midp M B a → midp M a B) True % 12.19/12.38 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (∀ (M : Iota), midp M a a_1 → midp M a_1 a) True % 12.19/12.38 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), Eq (midp a a_1 a_2 → midp a a_2 a_1) True % 12.19/12.38 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) False) (Eq (midp a a_2 a_1) True) % 12.19/12.38 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 12.19/12.38 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 12.19/12.38 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 % 12.19/12.38 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) % 12.19/12.38 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 12.19/12.38 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 12.19/12.38 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 % 12.19/12.41 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) % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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) % 12.19/12.41 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)) % 12.19/12.41 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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) % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 12.19/12.41 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) % 12.19/12.41 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 12.19/12.41 Or (Eq (cyclic a a_1 a_2 a_3) True) % 12.19/12.41 (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)) % 12.19/12.41 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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) % 12.19/12.41 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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 % 12.19/12.41 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) % 12.19/12.41 Clause #277 (by clausification #[63]): ∀ (a : Iota), Eq (∀ (B C D M : Iota), And (midp M a B) (midp M C D) → para a C B D) True % 12.19/12.41 Clause #278 (by clausification #[277]): ∀ (a a_1 : Iota), Eq (∀ (C D M : Iota), And (midp M a a_1) (midp M C D) → para a C a_1 D) True % 12.27/12.43 Clause #279 (by clausification #[278]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D M : Iota), And (midp M a a_1) (midp M a_2 D) → para a a_2 a_1 D) True % 12.27/12.43 Clause #280 (by clausification #[279]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (M : Iota), And (midp M a a_1) (midp M a_2 a_3) → para a a_2 a_1 a_3) True % 12.27/12.43 Clause #281 (by clausification #[280]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (And (midp a a_1 a_2) (midp a a_3 a_4) → para a_1 a_3 a_2 a_4) True % 12.27/12.43 Clause #282 (by clausification #[281]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (And (midp a a_1 a_2) (midp a a_3 a_4)) False) (Eq (para a_1 a_3 a_2 a_4) True) % 12.27/12.43 Clause #283 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.43 Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (midp a_4 a a_2) False) (Eq (midp a_4 a_1 a_3) False)) % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.43 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) % 12.27/12.43 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.43 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)) % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.43 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 % 12.27/12.43 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.27/12.43 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 % 12.27/12.43 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.27/12.43 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 % 12.27/12.43 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.43 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 % 12.27/12.43 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.43 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) % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.43 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 % 12.27/12.46 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 % 12.27/12.46 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) % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.46 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) % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.46 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 % 12.27/12.46 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.46 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) % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 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 % 12.27/12.46 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.27/12.48 Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a a_1 a_4 Q a_2 a_3 U V) True % 12.27/12.48 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.27/12.48 Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a a_1 a_4 a_5 a_2 a_3 U V) True % 12.27/12.48 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.27/12.48 Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a a_1 a_4 a_5 a_2 a_3 a_6 V) True % 12.27/12.48 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.48 Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True % 12.27/12.48 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.27/12.48 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) % 12.27/12.48 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 % 12.27/12.48 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 % 12.27/12.48 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 % 12.27/12.48 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 % 12.27/12.48 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 % 12.27/12.48 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 % 12.27/12.48 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) % 12.27/12.48 Clause #630 (by clausification #[94]): Eq % 12.27/12.48 (∀ (A B C D E F H A1 P Q : Iota), % 12.27/12.48 And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And (And (And (And (And (perp D A B C) (coll D B C)) (perp E B A C)) (coll E A C)) (perp F C A B)) % 12.27/12.48 (coll F A B)) % 12.27/12.48 (coll H B E)) % 12.27/12.48 (coll H C F)) % 12.27/12.48 (midp A1 C B)) % 12.27/12.48 (midp P E B)) % 12.27/12.48 (midp Q F C) → % 12.27/12.48 cyclic P Q H D) % 12.27/12.48 False % 12.27/12.48 Clause #631 (by clausification #[630]): ∀ (a : Iota), % 12.27/12.48 Eq % 12.27/12.48 (Not % 12.27/12.48 (∀ (B C D E F H A1 P Q : Iota), % 12.27/12.48 And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And (And (And (perp D (skS.0 5 a) B C) (coll D B C)) (perp E B (skS.0 5 a) C)) % 12.27/12.48 (coll E (skS.0 5 a) C)) % 12.27/12.48 (perp F C (skS.0 5 a) B)) % 12.27/12.48 (coll F (skS.0 5 a) B)) % 12.27/12.48 (coll H B E)) % 12.27/12.48 (coll H C F)) % 12.27/12.48 (midp A1 C B)) % 12.27/12.48 (midp P E B)) % 12.27/12.48 (midp Q F C) → % 12.27/12.48 cyclic P Q H D)) % 12.27/12.48 True % 12.27/12.48 Clause #632 (by clausification #[631]): ∀ (a : Iota), % 12.27/12.48 Eq % 12.27/12.48 (∀ (B C D E F H A1 P Q : Iota), % 12.27/12.48 And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And (And (And (perp D (skS.0 5 a) B C) (coll D B C)) (perp E B (skS.0 5 a) C)) % 12.27/12.48 (coll E (skS.0 5 a) C)) % 12.27/12.48 (perp F C (skS.0 5 a) B)) % 12.27/12.48 (coll F (skS.0 5 a) B)) % 12.27/12.48 (coll H B E)) % 12.27/12.48 (coll H C F)) % 12.27/12.48 (midp A1 C B)) % 12.27/12.48 (midp P E B)) % 12.27/12.48 (midp Q F C) → % 12.27/12.48 cyclic P Q H D) % 12.27/12.48 False % 12.27/12.48 Clause #633 (by clausification #[632]): ∀ (a a_1 : Iota), % 12.27/12.48 Eq % 12.27/12.48 (Not % 12.27/12.48 (∀ (C D E F H A1 P Q : Iota), % 12.27/12.48 And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And % 12.27/12.48 (And (And (perp D (skS.0 5 a) (skS.0 6 a a_1) C) (coll D (skS.0 6 a a_1) C)) % 12.27/12.48 (perp E (skS.0 6 a a_1) (skS.0 5 a) C)) % 12.34/12.50 (coll E (skS.0 5 a) C)) % 12.34/12.50 (perp F C (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll H (skS.0 6 a a_1) E)) % 12.34/12.50 (coll H C F)) % 12.34/12.50 (midp A1 C (skS.0 6 a a_1))) % 12.34/12.50 (midp P E (skS.0 6 a a_1))) % 12.34/12.50 (midp Q F C) → % 12.34/12.50 cyclic P Q H D)) % 12.34/12.50 True % 12.34/12.50 Clause #634 (by clausification #[633]): ∀ (a a_1 : Iota), % 12.34/12.50 Eq % 12.34/12.50 (∀ (C D E F H A1 P Q : Iota), % 12.34/12.50 And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And (And (perp D (skS.0 5 a) (skS.0 6 a a_1) C) (coll D (skS.0 6 a a_1) C)) % 12.34/12.50 (perp E (skS.0 6 a a_1) (skS.0 5 a) C)) % 12.34/12.50 (coll E (skS.0 5 a) C)) % 12.34/12.50 (perp F C (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll H (skS.0 6 a a_1) E)) % 12.34/12.50 (coll H C F)) % 12.34/12.50 (midp A1 C (skS.0 6 a a_1))) % 12.34/12.50 (midp P E (skS.0 6 a a_1))) % 12.34/12.50 (midp Q F C) → % 12.34/12.50 cyclic P Q H D) % 12.34/12.50 False % 12.34/12.50 Clause #635 (by clausification #[634]): ∀ (a a_1 a_2 : Iota), % 12.34/12.50 Eq % 12.34/12.50 (Not % 12.34/12.50 (∀ (D E F H A1 P Q : Iota), % 12.34/12.50 And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And (perp D (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.50 (coll D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll H (skS.0 6 a a_1) E)) % 12.34/12.50 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.50 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.50 (midp P E (skS.0 6 a a_1))) % 12.34/12.50 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.50 cyclic P Q H D)) % 12.34/12.50 True % 12.34/12.50 Clause #636 (by clausification #[635]): ∀ (a a_1 a_2 : Iota), % 12.34/12.50 Eq % 12.34/12.50 (∀ (D E F H A1 P Q : Iota), % 12.34/12.50 And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And (perp D (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.50 (coll D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.50 (coll H (skS.0 6 a a_1) E)) % 12.34/12.50 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.50 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.50 (midp P E (skS.0 6 a a_1))) % 12.34/12.50 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.50 cyclic P Q H D) % 12.34/12.50 False % 12.34/12.50 Clause #637 (by clausification #[636]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.50 Eq % 12.34/12.50 (Not % 12.34/12.50 (∀ (E F H A1 P Q : Iota), % 12.34/12.50 And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And % 12.34/12.50 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.50 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.50 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll H (skS.0 6 a a_1) E)) % 12.34/12.53 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.53 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.53 (midp P E (skS.0 6 a a_1))) % 12.34/12.53 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.53 cyclic P Q H (skS.0 8 a a_1 a_2 a_3))) % 12.34/12.53 True % 12.34/12.53 Clause #638 (by clausification #[637]): ∀ (a a_1 a_2 a_3 : Iota), % 12.34/12.53 Eq % 12.34/12.53 (∀ (E F H A1 P Q : Iota), % 12.34/12.53 And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.53 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp E (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll H (skS.0 6 a a_1) E)) % 12.34/12.53 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.53 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.53 (midp P E (skS.0 6 a a_1))) % 12.34/12.53 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.53 cyclic P Q H (skS.0 8 a a_1 a_2 a_3)) % 12.34/12.53 False % 12.34/12.53 Clause #639 (by clausification #[638]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.34/12.53 Eq % 12.34/12.53 (Not % 12.34/12.53 (∀ (F H A1 P Q : Iota), % 12.34/12.53 And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.53 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll H (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.53 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.53 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.53 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.53 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.53 cyclic P Q H (skS.0 8 a a_1 a_2 a_3))) % 12.34/12.53 True % 12.34/12.53 Clause #640 (by clausification #[639]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.34/12.53 Eq % 12.34/12.53 (∀ (F H A1 P Q : Iota), % 12.34/12.53 And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.53 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.53 (perp F (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll F (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.53 (coll H (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.53 (coll H (skS.0 7 a a_1 a_2) F)) % 12.34/12.53 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.53 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.53 (midp Q F (skS.0 7 a a_1 a_2)) → % 12.34/12.53 cyclic P Q H (skS.0 8 a a_1 a_2 a_3)) % 12.34/12.53 False % 12.34/12.53 Clause #641 (by clausification #[640]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.53 Eq % 12.34/12.53 (Not % 12.34/12.53 (∀ (H A1 P Q : Iota), % 12.34/12.53 And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.53 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.55 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll H (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.55 (coll H (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.55 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.55 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.55 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.34/12.55 cyclic P Q H (skS.0 8 a a_1 a_2 a_3))) % 12.34/12.55 True % 12.34/12.55 Clause #642 (by clausification #[641]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 12.34/12.55 Eq % 12.34/12.55 (∀ (H A1 P Q : Iota), % 12.34/12.55 And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.55 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll H (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.55 (coll H (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.55 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.55 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.55 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.34/12.55 cyclic P Q H (skS.0 8 a a_1 a_2 a_3)) % 12.34/12.55 False % 12.34/12.55 Clause #643 (by clausification #[642]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.34/12.55 Eq % 12.34/12.55 (Not % 12.34/12.55 (∀ (A1 P Q : Iota), % 12.34/12.55 And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.55 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.55 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.55 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.55 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.55 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.55 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.55 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.55 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.34/12.55 cyclic P Q (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))) % 12.34/12.55 True % 12.34/12.55 Clause #644 (by clausification #[643]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.34/12.55 Eq % 12.34/12.55 (∀ (A1 P Q : Iota), % 12.34/12.55 And % 12.34/12.55 (And % 12.34/12.55 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.57 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.57 (midp A1 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.57 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.57 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.34/12.57 cyclic P Q (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)) % 12.34/12.57 False % 12.34/12.57 Clause #645 (by clausification #[644]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.34/12.57 Eq % 12.34/12.57 (Not % 12.34/12.57 (∀ (P Q : Iota), % 12.34/12.57 And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.57 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.57 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.57 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.57 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.34/12.57 cyclic P Q (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))) % 12.34/12.57 True % 12.34/12.57 Clause #646 (by clausification #[645]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 12.34/12.57 Eq % 12.34/12.57 (∀ (P Q : Iota), % 12.34/12.57 And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And % 12.34/12.57 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.34/12.57 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.34/12.57 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.34/12.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.34/12.57 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.34/12.57 (midp P (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.34/12.57 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.44/12.59 cyclic P Q (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)) % 12.44/12.59 False % 12.44/12.59 Clause #647 (by clausification #[646]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.44/12.59 Eq % 12.44/12.59 (Not % 12.44/12.59 (∀ (Q : Iota), % 12.44/12.59 And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.44/12.59 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.59 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.59 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.44/12.59 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.44/12.59 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.44/12.59 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.44/12.59 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.44/12.59 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) Q (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 12.44/12.59 (skS.0 8 a a_1 a_2 a_3))) % 12.44/12.59 True % 12.44/12.59 Clause #648 (by clausification #[647]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.44/12.59 Eq % 12.44/12.59 (∀ (Q : Iota), % 12.44/12.59 And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.44/12.59 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.59 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.59 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.44/12.59 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.44/12.59 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.44/12.59 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.44/12.59 (midp Q (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.44/12.59 cyclic (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) Q (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) % 12.44/12.59 (skS.0 8 a a_1 a_2 a_3)) % 12.44/12.59 False % 12.44/12.59 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), % 12.44/12.59 Eq % 12.44/12.59 (Not % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And % 12.44/12.59 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.44/12.59 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.59 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.44/12.61 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.44/12.61 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) % 12.44/12.61 (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))) % 12.44/12.61 True % 12.44/12.61 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), % 12.44/12.61 Eq % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.44/12.61 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.44/12.61 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2)) → % 12.44/12.61 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) % 12.44/12.61 (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)) % 12.44/12.61 False % 12.44/12.61 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), % 12.44/12.61 Eq % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And % 12.44/12.61 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.44/12.61 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.44/12.61 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.44/12.61 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.44/12.61 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.44/12.61 (midp (skS.0 14 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2))) % 12.44/12.61 True % 12.44/12.61 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), % 12.44/12.61 Eq % 12.44/12.61 (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) % 12.44/12.61 (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)) % 12.47/12.64 False % 12.47/12.64 Clause #654 (by clausification #[651]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.47/12.64 Eq % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And % 12.47/12.64 (And (perp (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 12.47/12.64 (coll (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 12.47/12.64 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.47/12.64 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 12.47/12.64 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 12.47/12.64 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 6 a a_1))) % 12.47/12.64 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4))) % 12.47/12.64 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5))) % 12.47/12.64 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1))) % 12.47/12.64 (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1))) % 12.47/12.64 True % 12.47/12.64 Clause #872 (by clausification #[654]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.47/12.64 Eq (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1)) True % 12.47/12.64 Clause #875 (by superposition #[872, 111]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.47/12.64 Or (Eq True False) % 12.47/12.64 (Eq (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4)) True) % 12.47/12.64 Clause #878 (by superposition #[872, 283]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.47/12.64 Or (Eq (para (skS.0 9 a a_1 a_2 a_3 a_4) a_5 (skS.0 6 a a_1) a_6) True) % 12.47/12.64 (Or (Eq True False) (Eq (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_7 a_8 a_9 a_10) a_5 a_6) False)) % 12.47/12.64 Clause #884 (by clausification #[875]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 12.47/12.64 Eq (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4)) True % 12.47/12.64 Clause #1026 (by clausification #[878]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 12.47/12.64 Or (Eq (para (skS.0 9 a a_1 a_2 a_3 a_4) a_5 (skS.0 6 a a_1) a_6) True) % 12.47/12.64 (Eq (midp (skS.0 13 a a_1 a_2 a_3 a_4 a_7 a_8 a_9 a_10) a_5 a_6) False) % 12.47/12.64 Clause #1028 (by superposition #[1026, 884]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.47/12.64 Or (Eq (para (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4)) True) % 12.47/12.64 (Eq False True) % 12.47/12.64 Clause #1030 (by clausification #[1028]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.47/12.64 Eq (para (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4)) True % 12.47/12.64 Clause #1033 (by superposition #[1030, 189]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.47/12.64 Or (Eq True False) % 12.47/12.64 (Eq (para (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1)) True) % 12.47/12.64 Clause #1037 (by clausification #[1033]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 12.47/12.64 Eq (para (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1)) True % 12.47/12.64 Clause #1043 (by superposition #[1037, 610]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.64 Or (Eq True False) % 12.47/12.64 (Eq % 12.47/12.64 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6) % 12.47/12.64 True) % 12.47/12.64 Clause #1289 (by clausification #[1043]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.64 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6) % 12.47/12.64 True % 12.47/12.64 Clause #1291 (by superposition #[1289, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.64 Or (Eq True False) % 12.47/12.64 (Eq % 12.47/12.64 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6 a_5 a_6) % 12.47/12.64 True) % 12.47/12.64 Clause #1293 (by clausification #[1291]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.64 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6 a_5 a_6) % 12.47/12.64 True % 12.47/12.64 Clause #1296 (by superposition #[1293, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a_2 a_3 a_4 a_5 a_6) % 12.47/12.66 (skS.0 6 a_2 a_3)) % 12.47/12.66 True) % 12.47/12.66 Clause #1306 (by clausification #[1296]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq % 12.47/12.66 (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a_2 a_3 a_4 a_5 a_6) % 12.47/12.66 (skS.0 6 a_2 a_3)) % 12.47/12.66 True % 12.47/12.66 Clause #1308 (by superposition #[1306, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle a a_1 a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True) % 12.47/12.66 Clause #1313 (by clausification #[1308]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq % 12.47/12.66 (eqangle a a_1 a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True % 12.47/12.66 Clause #1317 (by superposition #[1313, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) a a_1 (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True) % 12.47/12.66 Clause #1320 (by clausification #[1317]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq % 12.47/12.66 (eqangle a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) a a_1 (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True % 12.47/12.66 Clause #1321 (by superposition #[1320, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) a_1 a (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True) % 12.47/12.66 Clause #1325 (by clausification #[1321]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq % 12.47/12.66 (eqangle a a_1 (skS.0 9 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a_2 a_3) a_1 a (skS.0 6 a_2 a_3) % 12.47/12.66 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.66 True % 12.47/12.66 Clause #1329 (by superposition #[1325, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) a_1 a (skS.0 9 a_2 a_3 a_4 a_5 a_6) % 12.47/12.66 (skS.0 6 a_2 a_3)) % 12.47/12.66 True) % 12.47/12.66 Clause #1334 (by clausification #[1329]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq % 12.47/12.66 (eqangle a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) a_1 a (skS.0 9 a_2 a_3 a_4 a_5 a_6) % 12.47/12.66 (skS.0 6 a_2 a_3)) % 12.47/12.66 True % 12.47/12.66 Clause #1337 (by superposition #[1334, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_6 a_5) % 12.47/12.66 True) % 12.47/12.66 Clause #1346 (by clausification #[1337]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_6 a_5) % 12.47/12.66 True % 12.47/12.66 Clause #1349 (by superposition #[1346, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6 a_6 a_5) % 12.47/12.66 True) % 12.47/12.66 Clause #1352 (by clausification #[1349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) a_5 a_6 a_6 a_5) % 12.47/12.66 True % 12.47/12.66 Clause #1354 (by superposition #[1352, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 a_6 a_5) % 12.47/12.66 True) % 12.47/12.66 Clause #1359 (by clausification #[1354]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq (eqangle (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 a_6 a_5) % 12.47/12.66 True % 12.47/12.66 Clause #1360 (by superposition #[1359, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Or (Eq True False) % 12.47/12.66 (Eq % 12.47/12.66 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 a_6 a_5) % 12.47/12.66 True) % 12.47/12.66 Clause #1371 (by clausification #[1360]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.66 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 a_6 a_5) % 12.47/12.69 True % 12.47/12.69 Clause #1378 (by superposition #[1371, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.69 Or (Eq True False) % 12.47/12.69 (Eq % 12.47/12.69 (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_6 a_5) % 12.47/12.69 True) % 12.47/12.69 Clause #1383 (by clausification #[1378]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.69 Eq (eqangle (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_5 a_6 (skS.0 6 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4) a_6 a_5) % 12.47/12.69 True % 12.47/12.69 Clause #1388 (by superposition #[1383, 397]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.69 Or (Eq True False) % 12.47/12.69 (Eq % 12.47/12.69 (eqangle a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) a_1 a (skS.0 6 a_2 a_3) % 12.47/12.69 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.69 True) % 12.47/12.69 Clause #1395 (by clausification #[1388]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 12.47/12.69 Eq % 12.47/12.69 (eqangle a a_1 (skS.0 6 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6) a_1 a (skS.0 6 a_2 a_3) % 12.47/12.69 (skS.0 9 a_2 a_3 a_4 a_5 a_6)) % 12.47/12.69 True % 12.47/12.69 Clause #1400 (by superposition #[1395, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 12.47/12.69 Clause #1408 (by clausification #[1400]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 12.47/12.69 Clause #1411 (by superposition #[1408, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 12.47/12.69 Clause #1414 (by superposition #[1408, 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) % 12.47/12.69 Clause #1441 (by clausification #[1411]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 12.47/12.69 Clause #1442 (by superposition #[1441, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 12.47/12.69 Clause #1447 (by clausification #[1442]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 12.47/12.69 Clause #1448 (by superposition #[1447, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 12.47/12.69 Clause #1457 (by clausification #[1448]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 12.47/12.69 Clause #1459 (by superposition #[1457, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 12.47/12.69 Clause #1468 (by clausification #[1459]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 12.47/12.69 Clause #1470 (by superposition #[1468, 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)) % 12.47/12.69 Clause #1480 (by clausification #[1414]): ∀ (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 % 12.47/12.69 Clause #1489 (by superposition #[1480, 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) % 12.47/12.69 Clause #1493 (by clausification #[1489]): ∀ (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 % 12.47/12.69 Clause #1497 (by superposition #[1493, 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) % 12.47/12.69 Clause #1551 (by clausification #[1497]): ∀ (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 % 12.47/12.69 Clause #1552 (by superposition #[1551, 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)) % 12.47/12.69 Clause #1563 (by clausification #[1470]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 12.47/12.69 Clause #1566 (by superposition #[1563, 1468]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 12.47/12.69 Clause #1567 (by clausification #[1566]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 12.47/12.69 Clause #1686 (by clausification #[1552]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (coll a_1 a_2 a) False) % 12.47/12.69 Clause #1687 (by forward demodulation #[1686, 1567]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq True False) % 12.47/12.69 Clause #1688 (by clausification #[1687]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 12.47/12.69 Clause #1689 (by superposition #[1688, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 12.47/12.69 Clause #1695 (by clausification #[1689]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 12.47/12.69 Clause #1699 (by superposition #[1695, 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)) % 12.47/12.70 Clause #2026 (by clausification #[1699]): ∀ (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) % 12.47/12.70 Clause #2028 (by superposition #[2026, 1695]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 12.47/12.70 Clause #2031 (by clausification #[2028]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 12.47/12.70 Clause #2041 (by superposition #[2031, 652]): Eq True False % 12.47/12.70 Clause #2048 (by clausification #[2041]): False % 12.47/12.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------