%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO541+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 214.88s 215.09s % Output : Proof 215.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GEO541+1 : TPTP v9.2.0. Released v7.5.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 11:55:08 EDT 2025 % 0.13/0.34 % CPUTime : % 214.88/215.09 SZS status Theorem for theBenchmark.p % 214.88/215.09 SZS output start Proof for theBenchmark.p % 214.88/215.09 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 214.88/215.09 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 214.88/215.09 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 214.88/215.09 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 214.88/215.09 Clause #10 (by assumption #[]): Eq (∀ (A B M : Iota), midp M B A → midp M A B) True % 214.88/215.09 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 % 214.88/215.09 Clause #18 (by assumption #[]): Eq (∀ (A B C D P Q U V : Iota), eqangle A B C D P Q U V → eqangle C D A B U V P Q) True % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 Clause #23 (by assumption #[]): Eq (∀ (A B C D : Iota), cong A B C D → cong C D A B) True % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 Clause #29 (by assumption #[]): Eq % 214.88/215.09 (∀ (A B C D E F G H P Q U V : Iota), % 214.88/215.09 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) % 214.88/215.09 True % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 Clause #56 (by assumption #[]): Eq (∀ (A B P Q : Iota), And (cong A P B P) (cong A Q B Q) → perp A B P Q) True % 214.88/215.09 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 % 214.88/215.09 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 % 214.88/215.09 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 214.88/215.09 Clause #68 (by assumption #[]): Eq (∀ (A B C : Iota), midp A B C → cong A B A C) True % 214.88/215.09 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 % 214.88/215.09 Clause #94 (by assumption #[]): Eq % 214.88/215.09 (Not % 214.88/215.09 (∀ (A B C D E F G : Iota), % 214.88/215.09 And (And (And (And (And (perp D C A B) (coll D A B)) (perp E B A C)) (coll E A C)) (midp F C B)) (midp G D E) → % 214.88/215.09 perp F G D E)) % 214.88/215.09 True % 214.88/215.09 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 214.88/215.09 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 214.88/215.09 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 % 214.88/215.09 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) % 214.88/215.09 Clause #108 (by clausification #[10]): ∀ (a : Iota), Eq (∀ (B M : Iota), midp M B a → midp M a B) True % 214.88/215.09 Clause #109 (by clausification #[108]): ∀ (a a_1 : Iota), Eq (∀ (M : Iota), midp M a a_1 → midp M a_1 a) True % 214.88/215.09 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 % 214.88/215.09 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) % 214.88/215.09 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 214.88/215.09 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 214.88/215.09 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 % 214.88/215.12 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) % 214.88/215.12 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 214.88/215.12 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 214.88/215.12 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 % 214.88/215.12 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) % 214.88/215.12 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 % 214.88/215.12 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 % 214.88/215.12 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 % 214.88/215.12 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 % 214.88/215.12 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) % 214.88/215.12 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)) % 214.88/215.12 Clause #126 (by clausification #[68]): ∀ (a : Iota), Eq (∀ (B C : Iota), midp a B C → cong a B a C) True % 214.88/215.12 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), midp a a_1 C → cong a a_1 a C) True % 214.88/215.12 Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 : Iota), Eq (midp a a_1 a_2 → cong a a_1 a a_2) True % 214.88/215.12 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), Or (Eq (midp a a_1 a_2) False) (Eq (cong a a_1 a a_2) True) % 214.88/215.12 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 214.88/215.12 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 % 214.88/215.12 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 % 214.88/215.12 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 % 214.88/215.12 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) % 214.88/215.12 Clause #190 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cong a B C D → cong C D a B) True % 214.88/215.12 Clause #191 (by clausification #[190]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cong a a_1 C D → cong C D a a_1) True % 214.88/215.12 Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cong a a_1 a_2 D → cong a_2 D a a_1) True % 214.88/215.12 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3 → cong a_2 a_3 a a_1) True % 214.88/215.12 Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) False) (Eq (cong a_2 a_3 a a_1) True) % 214.88/215.12 Clause #207 (by clausification #[56]): ∀ (a : Iota), Eq (∀ (B P Q : Iota), And (cong a P B P) (cong a Q B Q) → perp a B P Q) True % 214.88/215.12 Clause #208 (by clausification #[207]): ∀ (a a_1 : Iota), Eq (∀ (P Q : Iota), And (cong a P a_1 P) (cong a Q a_1 Q) → perp a a_1 P Q) True % 214.88/215.12 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Q : Iota), And (cong a a_1 a_2 a_1) (cong a Q a_2 Q) → perp a a_2 a_1 Q) True % 214.88/215.12 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (cong a a_1 a_2 a_1) (cong a a_3 a_2 a_3) → perp a a_2 a_1 a_3) True % 214.88/215.12 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (And (cong a a_1 a_2 a_1) (cong a a_3 a_2 a_3)) False) (Eq (perp a a_2 a_1 a_3) True) % 214.88/215.12 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 a_3 : Iota), % 214.88/215.12 Or (Eq (perp a a_1 a_2 a_3) True) (Or (Eq (cong a a_2 a_1 a_2) False) (Eq (cong a a_3 a_1 a_3) False)) % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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) % 214.94/215.15 Clause #283 (by clausification #[282]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.94/215.15 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)) % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.94/215.15 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 % 214.94/215.15 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 214.94/215.15 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 % 214.94/215.15 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 214.94/215.15 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 % 214.94/215.15 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.94/215.15 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 % 214.94/215.15 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.94/215.15 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) % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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 % 214.94/215.15 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) % 214.94/215.15 Clause #389 (by clausification #[18]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle C D a B U V P Q) True % 214.94/215.15 Clause #390 (by clausification #[389]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle C D a a_1 U V P Q) True % 214.94/215.15 Clause #391 (by clausification #[390]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a_2 D a a_1 U V P Q) True % 214.94/215.15 Clause #392 (by clausification #[391]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a_2 a_3 a a_1 U V P Q) True % 214.97/215.17 Clause #393 (by clausification #[392]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.97/215.17 Eq (∀ (Q U V : Iota), eqangle a a_1 a_2 a_3 a_4 Q U V → eqangle a_2 a_3 a a_1 U V a_4 Q) True % 214.97/215.17 Clause #394 (by clausification #[393]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 214.97/215.17 Eq (∀ (U V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 U V → eqangle a_2 a_3 a a_1 U V a_4 a_5) True % 214.97/215.17 Clause #395 (by clausification #[394]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 214.97/215.17 Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_2 a_3 a a_1 a_6 V a_4 a_5) True % 214.97/215.17 Clause #396 (by clausification #[395]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.97/215.17 Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True % 214.97/215.17 Clause #397 (by clausification #[396]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.97/215.17 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_2 a_3 a a_1 a_6 a_7 a_4 a_5) True) % 214.97/215.17 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 % 214.97/215.17 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 % 214.97/215.17 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 % 214.97/215.17 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 % 214.97/215.17 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.97/215.17 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 % 214.97/215.17 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 214.97/215.17 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 % 214.97/215.17 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 214.97/215.17 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 % 214.97/215.17 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.97/215.17 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 % 214.97/215.17 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 214.97/215.17 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) % 214.97/215.17 Clause #458 (by clausification #[94]): Eq % 214.97/215.17 (∀ (A B C D E F G : Iota), % 214.97/215.17 And (And (And (And (And (perp D C A B) (coll D A B)) (perp E B A C)) (coll E A C)) (midp F C B)) (midp G D E) → % 214.97/215.17 perp F G D E) % 214.97/215.17 False % 214.97/215.17 Clause #459 (by clausification #[458]): ∀ (a : Iota), % 214.97/215.17 Eq % 214.97/215.17 (Not % 214.97/215.17 (∀ (B C D E F G : Iota), % 214.97/215.17 And % 214.97/215.17 (And % 214.97/215.17 (And (And (And (perp D C (skS.0 4 a) B) (coll D (skS.0 4 a) B)) (perp E B (skS.0 4 a) C)) % 214.97/215.17 (coll E (skS.0 4 a) C)) % 214.97/215.17 (midp F C B)) % 214.97/215.17 (midp G D E) → % 214.97/215.17 perp F G D E)) % 214.97/215.17 True % 214.97/215.17 Clause #460 (by clausification #[459]): ∀ (a : Iota), % 214.97/215.17 Eq % 214.97/215.17 (∀ (B C D E F G : Iota), % 214.97/215.17 And % 214.97/215.17 (And % 214.97/215.17 (And (And (And (perp D C (skS.0 4 a) B) (coll D (skS.0 4 a) B)) (perp E B (skS.0 4 a) C)) % 214.97/215.17 (coll E (skS.0 4 a) C)) % 214.97/215.17 (midp F C B)) % 214.97/215.17 (midp G D E) → % 214.97/215.17 perp F G D E) % 214.97/215.17 False % 214.97/215.17 Clause #461 (by clausification #[460]): ∀ (a a_1 : Iota), % 214.97/215.17 Eq % 214.97/215.17 (Not % 214.97/215.17 (∀ (C D E F G : Iota), % 214.97/215.17 And % 214.97/215.17 (And % 214.97/215.17 (And % 214.97/215.17 (And (And (perp D C (skS.0 4 a) (skS.0 5 a a_1)) (coll D (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.17 (perp E (skS.0 5 a a_1) (skS.0 4 a) C)) % 214.97/215.17 (coll E (skS.0 4 a) C)) % 214.97/215.17 (midp F C (skS.0 5 a a_1))) % 214.97/215.17 (midp G D E) → % 214.97/215.17 perp F G D E)) % 214.97/215.17 True % 214.97/215.17 Clause #462 (by clausification #[461]): ∀ (a a_1 : Iota), % 214.97/215.17 Eq % 214.97/215.17 (∀ (C D E F G : Iota), % 214.97/215.17 And % 214.97/215.17 (And % 214.97/215.17 (And % 214.97/215.17 (And (And (perp D C (skS.0 4 a) (skS.0 5 a a_1)) (coll D (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp E (skS.0 5 a a_1) (skS.0 4 a) C)) % 214.97/215.20 (coll E (skS.0 4 a) C)) % 214.97/215.20 (midp F C (skS.0 5 a a_1))) % 214.97/215.20 (midp G D E) → % 214.97/215.20 perp F G D E) % 214.97/215.20 False % 214.97/215.20 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (Not % 214.97/215.20 (∀ (D E F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (And (perp D (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) (coll D (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp E (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll E (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G D E) → % 214.97/215.20 perp F G D E)) % 214.97/215.20 True % 214.97/215.20 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (∀ (D E F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (And (perp D (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) (coll D (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp E (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll E (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G D E) → % 214.97/215.20 perp F G D E) % 214.97/215.20 False % 214.97/215.20 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (Not % 214.97/215.20 (∀ (E F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 214.97/215.20 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp E (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll E (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G (skS.0 7 a a_1 a_2 a_3) E) → % 214.97/215.20 perp F G (skS.0 7 a a_1 a_2 a_3) E)) % 214.97/215.20 True % 214.97/215.20 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (∀ (E F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 214.97/215.20 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp E (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll E (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G (skS.0 7 a a_1 a_2 a_3) E) → % 214.97/215.20 perp F G (skS.0 7 a a_1 a_2 a_3) E) % 214.97/215.20 False % 214.97/215.20 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (Not % 214.97/215.20 (∀ (F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 214.97/215.20 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 214.97/215.20 perp F G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4))) % 214.97/215.20 True % 214.97/215.20 Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 214.97/215.20 Eq % 214.97/215.20 (∀ (F G : Iota), % 214.97/215.20 And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And % 214.97/215.20 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 214.97/215.20 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 214.97/215.20 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 214.97/215.20 (midp F (skS.0 6 a a_1 a_2) (skS.0 5 a a_1))) % 214.97/215.20 (midp G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 214.97/215.20 perp F G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.04/215.23 False % 215.04/215.23 Clause #469 (by clausification #[468]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.04/215.23 Eq % 215.04/215.23 (Not % 215.04/215.23 (∀ (G : Iota), % 215.04/215.23 And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.23 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.23 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (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))) % 215.04/215.23 (midp G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 215.04/215.23 perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4))) % 215.04/215.23 True % 215.04/215.23 Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.04/215.23 Eq % 215.04/215.23 (∀ (G : Iota), % 215.04/215.23 And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.23 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.23 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (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))) % 215.04/215.23 (midp G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 215.04/215.23 perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) G (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.04/215.23 False % 215.04/215.23 Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.23 Eq % 215.04/215.23 (Not % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.23 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.23 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (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))) % 215.04/215.23 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 215.04/215.23 perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) % 215.04/215.23 (skS.0 8 a a_1 a_2 a_3 a_4))) % 215.04/215.23 True % 215.04/215.23 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.23 Eq % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.23 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.23 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (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))) % 215.04/215.23 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) → % 215.04/215.23 perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) % 215.04/215.23 (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.04/215.23 False % 215.04/215.23 Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.23 Eq % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And % 215.04/215.23 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.23 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.23 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.23 (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))) % 215.04/215.23 (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4))) % 215.04/215.23 True % 215.04/215.23 Clause #474 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.26 Eq % 215.04/215.26 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) % 215.04/215.26 (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.04/215.26 False % 215.04/215.26 Clause #475 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.26 Eq (midp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4)) True % 215.04/215.26 Clause #476 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.04/215.26 Eq % 215.04/215.26 (And % 215.04/215.26 (And % 215.04/215.26 (And % 215.04/215.26 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 215.04/215.26 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 215.04/215.26 (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.26 (coll (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 215.04/215.26 (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))) % 215.04/215.26 True % 215.04/215.26 Clause #479 (by superposition #[475, 129]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.26 Or (Eq True False) % 215.04/215.26 (Eq % 215.04/215.26 (cong (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) % 215.04/215.26 (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.04/215.26 True) % 215.04/215.26 Clause #485 (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 % 215.04/215.26 Clause #486 (by clausification #[485]): ∀ (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 % 215.04/215.26 Clause #487 (by clausification #[486]): ∀ (a a_1 a_2 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #488 (by clausification #[487]): ∀ (a a_1 a_2 a_3 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #489 (by clausification #[488]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #490 (by clausification #[489]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #491 (by clausification #[490]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.04/215.26 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) % 215.04/215.26 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.04/215.26 Or (Eq (cong a a_1 a_2 a_3) True) % 215.04/215.26 (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)) % 215.04/215.26 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 % 215.04/215.26 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 % 215.04/215.26 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 % 215.04/215.26 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 % 215.04/215.26 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #510 (by clausification #[509]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.04/215.26 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 % 215.04/215.26 Clause #511 (by clausification #[510]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.04/215.26 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 % 215.08/215.29 Clause #512 (by clausification #[511]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #513 (by clausification #[512]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.29 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) % 215.08/215.29 Clause #586 (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 % 215.08/215.29 Clause #587 (by clausification #[586]): ∀ (a a_1 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #588 (by clausification #[587]): ∀ (a a_1 a_2 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #589 (by clausification #[588]): ∀ (a a_1 a_2 a_3 : Iota), % 215.08/215.29 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) % 215.08/215.29 True % 215.08/215.29 Clause #590 (by clausification #[589]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #591 (by clausification #[590]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.29 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) % 215.08/215.29 (Eq (eqratio a_4 a a a_2 a_4 a_1 a_1 a_3) True) % 215.08/215.29 Clause #592 (by clausification #[591]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.29 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 215.08/215.29 (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)) % 215.08/215.29 Clause #593 (by clausification #[592]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.29 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 215.08/215.29 (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))) % 215.08/215.29 Clause #608 (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 % 215.08/215.29 Clause #609 (by clausification #[608]): ∀ (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 % 215.08/215.29 Clause #610 (by clausification #[609]): ∀ (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 % 215.08/215.29 Clause #611 (by clausification #[610]): ∀ (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 % 215.08/215.29 Clause #612 (by clausification #[611]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #613 (by clausification #[612]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #614 (by clausification #[613]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #615 (by clausification #[614]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.29 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 % 215.08/215.29 Clause #616 (by clausification #[615]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.29 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) % 215.08/215.29 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 % 215.08/215.29 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 % 215.08/215.29 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 % 215.08/215.29 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 % 215.08/215.29 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 % 215.08/215.31 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 % 215.08/215.31 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) % 215.08/215.31 Clause #655 (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 % 215.08/215.31 Clause #656 (by clausification #[655]): ∀ (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 % 215.08/215.31 Clause #657 (by clausification #[656]): ∀ (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 % 215.08/215.31 Clause #658 (by clausification #[657]): ∀ (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 % 215.08/215.31 Clause #659 (by clausification #[658]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #660 (by clausification #[659]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #661 (by clausification #[660]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #662 (by clausification #[661]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #663 (by clausification #[662]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.31 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) % 215.08/215.31 Clause #713 (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 % 215.08/215.31 Clause #714 (by clausification #[713]): ∀ (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 % 215.08/215.31 Clause #715 (by clausification #[714]): ∀ (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 % 215.08/215.31 Clause #716 (by clausification #[715]): ∀ (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 % 215.08/215.31 Clause #717 (by clausification #[716]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #718 (by clausification #[717]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #719 (by clausification #[718]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #720 (by clausification #[719]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.31 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 % 215.08/215.31 Clause #721 (by clausification #[720]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.31 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) % 215.08/215.31 Clause #731 (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 % 215.08/215.31 Clause #732 (by clausification #[731]): ∀ (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 % 215.08/215.31 Clause #733 (by clausification #[732]): ∀ (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 % 215.08/215.31 Clause #734 (by clausification #[733]): ∀ (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 % 215.08/215.31 Clause #735 (by clausification #[734]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.34 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 % 215.08/215.34 Clause #736 (by clausification #[735]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.08/215.34 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 % 215.08/215.34 Clause #737 (by clausification #[736]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.08/215.34 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 % 215.08/215.34 Clause #738 (by clausification #[737]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.34 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 % 215.08/215.34 Clause #739 (by clausification #[738]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.34 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) % 215.08/215.34 Clause #777 (by clausification #[29]): ∀ (a : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (B C D E F G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #778 (by clausification #[777]): ∀ (a a_1 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (C D E F G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #779 (by clausification #[778]): ∀ (a a_1 a_2 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (D E F G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #780 (by clausification #[779]): ∀ (a a_1 a_2 a_3 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (E F G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #781 (by clausification #[780]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (F G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #782 (by clausification #[781]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (G H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #783 (by clausification #[782]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (H P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #784 (by clausification #[783]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (P Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #785 (by clausification #[784]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (Q U V : Iota), % 215.08/215.34 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) % 215.08/215.34 True % 215.08/215.34 Clause #786 (by clausification #[785]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (U V : Iota), % 215.08/215.34 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) → % 215.08/215.34 eqratio a a_1 a_2 a_3 a_6 a_7 a_8 a_9) % 215.08/215.34 True % 215.08/215.34 Clause #787 (by clausification #[786]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (∀ (V : Iota), % 215.08/215.34 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) → % 215.08/215.34 eqratio a a_1 a_2 a_3 a_7 a_8 a_9 a_10) % 215.08/215.34 True % 215.08/215.34 Clause #788 (by clausification #[787]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 215.08/215.34 Eq % 215.08/215.34 (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) → % 215.08/215.34 eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) % 215.08/215.34 True % 215.08/215.34 Clause #789 (by clausification #[788]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 215.08/215.34 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) % 215.08/215.34 (Eq (eqratio a a_1 a_2 a_3 a_8 a_9 a_10 a_11) True) % 215.08/215.34 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 a_11 : Iota), % 215.08/215.34 Or (Eq (eqratio a a_1 a_2 a_3 a_4 a_5 a_6 a_7) True) % 215.16/215.37 (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)) % 215.16/215.37 Clause #874 (by clausification #[476]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (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)) True % 215.16/215.37 Clause #877 (by superposition #[874, 111]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 215.16/215.37 Or (Eq True False) (Eq (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) True) % 215.16/215.37 Clause #886 (by clausification #[877]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (midp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) True % 215.16/215.37 Clause #891 (by superposition #[886, 283]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.16/215.37 Or (Eq (para (skS.0 5 a a_1) a_2 (skS.0 6 a a_1 a_3) a_4) True) % 215.16/215.37 (Or (Eq True False) (Eq (midp (skS.0 9 a a_1 a_3 a_5 a_6 a_7) a_2 a_4) False)) % 215.16/215.37 Clause #967 (by clausification #[891]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 215.16/215.37 Or (Eq (para (skS.0 5 a a_1) a_2 (skS.0 6 a a_1 a_3) a_4) True) % 215.16/215.37 (Eq (midp (skS.0 9 a a_1 a_3 a_5 a_6 a_7) a_2 a_4) False) % 215.16/215.37 Clause #968 (by superposition #[967, 874]): ∀ (a a_1 a_2 : Iota), % 215.16/215.37 Or (Eq (para (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)) True) (Eq False True) % 215.16/215.37 Clause #970 (by clausification #[479]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.16/215.37 Eq % 215.16/215.37 (cong (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) % 215.16/215.37 (skS.0 8 a a_1 a_2 a_3 a_4)) % 215.16/215.37 True % 215.16/215.37 Clause #995 (by clausification #[968]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1)) True % 215.16/215.37 Clause #1001 (by superposition #[995, 646]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4) True) % 215.16/215.37 Clause #1257 (by clausification #[1001]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4) True % 215.16/215.37 Clause #1259 (by superposition #[1257, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4 a_3 a_4) True) % 215.16/215.37 Clause #1261 (by clausification #[1259]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4 a_3 a_4) True % 215.16/215.37 Clause #1264 (by superposition #[1261, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle a a_1 a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3)) True) % 215.16/215.37 Clause #1274 (by clausification #[1264]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle a a_1 a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3)) True % 215.16/215.37 Clause #1276 (by superposition #[1274, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True) % 215.16/215.37 Clause #1281 (by clausification #[1276]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle a a_1 a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True % 215.16/215.37 Clause #1284 (by superposition #[1281, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True) % 215.16/215.37 Clause #1288 (by clausification #[1284]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True % 215.16/215.37 Clause #1289 (by superposition #[1288, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Or (Eq True False) % 215.16/215.37 (Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) a_1 a (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True) % 215.16/215.37 Clause #1293 (by clausification #[1289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.16/215.37 Eq (eqangle a a_1 (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3) a_1 a (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True % 215.16/215.37 Clause #1297 (by superposition #[1293, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3)) True) % 215.20/215.40 Clause #1302 (by clausification #[1297]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 6 a_2 a_3 a_4) (skS.0 5 a_2 a_3)) True % 215.20/215.40 Clause #1305 (by superposition #[1302, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_4 a_3) True) % 215.20/215.40 Clause #1312 (by clausification #[1305]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_4 a_3) True % 215.20/215.40 Clause #1315 (by superposition #[1312, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4 a_4 a_3) True) % 215.20/215.40 Clause #1318 (by clausification #[1315]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) a_3 a_4 a_4 a_3) True % 215.20/215.40 Clause #1320 (by superposition #[1318, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True) % 215.20/215.40 Clause #1325 (by clausification #[1320]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True % 215.20/215.40 Clause #1326 (by superposition #[1325, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True) % 215.20/215.40 Clause #1331 (by clausification #[1326]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 a_4 a_3) True % 215.20/215.40 Clause #1338 (by superposition #[1331, 513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_4 a_3) True) % 215.20/215.40 Clause #1343 (by clausification #[1338]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) a_4 a_3) True % 215.20/215.40 Clause #1348 (by superposition #[1343, 397]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Or (Eq True False) % 215.20/215.40 (Eq (eqangle a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True) % 215.20/215.40 Clause #1361 (by clausification #[1348]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.40 Eq (eqangle a a_1 (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 5 a_2 a_3) (skS.0 6 a_2 a_3 a_4)) True % 215.20/215.40 Clause #1366 (by superposition #[1361, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 215.20/215.40 Clause #1374 (by clausification #[1366]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 215.20/215.40 Clause #1377 (by superposition #[1374, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 215.20/215.40 Clause #1391 (by clausification #[1377]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 215.20/215.40 Clause #1392 (by superposition #[1391, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 215.20/215.40 Clause #1397 (by clausification #[1392]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 215.20/215.40 Clause #1400 (by superposition #[1397, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 215.20/215.40 Clause #1425 (by clausification #[1400]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 215.20/215.40 Clause #1428 (by superposition #[1425, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 215.20/215.40 Clause #1437 (by clausification #[1428]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 215.20/215.40 Clause #1439 (by superposition #[1437, 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)) % 215.20/215.40 Clause #1506 (by clausification #[1439]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 215.20/215.40 Clause #1509 (by superposition #[1506, 1437]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 215.20/215.43 Clause #1510 (by clausification #[1509]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 215.20/215.43 Clause #1523 (by backward demodulation #[1510, 593]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.43 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) % 215.20/215.43 (Or (Eq True False) (Or (Eq (para a_1 a_3 a_2 a_4) False) (Eq (coll a a_1 a_2) False))) % 215.20/215.43 Clause #2512 (by clausification #[1523]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.43 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) (Or (Eq (para a_1 a_3 a_2 a_4) False) (Eq (coll a a_1 a_2) False)) % 215.20/215.43 Clause #2513 (by forward demodulation #[2512, 1510]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 215.20/215.43 Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) (Or (Eq (para a_1 a_3 a_2 a_4) False) (Eq True False)) % 215.20/215.43 Clause #2514 (by clausification #[2513]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a_3 a_3 a_4) True) (Eq (para a_1 a_3 a_2 a_4) False) % 215.20/215.43 Clause #2517 (by superposition #[2514, 1374]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_2 a a_2 a_2 a_1) True) (Eq False True) % 215.20/215.43 Clause #2518 (by superposition #[2514, 1391]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a_1 a a_2 a_2 a_2) True) (Eq False True) % 215.20/215.43 Clause #2519 (by clausification #[2518]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a a_2 a_2 a_2) True % 215.20/215.43 Clause #2524 (by superposition #[2519, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a_2) True) % 215.20/215.43 Clause #2526 (by clausification #[2524]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a_2) True % 215.20/215.43 Clause #2528 (by superposition #[2526, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a a_2 a_2) True) % 215.20/215.43 Clause #2529 (by superposition #[2526, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a_2 a a_2 a_1) True) % 215.20/215.43 Clause #2531 (by clausification #[2529]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a_2 a a_2 a_1) True % 215.20/215.43 Clause #2532 (by superposition #[2531, 494]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a_1 a_1) True) (Or (Eq True False) (Eq (cong a_2 a a_2 a_1) False)) % 215.20/215.43 Clause #2534 (by clausification #[2528]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a a_2 a_2) True % 215.20/215.43 Clause #2536 (by superposition #[2534, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_1 a_1 a_2 a_2) True) % 215.20/215.43 Clause #2537 (by superposition #[2534, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_1 a a_2 a_2 a_1) True) % 215.20/215.43 Clause #2543 (by clausification #[2537]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_1 a a_2 a_2 a_1) True % 215.20/215.43 Clause #2546 (by superposition #[2543, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a_1 a_2) True) % 215.20/215.43 Clause #2548 (by clausification #[2546]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_1 a_2) True % 215.20/215.43 Clause #2550 (by superposition #[2548, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a_2 a_2 a_1) True) % 215.20/215.43 Clause #2552 (by clausification #[2550]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a_2 a_2 a_1) True % 215.20/215.43 Clause #2554 (by superposition #[2552, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_2) True) % 215.20/215.43 Clause #2556 (by clausification #[2554]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_2) True % 215.20/215.43 Clause #2558 (by superposition #[2556, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_1 a_2 a_2) True) % 215.20/215.43 Clause #2560 (by clausification #[2558]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_2 a_1 a_2 a_2) True % 215.20/215.43 Clause #2562 (by superposition #[2560, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a a_1 a_2 a_2 a_2 a_1) True) % 215.20/215.43 Clause #2575 (by clausification #[2562]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a a_1 a_2 a_2 a_2 a_1) True % 215.20/215.43 Clause #2576 (by superposition #[2575, 494]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a a_1) True) (Or (Eq True False) (Eq (cong a_2 a_2 a_2 a_1) False)) % 215.20/215.43 Clause #2581 (by clausification #[2536]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_1 a_1 a_2 a_2) True % 215.20/215.43 Clause #2583 (by superposition #[2581, 790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.26/215.45 Or (Eq (eqratio a a_1 a_2 a a_3 a_4 a_5 a_6) True) % 215.26/215.45 (Or (Eq True False) (Eq (eqratio a_1 a_1 a_2 a_2 a_3 a_4 a_5 a_6) False)) % 215.26/215.45 Clause #2595 (by clausification #[2517]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a_2 a_2 a_1) True % 215.26/215.45 Clause #2600 (by superposition #[2595, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a_2 a_2 a_1) True) % 215.26/215.45 Clause #2602 (by clausification #[2600]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a_2 a_2 a_1) True % 215.26/215.45 Clause #2605 (by superposition #[2602, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_2 a a_2 a_1) True) % 215.26/215.45 Clause #2608 (by clausification #[2605]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a a_2 a_1) True % 215.26/215.45 Clause #2610 (by superposition #[2608, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_2 a_1 a_2 a) True) % 215.26/215.45 Clause #2612 (by clausification #[2610]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_1 a_2 a) True % 215.26/215.45 Clause #2616 (by superposition #[2612, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a a_1 a_2 a) True) % 215.26/215.45 Clause #2618 (by clausification #[2616]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a a_1 a_2 a) True % 215.26/215.45 Clause #2621 (by superposition #[2618, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a_1 a_2 a_1) True) % 215.26/215.45 Clause #2623 (by clausification #[2621]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a a_1 a_2 a_1) True % 215.26/215.45 Clause #2626 (by superposition #[2623, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a_2 a_1 a_2) True) % 215.26/215.45 Clause #2628 (by clausification #[2626]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a_2 a_1 a_2) True % 215.26/215.45 Clause #2631 (by superposition #[2628, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a_2 a_1 a_2) True) % 215.26/215.45 Clause #2638 (by clausification #[2631]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a_2 a_1 a_2) True % 215.26/215.45 Clause #2640 (by superposition #[2638, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a_2 a a_2) True) % 215.26/215.45 Clause #2642 (by clausification #[2640]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a_2 a a_2) True % 215.26/215.45 Clause #2645 (by superposition #[2642, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a_2 a_2 a_1) True) % 215.26/215.45 Clause #2647 (by clausification #[2645]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a a_2 a_2 a_1) True % 215.26/215.45 Clause #2651 (by superposition #[2647, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a_1 a_2 a_1) True) % 215.26/215.45 Clause #2653 (by clausification #[2651]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a a_1 a_2 a_1) True % 215.26/215.45 Clause #2656 (by superposition #[2653, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a a_1 a a_2) True) % 215.26/215.45 Clause #2658 (by clausification #[2656]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a a_1 a a_2) True % 215.26/215.45 Clause #2661 (by superposition #[2658, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_2 a a_2 a_1) True) % 215.26/215.45 Clause #2664 (by clausification #[2661]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_2 a a_2 a_1) True % 215.26/215.45 Clause #2666 (by superposition #[2664, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_2 a_1 a_2 a) True) % 215.26/215.45 Clause #2668 (by clausification #[2666]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_2 a_1 a_2 a) True % 215.26/215.45 Clause #2672 (by superposition #[2668, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_2 a a_2 a) True) % 215.26/215.45 Clause #2674 (by clausification #[2672]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_2 a a_2 a) True % 215.26/215.45 Clause #2677 (by superposition #[2674, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_2 a a_2) True) % 215.26/215.45 Clause #2679 (by clausification #[2677]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_2 a a_2) True % 215.26/215.45 Clause #2682 (by superposition #[2679, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a_2 a_1 a_2) True) % 215.27/215.48 Clause #2684 (by clausification #[2682]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a a_2 a_1 a_2) True % 215.27/215.48 Clause #2687 (by superposition #[2684, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a_1 a_1 a_2) True) % 215.27/215.48 Clause #2700 (by clausification #[2687]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a a_1 a_1 a_2) True % 215.27/215.48 Clause #2702 (by superposition #[2700, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a a a_2) True) % 215.27/215.48 Clause #2704 (by clausification #[2702]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a a a_2) True % 215.27/215.48 Clause #2706 (by superposition #[2704, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_2 a_1 a a_2) True) % 215.27/215.48 Clause #2708 (by clausification #[2706]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_2 a_1 a a_2) True % 215.27/215.48 Clause #2711 (by superposition #[2708, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_2 a a a_2) True) % 215.27/215.48 Clause #2713 (by clausification #[2711]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_2 a a a_2) True % 215.27/215.48 Clause #2715 (by superposition #[2713, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_2 a_1 a_1 a_2) True) % 215.27/215.48 Clause #2717 (by clausification #[2715]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a a_2 a_1 a_1 a_2) True % 215.27/215.48 Clause #2720 (by superposition #[2717, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a a_2 a_1 a a_2) True) % 215.27/215.48 Clause #2724 (by clausification #[2720]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_1 a a_2) True % 215.27/215.48 Clause #2907 (by clausification #[2576]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a a_1) True) (Eq (cong a_2 a_2 a_2 a_1) False) % 215.27/215.48 Clause #2912 (by clausification #[2532]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq (cong a_2 a a_2 a_1) False) % 215.27/215.48 Clause #3065 (by clausification #[2583]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.27/215.48 Or (Eq (eqratio a a_1 a_2 a a_3 a_4 a_5 a_6) True) (Eq (eqratio a_1 a_1 a_2 a_2 a_3 a_4 a_5 a_6) False) % 215.27/215.48 Clause #3066 (by superposition #[3065, 2519]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_2) True) (Eq False True) % 215.27/215.48 Clause #3078 (by superposition #[3065, 2724]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_1 a_1 a_2) True) (Eq False True) % 215.27/215.48 Clause #3079 (by clausification #[3078]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_1 a_1 a_2) True % 215.27/215.48 Clause #3084 (by superposition #[3079, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_1 a a_1 a_2) True) % 215.27/215.48 Clause #3088 (by clausification #[3084]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_1 a_1 a a_1 a_2) True % 215.27/215.48 Clause #3091 (by superposition #[3088, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a a_2 a) True) % 215.27/215.48 Clause #3095 (by clausification #[3091]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a a_2 a) True % 215.27/215.48 Clause #3097 (by superposition #[3095, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a_1 a_2 a_1) True) % 215.27/215.48 Clause #3099 (by clausification #[3097]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a_1 a_2 a_1) True % 215.27/215.48 Clause #3103 (by superposition #[3099, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_2 a_2 a_1) True) % 215.27/215.48 Clause #3106 (by clausification #[3103]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_2 a_2 a_1) True % 215.27/215.48 Clause #3111 (by superposition #[3106, 3065]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_1) True) (Eq True False) % 215.27/215.48 Clause #3112 (by clausification #[3111]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_1) True % 215.27/215.48 Clause #3114 (by superposition #[3112, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a a_2 a_2 a) True) % 215.27/215.48 Clause #3185 (by clausification #[3114]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a a_2 a_2 a) True % 215.27/215.48 Clause #3187 (by superposition #[3185, 790]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.27/215.48 Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_5) True) % 215.27/215.48 (Or (Eq True False) (Eq (eqratio a a_6 a_6 a a_2 a_3 a_4 a_5) False)) % 215.27/215.50 Clause #3301 (by clausification #[3066]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_2) True % 215.27/215.50 Clause #3306 (by superposition #[3301, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a_1 a a_2 a_2) True) % 215.27/215.50 Clause #3310 (by clausification #[3306]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a_1 a a_2 a_2) True % 215.27/215.50 Clause #3312 (by superposition #[3310, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a a_1 a_2 a_2) True) % 215.27/215.50 Clause #3334 (by clausification #[3312]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a a_1 a_2 a_2) True % 215.27/215.50 Clause #3337 (by superposition #[3334, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a a_1 a a_2) True) % 215.27/215.50 Clause #3339 (by clausification #[3337]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_2 a_2 a a_1 a a_2) True % 215.27/215.50 Clause #3343 (by superposition #[3339, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_2 a_2 a a_2) True) % 215.27/215.50 Clause #3351 (by clausification #[3343]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_2 a a_2) True % 215.27/215.50 Clause #3356 (by superposition #[3351, 3065]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_2 a_1 a_2) True) (Eq True False) % 215.27/215.50 Clause #3357 (by clausification #[3356]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_2 a_1 a_2) True % 215.27/215.50 Clause #3360 (by superposition #[3357, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a a_2 a_1 a_1 a_2) True) % 215.27/215.50 Clause #3362 (by clausification #[3360]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a a_2 a_1 a_1 a_2) True % 215.27/215.50 Clause #3365 (by superposition #[3362, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a a_1 a_2 a_2 a a_2 a_1) True) % 215.27/215.50 Clause #3367 (by clausification #[3365]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a a_1 a_2 a_2 a a_2 a_1) True % 215.27/215.50 Clause #3369 (by superposition #[3367, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a) True) % 215.27/215.50 Clause #3371 (by clausification #[3369]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a_1 a_2 a) True % 215.27/215.50 Clause #3374 (by superposition #[3371, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_2 a_1 a a_2 a_2) True) % 215.27/215.50 Clause #3379 (by clausification #[3374]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_2 a_1 a a_2 a_2) True % 215.27/215.50 Clause #3381 (by superposition #[3379, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_2 a a_1 a_2 a_2) True) % 215.27/215.50 Clause #3383 (by clausification #[3381]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_2 a a_1 a_2 a_2) True % 215.27/215.50 Clause #3387 (by superposition #[3383, 739]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_1 a_2 a_2 a_2) True) % 215.27/215.50 Clause #3389 (by clausification #[3387]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_1 a_2 a_2 a_2) True % 215.27/215.50 Clause #3392 (by superposition #[3389, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a) True) % 215.27/215.50 Clause #3394 (by clausification #[3392]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a) True % 215.27/215.50 Clause #3396 (by superposition #[3394, 616]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a a_2 a_1 a_2 a_1) True) % 215.27/215.50 Clause #3411 (by clausification #[3396]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a a_2 a_1 a_2 a_1) True % 215.27/215.50 Clause #3414 (by superposition #[3411, 721]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_2 a_1 a_2 a_2) True) % 215.27/215.50 Clause #3425 (by clausification #[3414]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_1 a_2 a_2) True % 215.27/215.50 Clause #3428 (by superposition #[3425, 663]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a a_1 a_2 a_2 a_2 a_1) True) % 215.27/215.50 Clause #3431 (by clausification #[3428]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_2 a_2 a_1) True % 215.27/215.50 Clause #3434 (by superposition #[3431, 3065]): ∀ (a a_1 a_2 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_2 a_2 a_1) True) (Eq True False) % 215.27/215.50 Clause #3435 (by clausification #[3434]): ∀ (a a_1 a_2 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_2 a_2 a_1) True % 215.32/215.53 Clause #3792 (by clausification #[3187]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 215.32/215.53 Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_5) True) (Eq (eqratio a a_6 a_6 a a_2 a_3 a_4 a_5) False) % 215.32/215.53 Clause #3820 (by superposition #[3792, 3435]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_2 a_2 a_3) True) (Eq False True) % 215.32/215.53 Clause #3821 (by clausification #[3820]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_2 a_2 a_3) True % 215.32/215.53 Clause #3828 (by superposition #[3821, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_2 a_2 a_3) True) (Eq True False) % 215.32/215.53 Clause #3830 (by clausification #[3828]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_2 a_2 a_3) True % 215.32/215.53 Clause #3835 (by superposition #[3830, 739]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_2 a_1 a a_2 a_3) True) % 215.32/215.53 Clause #3837 (by clausification #[3835]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a_2 a_1 a a_2 a_3) True % 215.32/215.53 Clause #3842 (by superposition #[3837, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_2 a a_1 a_1 a_2 a_3) True) (Eq True False) % 215.32/215.53 Clause #3846 (by clausification #[3842]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a_1 a_1 a_2 a_3) True % 215.32/215.53 Clause #3851 (by superposition #[3846, 739]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_3) True) % 215.32/215.53 Clause #3855 (by clausification #[3851]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a_1 a_2 a a_2 a_3) True % 215.32/215.53 Clause #3863 (by superposition #[3855, 3792]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a a_2 a_3) True) (Eq True False) % 215.32/215.53 Clause #3864 (by clausification #[3863]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a_2 a a_2 a_3) True % 215.32/215.53 Clause #3869 (by superposition #[3864, 739]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a a_1 a_2 a_3) True) % 215.32/215.53 Clause #3875 (by clausification #[3869]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_2 a a a_1 a_2 a_3) True % 215.32/215.53 Clause #3882 (by superposition #[3875, 3792]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a a_2 a_2 a_3) True) (Eq True False) % 215.32/215.53 Clause #3883 (by clausification #[3882]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a a_2 a_2 a_3) True % 215.32/215.53 Clause #3890 (by superposition #[3883, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_3) True) (Eq True False) % 215.32/215.53 Clause #3891 (by clausification #[3890]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a a_1 a_2 a_2 a_3) True % 215.32/215.53 Clause #3898 (by superposition #[3891, 3792]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_3 a_4) True) (Eq True False) % 215.32/215.53 Clause #3899 (by clausification #[3898]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a_3 a_4) True % 215.32/215.53 Clause #3906 (by superposition #[3899, 3065]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_3 a_3 a_4) True) (Eq True False) % 215.32/215.53 Clause #3907 (by clausification #[3906]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_3 a_3 a_4) True % 215.32/215.53 Clause #3912 (by superposition #[3907, 739]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a a_3 a_4) True) % 215.32/215.53 Clause #3917 (by clausification #[3912]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a a_3 a_4) True % 215.32/215.53 Clause #3920 (by superposition #[3917, 721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a a_4 a_2) True) % 215.32/215.53 Clause #3924 (by clausification #[3920]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a a_4 a_2) True % 215.32/215.53 Clause #3930 (by superposition #[3924, 3792]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a a_3 a_2) True) (Eq True False) % 215.32/215.53 Clause #3931 (by clausification #[3930]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a_2 a a_3 a_2) True % 215.32/215.53 Clause #3938 (by superposition #[3931, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_1 a_3 a_2) True) (Eq True False) % 215.32/215.53 Clause #3939 (by clausification #[3938]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_1 a_3 a_2) True % 215.32/215.53 Clause #3946 (by superposition #[3939, 3792]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_2) True) (Eq True False) % 215.36/215.55 Clause #3952 (by clausification #[3946]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_2) True % 215.36/215.55 Clause #3956 (by superposition #[3952, 3065]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_3 a_4 a_2) True) (Eq True False) % 215.36/215.55 Clause #3957 (by clausification #[3956]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_3 a_4 a_2) True % 215.36/215.55 Clause #3959 (by superposition #[3957, 721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a a_3 a_4 a_4 a_3) True) % 215.36/215.55 Clause #3961 (by clausification #[3959]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a a_3 a_4 a_4 a_3) True % 215.36/215.55 Clause #3963 (by superposition #[3961, 616]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_4 a_3) True) % 215.36/215.55 Clause #3970 (by clausification #[3963]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_4 a_3) True % 215.36/215.55 Clause #3973 (by superposition #[3970, 739]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_3 a_2) True) % 215.36/215.55 Clause #3975 (by clausification #[3973]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_3 a_2) True % 215.36/215.55 Clause #3980 (by superposition #[3975, 3792]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a a_3) True) (Eq True False) % 215.36/215.55 Clause #3981 (by clausification #[3980]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a a_3) True % 215.36/215.55 Clause #3988 (by superposition #[3981, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_3 a_1 a_3) True) (Eq True False) % 215.36/215.55 Clause #3989 (by clausification #[3988]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_3 a_1 a_3) True % 215.36/215.55 Clause #3996 (by superposition #[3989, 3792]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_3) True) (Eq True False) % 215.36/215.55 Clause #3997 (by clausification #[3996]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a_4 a_3) True % 215.36/215.55 Clause #4000 (by superposition #[3997, 721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_3 a_4) True) % 215.36/215.55 Clause #4012 (by clausification #[4000]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_1 a_3 a_4 a_3 a_4) True % 215.36/215.55 Clause #4014 (by superposition #[4012, 739]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_2 a_3) True) % 215.36/215.55 Clause #4020 (by clausification #[4014]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a_1 a_2 a_3) True % 215.36/215.55 Clause #4022 (by superposition #[4020, 616]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_4 a a_2 a_3) True) % 215.36/215.55 Clause #4027 (by clausification #[4022]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_4 a a_2 a_3) True % 215.36/215.55 Clause #4029 (by superposition #[4027, 721]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a_1 a_4 a_2 a_3) True) % 215.36/215.55 Clause #4033 (by clausification #[4029]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a_1 a_4 a_2 a_3) True % 215.36/215.55 Clause #4038 (by superposition #[4033, 3792]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_2 a) True) (Eq True False) % 215.36/215.55 Clause #4039 (by clausification #[4038]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a_2 a) True % 215.36/215.55 Clause #4044 (by superposition #[4039, 3065]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (eqratio a a_1 a_1 a a_2 a_3 a_2 a_1) True) (Eq True False) % 215.36/215.55 Clause #4056 (by clausification #[4044]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqratio a a_1 a_1 a a_2 a_3 a_2 a_1) True % 215.36/215.55 Clause #4062 (by superposition #[4056, 3792]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (eqratio a a_1 a a_1 a_2 a_3 a_2 a_4) True) (Eq True False) % 215.36/215.55 Clause #4063 (by clausification #[4062]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a a_1 a_2 a_3 a_2 a_4) True % 215.36/215.55 Clause #4064 (by superposition #[4063, 494]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cong a a_1 a a_1) True) (Or (Eq True False) (Eq (cong a_2 a_3 a_2 a_4) False)) % 215.50/215.73 Clause #4068 (by superposition #[4063, 739]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq True False) (Eq (eqratio a a_1 a_2 a_3 a a_1 a_2 a_4) True) % 215.50/215.73 Clause #4089 (by clausification #[4068]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (eqratio a a_1 a_2 a_3 a a_1 a_2 a_4) True % 215.50/215.73 Clause #4090 (by superposition #[4089, 494]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a a_1 a_2 a_4) False)) % 215.50/215.73 Clause #4661 (by clausification #[4090]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq (cong a a_1 a_2 a_4) False) % 215.50/215.73 Clause #4667 (by clausification #[4064]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq (cong a_2 a_3 a_2 a_4) False) % 215.50/215.73 Clause #4668 (by superposition #[4667, 970]): ∀ (a a_1 : Iota), Or (Eq (cong a a_1 a a_1) True) (Eq False True) % 215.50/215.73 Clause #4669 (by clausification #[4668]): ∀ (a a_1 : Iota), Eq (cong a a_1 a a_1) True % 215.50/215.73 Clause #4686 (by superposition #[4669, 2907]): ∀ (a a_1 : Iota), Or (Eq (cong a a a a_1) True) (Eq True False) % 215.50/215.73 Clause #4749 (by clausification #[4686]): ∀ (a a_1 : Iota), Eq (cong a a a a_1) True % 215.50/215.73 Clause #4760 (by superposition #[4749, 2912]): ∀ (a a_1 : Iota), Or (Eq (cong a a a_1 a_1) True) (Eq True False) % 215.50/215.73 Clause #4845 (by clausification #[4760]): ∀ (a a_1 : Iota), Eq (cong a a a_1 a_1) True % 215.50/215.73 Clause #4854 (by superposition #[4845, 4661]): ∀ (a a_1 a_2 : Iota), Or (Eq (cong a a a_1 a_2) True) (Eq True False) % 215.50/215.73 Clause #4856 (by clausification #[4854]): ∀ (a a_1 a_2 : Iota), Eq (cong a a a_1 a_2) True % 215.50/215.73 Clause #4857 (by superposition #[4856, 194]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cong a a_1 a_2 a_2) True) % 215.50/215.73 Clause #4863 (by clausification #[4857]): ∀ (a a_1 a_2 : Iota), Eq (cong a a_1 a_2 a_2) True % 215.50/215.73 Clause #4875 (by superposition #[4863, 4661]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cong a a_1 a_2 a_3) True) (Eq True False) % 215.50/215.73 Clause #4876 (by clausification #[4875]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cong a a_1 a_2 a_3) True % 215.50/215.73 Clause #4884 (by superposition #[4876, 212]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cong a a_3 a_1 a_3) False)) % 215.50/215.73 Clause #8358 (by clausification #[4884]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Eq (cong a a_3 a_1 a_3) False) % 215.50/215.73 Clause #8359 (by superposition #[8358, 4876]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) True) (Eq False True) % 215.50/215.73 Clause #8360 (by clausification #[8359]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3) True % 215.50/215.73 Clause #8366 (by superposition #[8360, 474]): Eq True False % 215.50/215.73 Clause #8367 (by clausification #[8366]): False % 215.50/215.73 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------