%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO547+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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 11.52s 11.68s % Output : Proof 11.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : GEO547+1 : TPTP v9.2.0. Released v7.5.0. % 0.08/0.14 % Command : duper %s % 0.14/0.35 % Computer : n028.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 11:57:53 EDT 2025 % 0.14/0.35 % CPUTime : % 11.52/11.68 SZS status Theorem for theBenchmark.p % 11.52/11.68 SZS output start Proof for theBenchmark.p % 11.52/11.68 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 11.52/11.68 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 11.52/11.68 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.52/11.68 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 11.52/11.68 Clause #4 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para C D A B) True % 11.52/11.68 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 11.52/11.68 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 11.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 11.52/11.68 Clause #94 (by assumption #[]): Eq % 11.52/11.68 (Not % 11.52/11.68 (∀ (A B C O D E F G NWPNT1 : Iota), % 11.52/11.68 And % 11.52/11.68 (And % 11.52/11.68 (And % 11.52/11.68 (And (And (And (And (circle O A B C) (circle O A D NWPNT1)) (perp E D B C)) (coll E B C)) (perp F D A C)) % 11.52/11.68 (coll F A C)) % 11.52/11.68 (perp G D A B)) % 11.52/11.68 (coll G A B) → % 11.52/11.68 coll E F G)) % 11.52/11.68 True % 11.52/11.68 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 11.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 11.52/11.68 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 11.52/11.68 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.52/11.68 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.52/11.68 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 11.52/11.68 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 11.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.68 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.52/11.71 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 11.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 Clause #185 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para C D a B) True % 11.52/11.71 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 % 11.52/11.71 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 % 11.52/11.71 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 % 11.52/11.71 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) % 11.52/11.71 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 11.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 11.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.71 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.52/11.71 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.71 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.52/11.71 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.52/11.71 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.52/11.71 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.52/11.73 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.52/11.73 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.52/11.73 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.52/11.73 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 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.52/11.73 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.73 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.52/11.73 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.73 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.52/11.73 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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.52/11.73 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 % 11.52/11.73 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 % 11.52/11.73 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 % 11.52/11.73 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 % 11.52/11.73 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.52/11.73 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.73 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.73 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.73 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.73 Eq (∀ (V : Iota), eqangle a a_1 a_2 a_3 a_4 a_5 a_6 V → eqangle a_4 a_5 a_6 V a a_1 a_2 a_3) True % 11.52/11.73 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.73 Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7 → eqangle a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True % 11.52/11.73 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.73 Or (Eq (eqangle a a_1 a_2 a_3 a_4 a_5 a_6 a_7) False) (Eq (eqangle a_4 a_5 a_6 a_7 a a_1 a_2 a_3) True) % 11.52/11.73 Clause #488 (by clausification #[20]): ∀ (a : Iota), Eq (∀ (B C D P Q U V : Iota), eqangle a B C D P Q U V → eqangle a B P Q C D U V) True % 11.52/11.73 Clause #489 (by clausification #[488]): ∀ (a a_1 : Iota), Eq (∀ (C D P Q U V : Iota), eqangle a a_1 C D P Q U V → eqangle a a_1 P Q C D U V) True % 11.52/11.73 Clause #490 (by clausification #[489]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D P Q U V : Iota), eqangle a a_1 a_2 D P Q U V → eqangle a a_1 P Q a_2 D U V) True % 11.52/11.75 Clause #491 (by clausification #[490]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (P Q U V : Iota), eqangle a a_1 a_2 a_3 P Q U V → eqangle a a_1 P Q a_2 a_3 U V) True % 11.52/11.75 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.52/11.75 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.75 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.52/11.75 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.75 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.52/11.75 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.75 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.52/11.75 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.75 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.60/11.75 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.60/11.75 Clause #547 (by clausification #[94]): Eq % 11.60/11.75 (∀ (A B C O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And (And (And (And (And (circle O A B C) (circle O A D NWPNT1)) (perp E D B C)) (coll E B C)) (perp F D A C)) % 11.60/11.75 (coll F A C)) % 11.60/11.75 (perp G D A B)) % 11.60/11.75 (coll G A B) → % 11.60/11.75 coll E F G) % 11.60/11.75 False % 11.60/11.75 Clause #548 (by clausification #[547]): ∀ (a : Iota), % 11.60/11.75 Eq % 11.60/11.75 (Not % 11.60/11.75 (∀ (B C O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And (And (And (circle O (skS.0 4 a) B C) (circle O (skS.0 4 a) D NWPNT1)) (perp E D B C)) % 11.60/11.75 (coll E B C)) % 11.60/11.75 (perp F D (skS.0 4 a) C)) % 11.60/11.75 (coll F (skS.0 4 a) C)) % 11.60/11.75 (perp G D (skS.0 4 a) B)) % 11.60/11.75 (coll G (skS.0 4 a) B) → % 11.60/11.75 coll E F G)) % 11.60/11.75 True % 11.60/11.75 Clause #549 (by clausification #[548]): ∀ (a : Iota), % 11.60/11.75 Eq % 11.60/11.75 (∀ (B C O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And (And (And (circle O (skS.0 4 a) B C) (circle O (skS.0 4 a) D NWPNT1)) (perp E D B C)) (coll E B C)) % 11.60/11.75 (perp F D (skS.0 4 a) C)) % 11.60/11.75 (coll F (skS.0 4 a) C)) % 11.60/11.75 (perp G D (skS.0 4 a) B)) % 11.60/11.75 (coll G (skS.0 4 a) B) → % 11.60/11.75 coll E F G) % 11.60/11.75 False % 11.60/11.75 Clause #550 (by clausification #[549]): ∀ (a a_1 : Iota), % 11.60/11.75 Eq % 11.60/11.75 (Not % 11.60/11.75 (∀ (C O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And (And (circle O (skS.0 4 a) (skS.0 5 a a_1) C) (circle O (skS.0 4 a) D NWPNT1)) % 11.60/11.75 (perp E D (skS.0 5 a a_1) C)) % 11.60/11.75 (coll E (skS.0 5 a a_1) C)) % 11.60/11.75 (perp F D (skS.0 4 a) C)) % 11.60/11.75 (coll F (skS.0 4 a) C)) % 11.60/11.75 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.75 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.75 coll E F G)) % 11.60/11.75 True % 11.60/11.75 Clause #551 (by clausification #[550]): ∀ (a a_1 : Iota), % 11.60/11.75 Eq % 11.60/11.75 (∀ (C O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And (And (circle O (skS.0 4 a) (skS.0 5 a a_1) C) (circle O (skS.0 4 a) D NWPNT1)) % 11.60/11.75 (perp E D (skS.0 5 a a_1) C)) % 11.60/11.75 (coll E (skS.0 5 a a_1) C)) % 11.60/11.75 (perp F D (skS.0 4 a) C)) % 11.60/11.75 (coll F (skS.0 4 a) C)) % 11.60/11.75 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.75 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.75 coll E F G) % 11.60/11.75 False % 11.60/11.75 Clause #552 (by clausification #[551]): ∀ (a a_1 a_2 : Iota), % 11.60/11.75 Eq % 11.60/11.75 (Not % 11.60/11.75 (∀ (O D E F G NWPNT1 : Iota), % 11.60/11.75 And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And % 11.60/11.75 (And (circle O (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) (circle O (skS.0 4 a) D NWPNT1)) % 11.60/11.75 (perp E D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp F D (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.78 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.78 coll E F G)) % 11.60/11.78 True % 11.60/11.78 Clause #553 (by clausification #[552]): ∀ (a a_1 a_2 : Iota), % 11.60/11.78 Eq % 11.60/11.78 (∀ (O D E F G NWPNT1 : Iota), % 11.60/11.78 And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And (And (circle O (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) (circle O (skS.0 4 a) D NWPNT1)) % 11.60/11.78 (perp E D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp F D (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.78 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.78 coll E F G) % 11.60/11.78 False % 11.60/11.78 Clause #554 (by clausification #[553]): ∀ (a a_1 a_2 a_3 : Iota), % 11.60/11.78 Eq % 11.60/11.78 (Not % 11.60/11.78 (∀ (D E F G NWPNT1 : Iota), % 11.60/11.78 And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.60/11.78 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) D NWPNT1)) % 11.60/11.78 (perp E D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp F D (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.78 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.78 coll E F G)) % 11.60/11.78 True % 11.60/11.78 Clause #555 (by clausification #[554]): ∀ (a a_1 a_2 a_3 : Iota), % 11.60/11.78 Eq % 11.60/11.78 (∀ (D E F G NWPNT1 : Iota), % 11.60/11.78 And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.60/11.78 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) D NWPNT1)) % 11.60/11.78 (perp E D (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp F D (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp G D (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.78 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.78 coll E F G) % 11.60/11.78 False % 11.60/11.78 Clause #556 (by clausification #[555]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.60/11.78 Eq % 11.60/11.78 (Not % 11.60/11.78 (∀ (E F G NWPNT1 : Iota), % 11.60/11.78 And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.60/11.78 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.60/11.78 (perp E (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp F (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.60/11.78 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.60/11.78 coll E F G)) % 11.60/11.78 True % 11.60/11.78 Clause #557 (by clausification #[556]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 11.60/11.78 Eq % 11.60/11.78 (∀ (E F G NWPNT1 : Iota), % 11.60/11.78 And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And % 11.60/11.78 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.60/11.78 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.60/11.78 (perp E (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.60/11.78 (coll E (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (perp F (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.80 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.80 coll E F G) % 11.63/11.80 False % 11.63/11.80 Clause #558 (by clausification #[557]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.63/11.80 Eq % 11.63/11.80 (Not % 11.63/11.80 (∀ (F G NWPNT1 : Iota), % 11.63/11.80 And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.80 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.80 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.80 (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll (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))) % 11.63/11.80 (perp F (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.80 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.80 coll (skS.0 9 a a_1 a_2 a_3 a_4 a_5) F G)) % 11.63/11.80 True % 11.63/11.80 Clause #559 (by clausification #[558]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 11.63/11.80 Eq % 11.63/11.80 (∀ (F G NWPNT1 : Iota), % 11.63/11.80 And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.80 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.80 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.80 (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll (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))) % 11.63/11.80 (perp F (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.80 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.80 coll (skS.0 9 a a_1 a_2 a_3 a_4 a_5) F G) % 11.63/11.80 False % 11.63/11.80 Clause #560 (by clausification #[559]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.63/11.80 Eq % 11.63/11.80 (Not % 11.63/11.80 (∀ (G NWPNT1 : Iota), % 11.63/11.80 And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.80 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.80 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.80 (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll (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))) % 11.63/11.80 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) % 11.63/11.80 (skS.0 6 a a_1 a_2))) % 11.63/11.80 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.80 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.80 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.80 coll (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) G)) % 11.63/11.80 True % 11.63/11.80 Clause #561 (by clausification #[560]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 11.63/11.80 Eq % 11.63/11.80 (∀ (G NWPNT1 : Iota), % 11.63/11.80 And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And % 11.63/11.80 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.80 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.80 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.80 (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (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))) % 11.63/11.82 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (perp G (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.82 (coll G (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.82 coll (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) G) % 11.63/11.82 False % 11.63/11.82 Clause #562 (by clausification #[561]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.63/11.82 Eq % 11.63/11.82 (Not % 11.63/11.82 (∀ (NWPNT1 : Iota), % 11.63/11.82 And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.82 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.82 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.82 (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (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))) % 11.63/11.82 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) % 11.63/11.82 (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.82 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.82 coll (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) % 11.63/11.82 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 11.63/11.82 True % 11.63/11.82 Clause #563 (by clausification #[562]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.63/11.82 Eq % 11.63/11.82 (∀ (NWPNT1 : Iota), % 11.63/11.82 And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.82 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) NWPNT1)) % 11.63/11.82 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.82 (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (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))) % 11.63/11.82 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.63/11.82 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) → % 11.63/11.82 coll (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) % 11.63/11.82 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 11.63/11.82 False % 11.63/11.82 Clause #564 (by clausification #[563]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.63/11.82 Eq % 11.63/11.82 (Not % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And % 11.63/11.82 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.63/11.82 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) % 11.63/11.82 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 11.63/11.82 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.63/11.82 (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (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))) % 11.63/11.82 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.63/11.82 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.69/11.84 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) → % 11.69/11.84 coll (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) % 11.69/11.84 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 11.69/11.84 True % 11.69/11.84 Clause #565 (by clausification #[564]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.69/11.84 Eq % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.69/11.84 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) % 11.69/11.84 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 11.69/11.84 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) % 11.69/11.84 (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (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))) % 11.69/11.84 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.69/11.84 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) → % 11.69/11.84 coll (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) % 11.69/11.84 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 11.69/11.84 False % 11.69/11.84 Clause #566 (by clausification #[565]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.69/11.84 Eq % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.69/11.84 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) % 11.69/11.84 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 11.69/11.84 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (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))) % 11.69/11.84 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.69/11.84 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1))) % 11.69/11.84 True % 11.69/11.84 Clause #567 (by clausification #[565]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.69/11.84 Eq % 11.69/11.84 (coll (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 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 11.69/11.84 False % 11.69/11.84 Clause #569 (by clausification #[566]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 11.69/11.84 Eq % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And % 11.69/11.84 (And (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2)) % 11.69/11.84 (circle (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) % 11.69/11.84 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 11.69/11.84 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (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))) % 11.69/11.84 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 11.69/11.84 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1))) % 11.69/11.84 True % 11.69/11.84 Clause #627 (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.69/11.84 Clause #628 (by clausification #[627]): ∀ (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.69/11.84 Clause #629 (by clausification #[628]): ∀ (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.70/11.87 Clause #630 (by clausification #[629]): ∀ (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.70/11.87 Clause #631 (by clausification #[630]): ∀ (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.70/11.87 Clause #632 (by clausification #[631]): ∀ (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.70/11.87 Clause #633 (by clausification #[632]): ∀ (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.70/11.87 Clause #883 (by clausification #[569]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 4 a) (skS.0 5 a a_1)) True % 11.70/11.87 Clause #885 (by superposition #[883, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)) True) % 11.70/11.87 Clause #886 (by superposition #[883, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4)) True) % 11.70/11.87 Clause #1437 (by clausification #[886]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 4 a) (skS.0 5 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4)) True % 11.70/11.87 Clause #1438 (by superposition #[1437, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 4 a) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True) % 11.70/11.87 Clause #1449 (by clausification #[1438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 4 a) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 11.70/11.87 Clause #1450 (by superposition #[1449, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) True) % 11.70/11.87 Clause #1460 (by clausification #[1450]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 4 a) (skS.0 5 a a_1)) True % 11.70/11.87 Clause #1461 (by superposition #[1460, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 4 a)) True) % 11.70/11.87 Clause #1471 (by clausification #[1461]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 5 a a_1) (skS.0 4 a)) True % 11.70/11.87 Clause #1472 (by superposition #[1471, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 5 a a_1) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True) % 11.70/11.87 Clause #1483 (by clausification #[1472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 5 a a_1) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 11.70/11.87 Clause #1484 (by superposition #[1483, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Or (Eq True False) % 11.70/11.87 (Eq (perp (skS.0 5 a a_1) (skS.0 4 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4)) True) % 11.70/11.87 Clause #1494 (by clausification #[1484]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 5 a a_1) (skS.0 4 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4)) True % 11.70/11.87 Clause #1495 (by superposition #[1494, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 11.70/11.87 Or (Eq (para (skS.0 5 a a_1) (skS.0 4 a) a_2 a_3) True) % 11.70/11.87 (Or (Eq True False) (Eq (perp (skS.0 11 a a_1 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 8 a a_1 a_4 a_5 a_6) a_2 a_3) False)) % 11.70/11.87 Clause #1504 (by clausification #[885]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 11.70/11.87 Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1) (skS.0 4 a)) True % 11.70/11.90 Clause #1554 (by clausification #[1495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 11.70/11.90 Or (Eq (para (skS.0 5 a a_1) (skS.0 4 a) a_2 a_3) True) % 11.70/11.90 (Eq (perp (skS.0 11 a a_1 a_4 a_5 a_6 a_7 a_8 a_9) (skS.0 8 a a_1 a_4 a_5 a_6) a_2 a_3) False) % 11.70/11.90 Clause #1556 (by superposition #[1554, 1504]): ∀ (a a_1 : Iota), Or (Eq (para (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a)) True) (Eq False True) % 11.70/11.90 Clause #1557 (by clausification #[1556]): ∀ (a a_1 : Iota), Eq (para (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a)) True % 11.70/11.90 Clause #1559 (by superposition #[1557, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para (skS.0 5 a a_1) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1)) True) % 11.70/11.90 Clause #1563 (by clausification #[1559]): ∀ (a a_1 : Iota), Eq (para (skS.0 5 a a_1) (skS.0 4 a) (skS.0 4 a) (skS.0 5 a a_1)) True % 11.70/11.90 Clause #1567 (by superposition #[1563, 189]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para (skS.0 4 a) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a)) True) % 11.70/11.90 Clause #1571 (by clausification #[1567]): ∀ (a a_1 : Iota), Eq (para (skS.0 4 a) (skS.0 5 a a_1) (skS.0 5 a a_1) (skS.0 4 a)) True % 11.70/11.90 Clause #1574 (by superposition #[1571, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1)) True) % 11.70/11.90 Clause #1580 (by clausification #[1574]): ∀ (a a_1 : Iota), Eq (para (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1)) True % 11.70/11.90 Clause #1584 (by superposition #[1580, 633]): ∀ (a a_1 a_2 a_3 : Iota), % 11.70/11.90 Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3 (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3) True) % 11.70/11.90 Clause #1585 (by clausification #[1584]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3 (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3) True % 11.70/11.90 Clause #1593 (by superposition #[1585, 496]): ∀ (a a_1 a_2 a_3 : Iota), % 11.70/11.90 Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3 a_2 a_3) True) % 11.70/11.90 Clause #1597 (by clausification #[1593]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle (skS.0 4 a) (skS.0 5 a a_1) (skS.0 4 a) (skS.0 5 a a_1) a_2 a_3 a_2 a_3) True % 11.70/11.90 Clause #1603 (by superposition #[1597, 441]): ∀ (a a_1 a_2 a_3 : Iota), % 11.70/11.90 Or (Eq True False) (Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 5 a_2 a_3) (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True) % 11.70/11.90 Clause #1610 (by clausification #[1603]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 5 a_2 a_3) (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True % 11.70/11.90 Clause #1614 (by superposition #[1610, 352]): ∀ (a a_1 a_2 a_3 : Iota), % 11.70/11.90 Or (Eq True False) (Eq (eqangle a a_1 a_1 a (skS.0 4 a_2) (skS.0 5 a_2 a_3) (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True) % 11.70/11.90 Clause #1621 (by clausification #[1614]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_1 a (skS.0 4 a_2) (skS.0 5 a_2 a_3) (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True % 11.70/11.90 Clause #1628 (by superposition #[1621, 496]): ∀ (a a_1 a_2 a_3 : Iota), % 11.70/11.90 Or (Eq True False) (Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 5 a_2 a_3) a_1 a (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True) % 11.70/11.90 Clause #1633 (by clausification #[1628]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 5 a_2 a_3) a_1 a (skS.0 4 a_2) (skS.0 5 a_2 a_3)) True % 11.70/11.90 Clause #1637 (by superposition #[1633, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 11.70/11.90 Clause #1646 (by clausification #[1637]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 11.70/11.90 Clause #1655 (by superposition #[1646, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 11.70/11.90 Clause #1677 (by clausification #[1655]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 11.70/11.90 Clause #1678 (by superposition #[1677, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 11.70/11.90 Clause #1683 (by clausification #[1678]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 11.70/11.90 Clause #1693 (by superposition #[1683, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 11.70/11.90 Clause #1702 (by clausification #[1693]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 11.70/11.90 Clause #1715 (by superposition #[1702, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 11.70/11.90 Clause #1724 (by clausification #[1715]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 11.70/11.91 Clause #1738 (by superposition #[1724, 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.70/11.91 Clause #1844 (by clausification #[1738]): ∀ (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.70/11.91 Clause #1851 (by superposition #[1844, 1724]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 11.70/11.91 Clause #1852 (by clausification #[1851]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 11.70/11.91 Clause #1893 (by superposition #[1852, 567]): Eq True False % 11.70/11.91 Clause #1894 (by clausification #[1893]): False % 11.70/11.91 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------