%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO551+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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 13.97s 14.14s % Output : Proof 14.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GEO551+1 : TPTP v9.2.0. Released v7.5.0. % 0.06/0.13 % Command : duper %s % 0.14/0.34 % Computer : n007.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 11:36:08 EDT 2025 % 0.14/0.34 % CPUTime : % 13.97/14.14 SZS status Theorem for theBenchmark.p % 13.97/14.14 SZS output start Proof for theBenchmark.p % 13.97/14.14 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 13.97/14.14 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 13.97/14.14 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 13.97/14.14 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 13.97/14.14 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 13.97/14.14 Clause #10 (by assumption #[]): Eq (∀ (A B M : Iota), midp M B A → midp M A B) True % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 13.97/14.14 Clause #94 (by assumption #[]): Eq % 13.97/14.14 (Not % 13.97/14.14 (∀ (A B C D L M N : Iota), % 13.97/14.14 And (And (And (And (perp D A B C) (coll D B C)) (midp L A B)) (midp M C B)) (midp N A C) → cyclic L D M N)) % 13.97/14.14 True % 13.97/14.14 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 13.97/14.14 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 13.97/14.14 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 % 13.97/14.14 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) % 13.97/14.14 Clause #108 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (B M : Iota), midp M B a → midp M a B) True % 13.97/14.14 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (∀ (M : Iota), midp M a a_1 → midp M a_1 a) True % 13.97/14.14 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 % 13.97/14.14 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) % 13.97/14.14 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 13.97/14.14 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 13.97/14.14 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 % 13.97/14.14 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) % 13.97/14.14 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 13.97/14.14 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 13.97/14.14 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 % 13.97/14.14 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) % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.14 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 % 13.97/14.17 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 % 13.97/14.17 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) % 13.97/14.17 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)) % 13.97/14.17 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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) % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 13.97/14.17 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) % 13.97/14.17 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 13.97/14.17 Or (Eq (cyclic a a_1 a_2 a_3) True) % 13.97/14.17 (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)) % 13.97/14.17 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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) % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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) % 13.97/14.17 Clause #283 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.97/14.17 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)) % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.17 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.97/14.19 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) % 13.97/14.19 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.97/14.19 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)) % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.97/14.19 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 % 13.97/14.19 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 13.97/14.19 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 % 13.97/14.19 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 13.97/14.19 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 % 13.97/14.19 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.97/14.19 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 % 13.97/14.19 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 13.97/14.19 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) % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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) % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 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 % 13.97/14.19 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 13.97/14.19 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 % 14.06/14.22 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.06/14.22 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 % 14.06/14.22 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.22 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 % 14.06/14.22 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.06/14.22 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 % 14.06/14.22 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.06/14.22 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) % 14.06/14.22 Clause #458 (by clausification #[94]): Eq % 14.06/14.22 (∀ (A B C D L M N : Iota), % 14.06/14.22 And (And (And (And (perp D A B C) (coll D B C)) (midp L A B)) (midp M C B)) (midp N A C) → cyclic L D M N) % 14.06/14.22 False % 14.06/14.22 Clause #459 (by clausification #[458]): ∀ (a : Iota), % 14.06/14.22 Eq % 14.06/14.22 (Not % 14.06/14.22 (∀ (B C D L M N : Iota), % 14.06/14.22 And (And (And (And (perp D (skS.0 4 a) B C) (coll D B C)) (midp L (skS.0 4 a) B)) (midp M C B)) % 14.06/14.22 (midp N (skS.0 4 a) C) → % 14.06/14.22 cyclic L D M N)) % 14.06/14.22 True % 14.06/14.22 Clause #460 (by clausification #[459]): ∀ (a : Iota), % 14.06/14.22 Eq % 14.06/14.22 (∀ (B C D L M N : Iota), % 14.06/14.22 And (And (And (And (perp D (skS.0 4 a) B C) (coll D B C)) (midp L (skS.0 4 a) B)) (midp M C B)) % 14.06/14.22 (midp N (skS.0 4 a) C) → % 14.06/14.22 cyclic L D M N) % 14.06/14.22 False % 14.06/14.22 Clause #461 (by clausification #[460]): ∀ (a a_1 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (Not % 14.06/14.22 (∀ (C D L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And (And (perp D (skS.0 4 a) (skS.0 5 a a_1) C) (coll D (skS.0 5 a a_1) C)) % 14.06/14.22 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.22 (midp M C (skS.0 5 a a_1))) % 14.06/14.22 (midp N (skS.0 4 a) C) → % 14.06/14.22 cyclic L D M N)) % 14.06/14.22 True % 14.06/14.22 Clause #462 (by clausification #[461]): ∀ (a a_1 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (∀ (C D L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And (And (perp D (skS.0 4 a) (skS.0 5 a a_1) C) (coll D (skS.0 5 a a_1) C)) % 14.06/14.22 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.22 (midp M C (skS.0 5 a a_1))) % 14.06/14.22 (midp N (skS.0 4 a) C) → % 14.06/14.22 cyclic L D M N) % 14.06/14.22 False % 14.06/14.22 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (Not % 14.06/14.22 (∀ (D L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And % 14.06/14.22 (And (perp D (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.22 (coll D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.22 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.22 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.22 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.22 cyclic L D M N)) % 14.06/14.22 True % 14.06/14.22 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (∀ (D L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And % 14.06/14.22 (And (perp D (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.22 (coll D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.22 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.22 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.22 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.22 cyclic L D M N) % 14.06/14.22 False % 14.06/14.22 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (Not % 14.06/14.22 (∀ (L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And % 14.06/14.22 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.22 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.22 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.22 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.22 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.22 cyclic L (skS.0 7 a a_1 a_2 a_3) M N)) % 14.06/14.22 True % 14.06/14.22 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota), % 14.06/14.22 Eq % 14.06/14.22 (∀ (L M N : Iota), % 14.06/14.22 And % 14.06/14.22 (And % 14.06/14.22 (And % 14.06/14.22 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.22 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp L (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic L (skS.0 7 a a_1 a_2 a_3) M N) % 14.06/14.24 False % 14.06/14.24 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (Not % 14.06/14.24 (∀ (M N : Iota), % 14.06/14.24 And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) M N)) % 14.06/14.24 True % 14.06/14.24 Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (∀ (M N : Iota), % 14.06/14.24 And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp M (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) M N) % 14.06/14.24 False % 14.06/14.24 Clause #469 (by clausification #[468]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (Not % 14.06/14.24 (∀ (N : Iota), % 14.06/14.24 And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) N)) % 14.06/14.24 True % 14.06/14.24 Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (∀ (N : Iota), % 14.06/14.24 And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp N (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) N) % 14.06/14.24 False % 14.06/14.24 Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (Not % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.24 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) % 14.06/14.24 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6))) % 14.06/14.24 True % 14.06/14.24 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.24 Eq % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And % 14.06/14.24 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.24 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.24 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.24 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 14.06/14.27 cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) % 14.06/14.27 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)) % 14.06/14.27 False % 14.06/14.27 Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.27 Eq % 14.06/14.27 (And % 14.06/14.27 (And % 14.06/14.27 (And % 14.06/14.27 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 14.06/14.27 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 14.06/14.27 (midp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 14.06/14.27 (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 14.06/14.27 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 14.06/14.27 True % 14.06/14.27 Clause #474 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.27 Eq % 14.06/14.27 (cyclic (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3) (skS.0 9 a a_1 a_2 a_3 a_4 a_5) % 14.06/14.27 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6)) % 14.06/14.27 False % 14.06/14.27 Clause #475 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.27 Eq (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True % 14.06/14.27 Clause #478 (by superposition #[475, 111]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.27 Or (Eq True False) (Eq (midp (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)) True) % 14.06/14.27 Clause #481 (by superposition #[475, 283]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.06/14.27 Or (Eq (para (skS.0 4 a) a_1 (skS.0 6 a a_2 a_3) a_4) True) % 14.06/14.27 (Or (Eq True False) (Eq (midp (skS.0 10 a a_2 a_3 a_5 a_6 a_7 a_8) a_1 a_4) False)) % 14.06/14.27 Clause #505 (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 % 14.06/14.27 Clause #506 (by clausification #[505]): ∀ (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 % 14.06/14.27 Clause #507 (by clausification #[506]): ∀ (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 % 14.06/14.27 Clause #508 (by clausification #[507]): ∀ (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 % 14.06/14.27 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.06/14.27 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 % 14.06/14.27 Clause #510 (by clausification #[509]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.06/14.27 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 % 14.06/14.27 Clause #511 (by clausification #[510]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.06/14.27 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 % 14.06/14.27 Clause #512 (by clausification #[511]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.06/14.27 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 % 14.06/14.27 Clause #513 (by clausification #[512]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.06/14.27 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) % 14.06/14.27 Clause #640 (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 % 14.06/14.27 Clause #641 (by clausification #[640]): ∀ (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 % 14.06/14.27 Clause #642 (by clausification #[641]): ∀ (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 % 14.06/14.27 Clause #643 (by clausification #[642]): ∀ (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 % 14.06/14.27 Clause #644 (by clausification #[643]): ∀ (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 % 14.06/14.27 Clause #645 (by clausification #[644]): ∀ (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 % 14.06/14.27 Clause #646 (by clausification #[645]): ∀ (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) % 14.06/14.27 Clause #849 (by clausification #[478]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.14/14.30 Eq (midp (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)) True % 14.14/14.30 Clause #1055 (by clausification #[481]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.14/14.30 Or (Eq (para (skS.0 4 a) a_1 (skS.0 6 a a_2 a_3) a_4) True) % 14.14/14.30 (Eq (midp (skS.0 10 a a_2 a_3 a_5 a_6 a_7 a_8) a_1 a_4) False) % 14.14/14.30 Clause #1057 (by superposition #[1055, 849]): ∀ (a a_1 a_2 : Iota), % 14.14/14.30 Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) (Eq False True) % 14.14/14.30 Clause #1058 (by clausification #[1057]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 14.14/14.30 Clause #1061 (by superposition #[1058, 189]): ∀ (a a_1 a_2 : Iota), % 14.14/14.30 Or (Eq True False) (Eq (para (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True) % 14.14/14.30 Clause #1065 (by clausification #[1061]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True % 14.14/14.30 Clause #1067 (by superposition #[1065, 156]): ∀ (a a_1 a_2 : Iota), % 14.14/14.30 Or (Eq True False) (Eq (para (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) % 14.14/14.30 Clause #1072 (by clausification #[1067]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 14.14/14.30 Clause #1077 (by superposition #[1072, 646]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Or (Eq True False) (Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4) True) % 14.14/14.30 Clause #1418 (by clausification #[1077]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4) True % 14.14/14.30 Clause #1425 (by superposition #[1418, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Or (Eq True False) (Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_3 a_4) True) % 14.14/14.30 Clause #1430 (by clausification #[1425]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) a_3 a_4 a_3 a_4) True % 14.14/14.30 Clause #1436 (by superposition #[1430, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Or (Eq True False) % 14.14/14.30 (Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True) % 14.14/14.30 Clause #1448 (by clausification #[1436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True % 14.14/14.30 Clause #1452 (by superposition #[1448, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Or (Eq True False) % 14.14/14.30 (Eq (eqangle a a_1 a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True) % 14.14/14.30 Clause #1459 (by clausification #[1452]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Eq (eqangle a a_1 a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True % 14.14/14.30 Clause #1466 (by superposition #[1459, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Or (Eq True False) % 14.14/14.30 (Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True) % 14.14/14.30 Clause #1471 (by clausification #[1466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.14/14.30 Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2)) True % 14.14/14.30 Clause #1475 (by superposition #[1471, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 14.14/14.30 Clause #1484 (by clausification #[1475]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 14.14/14.30 Clause #1487 (by superposition #[1484, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 14.14/14.30 Clause #1490 (by superposition #[1484, 646]): ∀ (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) % 14.14/14.30 Clause #1516 (by clausification #[1487]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 14.14/14.30 Clause #1517 (by superposition #[1516, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 14.14/14.30 Clause #1522 (by clausification #[1517]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 14.14/14.30 Clause #1524 (by superposition #[1522, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 14.14/14.30 Clause #1533 (by clausification #[1524]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 14.14/14.32 Clause #1535 (by superposition #[1533, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 14.14/14.32 Clause #1544 (by clausification #[1535]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 14.14/14.32 Clause #1546 (by superposition #[1544, 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)) % 14.14/14.32 Clause #1556 (by clausification #[1490]): ∀ (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 % 14.14/14.32 Clause #1564 (by superposition #[1556, 513]): ∀ (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) % 14.14/14.32 Clause #1569 (by clausification #[1564]): ∀ (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 % 14.14/14.32 Clause #1573 (by superposition #[1569, 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) % 14.14/14.32 Clause #1616 (by clausification #[1573]): ∀ (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 % 14.14/14.32 Clause #1617 (by superposition #[1616, 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)) % 14.14/14.32 Clause #1639 (by clausification #[1546]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 14.14/14.32 Clause #1642 (by superposition #[1639, 1544]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 14.14/14.32 Clause #1643 (by clausification #[1642]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 14.14/14.32 Clause #1718 (by clausification #[1617]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (coll a_1 a_2 a) False) % 14.14/14.32 Clause #1719 (by forward demodulation #[1718, 1643]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq True False) % 14.14/14.32 Clause #1720 (by clausification #[1719]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 14.14/14.32 Clause #1724 (by superposition #[1720, 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 a a_1 a_3) False)) % 14.14/14.32 Clause #2162 (by clausification #[1724]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq (cyclic a a a_1 a_3) False) % 14.14/14.32 Clause #2163 (by superposition #[2162, 1720]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 14.14/14.32 Clause #2164 (by clausification #[2163]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 14.14/14.32 Clause #2173 (by superposition #[2164, 474]): Eq True False % 14.14/14.32 Clause #2175 (by clausification #[2173]): False % 14.14/14.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------