%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO620+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:46 PM UTC 2025 % Result : Theorem 27.91s 28.19s % Output : Proof 28.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GEO620+1 : TPTP v9.2.0. Released v7.5.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n002.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 11:59:38 EDT 2025 % 0.13/0.35 % CPUTime : % 27.91/28.19 SZS status Theorem for theBenchmark.p % 27.91/28.19 SZS output start Proof for theBenchmark.p % 27.91/28.19 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 27.91/28.19 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 27.91/28.19 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 27.91/28.19 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 27.91/28.19 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 27.91/28.19 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 27.91/28.19 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 27.91/28.19 Clause #94 (by assumption #[]): Eq % 27.91/28.19 (Not % 27.91/28.19 (∀ (A B C O I E J L : Iota), % 27.91/28.19 And % 27.91/28.19 (And % 27.91/28.19 (And % 27.91/28.19 (And % 27.91/28.19 (And % 27.91/28.19 (And % 27.91/28.19 (And (And (And (eqangle O A A B O A A C) (eqangle O B B C O B B A)) (eqangle O C C A O C C B)) % 27.91/28.19 (perp I C A O)) % 27.91/28.19 (coll I A O)) % 27.91/28.19 (perp A O A E)) % 27.91/28.19 (perp J C A E)) % 27.91/28.19 (coll J A E)) % 27.91/28.19 (perp L C B O)) % 27.91/28.19 (coll L B O) → % 27.91/28.19 coll I L J)) % 27.91/28.19 True % 27.91/28.19 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 27.91/28.19 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 27.91/28.19 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 % 27.91/28.19 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) % 27.91/28.19 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 27.91/28.19 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 27.91/28.19 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 % 27.91/28.19 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) % 27.91/28.19 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 27.91/28.19 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 27.91/28.19 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 % 27.91/28.19 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) % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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 % 27.91/28.19 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) % 28.01/28.23 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)) % 28.01/28.23 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 28.01/28.23 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 % 28.01/28.23 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 % 28.01/28.23 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 % 28.01/28.23 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) % 28.01/28.23 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 28.01/28.23 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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) % 28.01/28.24 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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) % 28.01/28.24 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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) % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 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 % 28.01/28.24 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.01/28.24 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) % 28.01/28.24 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.01/28.24 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)) % 28.01/28.24 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.01/28.29 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) % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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) % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 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 % 28.01/28.29 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.01/28.29 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 % 28.01/28.29 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.01/28.29 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) % 28.01/28.29 Clause #458 (by clausification #[94]): Eq % 28.01/28.29 (∀ (A B C O I E J L : Iota), % 28.01/28.29 And % 28.01/28.29 (And % 28.01/28.29 (And % 28.01/28.29 (And % 28.01/28.29 (And % 28.01/28.29 (And % 28.01/28.29 (And (And (And (eqangle O A A B O A A C) (eqangle O B B C O B B A)) (eqangle O C C A O C C B)) % 28.11/28.34 (perp I C A O)) % 28.11/28.34 (coll I A O)) % 28.11/28.34 (perp A O A E)) % 28.11/28.34 (perp J C A E)) % 28.11/28.34 (coll J A E)) % 28.11/28.34 (perp L C B O)) % 28.11/28.34 (coll L B O) → % 28.11/28.34 coll I L J) % 28.11/28.34 False % 28.11/28.34 Clause #459 (by clausification #[458]): ∀ (a : Iota), % 28.11/28.34 Eq % 28.11/28.34 (Not % 28.11/28.34 (∀ (B C O I E J L : Iota), % 28.11/28.34 And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And (eqangle O (skS.0 4 a) (skS.0 4 a) B O (skS.0 4 a) (skS.0 4 a) C) % 28.11/28.34 (eqangle O B B C O B B (skS.0 4 a))) % 28.11/28.34 (eqangle O C C (skS.0 4 a) O C C B)) % 28.11/28.34 (perp I C (skS.0 4 a) O)) % 28.11/28.34 (coll I (skS.0 4 a) O)) % 28.11/28.34 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.34 (perp J C (skS.0 4 a) E)) % 28.11/28.34 (coll J (skS.0 4 a) E)) % 28.11/28.34 (perp L C B O)) % 28.11/28.34 (coll L B O) → % 28.11/28.34 coll I L J)) % 28.11/28.34 True % 28.11/28.34 Clause #460 (by clausification #[459]): ∀ (a : Iota), % 28.11/28.34 Eq % 28.11/28.34 (∀ (B C O I E J L : Iota), % 28.11/28.34 And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And (eqangle O (skS.0 4 a) (skS.0 4 a) B O (skS.0 4 a) (skS.0 4 a) C) % 28.11/28.34 (eqangle O B B C O B B (skS.0 4 a))) % 28.11/28.34 (eqangle O C C (skS.0 4 a) O C C B)) % 28.11/28.34 (perp I C (skS.0 4 a) O)) % 28.11/28.34 (coll I (skS.0 4 a) O)) % 28.11/28.34 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.34 (perp J C (skS.0 4 a) E)) % 28.11/28.34 (coll J (skS.0 4 a) E)) % 28.11/28.34 (perp L C B O)) % 28.11/28.34 (coll L B O) → % 28.11/28.34 coll I L J) % 28.11/28.34 False % 28.11/28.34 Clause #461 (by clausification #[460]): ∀ (a a_1 : Iota), % 28.11/28.34 Eq % 28.11/28.34 (Not % 28.11/28.34 (∀ (C O I E J L : Iota), % 28.11/28.34 And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And (eqangle O (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) O (skS.0 4 a) (skS.0 4 a) C) % 28.11/28.34 (eqangle O (skS.0 5 a a_1) (skS.0 5 a a_1) C O (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.11/28.34 (eqangle O C C (skS.0 4 a) O C C (skS.0 5 a a_1))) % 28.11/28.34 (perp I C (skS.0 4 a) O)) % 28.11/28.34 (coll I (skS.0 4 a) O)) % 28.11/28.34 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.34 (perp J C (skS.0 4 a) E)) % 28.11/28.34 (coll J (skS.0 4 a) E)) % 28.11/28.34 (perp L C (skS.0 5 a a_1) O)) % 28.11/28.34 (coll L (skS.0 5 a a_1) O) → % 28.11/28.34 coll I L J)) % 28.11/28.34 True % 28.11/28.34 Clause #462 (by clausification #[461]): ∀ (a a_1 : Iota), % 28.11/28.34 Eq % 28.11/28.34 (∀ (C O I E J L : Iota), % 28.11/28.34 And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And (eqangle O (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) O (skS.0 4 a) (skS.0 4 a) C) % 28.11/28.34 (eqangle O (skS.0 5 a a_1) (skS.0 5 a a_1) C O (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.11/28.34 (eqangle O C C (skS.0 4 a) O C C (skS.0 5 a a_1))) % 28.11/28.34 (perp I C (skS.0 4 a) O)) % 28.11/28.34 (coll I (skS.0 4 a) O)) % 28.11/28.34 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.34 (perp J C (skS.0 4 a) E)) % 28.11/28.34 (coll J (skS.0 4 a) E)) % 28.11/28.34 (perp L C (skS.0 5 a a_1) O)) % 28.11/28.34 (coll L (skS.0 5 a a_1) O) → % 28.11/28.34 coll I L J) % 28.11/28.34 False % 28.11/28.34 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota), % 28.11/28.34 Eq % 28.11/28.34 (Not % 28.11/28.34 (∀ (O I E J L : Iota), % 28.11/28.34 And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.34 (And % 28.11/28.38 (eqangle O (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) O (skS.0 4 a) (skS.0 4 a) % 28.11/28.38 (skS.0 6 a a_1 a_2)) % 28.11/28.38 (eqangle O (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) O (skS.0 5 a a_1) % 28.11/28.38 (skS.0 5 a a_1) (skS.0 4 a))) % 28.11/28.38 (eqangle O (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) O (skS.0 6 a a_1 a_2) % 28.11/28.38 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.11/28.38 (perp I (skS.0 6 a a_1 a_2) (skS.0 4 a) O)) % 28.11/28.38 (coll I (skS.0 4 a) O)) % 28.11/28.38 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.38 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.11/28.38 (coll J (skS.0 4 a) E)) % 28.11/28.38 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) O)) % 28.11/28.38 (coll L (skS.0 5 a a_1) O) → % 28.11/28.38 coll I L J)) % 28.11/28.38 True % 28.11/28.38 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 : Iota), % 28.11/28.38 Eq % 28.11/28.38 (∀ (O I E J L : Iota), % 28.11/28.38 And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (eqangle O (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) O (skS.0 4 a) (skS.0 4 a) % 28.11/28.38 (skS.0 6 a a_1 a_2)) % 28.11/28.38 (eqangle O (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) O (skS.0 5 a a_1) % 28.11/28.38 (skS.0 5 a a_1) (skS.0 4 a))) % 28.11/28.38 (eqangle O (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) O (skS.0 6 a a_1 a_2) % 28.11/28.38 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.11/28.38 (perp I (skS.0 6 a a_1 a_2) (skS.0 4 a) O)) % 28.11/28.38 (coll I (skS.0 4 a) O)) % 28.11/28.38 (perp (skS.0 4 a) O (skS.0 4 a) E)) % 28.11/28.38 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.11/28.38 (coll J (skS.0 4 a) E)) % 28.11/28.38 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) O)) % 28.11/28.38 (coll L (skS.0 5 a a_1) O) → % 28.11/28.38 coll I L J) % 28.11/28.38 False % 28.11/28.38 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota), % 28.11/28.38 Eq % 28.11/28.38 (Not % 28.11/28.38 (∀ (I E J L : Iota), % 28.11/28.38 And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.11/28.38 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.11/28.38 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.11/28.38 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.11/28.38 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.11/28.38 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.11/28.38 (perp I (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.11/28.38 (coll I (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.11/28.38 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) E)) % 28.11/28.38 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.11/28.38 (coll J (skS.0 4 a) E)) % 28.11/28.38 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.11/28.38 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.11/28.38 coll I L J)) % 28.11/28.38 True % 28.11/28.38 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota), % 28.11/28.38 Eq % 28.11/28.38 (∀ (I E J L : Iota), % 28.11/28.38 And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (And % 28.11/28.38 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.11/28.38 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.11/28.38 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.43 (perp I (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll I (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) E)) % 28.21/28.43 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.21/28.43 (coll J (skS.0 4 a) E)) % 28.21/28.43 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.21/28.43 coll I L J) % 28.21/28.43 False % 28.21/28.43 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 28.21/28.43 Eq % 28.21/28.43 (Not % 28.21/28.43 (∀ (E J L : Iota), % 28.21/28.43 And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.43 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) E)) % 28.21/28.43 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.21/28.43 (coll J (skS.0 4 a) E)) % 28.21/28.43 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.21/28.43 coll (skS.0 8 a a_1 a_2 a_3 a_4) L J)) % 28.21/28.43 True % 28.21/28.43 Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 28.21/28.43 Eq % 28.21/28.43 (∀ (E J L : Iota), % 28.21/28.43 And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.43 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.43 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.43 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) E)) % 28.21/28.43 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) E)) % 28.21/28.43 (coll J (skS.0 4 a) E)) % 28.21/28.43 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.43 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.21/28.43 coll (skS.0 8 a a_1 a_2 a_3 a_4) L J) % 28.21/28.43 False % 28.21/28.43 Clause #469 (by clausification #[468]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.21/28.43 Eq % 28.21/28.43 (Not % 28.21/28.43 (∀ (J L : Iota), % 28.21/28.43 And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.43 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.47 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (coll J (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.21/28.47 coll (skS.0 8 a a_1 a_2 a_3 a_4) L J)) % 28.21/28.47 True % 28.21/28.47 Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.21/28.47 Eq % 28.21/28.47 (∀ (J L : Iota), % 28.21/28.47 And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.47 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (perp J (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (coll J (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.21/28.47 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.21/28.47 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.21/28.47 coll (skS.0 8 a a_1 a_2 a_3 a_4) L J) % 28.21/28.47 False % 28.21/28.47 Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 28.21/28.47 Eq % 28.21/28.47 (Not % 28.21/28.47 (∀ (L : Iota), % 28.21/28.47 And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (And % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.21/28.47 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.21/28.47 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.21/28.47 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.51 (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.31/28.51 coll (skS.0 8 a a_1 a_2 a_3 a_4) L (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6))) % 28.31/28.51 True % 28.31/28.51 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 28.31/28.51 Eq % 28.31/28.51 (∀ (L : Iota), % 28.31/28.51 And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.31/28.51 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.51 (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp L (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll L (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.31/28.51 coll (skS.0 8 a a_1 a_2 a_3 a_4) L (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)) % 28.31/28.51 False % 28.31/28.51 Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.51 Eq % 28.31/28.51 (Not % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (And % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.31/28.51 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.51 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.31/28.51 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.51 (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.51 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.51 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.31/28.57 coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6))) % 28.31/28.57 True % 28.31/28.57 Clause #474 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.57 Eq % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) % 28.31/28.57 (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.31/28.57 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.57 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.31/28.57 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.57 (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) → % 28.31/28.57 coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)) % 28.31/28.57 False % 28.31/28.57 Clause #475 (by clausification #[474]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.57 Eq % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) % 28.31/28.57 (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.31/28.57 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.57 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.31/28.57 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.57 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.57 True % 28.31/28.57 Clause #476 (by clausification #[474]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.57 Eq (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)) % 28.31/28.57 False % 28.31/28.57 Clause #478 (by clausification #[475]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.57 Eq % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (And % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) % 28.31/28.57 (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) % 28.31/28.57 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) % 28.31/28.61 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a))) % 28.31/28.61 (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a) % 28.31/28.61 (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 28.31/28.61 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.61 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.61 (perp (skS.0 4 a) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.61 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.61 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 28.31/28.61 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3))) % 28.31/28.61 True % 28.31/28.61 Clause #503 (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 % 28.31/28.61 Clause #504 (by clausification #[503]): ∀ (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 % 28.31/28.61 Clause #505 (by clausification #[504]): ∀ (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 % 28.31/28.61 Clause #506 (by clausification #[505]): ∀ (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 % 28.31/28.61 Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 28.31/28.61 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 % 28.31/28.61 Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.31/28.61 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 % 28.31/28.61 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 28.31/28.61 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 % 28.31/28.61 Clause #510 (by clausification #[509]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.61 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 % 28.31/28.61 Clause #511 (by clausification #[510]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.61 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) % 28.31/28.61 Clause #639 (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 % 28.31/28.61 Clause #640 (by clausification #[639]): ∀ (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 % 28.31/28.61 Clause #641 (by clausification #[640]): ∀ (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 % 28.31/28.61 Clause #642 (by clausification #[641]): ∀ (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 % 28.31/28.61 Clause #643 (by clausification #[642]): ∀ (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 % 28.31/28.61 Clause #644 (by clausification #[643]): ∀ (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 % 28.31/28.61 Clause #645 (by clausification #[644]): ∀ (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) % 28.31/28.61 Clause #876 (by clausification #[478]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.61 Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) True % 28.31/28.61 Clause #879 (by superposition #[876, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.61 Or (Eq True False) % 28.31/28.61 (Eq (perp (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2)) % 28.31/28.61 True) % 28.31/28.61 Clause #914 (by clausification #[879]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.31/28.61 Eq (perp (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1 a_2)) True % 28.42/28.66 Clause #915 (by superposition #[914, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (perp (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 28.42/28.66 True) % 28.42/28.66 Clause #955 (by clausification #[915]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Eq (perp (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 28.42/28.66 Clause #956 (by superposition #[955, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) % 28.42/28.66 True) % 28.42/28.66 Clause #957 (by superposition #[955, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 28.42/28.66 Or (Eq (para (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) a_4 a_5) True) % 28.42/28.66 (Or (Eq True False) (Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_6 a_7 a_8 a_9) a_4 a_5) False)) % 28.42/28.66 Clause #964 (by clausification #[956]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) True % 28.42/28.66 Clause #965 (by superposition #[964, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) % 28.42/28.66 True) % 28.42/28.66 Clause #972 (by clausification #[965]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 28.42/28.66 Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) True % 28.42/28.66 Clause #1830 (by clausification #[957]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 28.42/28.66 Or (Eq (para (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) a_4 a_5) True) % 28.42/28.66 (Eq (perp (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_6 a_7 a_8 a_9) a_4 a_5) False) % 28.42/28.66 Clause #1832 (by superposition #[1830, 972]): ∀ (a a_1 a_2 a_3 : Iota), % 28.42/28.66 Or (Eq (para (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) True) (Eq False True) % 28.42/28.66 Clause #1833 (by clausification #[1832]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) True % 28.42/28.66 Clause #1837 (by superposition #[1833, 189]): ∀ (a a_1 a_2 a_3 : Iota), % 28.42/28.66 Or (Eq True False) (Eq (para (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) True) % 28.42/28.66 Clause #1841 (by clausification #[1837]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3)) True % 28.42/28.66 Clause #1844 (by superposition #[1841, 156]): ∀ (a a_1 a_2 a_3 : Iota), % 28.42/28.66 Or (Eq True False) (Eq (para (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) True) % 28.42/28.66 Clause #1850 (by clausification #[1844]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1)) True % 28.42/28.66 Clause #1854 (by superposition #[1850, 645]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5) True) % 28.42/28.66 Clause #1860 (by clausification #[1854]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.42/28.66 Eq (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5 (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5) True % 28.42/28.66 Clause #1867 (by superposition #[1860, 511]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5 a_4 a_5) True) % 28.42/28.66 Clause #1873 (by clausification #[1867]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.42/28.66 Eq (eqangle (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) a_4 a_5 a_4 a_5) True % 28.42/28.66 Clause #1879 (by superposition #[1873, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.42/28.66 Or (Eq True False) % 28.42/28.66 (Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) % 28.42/28.66 True) % 28.52/28.72 Clause #1885 (by clausification #[1879]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.52/28.72 Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) True % 28.52/28.72 Clause #1889 (by superposition #[1885, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.52/28.72 Or (Eq True False) % 28.52/28.72 (Eq (eqangle a a_1 a_1 a (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) % 28.52/28.72 True) % 28.52/28.72 Clause #1896 (by clausification #[1889]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.52/28.72 Eq (eqangle a a_1 a_1 a (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) True % 28.52/28.72 Clause #1903 (by superposition #[1896, 511]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.52/28.72 Or (Eq True False) % 28.52/28.72 (Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) a_1 a (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) % 28.52/28.72 True) % 28.52/28.72 Clause #1908 (by clausification #[1903]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 28.52/28.72 Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3) a_1 a (skS.0 7 a_2 a_3 a_4 a_5) (skS.0 5 a_2 a_3)) True % 28.52/28.72 Clause #1912 (by superposition #[1908, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 28.52/28.72 Clause #1921 (by clausification #[1912]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 28.52/28.72 Clause #1931 (by superposition #[1921, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 28.52/28.72 Clause #1956 (by clausification #[1931]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 28.52/28.72 Clause #1957 (by superposition #[1956, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 28.52/28.72 Clause #1962 (by clausification #[1957]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 28.52/28.72 Clause #1975 (by superposition #[1962, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 28.52/28.72 Clause #1984 (by clausification #[1975]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 28.52/28.72 Clause #2001 (by superposition #[1984, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 28.52/28.72 Clause #2010 (by clausification #[2001]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 28.52/28.72 Clause #2024 (by superposition #[2010, 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)) % 28.52/28.72 Clause #2146 (by clausification #[2024]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 28.52/28.72 Clause #2153 (by superposition #[2146, 2010]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 28.52/28.72 Clause #2154 (by clausification #[2153]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 28.52/28.72 Clause #2197 (by superposition #[2154, 476]): Eq True False % 28.52/28.72 Clause #2203 (by clausification #[2197]): False % 28.52/28.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------