%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO579+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:43 PM UTC 2025 % Result : Theorem 11.34s 11.52s % Output : Proof 11.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO579+1 : TPTP v9.2.0. Released v7.5.0. % 0.11/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 12:05:38 EDT 2025 % 0.13/0.35 % CPUTime : % 11.34/11.52 SZS status Theorem for theBenchmark.p % 11.34/11.52 SZS output start Proof for theBenchmark.p % 11.34/11.52 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 11.34/11.52 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 11.34/11.52 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 11.34/11.52 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 11.34/11.52 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 11.34/11.52 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 11.34/11.52 Clause #8 (by assumption #[]): Eq (∀ (A B C D E F : Iota), And (perp A B C D) (perp C D E F) → para A B E F) True % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 11.34/11.52 Clause #94 (by assumption #[]): Eq % 11.34/11.52 (Not % 11.34/11.52 (∀ (A B C I Y L X : Iota), % 11.34/11.52 And % 11.34/11.52 (And % 11.34/11.52 (And % 11.34/11.52 (And % 11.34/11.52 (And % 11.34/11.52 (And (And (And (eqangle I A A B I A A C) (eqangle I B B C I B B A)) (eqangle I C C A I C C B)) % 11.34/11.52 (perp Y I A C)) % 11.34/11.52 (coll Y A C)) % 11.34/11.52 (perp L I B C)) % 11.34/11.52 (coll L B C)) % 11.34/11.52 (perp X B A I)) % 11.34/11.52 (coll X A I) → % 11.34/11.52 coll X Y L)) % 11.34/11.52 True % 11.34/11.52 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 11.34/11.52 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 11.34/11.52 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 % 11.34/11.52 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) % 11.34/11.52 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 11.34/11.52 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 11.34/11.52 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 % 11.34/11.52 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) % 11.34/11.52 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 11.34/11.52 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 11.34/11.52 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 % 11.34/11.52 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) % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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 % 11.34/11.52 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) % 11.34/11.52 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)) % 11.38/11.54 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 11.38/11.54 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 % 11.38/11.54 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 % 11.38/11.54 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 % 11.38/11.54 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) % 11.38/11.54 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 11.38/11.54 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), perp a a_1 C D → perp a a_1 D C) True % 11.38/11.54 Clause #263 (by clausification #[262]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), perp a a_1 a_2 D → perp a a_1 D a_2) True % 11.38/11.54 Clause #264 (by clausification #[263]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3 → perp a a_1 a_3 a_2) True % 11.38/11.54 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) False) (Eq (perp a a_1 a_3 a_2) True) % 11.38/11.54 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 11.38/11.54 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), perp a a_1 C D → perp C D a a_1) True % 11.38/11.54 Clause #268 (by clausification #[267]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), perp a a_1 a_2 D → perp a_2 D a a_1) True % 11.38/11.54 Clause #269 (by clausification #[268]): ∀ (a a_1 a_2 a_3 : Iota), Eq (perp a a_1 a_2 a_3 → perp a_2 a_3 a a_1) True % 11.38/11.54 Clause #270 (by clausification #[269]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (perp a a_1 a_2 a_3) False) (Eq (perp a_2 a_3 a a_1) True) % 11.38/11.54 Clause #298 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (B C D E F : Iota), And (perp a B C D) (perp C D E F) → para a B E F) True % 11.38/11.54 Clause #299 (by clausification #[298]): ∀ (a a_1 : Iota), Eq (∀ (C D E F : Iota), And (perp a a_1 C D) (perp C D E F) → para a a_1 E F) True % 11.38/11.54 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E F : Iota), And (perp a a_1 a_2 D) (perp a_2 D E F) → para a a_1 E F) True % 11.38/11.54 Clause #301 (by clausification #[300]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 E F) → para a a_1 E F) True % 11.38/11.54 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (∀ (F : Iota), And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 F) → para a a_1 a_4 F) True % 11.38/11.54 Clause #303 (by clausification #[302]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5) → para a a_1 a_4 a_5) True % 11.38/11.54 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.38/11.54 Or (Eq (And (perp a a_1 a_2 a_3) (perp a_2 a_3 a_4 a_5)) False) (Eq (para a a_1 a_4 a_5) True) % 11.38/11.54 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.38/11.54 Or (Eq (para a a_1 a_2 a_3) True) (Or (Eq (perp a a_1 a_4 a_5) False) (Eq (perp a_4 a_5 a_2 a_3) False)) % 11.38/11.54 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 % 11.38/11.54 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 % 11.38/11.54 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 % 11.38/11.54 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 % 11.38/11.54 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.38/11.54 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 % 11.38/11.54 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.38/11.54 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 % 11.38/11.56 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.38/11.56 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 % 11.38/11.56 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.38/11.56 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 % 11.38/11.56 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.38/11.56 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) % 11.38/11.56 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 % 11.38/11.56 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 % 11.38/11.56 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 % 11.38/11.56 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 % 11.38/11.56 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 % 11.38/11.56 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 % 11.38/11.56 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) % 11.38/11.56 Clause #398 (by clausification #[94]): Eq % 11.38/11.56 (∀ (A B C I Y L X : Iota), % 11.38/11.56 And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And (And (And (eqangle I A A B I A A C) (eqangle I B B C I B B A)) (eqangle I C C A I C C B)) % 11.38/11.56 (perp Y I A C)) % 11.38/11.56 (coll Y A C)) % 11.38/11.56 (perp L I B C)) % 11.38/11.56 (coll L B C)) % 11.38/11.56 (perp X B A I)) % 11.38/11.56 (coll X A I) → % 11.38/11.56 coll X Y L) % 11.38/11.56 False % 11.38/11.56 Clause #399 (by clausification #[398]): ∀ (a : Iota), % 11.38/11.56 Eq % 11.38/11.56 (Not % 11.38/11.56 (∀ (B C I Y L X : Iota), % 11.38/11.56 And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And (eqangle I (skS.0 2 a) (skS.0 2 a) B I (skS.0 2 a) (skS.0 2 a) C) % 11.38/11.56 (eqangle I B B C I B B (skS.0 2 a))) % 11.38/11.56 (eqangle I C C (skS.0 2 a) I C C B)) % 11.38/11.56 (perp Y I (skS.0 2 a) C)) % 11.38/11.56 (coll Y (skS.0 2 a) C)) % 11.38/11.56 (perp L I B C)) % 11.38/11.56 (coll L B C)) % 11.38/11.56 (perp X B (skS.0 2 a) I)) % 11.38/11.56 (coll X (skS.0 2 a) I) → % 11.38/11.56 coll X Y L)) % 11.38/11.56 True % 11.38/11.56 Clause #400 (by clausification #[399]): ∀ (a : Iota), % 11.38/11.56 Eq % 11.38/11.56 (∀ (B C I Y L X : Iota), % 11.38/11.56 And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And % 11.38/11.56 (And (eqangle I (skS.0 2 a) (skS.0 2 a) B I (skS.0 2 a) (skS.0 2 a) C) % 11.38/11.57 (eqangle I B B C I B B (skS.0 2 a))) % 11.38/11.57 (eqangle I C C (skS.0 2 a) I C C B)) % 11.38/11.57 (perp Y I (skS.0 2 a) C)) % 11.38/11.57 (coll Y (skS.0 2 a) C)) % 11.38/11.57 (perp L I B C)) % 11.38/11.57 (coll L B C)) % 11.38/11.57 (perp X B (skS.0 2 a) I)) % 11.38/11.57 (coll X (skS.0 2 a) I) → % 11.38/11.57 coll X Y L) % 11.38/11.57 False % 11.38/11.57 Clause #401 (by clausification #[400]): ∀ (a a_1 : Iota), % 11.38/11.57 Eq % 11.38/11.57 (Not % 11.38/11.57 (∀ (C I Y L X : Iota), % 11.38/11.57 And % 11.38/11.57 (And % 11.38/11.57 (And % 11.38/11.57 (And % 11.38/11.57 (And % 11.38/11.57 (And % 11.38/11.57 (And % 11.38/11.57 (And (eqangle I (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) I (skS.0 2 a) (skS.0 2 a) C) % 11.38/11.57 (eqangle I (skS.0 3 a a_1) (skS.0 3 a a_1) C I (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.38/11.57 (eqangle I C C (skS.0 2 a) I C C (skS.0 3 a a_1))) % 11.38/11.57 (perp Y I (skS.0 2 a) C)) % 11.38/11.59 (coll Y (skS.0 2 a) C)) % 11.38/11.59 (perp L I (skS.0 3 a a_1) C)) % 11.38/11.59 (coll L (skS.0 3 a a_1) C)) % 11.38/11.59 (perp X (skS.0 3 a a_1) (skS.0 2 a) I)) % 11.38/11.59 (coll X (skS.0 2 a) I) → % 11.38/11.59 coll X Y L)) % 11.38/11.59 True % 11.38/11.59 Clause #402 (by clausification #[401]): ∀ (a a_1 : Iota), % 11.38/11.59 Eq % 11.38/11.59 (∀ (C I Y L X : Iota), % 11.38/11.59 And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And (eqangle I (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) I (skS.0 2 a) (skS.0 2 a) C) % 11.38/11.59 (eqangle I (skS.0 3 a a_1) (skS.0 3 a a_1) C I (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.38/11.59 (eqangle I C C (skS.0 2 a) I C C (skS.0 3 a a_1))) % 11.38/11.59 (perp Y I (skS.0 2 a) C)) % 11.38/11.59 (coll Y (skS.0 2 a) C)) % 11.38/11.59 (perp L I (skS.0 3 a a_1) C)) % 11.38/11.59 (coll L (skS.0 3 a a_1) C)) % 11.38/11.59 (perp X (skS.0 3 a a_1) (skS.0 2 a) I)) % 11.38/11.59 (coll X (skS.0 2 a) I) → % 11.38/11.59 coll X Y L) % 11.38/11.59 False % 11.38/11.59 Clause #403 (by clausification #[402]): ∀ (a a_1 a_2 : Iota), % 11.38/11.59 Eq % 11.38/11.59 (Not % 11.38/11.59 (∀ (I Y L X : Iota), % 11.38/11.59 And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (eqangle I (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) I (skS.0 2 a) (skS.0 2 a) % 11.38/11.59 (skS.0 4 a a_1 a_2)) % 11.38/11.59 (eqangle I (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) I (skS.0 3 a a_1) % 11.38/11.59 (skS.0 3 a a_1) (skS.0 2 a))) % 11.38/11.59 (eqangle I (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) I (skS.0 4 a a_1 a_2) % 11.38/11.59 (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.38/11.59 (perp Y I (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (coll Y (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (perp L I (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (perp X (skS.0 3 a a_1) (skS.0 2 a) I)) % 11.38/11.59 (coll X (skS.0 2 a) I) → % 11.38/11.59 coll X Y L)) % 11.38/11.59 True % 11.38/11.59 Clause #404 (by clausification #[403]): ∀ (a a_1 a_2 : Iota), % 11.38/11.59 Eq % 11.38/11.59 (∀ (I Y L X : Iota), % 11.38/11.59 And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (eqangle I (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) I (skS.0 2 a) (skS.0 2 a) % 11.38/11.59 (skS.0 4 a a_1 a_2)) % 11.38/11.59 (eqangle I (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) I (skS.0 3 a a_1) (skS.0 3 a a_1) % 11.38/11.59 (skS.0 2 a))) % 11.38/11.59 (eqangle I (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) I (skS.0 4 a a_1 a_2) % 11.38/11.59 (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.38/11.59 (perp Y I (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (coll Y (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (perp L I (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.38/11.59 (perp X (skS.0 3 a a_1) (skS.0 2 a) I)) % 11.38/11.59 (coll X (skS.0 2 a) I) → % 11.38/11.59 coll X Y L) % 11.38/11.59 False % 11.38/11.59 Clause #405 (by clausification #[404]): ∀ (a a_1 a_2 a_3 : Iota), % 11.38/11.59 Eq % 11.38/11.59 (Not % 11.38/11.59 (∀ (Y L X : Iota), % 11.38/11.59 And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (And % 11.38/11.59 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) % 11.38/11.59 (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.38/11.59 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.38/11.59 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.38/11.59 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.61 (perp Y (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll Y (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp L (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.61 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.61 coll X Y L)) % 11.45/11.61 True % 11.45/11.61 Clause #406 (by clausification #[405]): ∀ (a a_1 a_2 a_3 : Iota), % 11.45/11.61 Eq % 11.45/11.61 (∀ (Y L X : Iota), % 11.45/11.61 And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.61 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.61 (perp Y (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll Y (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp L (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.61 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.61 coll X Y L) % 11.45/11.61 False % 11.45/11.61 Clause #407 (by clausification #[406]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.45/11.61 Eq % 11.45/11.61 (Not % 11.45/11.61 (∀ (L X : Iota), % 11.45/11.61 And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.61 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp L (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.61 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.61 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.61 coll X (skS.0 6 a a_1 a_2 a_3 a_4) L)) % 11.45/11.61 True % 11.45/11.61 Clause #408 (by clausification #[407]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.45/11.61 Eq % 11.45/11.61 (∀ (L X : Iota), % 11.45/11.61 And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (And % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.61 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.61 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.61 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.64 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (perp L (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll L (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.64 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.64 coll X (skS.0 6 a a_1 a_2 a_3 a_4) L) % 11.45/11.64 False % 11.45/11.64 Clause #409 (by clausification #[408]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.45/11.64 Eq % 11.45/11.64 (Not % 11.45/11.64 (∀ (X : Iota), % 11.45/11.64 And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.64 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll (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))) % 11.45/11.64 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.64 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.64 coll X (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))) % 11.45/11.64 True % 11.45/11.64 Clause #410 (by clausification #[409]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.45/11.64 Eq % 11.45/11.64 (∀ (X : Iota), % 11.45/11.64 And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.64 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.64 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.64 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.64 (coll (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))) % 11.45/11.64 (perp X (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.64 (coll X (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.64 coll X (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)) % 11.45/11.64 False % 11.45/11.64 Clause #411 (by clausification #[410]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.64 Eq % 11.45/11.64 (Not % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (And % 11.45/11.64 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.64 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.65 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (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))) % 11.45/11.65 (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.65 (coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.65 coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (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))) % 11.45/11.65 True % 11.45/11.65 Clause #412 (by clausification #[411]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.65 Eq % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.65 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.65 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (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))) % 11.45/11.65 (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.65 (coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) → % 11.45/11.65 coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (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)) % 11.45/11.65 False % 11.45/11.65 Clause #413 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.45/11.65 Eq % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (And % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.45/11.65 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.45/11.65 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.45/11.65 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.45/11.65 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.45/11.65 (coll (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))) % 11.45/11.65 (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.45/11.65 (coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.52/11.68 True % 11.52/11.68 Clause #414 (by clausification #[412]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.68 Eq (coll (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (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)) False % 11.52/11.68 Clause #416 (by clausification #[413]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.68 Eq % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) % 11.52/11.68 (skS.0 2 a) (skS.0 2 a) (skS.0 4 a a_1 a_2)) % 11.52/11.68 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2) % 11.52/11.68 (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 3 a a_1) (skS.0 2 a))) % 11.52/11.68 (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 2 a) % 11.52/11.68 (skS.0 5 a a_1 a_2 a_3) (skS.0 4 a a_1 a_2) (skS.0 4 a a_1 a_2) (skS.0 3 a a_1))) % 11.52/11.68 (perp (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.52/11.68 (coll (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 2 a) (skS.0 4 a a_1 a_2))) % 11.52/11.68 (perp (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))) % 11.52/11.68 (coll (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))) % 11.52/11.68 (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))) % 11.52/11.68 True % 11.52/11.68 Clause #451 (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 % 11.52/11.68 Clause #452 (by clausification #[451]): ∀ (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 % 11.52/11.68 Clause #453 (by clausification #[452]): ∀ (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 % 11.52/11.68 Clause #454 (by clausification #[453]): ∀ (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 % 11.52/11.68 Clause #455 (by clausification #[454]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #456 (by clausification #[455]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #457 (by clausification #[456]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #458 (by clausification #[457]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #459 (by clausification #[458]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.68 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) % 11.52/11.68 Clause #501 (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 % 11.52/11.68 Clause #502 (by clausification #[501]): ∀ (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 % 11.52/11.68 Clause #503 (by clausification #[502]): ∀ (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 % 11.52/11.68 Clause #504 (by clausification #[503]): ∀ (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 % 11.52/11.68 Clause #505 (by clausification #[504]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #506 (by clausification #[505]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.68 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 % 11.52/11.68 Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.68 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 % 11.52/11.71 Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.71 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 % 11.52/11.71 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.71 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) % 11.52/11.71 Clause #637 (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 % 11.52/11.71 Clause #638 (by clausification #[637]): ∀ (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 % 11.52/11.71 Clause #639 (by clausification #[638]): ∀ (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 % 11.52/11.71 Clause #640 (by clausification #[639]): ∀ (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 % 11.52/11.71 Clause #641 (by clausification #[640]): ∀ (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 % 11.52/11.71 Clause #642 (by clausification #[641]): ∀ (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 % 11.52/11.71 Clause #643 (by clausification #[642]): ∀ (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) % 11.52/11.71 Clause #886 (by clausification #[416]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) True % 11.52/11.71 Clause #888 (by superposition #[886, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a)) True) % 11.52/11.71 Clause #889 (by superposition #[886, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1)) True) % 11.52/11.71 Clause #912 (by clausification #[889]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1)) True % 11.52/11.71 Clause #913 (by superposition #[912, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) True) % 11.52/11.71 Clause #953 (by clausification #[913]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) True % 11.52/11.71 Clause #954 (by superposition #[953, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) True) % 11.52/11.71 Clause #962 (by clausification #[954]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) True % 11.52/11.71 Clause #963 (by superposition #[962, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 3 a a_1) (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) (skS.0 2 a)) True) % 11.52/11.71 Clause #970 (by clausification #[963]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 3 a a_1) (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) (skS.0 2 a)) True % 11.52/11.71 Clause #971 (by superposition #[970, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) True) % 11.52/11.71 Clause #978 (by clausification #[971]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Eq (perp (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) True % 11.52/11.71 Clause #979 (by superposition #[978, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.71 Or (Eq True False) % 11.52/11.71 (Eq (perp (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1)) True) % 11.52/11.71 Clause #986 (by clausification #[979]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.73 Eq (perp (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1)) True % 11.52/11.73 Clause #987 (by superposition #[986, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.52/11.73 Or (Eq (para (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5) True) % 11.52/11.73 (Or (Eq True False) (Eq (perp (skS.0 8 a a_1 a_2 a_3 a_6 a_7 a_8) (skS.0 3 a a_1) a_4 a_5) False)) % 11.52/11.73 Clause #993 (by clausification #[888]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.73 Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a)) True % 11.52/11.73 Clause #1531 (by clausification #[987]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.52/11.73 Or (Eq (para (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5) True) % 11.52/11.73 (Eq (perp (skS.0 8 a a_1 a_2 a_3 a_6 a_7 a_8) (skS.0 3 a a_1) a_4 a_5) False) % 11.52/11.73 Clause #1533 (by superposition #[1531, 993]): ∀ (a a_1 a_2 a_3 : Iota), % 11.52/11.73 Or (Eq (para (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a)) True) (Eq False True) % 11.52/11.73 Clause #1545 (by clausification #[1533]): ∀ (a a_1 a_2 a_3 : Iota), Eq (para (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a)) True % 11.52/11.73 Clause #1550 (by superposition #[1545, 643]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Or (Eq True False) % 11.52/11.73 (Eq (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5 (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5) True) % 11.52/11.73 Clause #1572 (by clausification #[1550]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Eq (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5 (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5) True % 11.52/11.73 Clause #1579 (by superposition #[1572, 509]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Or (Eq True False) % 11.52/11.73 (Eq (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5 a_4 a_5) True) % 11.52/11.73 Clause #1584 (by clausification #[1579]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Eq (eqangle (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) (skS.0 2 a) a_4 a_5 a_4 a_5) True % 11.52/11.73 Clause #1590 (by superposition #[1584, 459]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Or (Eq True False) % 11.52/11.73 (Eq (eqangle a a_1 a a_1 (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True) % 11.52/11.73 Clause #1596 (by clausification #[1590]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Eq (eqangle a a_1 a a_1 (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True % 11.52/11.73 Clause #1600 (by superposition #[1596, 352]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Or (Eq True False) % 11.52/11.73 (Eq (eqangle a a_1 a_1 a (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True) % 11.52/11.73 Clause #1607 (by clausification #[1600]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Eq (eqangle a a_1 a_1 a (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True % 11.52/11.73 Clause #1614 (by superposition #[1607, 509]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Or (Eq True False) % 11.52/11.73 (Eq (eqangle a a_1 (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) a_1 a (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True) % 11.52/11.73 Clause #1623 (by clausification #[1614]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 Eq (eqangle a a_1 (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2) a_1 a (skS.0 5 a_2 a_3 a_4 a_5) (skS.0 2 a_2)) True % 11.52/11.73 Clause #1627 (by superposition #[1623, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 11.52/11.73 Clause #1636 (by clausification #[1627]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 11.52/11.73 Clause #1644 (by superposition #[1636, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 11.52/11.73 Clause #1662 (by clausification #[1644]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 11.52/11.73 Clause #1663 (by superposition #[1662, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 11.52/11.73 Clause #1669 (by clausification #[1663]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 11.52/11.73 Clause #1677 (by superposition #[1669, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 11.52/11.73 Clause #1686 (by clausification #[1677]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 11.52/11.73 Clause #1696 (by superposition #[1686, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 11.52/11.75 Clause #1705 (by clausification #[1696]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 11.52/11.75 Clause #1714 (by superposition #[1705, 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)) % 11.52/11.75 Clause #1743 (by clausification #[1714]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 11.52/11.75 Clause #1749 (by superposition #[1743, 1705]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 11.52/11.75 Clause #1750 (by clausification #[1749]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 11.52/11.75 Clause #1785 (by superposition #[1750, 414]): Eq True False % 11.52/11.75 Clause #1786 (by clausification #[1785]): False % 11.52/11.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------