%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO587+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.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:43 PM UTC 2025 % Result : Theorem 46.46s 46.63s % Output : Proof 46.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO587+1 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 12:32:53 EDT 2025 % 0.13/0.34 % CPUTime : % 46.46/46.63 SZS status Theorem for theBenchmark.p % 46.46/46.63 SZS output start Proof for theBenchmark.p % 46.46/46.63 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 46.46/46.63 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 46.46/46.63 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 46.46/46.63 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 46.46/46.63 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 46.46/46.63 Clause #10 (by assumption #[]): Eq (∀ (A B M : Iota), midp M B A → midp M A B) True % 46.46/46.63 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 % 46.46/46.63 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 % 46.46/46.63 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 % 46.46/46.63 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 % 46.46/46.63 Clause #25 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio B A C D P Q U V) True % 46.46/46.63 Clause #26 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio C D A B U V P Q) True % 46.46/46.63 Clause #27 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio P Q U V A B C D) True % 46.46/46.63 Clause #28 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqratio A B C D P Q U V → eqratio A B P Q C D U V) True % 46.46/46.63 Clause #29 (by assumption #[]): Eq % 46.46/46.63 (∀ (A B C D E F G H P Q U V : Iota), % 46.46/46.63 And (eqratio A B C D P Q U V) (eqratio P Q U V E F G H) → eqratio A B C D E F G H) % 46.46/46.63 True % 46.46/46.63 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 % 46.46/46.63 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 % 46.46/46.63 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 % 46.46/46.63 Clause #43 (by assumption #[]): Eq % 46.46/46.63 (∀ (A B C P Q R : Iota), % 46.46/46.63 And (And (And (cyclic A B C P) (cyclic A B C Q)) (cyclic A B C R)) (eqangle C A C B R P R Q) → cong A B P Q) % 46.46/46.63 True % 46.46/46.63 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 % 46.46/46.63 Clause #65 (by assumption #[]): Eq (∀ (A B C D O : Iota), And (And (para A B C D) (coll O A C)) (coll O B D) → eqratio O A A C O B B D) True % 46.46/46.63 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 46.46/46.63 Clause #75 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), And (eqratio A B C D P Q U V) (cong P Q U V) → cong A B C D) True % 46.46/46.63 Clause #94 (by assumption #[]): Eq % 46.46/46.63 (Not % 46.46/46.63 (∀ (A C B D P Q R S O : Iota), % 46.46/46.63 And (And (And (And (And (And (perp A C B D) (midp P B A)) (midp Q C B)) (midp R D C)) (midp S A D)) (coll O P R)) % 46.46/46.63 (coll O Q S) → % 46.46/46.63 cong O S O R)) % 46.46/46.63 True % 46.46/46.63 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 46.46/46.63 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 46.46/46.63 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 % 46.46/46.63 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) % 46.46/46.63 Clause #108 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (B M : Iota), midp M B a → midp M a B) True % 46.46/46.63 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (∀ (M : Iota), midp M a a_1 → midp M a_1 a) True % 46.46/46.63 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 % 46.46/46.63 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) % 46.46/46.63 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 46.46/46.63 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 46.46/46.65 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 % 46.46/46.65 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) % 46.46/46.65 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 46.46/46.65 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 46.46/46.65 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 % 46.46/46.65 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) % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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) % 46.46/46.65 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)) % 46.46/46.65 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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) % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 46.46/46.65 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) % 46.46/46.65 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 46.46/46.65 Or (Eq (cyclic a a_1 a_2 a_3) True) % 46.46/46.65 (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)) % 46.46/46.65 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.65 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) % 46.46/46.65 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 % 46.46/46.65 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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) % 46.46/46.68 Clause #283 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.68 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)) % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.68 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) % 46.46/46.68 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.68 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)) % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.68 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 % 46.46/46.68 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.68 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 % 46.46/46.68 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.46/46.68 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 % 46.46/46.68 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.46/46.68 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 % 46.46/46.68 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.46/46.68 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) % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.68 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 % 46.46/46.70 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 % 46.46/46.70 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) % 46.46/46.70 Clause #360 (by clausification #[43]): ∀ (a : Iota), % 46.46/46.70 Eq % 46.46/46.70 (∀ (B C P Q R : Iota), % 46.46/46.70 And (And (And (cyclic a B C P) (cyclic a B C Q)) (cyclic a B C R)) (eqangle C a C B R P R Q) → cong a B P Q) % 46.46/46.70 True % 46.46/46.70 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 46.46/46.70 Eq % 46.46/46.70 (∀ (C P Q R : Iota), % 46.46/46.70 And (And (And (cyclic a a_1 C P) (cyclic a a_1 C Q)) (cyclic a a_1 C R)) (eqangle C a C a_1 R P R Q) → % 46.46/46.70 cong a a_1 P Q) % 46.46/46.70 True % 46.46/46.70 Clause #362 (by clausification #[361]): ∀ (a a_1 a_2 : Iota), % 46.46/46.70 Eq % 46.46/46.70 (∀ (P Q R : Iota), % 46.46/46.70 And (And (And (cyclic a a_1 a_2 P) (cyclic a a_1 a_2 Q)) (cyclic a a_1 a_2 R)) (eqangle a_2 a a_2 a_1 R P R Q) → % 46.46/46.70 cong a a_1 P Q) % 46.46/46.70 True % 46.46/46.70 Clause #363 (by clausification #[362]): ∀ (a a_1 a_2 a_3 : Iota), % 46.46/46.70 Eq % 46.46/46.70 (∀ (Q R : Iota), % 46.46/46.70 And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 Q)) (cyclic a a_1 a_2 R)) % 46.46/46.70 (eqangle a_2 a a_2 a_1 R a_3 R Q) → % 46.46/46.70 cong a a_1 a_3 Q) % 46.46/46.70 True % 46.46/46.70 Clause #364 (by clausification #[363]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.70 Eq % 46.46/46.70 (∀ (R : Iota), % 46.46/46.70 And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 R)) % 46.46/46.70 (eqangle a_2 a a_2 a_1 R a_3 R a_4) → % 46.46/46.70 cong a a_1 a_3 a_4) % 46.46/46.70 True % 46.46/46.70 Clause #365 (by clausification #[364]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 Eq % 46.46/46.70 (And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 a_5)) % 46.46/46.70 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4) → % 46.46/46.70 cong a a_1 a_3 a_4) % 46.46/46.70 True % 46.46/46.70 Clause #366 (by clausification #[365]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 Or % 46.46/46.70 (Eq % 46.46/46.70 (And (And (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) (cyclic a a_1 a_2 a_5)) % 46.46/46.70 (eqangle a_2 a a_2 a_1 a_5 a_3 a_5 a_4)) % 46.46/46.70 False) % 46.46/46.70 (Eq (cong a a_1 a_3 a_4) True) % 46.46/46.70 Clause #367 (by clausification #[366]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 Or (Eq (cong a a_1 a_2 a_3) True) % 46.46/46.70 (Or (Eq (And (And (cyclic a a_1 a_4 a_2) (cyclic a a_1 a_4 a_3)) (cyclic a a_1 a_4 a_5)) False) % 46.46/46.70 (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False)) % 46.46/46.70 Clause #368 (by clausification #[367]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 Or (Eq (cong a a_1 a_2 a_3) True) % 46.46/46.70 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 46.46/46.70 (Or (Eq (And (cyclic a a_1 a_4 a_2) (cyclic a a_1 a_4 a_3)) False) (Eq (cyclic a a_1 a_4 a_5) False))) % 46.46/46.70 Clause #369 (by clausification #[368]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 Or (Eq (cong a a_1 a_2 a_3) True) % 46.46/46.70 (Or (Eq (eqangle a_4 a a_4 a_1 a_5 a_2 a_5 a_3) False) % 46.46/46.70 (Or (Eq (cyclic a a_1 a_4 a_5) False) (Or (Eq (cyclic a a_1 a_4 a_2) False) (Eq (cyclic a a_1 a_4 a_3) False)))) % 46.46/46.70 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 % 46.46/46.70 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 % 46.46/46.70 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 % 46.46/46.70 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 % 46.46/46.70 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.46/46.70 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 % 46.46/46.70 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.46/46.70 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 % 46.46/46.70 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 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) % 46.56/46.73 Clause #458 (by clausification #[75]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), And (eqratio a B C D P Q U V) (cong P Q U V) → cong a B C D) True % 46.56/46.73 Clause #459 (by clausification #[458]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), And (eqratio a a_1 C D P Q U V) (cong P Q U V) → cong a a_1 C D) True % 46.56/46.73 Clause #460 (by clausification #[459]): ∀ (a a_1 a_2 : Iota), % 46.56/46.73 Eq (∀ (D P Q U V : Iota), And (eqratio a a_1 a_2 D P Q U V) (cong P Q U V) → cong a a_1 a_2 D) True % 46.56/46.73 Clause #461 (by clausification #[460]): ∀ (a a_1 a_2 a_3 : Iota), % 46.56/46.73 Eq (∀ (P Q U V : Iota), And (eqratio a a_1 a_2 a_3 P Q U V) (cong P Q U V) → cong a a_1 a_2 a_3) True % 46.56/46.73 Clause #462 (by clausification #[461]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.73 Eq (∀ (Q U V : Iota), And (eqratio a a_1 a_2 a_3 a_4 Q U V) (cong a_4 Q U V) → cong a a_1 a_2 a_3) True % 46.56/46.73 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.56/46.73 Eq (∀ (U V : Iota), And (eqratio a a_1 a_2 a_3 a_4 a_5 U V) (cong a_4 a_5 U V) → cong a a_1 a_2 a_3) True % 46.56/46.73 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.73 Eq (∀ (V : Iota), And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V) (cong a_4 a_5 a_6 V) → cong a a_1 a_2 a_3) True % 46.56/46.73 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (cong a_4 a_5 a_6 a_7) → cong a a_1 a_2 a_3) True % 46.56/46.73 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 Or (Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (cong a_4 a_5 a_6 a_7)) False) (Eq (cong a a_1 a_2 a_3) True) % 46.56/46.73 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 Or (Eq (cong a a_1 a_2 a_3) True) % 46.56/46.73 (Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (cong a_4 a_5 a_6 a_7) False)) % 46.56/46.73 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 % 46.56/46.73 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 % 46.56/46.73 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 % 46.56/46.73 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 % 46.56/46.73 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 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 % 46.56/46.73 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.73 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) % 46.56/46.73 Clause #547 (by clausification #[65]): ∀ (a : Iota), Eq (∀ (B C D O : Iota), And (And (para a B C D) (coll O a C)) (coll O B D) → eqratio O a a C O B B D) True % 46.56/46.73 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), % 46.56/46.73 Eq (∀ (C D O : Iota), And (And (para a a_1 C D) (coll O a C)) (coll O a_1 D) → eqratio O a a C O a_1 a_1 D) True % 46.56/46.76 Clause #549 (by clausification #[548]): ∀ (a a_1 a_2 : Iota), % 46.56/46.76 Eq (∀ (D O : Iota), And (And (para a a_1 a_2 D) (coll O a a_2)) (coll O a_1 D) → eqratio O a a a_2 O a_1 a_1 D) True % 46.56/46.76 Clause #550 (by clausification #[549]): ∀ (a a_1 a_2 a_3 : Iota), % 46.56/46.76 Eq (∀ (O : Iota), And (And (para a a_1 a_2 a_3) (coll O a a_2)) (coll O a_1 a_3) → eqratio O a a a_2 O a_1 a_1 a_3) % 46.56/46.76 True % 46.56/46.76 Clause #551 (by clausification #[550]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.76 Eq (And (And (para a a_1 a_2 a_3) (coll a_4 a a_2)) (coll a_4 a_1 a_3) → eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True % 46.56/46.76 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.76 Or (Eq (And (And (para a a_1 a_2 a_3) (coll a_4 a a_2)) (coll a_4 a_1 a_3)) False) % 46.56/46.76 (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True) % 46.56/46.76 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.76 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 46.56/46.76 (Or (Eq (And (para a_1 a_3 a_2 a_4) (coll a a_1 a_2)) False) (Eq (coll a a_3 a_4) False)) % 46.56/46.76 Clause #554 (by clausification #[553]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.76 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 46.56/46.76 (Or (Eq (coll a a_3 a_4) False) (Or (Eq (para a_1 a_3 a_2 a_4) False) (Eq (coll a a_1 a_2) False))) % 46.56/46.76 Clause #588 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio B a C D P Q U V) True % 46.56/46.76 Clause #589 (by clausification #[588]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio a_1 a C D P Q U V) True % 46.56/46.76 Clause #590 (by clausification #[589]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a_1 a a_2 D P Q U V) True % 46.56/46.76 Clause #591 (by clausification #[590]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a_1 a a_2 a_3 P Q U V) True % 46.56/46.76 Clause #592 (by clausification #[591]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.76 Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_1 a a_2 a_3 a_4 Q U V) True % 46.56/46.76 Clause #593 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.56/46.76 Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_1 a a_2 a_3 a_4 a_5 U V) True % 46.56/46.76 Clause #594 (by clausification #[593]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.76 Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_1 a a_2 a_3 a_4 a_5 a_6 V) True % 46.56/46.76 Clause #595 (by clausification #[594]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.76 Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True % 46.56/46.76 Clause #596 (by clausification #[595]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.56/46.76 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_1 a a_2 a_3 a_4 a_5 a_6 a_7) True) % 46.56/46.76 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 % 46.56/46.76 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 % 46.56/46.76 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 % 46.56/46.76 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 % 46.56/46.76 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 % 46.56/46.76 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 % 46.56/46.76 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) % 46.56/46.76 Clause #611 (by clausification #[94]): Eq % 46.56/46.76 (∀ (A C B D P Q R S O : Iota), % 46.56/46.76 And (And (And (And (And (And (perp A C B D) (midp P B A)) (midp Q C B)) (midp R D C)) (midp S A D)) (coll O P R)) % 46.56/46.76 (coll O Q S) → % 46.56/46.76 cong O S O R) % 46.56/46.76 False % 46.56/46.76 Clause #612 (by clausification #[611]): ∀ (a : Iota), % 46.56/46.78 Eq % 46.56/46.78 (Not % 46.56/46.78 (∀ (C B D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And (And (And (And (perp (skS.0 5 a) C B D) (midp P B (skS.0 5 a))) (midp Q C B)) (midp R D C)) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R)) % 46.56/46.78 True % 46.56/46.78 Clause #613 (by clausification #[612]): ∀ (a : Iota), % 46.56/46.78 Eq % 46.56/46.78 (∀ (C B D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And (And (And (And (perp (skS.0 5 a) C B D) (midp P B (skS.0 5 a))) (midp Q C B)) (midp R D C)) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R) % 46.56/46.78 False % 46.56/46.78 Clause #614 (by clausification #[613]): ∀ (a a_1 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (Not % 46.56/46.78 (∀ (B D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (And (perp (skS.0 5 a) (skS.0 6 a a_1) B D) (midp P B (skS.0 5 a))) (midp Q (skS.0 6 a a_1) B)) % 46.56/46.78 (midp R D (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R)) % 46.56/46.78 True % 46.56/46.78 Clause #615 (by clausification #[614]): ∀ (a a_1 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (∀ (B D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (And (And (perp (skS.0 5 a) (skS.0 6 a a_1) B D) (midp P B (skS.0 5 a))) (midp Q (skS.0 6 a a_1) B)) % 46.56/46.78 (midp R D (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R) % 46.56/46.78 False % 46.56/46.78 Clause #616 (by clausification #[615]): ∀ (a a_1 a_2 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (Not % 46.56/46.78 (∀ (D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) D) % 46.56/46.78 (midp P (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.78 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.78 (midp R D (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R)) % 46.56/46.78 True % 46.56/46.78 Clause #617 (by clausification #[616]): ∀ (a a_1 a_2 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (∀ (D P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) D) % 46.56/46.78 (midp P (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.78 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.78 (midp R D (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) D)) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R) % 46.56/46.78 False % 46.56/46.78 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 a_3 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (Not % 46.56/46.78 (∀ (P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.78 (midp P (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.78 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.78 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R)) % 46.56/46.78 True % 46.56/46.78 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 a_3 : Iota), % 46.56/46.78 Eq % 46.56/46.78 (∀ (P Q R S O : Iota), % 46.56/46.78 And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And % 46.56/46.78 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.78 (midp P (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.78 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.78 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.78 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.78 (coll O P R)) % 46.56/46.78 (coll O Q S) → % 46.56/46.78 cong O S O R) % 46.56/46.78 False % 46.56/46.78 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (Not % 46.56/46.80 (∀ (Q R S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.80 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.80 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.80 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.80 (coll O (skS.0 9 a a_1 a_2 a_3 a_4) R)) % 46.56/46.80 (coll O Q S) → % 46.56/46.80 cong O S O R)) % 46.56/46.80 True % 46.56/46.80 Clause #621 (by clausification #[620]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (∀ (Q R S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.80 (midp Q (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.80 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.80 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.80 (coll O (skS.0 9 a a_1 a_2 a_3 a_4) R)) % 46.56/46.80 (coll O Q S) → % 46.56/46.80 cong O S O R) % 46.56/46.80 False % 46.56/46.80 Clause #622 (by clausification #[621]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (Not % 46.56/46.80 (∀ (R S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.80 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.80 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.80 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.80 (coll O (skS.0 9 a a_1 a_2 a_3 a_4) R)) % 46.56/46.80 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) S) → % 46.56/46.80 cong O S O R)) % 46.56/46.80 True % 46.56/46.80 Clause #623 (by clausification #[622]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (∀ (R S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.80 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.80 (midp R (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.80 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.80 (coll O (skS.0 9 a a_1 a_2 a_3 a_4) R)) % 46.56/46.80 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) S) → % 46.56/46.80 cong O S O R) % 46.56/46.80 False % 46.56/46.80 Clause #624 (by clausification #[623]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (Not % 46.56/46.80 (∀ (S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.56/46.80 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.56/46.80 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.56/46.80 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.56/46.80 (coll O (skS.0 9 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))) % 46.56/46.80 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) S) → % 46.56/46.80 cong O S O (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.56/46.80 True % 46.56/46.80 Clause #625 (by clausification #[624]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.56/46.80 Eq % 46.56/46.80 (∀ (S O : Iota), % 46.56/46.80 And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And % 46.56/46.80 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.56/46.80 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.83 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.83 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.83 (midp S (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.83 (coll O (skS.0 9 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))) % 46.66/46.83 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) S) → % 46.66/46.83 cong O S O (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 46.66/46.83 False % 46.66/46.83 Clause #626 (by clausification #[625]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.83 Eq % 46.66/46.83 (Not % 46.66/46.83 (∀ (O : Iota), % 46.66/46.83 And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.83 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.83 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.83 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.83 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.83 (coll O (skS.0 9 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))) % 46.66/46.83 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 46.66/46.83 cong O (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) O (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.83 True % 46.66/46.83 Clause #627 (by clausification #[626]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.83 Eq % 46.66/46.83 (∀ (O : Iota), % 46.66/46.83 And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.83 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.83 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.83 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.83 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.83 (coll O (skS.0 9 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))) % 46.66/46.83 (coll O (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 46.66/46.83 cong O (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) O (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 46.66/46.83 False % 46.66/46.83 Clause #628 (by clausification #[627]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.66/46.83 Eq % 46.66/46.83 (Not % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.83 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.83 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.83 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.83 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.83 (coll (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) % 46.66/46.83 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.83 (coll (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 46.66/46.83 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 46.66/46.83 cong (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 46.66/46.83 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.83 True % 46.66/46.83 Clause #629 (by clausification #[628]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.66/46.83 Eq % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And % 46.66/46.83 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.83 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.83 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.83 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.85 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.85 (coll (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) % 46.66/46.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.85 (coll (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 46.66/46.85 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 46.66/46.85 cong (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 46.66/46.85 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 46.66/46.85 False % 46.66/46.85 Clause #630 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.66/46.85 Eq % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.85 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.85 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.85 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.85 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.85 (coll (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) % 46.66/46.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.85 (coll (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 46.66/46.85 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 46.66/46.85 True % 46.66/46.85 Clause #631 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.66/46.85 Eq % 46.66/46.85 (cong (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 46.66/46.85 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6)) % 46.66/46.85 False % 46.66/46.85 Clause #633 (by clausification #[630]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.66/46.85 Eq % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And % 46.66/46.85 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.66/46.85 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.66/46.85 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.66/46.85 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.66/46.85 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.66/46.85 (coll (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) % 46.66/46.85 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6))) % 46.66/46.85 True % 46.66/46.85 Clause #659 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio C D a B U V P Q) True % 46.66/46.85 Clause #660 (by clausification #[659]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio C D a a_1 U V P Q) True % 46.66/46.85 Clause #661 (by clausification #[660]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a_2 D a a_1 U V P Q) True % 46.66/46.85 Clause #662 (by clausification #[661]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a_2 a_3 a a_1 U V P Q) True % 46.66/46.85 Clause #663 (by clausification #[662]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.66/46.85 Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_2 a_3 a a_1 U V a_4 Q) True % 46.66/46.85 Clause #664 (by clausification #[663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.66/46.85 Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_2 a_3 a a_1 U V a_4 a_5) True % 46.66/46.85 Clause #665 (by clausification #[664]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.66/46.85 Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_2 a_3 a a_1 a_6 V a_4 a_5) True % 46.66/46.85 Clause #666 (by clausification #[665]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.85 Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True % 46.66/46.85 Clause #667 (by clausification #[666]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.85 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True) % 46.66/46.88 Clause #714 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio P Q U V a B C D) True % 46.66/46.88 Clause #715 (by clausification #[714]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio P Q U V a a_1 C D) True % 46.66/46.88 Clause #716 (by clausification #[715]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio P Q U V a a_1 a_2 D) True % 46.66/46.88 Clause #717 (by clausification #[716]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio P Q U V a a_1 a_2 a_3) True % 46.66/46.88 Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.66/46.88 Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a_4 Q U V a a_1 a_2 a_3) True % 46.66/46.88 Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.66/46.88 Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a_4 a_5 U V a a_1 a_2 a_3) True % 46.66/46.88 Clause #720 (by clausification #[719]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.66/46.88 Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a_4 a_5 a_6 V a a_1 a_2 a_3) True % 46.66/46.88 Clause #721 (by clausification #[720]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.88 Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True % 46.66/46.88 Clause #722 (by clausification #[721]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.88 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True) % 46.66/46.88 Clause #732 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqratio a B C D P Q U V → eqratio a B P Q C D U V) True % 46.66/46.88 Clause #733 (by clausification #[732]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqratio a a_1 C D P Q U V → eqratio a a_1 P Q C D U V) True % 46.66/46.88 Clause #734 (by clausification #[733]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqratio a a_1 a_2 D P Q U V → eqratio a a_1 P Q a_2 D U V) True % 46.66/46.88 Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqratio a a_1 a_2 a_3 P Q U V → eqratio a a_1 P Q a_2 a_3 U V) True % 46.66/46.88 Clause #736 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.66/46.88 Eq (∀ (Q U V : Iota), eqratio a a_1 a_2 a_3 a_4 Q U V → eqratio a a_1 a_4 Q a_2 a_3 U V) True % 46.66/46.88 Clause #737 (by clausification #[736]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.66/46.88 Eq (∀ (U V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 U V → eqratio a a_1 a_4 a_5 a_2 a_3 U V) True % 46.66/46.88 Clause #738 (by clausification #[737]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.66/46.88 Eq (∀ (V : Iota), eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V → eqratio a a_1 a_4 a_5 a_2 a_3 a_6 V) True % 46.66/46.88 Clause #739 (by clausification #[738]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.88 Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqratio a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True % 46.66/46.88 Clause #740 (by clausification #[739]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.66/46.88 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqratio a a_1 a_4 a_5 a_2 a_3 a_6 a_7) True) % 46.66/46.88 Clause #780 (by clausification #[29]): ∀ (a : Iota), % 46.66/46.88 Eq % 46.66/46.88 (∀ (B C D E F G H P Q U V : Iota), % 46.66/46.88 And (eqratio a B C D P Q U V) (eqratio P Q U V E F G H) → eqratio a B C D E F G H) % 46.66/46.88 True % 46.66/46.88 Clause #781 (by clausification #[780]): ∀ (a a_1 : Iota), % 46.66/46.88 Eq % 46.66/46.88 (∀ (C D E F G H P Q U V : Iota), % 46.66/46.88 And (eqratio a a_1 C D P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 C D E F G H) % 46.66/46.88 True % 46.66/46.88 Clause #782 (by clausification #[781]): ∀ (a a_1 a_2 : Iota), % 46.66/46.88 Eq % 46.66/46.88 (∀ (D E F G H P Q U V : Iota), % 46.66/46.88 And (eqratio a a_1 a_2 D P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 a_2 D E F G H) % 46.66/46.88 True % 46.66/46.88 Clause #783 (by clausification #[782]): ∀ (a a_1 a_2 a_3 : Iota), % 46.66/46.88 Eq % 46.66/46.88 (∀ (E F G H P Q U V : Iota), % 46.66/46.88 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V E F G H) → eqratio a a_1 a_2 a_3 E F G H) % 46.66/46.88 True % 46.66/46.88 Clause #784 (by clausification #[783]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 46.66/46.88 Eq % 46.66/46.88 (∀ (F G H P Q U V : Iota), % 46.66/46.88 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 F G H) → eqratio a a_1 a_2 a_3 a_4 F G H) % 46.75/46.90 True % 46.75/46.90 Clause #785 (by clausification #[784]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (G H P Q U V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 G H) → eqratio a a_1 a_2 a_3 a_4 a_5 G H) % 46.75/46.90 True % 46.75/46.90 Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (H P Q U V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 H) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 H) % 46.75/46.90 True % 46.75/46.90 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (P Q U V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 P Q U V) (eqratio P Q U V a_4 a_5 a_6 a_7) → eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 46.75/46.90 True % 46.75/46.90 Clause #788 (by clausification #[787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (Q U V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 a_4 Q U V) (eqratio a_4 Q U V a_5 a_6 a_7 a_8) → eqratio a a_1 a_2 a_3 a_5 a_6 a_7 a_8) % 46.75/46.90 True % 46.75/46.90 Clause #789 (by clausification #[788]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (U V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 a_4 a_5 U V) (eqratio a_4 a_5 U V a_6 a_7 a_8 a_9) → % 46.75/46.90 eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9) % 46.75/46.90 True % 46.75/46.90 Clause #790 (by clausification #[789]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (∀ (V : Iota), % 46.75/46.90 And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 V) (eqratio a_4 a_5 a_6 V a_7 a_8 a_9 a_10) → % 46.75/46.90 eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10) % 46.75/46.90 True % 46.75/46.90 Clause #791 (by clausification #[790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqratio a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) → % 46.75/46.90 eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 46.75/46.90 True % 46.75/46.90 Clause #792 (by clausification #[791]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 46.75/46.90 Or (Eq (And (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (eqratio a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11)) False) % 46.75/46.90 (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 46.75/46.90 Clause #793 (by clausification #[792]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 46.75/46.90 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 46.75/46.90 (Or (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) False) (Eq (eqratio a_8 a_9 a_10 a_11 a_4 a_5 a_6 a_7) False)) % 46.75/46.90 Clause #862 (by clausification #[633]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.75/46.90 Eq % 46.75/46.90 (And % 46.75/46.90 (And % 46.75/46.90 (And % 46.75/46.90 (And (perp (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3)) % 46.75/46.90 (midp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a))) % 46.75/46.90 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 46.75/46.90 (midp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3) (skS.0 6 a a_1))) % 46.75/46.90 (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3))) % 46.75/46.90 True % 46.75/46.90 Clause #1221 (by clausification #[862]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.75/46.90 Eq (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3)) True % 46.75/46.90 Clause #1224 (by superposition #[1221, 111]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.75/46.90 Or (Eq True False) (Eq (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True) % 46.75/46.90 Clause #1227 (by superposition #[1221, 283]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 46.75/46.90 Or (Eq (para (skS.0 5 a) a_1 (skS.0 8 a a_2 a_3 a_4) a_5) True) % 46.75/46.90 (Or (Eq True False) (Eq (midp (skS.0 12 a a_2 a_3 a_4 a_6 a_7 a_8 a_9) a_1 a_5) False)) % 46.75/46.90 Clause #1235 (by clausification #[1224]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.75/46.90 Eq (midp (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True % 46.75/46.90 Clause #1314 (by clausification #[1227]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 46.75/46.90 Or (Eq (para (skS.0 5 a) a_1 (skS.0 8 a a_2 a_3 a_4) a_5) True) % 46.75/46.90 (Eq (midp (skS.0 12 a a_2 a_3 a_4 a_6 a_7 a_8 a_9) a_1 a_5) False) % 46.75/46.90 Clause #1316 (by superposition #[1314, 1235]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.90 Or (Eq (para (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True) (Eq False True) % 46.75/46.93 Clause #1317 (by clausification #[1316]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True % 46.75/46.93 Clause #1320 (by superposition #[1317, 189]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.93 Or (Eq True False) (Eq (para (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3)) True) % 46.75/46.93 Clause #1325 (by clausification #[1320]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3)) True % 46.75/46.93 Clause #1327 (by superposition #[1325, 156]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.93 Or (Eq True False) (Eq (para (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True) % 46.75/46.93 Clause #1332 (by clausification #[1327]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a)) True % 46.75/46.93 Clause #1337 (by superposition #[1332, 610]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Or (Eq True False) % 46.75/46.93 (Eq (eqangle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5 (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5) True) % 46.75/46.93 Clause #1550 (by clausification #[1337]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Eq (eqangle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5 (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5) True % 46.75/46.93 Clause #1558 (by superposition #[1550, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Or (Eq True False) % 46.75/46.93 (Eq (eqangle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5 a_4 a_5) True) % 46.75/46.93 Clause #1562 (by clausification #[1558]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Eq (eqangle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) a_4 a_5 a_4 a_5) True % 46.75/46.93 Clause #1568 (by superposition #[1562, 441]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Or (Eq True False) % 46.75/46.93 (Eq (eqangle a a_1 a a_1 (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True) % 46.75/46.93 Clause #1576 (by clausification #[1568]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Eq (eqangle a a_1 a a_1 (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True % 46.75/46.93 Clause #1580 (by superposition #[1576, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Or (Eq True False) % 46.75/46.93 (Eq (eqangle a a_1 a_1 a (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True) % 46.75/46.93 Clause #1587 (by clausification #[1580]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Eq (eqangle a a_1 a_1 a (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True % 46.75/46.93 Clause #1594 (by superposition #[1587, 496]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Or (Eq True False) % 46.75/46.93 (Eq (eqangle a a_1 (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) a_1 a (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True) % 46.75/46.93 Clause #1599 (by clausification #[1594]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.93 Eq (eqangle a a_1 (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2) a_1 a (skS.0 8 a_2 a_3 a_4 a_5) (skS.0 5 a_2)) True % 46.75/46.93 Clause #1603 (by superposition #[1599, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 46.75/46.93 Clause #1612 (by clausification #[1603]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 46.75/46.93 Clause #1621 (by superposition #[1612, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 46.75/46.93 Clause #1624 (by superposition #[1612, 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) % 46.75/46.93 Clause #1641 (by clausification #[1621]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 46.75/46.93 Clause #1642 (by superposition #[1641, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 46.75/46.93 Clause #1647 (by clausification #[1642]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 46.75/46.93 Clause #1657 (by superposition #[1647, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 46.75/46.93 Clause #1666 (by clausification #[1657]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 46.75/46.93 Clause #1677 (by superposition #[1666, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 46.75/46.93 Clause #1680 (by superposition #[1666, 554]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.93 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) % 46.75/46.95 (Or (Eq True False) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq (coll a a_1 a_2) False))) % 46.75/46.95 Clause #1686 (by clausification #[1677]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 46.75/46.95 Clause #1696 (by superposition #[1686, 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)) % 46.75/46.95 Clause #1732 (by clausification #[1624]): ∀ (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 % 46.75/46.95 Clause #1741 (by superposition #[1732, 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) % 46.75/46.95 Clause #1750 (by clausification #[1741]): ∀ (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 % 46.75/46.95 Clause #1754 (by superposition #[1750, 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) % 46.75/46.95 Clause #1756 (by superposition #[1750, 441]): ∀ (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_3 a_2) True) % 46.75/46.95 Clause #1763 (by clausification #[1756]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 a_2 a_3 a_3 a_2) True % 46.75/46.95 Clause #1767 (by superposition #[1763, 352]): ∀ (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_3 a_2) True) % 46.75/46.95 Clause #1775 (by clausification #[1767]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a a_2 a_3 a_3 a_2) True % 46.75/46.95 Clause #1783 (by superposition #[1775, 496]): ∀ (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_3 a_2) True) % 46.75/46.95 Clause #1788 (by clausification #[1783]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a_1 a a_3 a_2) True % 46.75/46.95 Clause #1789 (by superposition #[1788, 369]): ∀ (a a_1 : Iota), % 46.75/46.95 Or (Eq (cong a a a_1 a_1) True) % 46.75/46.95 (Or (Eq True False) % 46.75/46.95 (Or (Eq (cyclic a a a_1 a) False) (Or (Eq (cyclic a a a_1 a_1) False) (Eq (cyclic a a a_1 a_1) False)))) % 46.75/46.95 Clause #1794 (by clausification #[1754]): ∀ (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 % 46.75/46.95 Clause #1795 (by superposition #[1794, 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)) % 46.75/46.95 Clause #1826 (by clausification #[1696]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 46.75/46.95 Clause #1830 (by superposition #[1826, 1686]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 46.75/46.95 Clause #1831 (by clausification #[1830]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 46.75/46.95 Clause #1917 (by clausification #[1795]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq (coll a_1 a_2 a) False) % 46.75/46.95 Clause #1918 (by forward demodulation #[1917, 1831]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a a_1 a_2) True) (Eq True False) % 46.75/46.95 Clause #1919 (by clausification #[1918]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 46.75/46.95 Clause #1923 (by superposition #[1919, 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)) % 46.75/46.95 Clause #2222 (by clausification #[1923]): ∀ (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) % 46.75/46.95 Clause #2223 (by superposition #[2222, 1919]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 46.75/46.95 Clause #2230 (by clausification #[2223]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 46.75/46.95 Clause #2787 (by clausification #[1680]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.95 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq (coll a a_1 a_2) False)) % 46.75/46.95 Clause #2788 (by forward demodulation #[2787, 1831]): ∀ (a a_1 a_2 a_3 : Iota), % 46.75/46.95 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Or (Eq (para a_1 a_3 a_2 a) False) (Eq True False)) % 46.75/46.95 Clause #2789 (by clausification #[2788]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a) True) (Eq (para a_1 a_3 a_2 a) False) % 46.75/46.95 Clause #2792 (by superposition #[2789, 1612]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a_1 a a_1 a_1 a) True) (Eq False True) % 46.75/46.95 Clause #2793 (by superposition #[2789, 1641]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a a a a) True) (Eq False True) % 46.75/46.98 Clause #2794 (by clausification #[2793]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a a a) True % 46.75/46.98 Clause #2799 (by superposition #[2794, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a_1 a a) True) % 46.75/46.98 Clause #2801 (by clausification #[2799]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a_1 a a) True % 46.75/46.98 Clause #2805 (by superposition #[2801, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_1 a a_1 a_1) True) % 46.75/46.98 Clause #2808 (by clausification #[2805]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a_1 a_1 a a_1 a_1) True % 46.75/46.98 Clause #2810 (by superposition #[2808, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a a a_1) True) % 46.75/46.98 Clause #2813 (by clausification #[2810]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a_1 a a a a_1) True % 46.75/46.98 Clause #2815 (by superposition #[2813, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a_1 a a_1) True) % 46.75/46.98 Clause #2817 (by clausification #[2815]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a_1 a a_1) True % 46.75/46.98 Clause #2819 (by superposition #[2817, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.98 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Or (Eq True False) (Eq (eqratio a_5 a_5 a a_5 a_1 a_2 a_3 a_4) False)) % 46.75/46.98 Clause #2856 (by clausification #[2792]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a_1 a_1 a) True % 46.75/46.98 Clause #2859 (by superposition #[2856, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a a_1) True) % 46.75/46.98 Clause #2861 (by clausification #[2859]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a a_1) True % 46.75/46.98 Clause #2863 (by superposition #[2861, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_1 a_1 a) True) % 46.75/46.98 Clause #2867 (by clausification #[2863]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_1 a_1 a) True % 46.75/46.98 Clause #2871 (by superposition #[2867, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True) % 46.75/46.98 Clause #2873 (by clausification #[2871]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_1 a_1 a) True % 46.75/46.98 Clause #2876 (by superposition #[2873, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True) % 46.75/46.98 Clause #2879 (by clausification #[2876]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a_1 a_1 a_1) True % 46.75/46.98 Clause #2881 (by superposition #[2879, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a a a) True) % 46.75/46.98 Clause #2882 (by superposition #[2879, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a a_1 a) True) % 46.75/46.98 Clause #2884 (by clausification #[2882]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a a_1 a) True % 46.75/46.98 Clause #2887 (by superposition #[2884, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_1 a a_1 a) True) % 46.75/46.98 Clause #2889 (by clausification #[2887]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a_1 a a_1 a) True % 46.75/46.98 Clause #2891 (by superposition #[2889, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a a_1 a a_1) True) % 46.75/46.98 Clause #2893 (by clausification #[2891]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_1 a a_1) True % 46.75/46.98 Clause #2895 (by superposition #[2893, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_1 a a_1 a) True) % 46.75/46.98 Clause #2925 (by clausification #[2881]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a_1 a_1 a a a) True % 46.75/46.98 Clause #2929 (by superposition #[2925, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a a_1 a a) True) % 46.75/46.98 Clause #2931 (by clausification #[2929]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a a_1 a a) True % 46.75/46.98 Clause #2933 (by superposition #[2931, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a) True) % 46.75/46.98 Clause #2935 (by clausification #[2933]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a) True % 46.75/46.98 Clause #2992 (by clausification #[2895]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a_1 a a_1 a) True % 46.75/46.98 Clause #3083 (by clausification #[2819]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.75/46.98 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Eq (eqratio a_5 a_5 a a_5 a_1 a_2 a_3 a_4) False) % 46.75/46.98 Clause #3093 (by superposition #[3083, 2992]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a a a_1 a a_1) True) (Eq False True) % 46.85/47.01 Clause #3096 (by clausification #[3093]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a_1 a a_1) True % 46.85/47.01 Clause #3099 (by superposition #[3096, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a a a a_1) True) % 46.85/47.01 Clause #3101 (by clausification #[3099]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a a a_1) True % 46.85/47.01 Clause #3103 (by superposition #[3101, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a a_1 a a) True) % 46.85/47.01 Clause #3106 (by clausification #[3103]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a a a a_1 a a) True % 46.85/47.01 Clause #3108 (by superposition #[3106, 596]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True) % 46.85/47.01 Clause #3110 (by clausification #[3108]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a_1 a_1 a a_1 a_1) True % 46.85/47.01 Clause #3112 (by superposition #[3110, 667]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a a a a_1) True) % 46.85/47.01 Clause #3114 (by superposition #[3110, 740]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a_1) True) % 46.85/47.01 Clause #3117 (by clausification #[3114]): ∀ (a a_1 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_1 a_1 a_1) True % 46.85/47.01 Clause #3120 (by superposition #[3117, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a_1 a a a_1) True) % 46.85/47.01 Clause #3122 (by clausification #[3120]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a_1 a a a_1) True % 46.85/47.01 Clause #3125 (by superposition #[3122, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Or (Eq True False) (Eq (eqratio a_5 a a a_5 a_1 a_2 a_3 a_4) False)) % 46.85/47.01 Clause #3163 (by clausification #[3112]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a a_1) True % 46.85/47.01 Clause #3165 (by superposition #[3163, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) False)) % 46.85/47.01 Clause #3227 (by clausification #[3165]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Eq (eqratio a a a a_1 a_2 a_3 a_4 a_5) False) % 46.85/47.01 Clause #3249 (by clausification #[3125]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Eq (eqratio a_5 a a a_5 a_1 a_2 a_3 a_4) False) % 46.85/47.01 Clause #3251 (by superposition #[3249, 2935]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a a a a a a_1) True) (Eq False True) % 46.85/47.01 Clause #3263 (by clausification #[3251]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a a a_1) True % 46.85/47.01 Clause #3266 (by superposition #[3263, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a a a a) True) % 46.85/47.01 Clause #3273 (by clausification #[3266]): ∀ (a a_1 : Iota), Eq (eqratio a a a a_1 a a a a) True % 46.85/47.01 Clause #3278 (by superposition #[3273, 3227]): ∀ (a a_1 : Iota), Or (Eq (eqratio a a a_1 a a a a a) True) (Eq True False) % 46.85/47.01 Clause #3279 (by clausification #[3278]): ∀ (a a_1 : Iota), Eq (eqratio a a a_1 a a a a a) True % 46.85/47.01 Clause #3282 (by superposition #[3279, 722]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (eqratio a a a a a a a_1 a) True) % 46.85/47.01 Clause #3284 (by superposition #[3279, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Or (Eq True False) (Eq (eqratio a a a a a_2 a_3 a_4 a_5) False)) % 46.85/47.01 Clause #3297 (by clausification #[3282]): ∀ (a a_1 : Iota), Eq (eqratio a a a a a a a_1 a) True % 46.85/47.01 Clause #3320 (by clausification #[3284]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 46.85/47.01 Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Eq (eqratio a a a a a_2 a_3 a_4 a_5) False) % 46.85/47.01 Clause #3336 (by superposition #[3320, 3297]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a_1 a a a a_2 a) True) (Eq False True) % 46.85/47.01 Clause #3337 (by clausification #[3336]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a a a_2 a) True % 46.85/47.01 Clause #3343 (by superposition #[3337, 3083]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a a a a_1 a_1 a_2 a_1) True) (Eq True False) % 46.85/47.01 Clause #3348 (by clausification #[3343]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a a_1 a_1 a_2 a_1) True % 46.85/47.01 Clause #3354 (by superposition #[3348, 3320]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a_2 a_2 a_3 a_2) True) (Eq True False) % 46.86/47.03 Clause #3355 (by clausification #[3354]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a_2 a_2 a_3 a_2) True % 46.86/47.03 Clause #3359 (by superposition #[3355, 740]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a a_3 a_1) True) % 46.86/47.03 Clause #3361 (by clausification #[3359]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a_1 a_2 a a_3 a_1) True % 46.86/47.03 Clause #3365 (by superposition #[3361, 3320]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a_2 a a_3 a) True) (Eq True False) % 46.86/47.03 Clause #3366 (by clausification #[3365]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a_2 a a_3 a) True % 46.86/47.03 Clause #3372 (by superposition #[3366, 3083]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a a_1 a_2 a_3 a_2) True) (Eq True False) % 46.86/47.03 Clause #3378 (by clausification #[3372]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a_1 a_2 a_3 a_2) True % 46.86/47.03 Clause #3384 (by superposition #[3378, 3320]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_3) True) (Eq True False) % 46.86/47.03 Clause #3385 (by clausification #[3384]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a a_2 a_3 a_4 a_3) True % 46.86/47.03 Clause #3389 (by superposition #[3385, 740]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_3 a a_4 a_2) True) % 46.86/47.03 Clause #3391 (by clausification #[3389]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a_2 a_3 a a_4 a_2) True % 46.86/47.03 Clause #3396 (by superposition #[3391, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.86/47.03 Or (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_6) True) % 46.86/47.03 (Or (Eq True False) (Eq (eqratio a_7 a a_8 a_2 a_3 a_4 a_5 a_6) False)) % 46.86/47.03 Clause #3397 (by superposition #[3391, 3227]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a_1 a a_2 a a_3 a_1) True) (Eq True False) % 46.86/47.03 Clause #3398 (by clausification #[3397]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a_1 a a_2 a a_3 a_1) True % 46.86/47.03 Clause #3404 (by superposition #[3398, 3083]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a a a a_1 a_2 a_3 a) True) (Eq True False) % 46.86/47.03 Clause #3405 (by clausification #[3404]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a a a a_1 a_2 a_3 a) True % 46.86/47.03 Clause #3411 (by superposition #[3405, 3320]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a) True) (Eq True False) % 46.86/47.03 Clause #3413 (by clausification #[3411]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a_1 a a_2 a_3 a_4 a) True % 46.86/47.03 Clause #3419 (by superposition #[3413, 3083]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a a a a_1 a_2 a_3 a_4) True) (Eq True False) % 46.86/47.03 Clause #3420 (by clausification #[3419]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a a a a_1 a_2 a_3 a_4) True % 46.86/47.03 Clause #3426 (by superposition #[3420, 3320]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True) (Eq True False) % 46.86/47.03 Clause #3427 (by clausification #[3426]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a a_2 a_3 a_4 a_5) True % 46.86/47.03 Clause #3431 (by superposition #[3427, 740]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_3 a a_4 a_5) True) % 46.86/47.03 Clause #3433 (by clausification #[3431]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a a_4 a_5) True % 46.86/47.03 Clause #3435 (by superposition #[3433, 667]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_2) True) % 46.86/47.03 Clause #3436 (by superposition #[3433, 722]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_5) True) % 46.86/47.03 Clause #3444 (by clausification #[3436]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_1 a_4 a_5) True % 46.86/47.03 Clause #3446 (by superposition #[3444, 596]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a a a_4 a_5) True) % 46.86/47.03 Clause #3456 (by clausification #[3446]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a a a_4 a_5) True % 46.86/47.03 Clause #3460 (by superposition #[3456, 740]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_3 a_4 a_5) True) % 46.86/47.06 Clause #3462 (by clausification #[3460]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a a a_2 a_3 a_4 a_5) True % 46.86/47.06 Clause #3465 (by superposition #[3462, 722]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_4 a_4) True) % 46.86/47.06 Clause #3468 (by clausification #[3465]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_4 a_4) True % 46.86/47.06 Clause #3470 (by superposition #[3468, 667]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_4 a_4 a_5) True) % 46.86/47.06 Clause #3472 (by clausification #[3470]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_4 a_4 a_5) True % 46.86/47.06 Clause #3475 (by superposition #[3472, 793]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 46.86/47.06 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 46.86/47.06 (Or (Eq True False) (Eq (eqratio a_8 a_8 a_8 a_9 a_4 a_5 a_6 a_7) False)) % 46.86/47.06 Clause #3489 (by clausification #[3435]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_4 a_5 a_2) True % 46.86/47.06 Clause #3625 (by clausification #[3396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 46.86/47.06 Or (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_6) True) (Eq (eqratio a_7 a a_8 a_2 a_3 a_4 a_5 a_6) False) % 46.86/47.06 Clause #3638 (by superposition #[3625, 3489]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_2) True) (Eq False True) % 46.86/47.06 Clause #3641 (by clausification #[3638]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_2) True % 46.86/47.06 Clause #3645 (by superposition #[3641, 740]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_4) True) % 46.86/47.06 Clause #3653 (by clausification #[3645]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_4) True % 46.86/47.06 Clause #3656 (by superposition #[3653, 722]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_3 a_4 a_5) True) % 46.86/47.06 Clause #3660 (by clausification #[3656]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_3 a_4 a_5) True % 46.86/47.06 Clause #3663 (by superposition #[3660, 667]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_5 a_5) True) % 46.86/47.06 Clause #3668 (by clausification #[3663]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_5 a_5) True % 46.86/47.06 Clause #3671 (by superposition #[3668, 740]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_5 a_5) True) % 46.86/47.06 Clause #3675 (by clausification #[3671]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_5 a_5) True % 46.86/47.06 Clause #3677 (by superposition #[3675, 596]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a a_5 a_5) True) % 46.86/47.06 Clause #3681 (by clausification #[3677]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a a_5 a_5) True % 46.86/47.06 Clause #3686 (by superposition #[3681, 3625]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_5) True) (Eq True False) % 46.86/47.06 Clause #3692 (by clausification #[3686]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_5) True % 46.86/47.06 Clause #3694 (by superposition #[3692, 667]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_4 a_5) True) % 46.86/47.06 Clause #3697 (by clausification #[3694]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a_1 a_2 a_2 a_3 a_3 a_4 a_5) True % 46.86/47.06 Clause #3700 (by superposition #[3697, 3625]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq (eqratio a a a_1 a_2 a_3 a_3 a_4 a_5) True) (Eq True False) % 46.86/47.06 Clause #3701 (by clausification #[3700]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_3 a_4 a_5) True % 46.86/47.06 Clause #3705 (by superposition #[3701, 740]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True) % 46.86/47.06 Clause #3707 (by clausification #[3705]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (eqratio a a a_1 a_1 a_2 a_3 a_4 a_5) True % 46.86/47.06 Clause #3711 (by superposition #[3707, 3625]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Or (Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_6) True) (Eq True False) % 46.86/47.11 Clause #3713 (by clausification #[3711]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (eqratio a a a_1 a_2 a_3 a_4 a_5 a_6) True % 46.86/47.11 Clause #3788 (by clausification #[3475]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 46.86/47.11 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq (eqratio a_8 a_8 a_8 a_9 a_4 a_5 a_6 a_7) False) % 46.86/47.11 Clause #3789 (by superposition #[3788, 3713]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) (Eq False True) % 46.86/47.11 Clause #3797 (by clausification #[3789]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True % 46.86/47.11 Clause #3798 (by superposition #[3797, 467]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 46.86/47.11 Or (Eq (cong a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a_4 a_5 a_6 a_7) False)) % 46.86/47.11 Clause #3799 (by clausification #[3798]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq (cong a_4 a_5 a_6 a_7) False) % 46.86/47.11 Clause #4004 (by clausification #[1789]): ∀ (a a_1 : Iota), % 46.86/47.11 Or (Eq (cong a a a_1 a_1) True) % 46.86/47.11 (Or (Eq (cyclic a a a_1 a) False) (Or (Eq (cyclic a a a_1 a_1) False) (Eq (cyclic a a a_1 a_1) False))) % 46.86/47.11 Clause #4005 (by eliminate duplicate literals #[4004]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Or (Eq (cyclic a a a_1 a) False) (Eq (cyclic a a a_1 a_1) False)) % 46.86/47.11 Clause #4006 (by superposition #[4005, 2230]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Or (Eq (cyclic a a a_1 a_1) False) (Eq False True)) % 46.86/47.11 Clause #4007 (by clausification #[4006]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq (cyclic a a a_1 a_1) False) % 46.86/47.11 Clause #4008 (by superposition #[4007, 2230]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq False True) % 46.86/47.11 Clause #4009 (by clausification #[4008]): ∀ (a a_1 : Iota), Eq (cong a a a_1 a_1) True % 46.86/47.11 Clause #4017 (by superposition #[4009, 3799]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False) % 46.86/47.11 Clause #4072 (by clausification #[4017]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True % 46.86/47.11 Clause #4076 (by superposition #[4072, 631]): Eq True False % 46.86/47.11 Clause #4082 (by clausification #[4076]): False % 46.86/47.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------