%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO566+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:42 PM UTC 2025 % Result : Theorem 10.67s 10.91s % Output : Proof 10.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GEO566+1 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.14 % Command : duper %s % 0.13/0.35 % Computer : n002.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 12:12:08 EDT 2025 % 0.13/0.35 % CPUTime : % 10.67/10.91 SZS status Theorem for theBenchmark.p % 10.67/10.91 SZS output start Proof for theBenchmark.p % 10.67/10.91 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 10.67/10.91 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 10.67/10.91 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 10.67/10.91 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 10.67/10.91 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 10.67/10.91 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 10.67/10.91 Clause #94 (by assumption #[]): Eq % 10.67/10.91 (Not % 10.67/10.91 (∀ (A B C F H T Q P : Iota), % 10.67/10.91 And % 10.67/10.91 (And % 10.67/10.91 (And % 10.67/10.91 (And % 10.67/10.91 (And (And (And (And (And (perp F C A B) (coll F A B)) (perp B C A H)) (perp A C B H)) (perp T F B C)) % 10.67/10.91 (coll T B C)) % 10.67/10.91 (perp Q F A H)) % 10.67/10.91 (coll Q A H)) % 10.67/10.91 (perp P F A C)) % 10.67/10.91 (coll P A C) → % 10.67/10.91 coll P Q T)) % 10.67/10.91 True % 10.67/10.91 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 10.67/10.91 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 10.67/10.91 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 % 10.67/10.91 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) % 10.67/10.91 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 10.67/10.91 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 10.67/10.91 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 % 10.67/10.91 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) % 10.67/10.91 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 10.67/10.91 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 10.67/10.91 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 % 10.67/10.91 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) % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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 % 10.67/10.91 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) % 10.67/10.91 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)) % 10.67/10.91 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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) % 10.77/10.93 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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) % 10.77/10.93 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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) % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.77/10.93 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) % 10.77/10.93 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.77/10.93 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)) % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 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 % 10.77/10.93 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.77/10.93 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 % 10.77/10.93 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.77/10.93 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 % 10.77/10.96 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.77/10.96 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) % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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) % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 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 % 10.77/10.96 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.77/10.96 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 % 10.77/10.96 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.77/10.96 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) % 10.77/10.96 Clause #458 (by clausification #[94]): Eq % 10.77/10.96 (∀ (A B C F H T Q P : Iota), % 10.77/10.96 And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And (And (And (And (And (perp F C A B) (coll F A B)) (perp B C A H)) (perp A C B H)) (perp T F B C)) % 10.77/10.96 (coll T B C)) % 10.77/10.96 (perp Q F A H)) % 10.77/10.96 (coll Q A H)) % 10.77/10.96 (perp P F A C)) % 10.77/10.96 (coll P A C) → % 10.77/10.96 coll P Q T) % 10.77/10.96 False % 10.77/10.96 Clause #459 (by clausification #[458]): ∀ (a : Iota), % 10.77/10.96 Eq % 10.77/10.96 (Not % 10.77/10.96 (∀ (B C F H T Q P : Iota), % 10.77/10.96 And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And % 10.77/10.96 (And (And (And (perp F C (skS.0 4 a) B) (coll F (skS.0 4 a) B)) (perp B C (skS.0 4 a) H)) % 10.77/10.96 (perp (skS.0 4 a) C B H)) % 10.77/10.96 (perp T F B C)) % 10.77/10.96 (coll T B C)) % 10.77/10.96 (perp Q F (skS.0 4 a) H)) % 10.77/10.96 (coll Q (skS.0 4 a) H)) % 10.77/10.96 (perp P F (skS.0 4 a) C)) % 10.77/10.96 (coll P (skS.0 4 a) C) → % 10.77/10.98 coll P Q T)) % 10.77/10.98 True % 10.77/10.98 Clause #460 (by clausification #[459]): ∀ (a : Iota), % 10.77/10.98 Eq % 10.77/10.98 (∀ (B C F H T Q P : Iota), % 10.77/10.98 And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And (And (And (perp F C (skS.0 4 a) B) (coll F (skS.0 4 a) B)) (perp B C (skS.0 4 a) H)) % 10.77/10.98 (perp (skS.0 4 a) C B H)) % 10.77/10.98 (perp T F B C)) % 10.77/10.98 (coll T B C)) % 10.77/10.98 (perp Q F (skS.0 4 a) H)) % 10.77/10.98 (coll Q (skS.0 4 a) H)) % 10.77/10.98 (perp P F (skS.0 4 a) C)) % 10.77/10.98 (coll P (skS.0 4 a) C) → % 10.77/10.98 coll P Q T) % 10.77/10.98 False % 10.77/10.98 Clause #461 (by clausification #[460]): ∀ (a a_1 : Iota), % 10.77/10.98 Eq % 10.77/10.98 (Not % 10.77/10.98 (∀ (C F H T Q P : Iota), % 10.77/10.98 And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And (And (perp F C (skS.0 4 a) (skS.0 5 a a_1)) (coll F (skS.0 4 a) (skS.0 5 a a_1))) % 10.77/10.98 (perp (skS.0 5 a a_1) C (skS.0 4 a) H)) % 10.77/10.98 (perp (skS.0 4 a) C (skS.0 5 a a_1) H)) % 10.77/10.98 (perp T F (skS.0 5 a a_1) C)) % 10.77/10.98 (coll T (skS.0 5 a a_1) C)) % 10.77/10.98 (perp Q F (skS.0 4 a) H)) % 10.77/10.98 (coll Q (skS.0 4 a) H)) % 10.77/10.98 (perp P F (skS.0 4 a) C)) % 10.77/10.98 (coll P (skS.0 4 a) C) → % 10.77/10.98 coll P Q T)) % 10.77/10.98 True % 10.77/10.98 Clause #462 (by clausification #[461]): ∀ (a a_1 : Iota), % 10.77/10.98 Eq % 10.77/10.98 (∀ (C F H T Q P : Iota), % 10.77/10.98 And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And (And (perp F C (skS.0 4 a) (skS.0 5 a a_1)) (coll F (skS.0 4 a) (skS.0 5 a a_1))) % 10.77/10.98 (perp (skS.0 5 a a_1) C (skS.0 4 a) H)) % 10.77/10.98 (perp (skS.0 4 a) C (skS.0 5 a a_1) H)) % 10.77/10.98 (perp T F (skS.0 5 a a_1) C)) % 10.77/10.98 (coll T (skS.0 5 a a_1) C)) % 10.77/10.98 (perp Q F (skS.0 4 a) H)) % 10.77/10.98 (coll Q (skS.0 4 a) H)) % 10.77/10.98 (perp P F (skS.0 4 a) C)) % 10.77/10.98 (coll P (skS.0 4 a) C) → % 10.77/10.98 coll P Q T) % 10.77/10.98 False % 10.77/10.98 Clause #463 (by clausification #[462]): ∀ (a a_1 a_2 : Iota), % 10.77/10.98 Eq % 10.77/10.98 (Not % 10.77/10.98 (∀ (F H T Q P : Iota), % 10.77/10.98 And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And (perp F (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.77/10.98 (coll F (skS.0 4 a) (skS.0 5 a a_1))) % 10.77/10.98 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) H)) % 10.77/10.98 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) H)) % 10.77/10.98 (perp T F (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (perp Q F (skS.0 4 a) H)) % 10.77/10.98 (coll Q (skS.0 4 a) H)) % 10.77/10.98 (perp P F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.77/10.98 coll P Q T)) % 10.77/10.98 True % 10.77/10.98 Clause #464 (by clausification #[463]): ∀ (a a_1 a_2 : Iota), % 10.77/10.98 Eq % 10.77/10.98 (∀ (F H T Q P : Iota), % 10.77/10.98 And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And % 10.77/10.98 (And (perp F (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.77/10.98 (coll F (skS.0 4 a) (skS.0 5 a a_1))) % 10.77/10.98 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) H)) % 10.77/10.98 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) H)) % 10.77/10.98 (perp T F (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (perp Q F (skS.0 4 a) H)) % 10.77/10.98 (coll Q (skS.0 4 a) H)) % 10.77/10.98 (perp P F (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.77/10.98 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.77/10.98 coll P Q T) % 10.77/10.98 False % 10.77/10.98 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota), % 10.84/11.00 Eq % 10.84/11.00 (Not % 10.84/11.00 (∀ (H T Q P : Iota), % 10.84/11.00 And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.00 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.00 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) H)) % 10.84/11.00 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) H)) % 10.84/11.00 (perp T (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (perp Q (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) H)) % 10.84/11.00 (coll Q (skS.0 4 a) H)) % 10.84/11.00 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.00 coll P Q T)) % 10.84/11.00 True % 10.84/11.00 Clause #466 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota), % 10.84/11.00 Eq % 10.84/11.00 (∀ (H T Q P : Iota), % 10.84/11.00 And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.00 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.00 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) H)) % 10.84/11.00 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) H)) % 10.84/11.00 (perp T (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (perp Q (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) H)) % 10.84/11.00 (coll Q (skS.0 4 a) H)) % 10.84/11.00 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.00 coll P Q T) % 10.84/11.00 False % 10.84/11.00 Clause #467 (by clausification #[466]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.84/11.00 Eq % 10.84/11.00 (Not % 10.84/11.00 (∀ (T Q P : Iota), % 10.84/11.00 And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.00 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.00 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.00 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.00 (perp T (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (perp Q (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))) % 10.84/11.00 (coll Q (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.00 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.00 coll P Q T)) % 10.84/11.00 True % 10.84/11.00 Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.84/11.00 Eq % 10.84/11.00 (∀ (T Q P : Iota), % 10.84/11.00 And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And % 10.84/11.00 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.00 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.00 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.00 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.00 (perp T (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.00 (coll T (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.02 (perp Q (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))) % 10.84/11.02 (coll Q (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.02 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.02 coll P Q T) % 10.84/11.02 False % 10.84/11.02 Clause #469 (by clausification #[468]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.84/11.02 Eq % 10.84/11.02 (Not % 10.84/11.02 (∀ (Q P : Iota), % 10.84/11.02 And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.02 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.02 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) % 10.84/11.02 (skS.0 6 a a_1 a_2))) % 10.84/11.02 (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))) % 10.84/11.02 (perp Q (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))) % 10.84/11.02 (coll Q (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.02 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.02 coll P Q (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.84/11.02 True % 10.84/11.02 Clause #470 (by clausification #[469]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.84/11.02 Eq % 10.84/11.02 (∀ (Q P : Iota), % 10.84/11.02 And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.02 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.02 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.02 (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))) % 10.84/11.02 (perp Q (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))) % 10.84/11.02 (coll Q (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.02 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.02 coll P Q (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.84/11.02 False % 10.84/11.02 Clause #471 (by clausification #[470]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.84/11.02 Eq % 10.84/11.02 (Not % 10.84/11.02 (∀ (P : Iota), % 10.84/11.02 And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And % 10.84/11.02 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.02 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.02 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) % 10.84/11.02 (skS.0 6 a a_1 a_2))) % 10.84/11.02 (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))) % 10.84/11.02 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) % 10.84/11.02 (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.02 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.04 coll P (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.84/11.04 True % 10.84/11.04 Clause #472 (by clausification #[471]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.84/11.04 Eq % 10.84/11.04 (∀ (P : Iota), % 10.84/11.04 And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.04 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.04 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (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))) % 10.84/11.04 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) % 10.84/11.04 (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp P (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (coll P (skS.0 4 a) (skS.0 6 a a_1 a_2)) → % 10.84/11.04 coll P (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.84/11.04 False % 10.84/11.04 Clause #473 (by clausification #[472]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.84/11.04 Eq % 10.84/11.04 (Not % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.04 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.04 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (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))) % 10.84/11.04 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) % 10.84/11.04 (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (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 6 a a_1 a_2)) → % 10.84/11.04 coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) % 10.84/11.04 (skS.0 9 a a_1 a_2 a_3 a_4 a_5))) % 10.84/11.04 True % 10.84/11.04 Clause #474 (by clausification #[473]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.84/11.04 Eq % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And % 10.84/11.04 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.04 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.04 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.04 (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))) % 10.84/11.04 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) % 10.84/11.04 (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.04 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.06 (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 6 a a_1 a_2)) → % 10.84/11.06 coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) % 10.84/11.06 (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.84/11.06 False % 10.84/11.06 Clause #475 (by clausification #[474]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.84/11.06 Eq % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.06 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.06 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.06 (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))) % 10.84/11.06 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.06 (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 6 a a_1 a_2))) % 10.84/11.06 True % 10.84/11.06 Clause #476 (by clausification #[474]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.84/11.06 Eq % 10.84/11.06 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5)) % 10.84/11.06 False % 10.84/11.06 Clause #478 (by clausification #[475]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.84/11.06 Eq % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And % 10.84/11.06 (And (perp (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 5 a a_1)) % 10.84/11.06 (coll (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 5 a a_1))) % 10.84/11.06 (perp (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 5 a a_1) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 9 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2 a_3) (skS.0 5 a a_1) (skS.0 6 a a_1 a_2))) % 10.84/11.06 (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))) % 10.84/11.06 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 4 a) (skS.0 8 a a_1 a_2 a_3 a_4))) % 10.84/11.06 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2))) % 10.84/11.06 True % 10.84/11.06 Clause #503 (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 % 10.84/11.06 Clause #504 (by clausification #[503]): ∀ (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 % 10.84/11.06 Clause #505 (by clausification #[504]): ∀ (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 % 10.84/11.06 Clause #506 (by clausification #[505]): ∀ (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 % 10.84/11.06 Clause #507 (by clausification #[506]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.84/11.06 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 % 10.84/11.06 Clause #508 (by clausification #[507]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 10.84/11.06 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 % 10.84/11.06 Clause #509 (by clausification #[508]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 10.84/11.06 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 % 10.84/11.06 Clause #510 (by clausification #[509]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 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 % 10.91/11.08 Clause #511 (by clausification #[510]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 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) % 10.91/11.08 Clause #639 (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 % 10.91/11.08 Clause #640 (by clausification #[639]): ∀ (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 % 10.91/11.08 Clause #641 (by clausification #[640]): ∀ (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 % 10.91/11.08 Clause #642 (by clausification #[641]): ∀ (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 % 10.91/11.08 Clause #643 (by clausification #[642]): ∀ (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 % 10.91/11.08 Clause #644 (by clausification #[643]): ∀ (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 % 10.91/11.08 Clause #645 (by clausification #[644]): ∀ (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) % 10.91/11.08 Clause #881 (by clausification #[478]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True % 10.91/11.08 Clause #883 (by superposition #[881, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 Or (Eq True False) % 10.91/11.08 (Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) % 10.91/11.08 Clause #884 (by superposition #[881, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 Or (Eq True False) % 10.91/11.08 (Eq (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3)) True) % 10.91/11.08 Clause #1352 (by clausification #[884]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 Eq (perp (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3)) True % 10.91/11.08 Clause #1355 (by superposition #[1352, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 10.91/11.08 Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True) % 10.91/11.08 (Or (Eq True False) (Eq (perp (skS.0 11 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 7 a a_1 a_2 a_5) a_3 a_4) False)) % 10.91/11.08 Clause #1419 (by clausification #[883]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 10.91/11.08 Eq (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2 a_3) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 10.91/11.08 Clause #1497 (by clausification #[1355]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 10.91/11.08 Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True) % 10.91/11.08 (Eq (perp (skS.0 11 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 7 a a_1 a_2 a_5) a_3 a_4) False) % 10.91/11.08 Clause #1499 (by superposition #[1497, 1419]): ∀ (a a_1 a_2 : Iota), % 10.91/11.08 Or (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) (Eq False True) % 10.91/11.08 Clause #1500 (by clausification #[1499]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 10.91/11.08 Clause #1503 (by superposition #[1500, 156]): ∀ (a a_1 a_2 : Iota), % 10.91/11.08 Or (Eq True False) (Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True) % 10.91/11.08 Clause #1525 (by clausification #[1503]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2)) True % 10.91/11.08 Clause #1529 (by superposition #[1525, 645]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.91/11.08 Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True) % 10.91/11.08 Clause #1530 (by clausification #[1529]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.91/11.08 Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4) True % 10.91/11.08 Clause #1537 (by superposition #[1530, 511]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.91/11.08 Or (Eq True False) (Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_3 a_4) True) % 10.94/11.11 Clause #1542 (by clausification #[1537]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Eq (eqangle (skS.0 4 a) (skS.0 6 a a_1 a_2) (skS.0 4 a) (skS.0 6 a a_1 a_2) a_3 a_4 a_3 a_4) True % 10.94/11.11 Clause #1548 (by superposition #[1542, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Or (Eq True False) % 10.94/11.11 (Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True) % 10.94/11.11 Clause #1555 (by clausification #[1548]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Eq (eqangle a a_1 a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True % 10.94/11.11 Clause #1559 (by superposition #[1555, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Or (Eq True False) % 10.94/11.11 (Eq (eqangle a a_1 a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True) % 10.94/11.11 Clause #1566 (by clausification #[1559]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Eq (eqangle a a_1 a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True % 10.94/11.11 Clause #1573 (by superposition #[1566, 511]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Or (Eq True False) % 10.94/11.11 (Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True) % 10.94/11.11 Clause #1578 (by clausification #[1573]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 10.94/11.11 Eq (eqangle a a_1 (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4) a_1 a (skS.0 4 a_2) (skS.0 6 a_2 a_3 a_4)) True % 10.94/11.11 Clause #1582 (by superposition #[1578, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 10.94/11.11 Clause #1591 (by clausification #[1582]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 10.94/11.11 Clause #1599 (by superposition #[1591, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 10.94/11.11 Clause #1628 (by clausification #[1599]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 10.94/11.11 Clause #1629 (by superposition #[1628, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 10.94/11.11 Clause #1634 (by clausification #[1629]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 10.94/11.11 Clause #1646 (by superposition #[1634, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 10.94/11.11 Clause #1655 (by clausification #[1646]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 10.94/11.11 Clause #1668 (by superposition #[1655, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 10.94/11.11 Clause #1677 (by clausification #[1668]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 10.94/11.11 Clause #1690 (by superposition #[1677, 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)) % 10.94/11.11 Clause #1782 (by clausification #[1690]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 10.94/11.11 Clause #1789 (by superposition #[1782, 1677]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 10.94/11.11 Clause #1790 (by clausification #[1789]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 10.94/11.11 Clause #1828 (by superposition #[1790, 476]): Eq True False % 10.94/11.11 Clause #1829 (by clausification #[1828]): False % 10.94/11.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------