%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO603+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:48:45 PM UTC 2025 % Result : Theorem 34.09s 34.29s % Output : Proof 34.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : GEO603+1 : TPTP v9.2.0. Released v7.5.0. % 0.08/0.13 % Command : duper %s % 0.12/0.34 % Computer : n002.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 12:35:23 EDT 2025 % 0.12/0.34 % CPUTime : % 34.09/34.29 SZS status Theorem for theBenchmark.p % 34.09/34.29 SZS output start Proof for theBenchmark.p % 34.09/34.29 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 34.09/34.29 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 34.09/34.29 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 34.09/34.29 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 34.09/34.29 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 34.09/34.29 Clause #5 (by assumption #[]): Eq (∀ (A B C D E F : Iota), And (para A B C D) (para C D E F) → para A B E F) True % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 34.09/34.29 Clause #94 (by assumption #[]): Eq % 34.09/34.29 (Not % 34.09/34.29 (∀ (A B C D E F G : Iota), % 34.09/34.29 And (And (And (And (circle D A B C) (coll E A B)) (para B C F E)) (coll F A C)) (circle G A E F) → coll A G D)) % 34.09/34.29 True % 34.09/34.29 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 34.09/34.29 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 34.09/34.29 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 % 34.09/34.29 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) % 34.09/34.29 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 34.09/34.29 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 34.09/34.29 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 % 34.09/34.29 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) % 34.09/34.29 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 34.09/34.29 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 34.09/34.29 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 % 34.09/34.29 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) % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.29 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) % 34.09/34.29 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)) % 34.09/34.29 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 34.09/34.29 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 % 34.09/34.29 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 % 34.09/34.31 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 % 34.09/34.31 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) % 34.09/34.31 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 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) % 34.09/34.31 Clause #220 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (B C D E F : Iota), And (para a B C D) (para C D E F) → para a B E F) True % 34.09/34.31 Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), Eq (∀ (C D E F : Iota), And (para a a_1 C D) (para C D E F) → para a a_1 E F) True % 34.09/34.31 Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E F : Iota), And (para a a_1 a_2 D) (para a_2 D E F) → para a a_1 E F) True % 34.09/34.31 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E F : Iota), And (para a a_1 a_2 a_3) (para a_2 a_3 E F) → para a a_1 E F) True % 34.09/34.31 Clause #224 (by clausification #[223]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (F : Iota), And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 F) → para a a_1 a_4 F) True % 34.09/34.31 Clause #225 (by clausification #[224]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 a_5) → para a a_1 a_4 a_5) True % 34.09/34.31 Clause #226 (by clausification #[225]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.09/34.31 Or (Eq (And (para a a_1 a_2 a_3) (para a_2 a_3 a_4 a_5)) False) (Eq (para a a_1 a_4 a_5) True) % 34.09/34.31 Clause #227 (by clausification #[226]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.09/34.31 Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (para a a_1 a_4 a_5) False) (Eq (para a_4 a_5 a_2 a_3) False)) % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.09/34.31 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 % 34.09/34.31 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.09/34.31 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 % 34.09/34.31 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.09/34.31 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 % 34.09/34.31 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.09/34.31 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 % 34.09/34.31 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.09/34.31 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) % 34.09/34.31 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 % 34.09/34.31 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 % 34.09/34.31 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 % 34.16/34.34 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 % 34.16/34.34 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 % 34.16/34.34 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 % 34.16/34.34 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) % 34.16/34.34 Clause #398 (by clausification #[94]): Eq % 34.16/34.34 (∀ (A B C D E F G : Iota), % 34.16/34.34 And (And (And (And (circle D A B C) (coll E A B)) (para B C F E)) (coll F A C)) (circle G A E F) → coll A G D) % 34.16/34.34 False % 34.16/34.34 Clause #399 (by clausification #[398]): ∀ (a : Iota), % 34.16/34.34 Eq % 34.16/34.34 (Not % 34.16/34.34 (∀ (B C D E F G : Iota), % 34.16/34.34 And (And (And (And (circle D (skS.0 2 a) B C) (coll E (skS.0 2 a) B)) (para B C F E)) (coll F (skS.0 2 a) C)) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D)) % 34.16/34.34 True % 34.16/34.34 Clause #400 (by clausification #[399]): ∀ (a : Iota), % 34.16/34.34 Eq % 34.16/34.34 (∀ (B C D E F G : Iota), % 34.16/34.34 And (And (And (And (circle D (skS.0 2 a) B C) (coll E (skS.0 2 a) B)) (para B C F E)) (coll F (skS.0 2 a) C)) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D) % 34.16/34.34 False % 34.16/34.34 Clause #401 (by clausification #[400]): ∀ (a a_1 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (Not % 34.16/34.34 (∀ (C D E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And (And (circle D (skS.0 2 a) (skS.0 3 a a_1) C) (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) C F E)) % 34.16/34.34 (coll F (skS.0 2 a) C)) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D)) % 34.16/34.34 True % 34.16/34.34 Clause #402 (by clausification #[401]): ∀ (a a_1 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (∀ (C D E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And (And (circle D (skS.0 2 a) (skS.0 3 a a_1) C) (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) C F E)) % 34.16/34.34 (coll F (skS.0 2 a) C)) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D) % 34.16/34.34 False % 34.16/34.34 Clause #403 (by clausification #[402]): ∀ (a a_1 a_2 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (Not % 34.16/34.34 (∀ (D E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And (And (circle D (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F E)) % 34.16/34.34 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D)) % 34.16/34.34 True % 34.16/34.34 Clause #404 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (∀ (D E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And (And (circle D (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F E)) % 34.16/34.34 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G D) % 34.16/34.34 False % 34.16/34.34 Clause #405 (by clausification #[404]): ∀ (a a_1 a_2 a_3 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (Not % 34.16/34.34 (∀ (E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And % 34.16/34.34 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.16/34.34 (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F E)) % 34.16/34.34 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.16/34.34 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3))) % 34.16/34.34 True % 34.16/34.34 Clause #406 (by clausification #[405]): ∀ (a a_1 a_2 a_3 : Iota), % 34.16/34.34 Eq % 34.16/34.34 (∀ (E F G : Iota), % 34.16/34.34 And % 34.16/34.34 (And % 34.16/34.34 (And % 34.16/34.34 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.16/34.34 (coll E (skS.0 2 a) (skS.0 3 a a_1))) % 34.16/34.34 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F E)) % 34.16/34.34 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.16/34.34 (circle G (skS.0 2 a) E F) → % 34.20/34.36 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3)) % 34.20/34.36 False % 34.20/34.36 Clause #407 (by clausification #[406]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (Not % 34.20/34.36 (∀ (F G : Iota), % 34.20/34.36 And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle G (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) F) → % 34.20/34.36 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3))) % 34.20/34.36 True % 34.20/34.36 Clause #408 (by clausification #[407]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (∀ (F G : Iota), % 34.20/34.36 And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) F (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll F (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle G (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) F) → % 34.20/34.36 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3)) % 34.20/34.36 False % 34.20/34.36 Clause #409 (by clausification #[408]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (Not % 34.20/34.36 (∀ (G : Iota), % 34.20/34.36 And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle G (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) → % 34.20/34.36 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3))) % 34.20/34.36 True % 34.20/34.36 Clause #410 (by clausification #[409]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (∀ (G : Iota), % 34.20/34.36 And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle G (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) → % 34.20/34.36 coll (skS.0 2 a) G (skS.0 5 a a_1 a_2 a_3)) % 34.20/34.36 False % 34.20/34.36 Clause #411 (by clausification #[410]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (Not % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) % 34.20/34.36 (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) → % 34.20/34.36 coll (skS.0 2 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1 a_2 a_3))) % 34.20/34.36 True % 34.20/34.36 Clause #412 (by clausification #[411]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.36 Eq % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And % 34.20/34.36 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.36 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.36 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.36 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.36 (circle (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) % 34.20/34.36 (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) → % 34.20/34.36 coll (skS.0 2 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1 a_2 a_3)) % 34.20/34.39 False % 34.20/34.39 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.39 Eq % 34.20/34.39 (And % 34.20/34.39 (And % 34.20/34.39 (And % 34.20/34.39 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.39 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.39 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.39 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.39 (circle (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) % 34.20/34.39 (skS.0 7 a a_1 a_2 a_3 a_4 a_5))) % 34.20/34.39 True % 34.20/34.39 Clause #414 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.39 Eq (coll (skS.0 2 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a a_1 a_2 a_3)) False % 34.20/34.39 Clause #416 (by clausification #[413]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.39 Eq % 34.20/34.39 (And % 34.20/34.39 (And % 34.20/34.39 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.39 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.39 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.39 (coll (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 34.20/34.39 True % 34.20/34.39 Clause #450 (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 % 34.20/34.39 Clause #451 (by clausification #[450]): ∀ (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 % 34.20/34.39 Clause #452 (by clausification #[451]): ∀ (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 % 34.20/34.39 Clause #453 (by clausification #[452]): ∀ (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 % 34.20/34.39 Clause #454 (by clausification #[453]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #455 (by clausification #[454]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #456 (by clausification #[455]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #457 (by clausification #[456]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #458 (by clausification #[457]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.20/34.39 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) % 34.20/34.39 Clause #500 (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 % 34.20/34.39 Clause #501 (by clausification #[500]): ∀ (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 % 34.20/34.39 Clause #502 (by clausification #[501]): ∀ (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 % 34.20/34.39 Clause #503 (by clausification #[502]): ∀ (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 % 34.20/34.39 Clause #504 (by clausification #[503]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #505 (by clausification #[504]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #506 (by clausification #[505]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 34.20/34.39 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 % 34.20/34.39 Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.20/34.41 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 % 34.20/34.41 Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.20/34.41 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) % 34.20/34.41 Clause #628 (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 % 34.20/34.41 Clause #629 (by clausification #[628]): ∀ (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 % 34.20/34.41 Clause #630 (by clausification #[629]): ∀ (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 % 34.20/34.41 Clause #631 (by clausification #[630]): ∀ (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 % 34.20/34.41 Clause #632 (by clausification #[631]): ∀ (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 % 34.20/34.41 Clause #633 (by clausification #[632]): ∀ (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 % 34.20/34.41 Clause #634 (by clausification #[633]): ∀ (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) % 34.20/34.41 Clause #853 (by clausification #[416]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq % 34.20/34.41 (And % 34.20/34.41 (And (circle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) % 34.20/34.41 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 3 a a_1))) % 34.20/34.41 (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4))) % 34.20/34.41 True % 34.20/34.41 Clause #1135 (by clausification #[853]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4)) True % 34.20/34.41 Clause #1139 (by superposition #[1135, 189]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Or (Eq True False) % 34.20/34.41 (Eq (para (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True) % 34.20/34.41 Clause #1627 (by clausification #[1139]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True % 34.20/34.41 Clause #1629 (by superposition #[1627, 156]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Or (Eq True False) % 34.20/34.41 (Eq (para (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True) % 34.20/34.41 Clause #1635 (by clausification #[1629]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True % 34.20/34.41 Clause #1637 (by superposition #[1635, 189]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Or (Eq True False) % 34.20/34.41 (Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4)) True) % 34.20/34.41 Clause #1641 (by clausification #[1637]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1 a_2 a_3 a_4)) True % 34.20/34.41 Clause #1643 (by superposition #[1641, 156]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Or (Eq True False) % 34.20/34.41 (Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) True) % 34.20/34.41 Clause #1647 (by clausification #[1643]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5)) True % 34.20/34.41 Clause #1649 (by superposition #[1647, 189]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Or (Eq True False) % 34.20/34.41 (Eq (para (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True) % 34.20/34.41 Clause #1650 (by superposition #[1647, 227]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.20/34.41 Or (Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) a_3 a_4) True) % 34.20/34.41 (Or (Eq True False) (Eq (para (skS.0 6 a a_1 a_2 a_5 a_6) (skS.0 7 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False)) % 34.20/34.41 Clause #1653 (by clausification #[1649]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.20/34.41 Eq (para (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True % 34.27/34.44 Clause #1655 (by superposition #[1653, 156]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (para (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True) % 34.27/34.44 Clause #1659 (by clausification #[1655]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 34.27/34.44 Eq (para (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True % 34.27/34.44 Clause #2097 (by clausification #[1650]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 34.27/34.44 Or (Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) a_3 a_4) True) % 34.27/34.44 (Eq (para (skS.0 6 a a_1 a_2 a_5 a_6) (skS.0 7 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False) % 34.27/34.44 Clause #2099 (by superposition #[2097, 1659]): ∀ (a a_1 a_2 : Iota), % 34.27/34.44 Or (Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True) (Eq False True) % 34.27/34.44 Clause #2100 (by clausification #[2099]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True % 34.27/34.44 Clause #2103 (by superposition #[2100, 189]): ∀ (a a_1 a_2 : Iota), % 34.27/34.44 Or (Eq True False) (Eq (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True) % 34.27/34.44 Clause #2107 (by clausification #[2103]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1)) True % 34.27/34.44 Clause #2109 (by superposition #[2107, 156]): ∀ (a a_1 a_2 : Iota), % 34.27/34.44 Or (Eq True False) (Eq (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True) % 34.27/34.44 Clause #2115 (by clausification #[2109]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True % 34.27/34.44 Clause #2120 (by superposition #[2115, 634]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (eqangle (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4) True) % 34.27/34.44 Clause #2782 (by clausification #[2120]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Eq (eqangle (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4 (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4) True % 34.27/34.44 Clause #2789 (by superposition #[2782, 508]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (eqangle (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4 a_3 a_4) True) % 34.27/34.44 Clause #2795 (by clausification #[2789]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Eq (eqangle (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) a_3 a_4 a_3 a_4) True % 34.27/34.44 Clause #2801 (by superposition #[2795, 458]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (eqangle a a_1 a a_1 (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True) % 34.27/34.44 Clause #2807 (by clausification #[2801]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Eq (eqangle a a_1 a a_1 (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True % 34.27/34.44 Clause #2811 (by superposition #[2807, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (eqangle a a_1 a_1 a (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True) % 34.27/34.44 Clause #2818 (by clausification #[2811]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Eq (eqangle a a_1 a_1 a (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True % 34.27/34.44 Clause #2825 (by superposition #[2818, 508]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Or (Eq True False) % 34.27/34.44 (Eq (eqangle a a_1 (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) a_1 a (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True) % 34.27/34.44 Clause #2830 (by clausification #[2825]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 34.27/34.44 Eq (eqangle a a_1 (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4) a_1 a (skS.0 3 a_2 a_3) (skS.0 4 a_2 a_3 a_4)) True % 34.27/34.44 Clause #2834 (by superposition #[2830, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 34.27/34.44 Clause #2843 (by clausification #[2834]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 34.27/34.44 Clause #2870 (by superposition #[2843, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 34.27/34.44 Clause #2908 (by clausification #[2870]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 34.31/34.47 Clause #2911 (by superposition #[2908, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 34.31/34.47 Clause #2917 (by clausification #[2911]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 34.31/34.47 Clause #2953 (by superposition #[2917, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 34.31/34.47 Clause #2962 (by clausification #[2953]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 34.31/34.47 Clause #2993 (by superposition #[2962, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 34.31/34.47 Clause #3002 (by clausification #[2993]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 34.31/34.47 Clause #3036 (by superposition #[3002, 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)) % 34.31/34.47 Clause #3047 (by clausification #[3036]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 34.31/34.47 Clause #3059 (by superposition #[3047, 3002]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 34.31/34.47 Clause #3060 (by clausification #[3059]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 34.31/34.47 Clause #3124 (by superposition #[3060, 414]): Eq True False % 34.31/34.47 Clause #3126 (by clausification #[3124]): False % 34.31/34.47 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------