%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GEO612+1 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:48:45 PM UTC 2025 % Result : Theorem 35.32s 35.56s % Output : Proof 35.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : GEO612+1 : TPTP v9.2.0. Released v7.5.0. % 0.06/0.13 % Command : duper %s % 0.12/0.34 % Computer : n006.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 12:05:08 EDT 2025 % 0.12/0.34 % CPUTime : % 35.32/35.56 SZS status Theorem for theBenchmark.p % 35.32/35.56 SZS output start Proof for theBenchmark.p % 35.32/35.56 Clause #0 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll A C B) True % 35.32/35.56 Clause #1 (by assumption #[]): Eq (∀ (A B C : Iota), coll A B C → coll B A C) True % 35.32/35.56 Clause #2 (by assumption #[]): Eq (∀ (A B C D : Iota), And (coll A B C) (coll A B D) → coll C D A) True % 35.32/35.56 Clause #3 (by assumption #[]): Eq (∀ (A B C D : Iota), para A B C D → para A B D C) True % 35.32/35.56 Clause #6 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp A B D C) True % 35.32/35.56 Clause #7 (by assumption #[]): Eq (∀ (A B C D : Iota), perp A B C D → perp C D A B) True % 35.32/35.56 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 % 35.32/35.56 Clause #13 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A B D C) True % 35.32/35.56 Clause #14 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic A C B D) True % 35.32/35.56 Clause #15 (by assumption #[]): Eq (∀ (A B C D : Iota), cyclic A B C D → cyclic B A C D) True % 35.32/35.56 Clause #16 (by assumption #[]): Eq (∀ (A B C D E : Iota), And (cyclic A B C D) (cyclic A B C E) → cyclic B C D E) True % 35.32/35.56 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 % 35.32/35.56 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 % 35.32/35.56 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 % 35.32/35.56 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 % 35.32/35.56 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 % 35.32/35.56 Clause #42 (by assumption #[]): Eq (∀ (A B P Q : Iota), And (eqangle P A P B Q A Q B) (coll P Q B) → cyclic A B P Q) True % 35.32/35.56 Clause #66 (by assumption #[]): Eq (∀ (A B C : Iota), para A B A C → coll A B C) True % 35.32/35.56 Clause #94 (by assumption #[]): Eq % 35.32/35.56 (Not % 35.32/35.56 (∀ (A B C O G D E F NWPNT1 : Iota), % 35.32/35.56 And % 35.32/35.56 (And % 35.32/35.56 (And % 35.32/35.56 (And % 35.32/35.56 (And (And (And (And (circle O A B C) (perp G C A B)) (coll G A B)) (circle O C D NWPNT1)) (coll D C G)) % 35.32/35.56 (perp E D A C)) % 35.32/35.56 (coll E A C)) % 35.32/35.56 (perp F D B C)) % 35.32/35.56 (coll F B C) → % 35.32/35.56 cyclic A E F B)) % 35.32/35.56 True % 35.32/35.56 Clause #104 (by clausification #[66]): ∀ (a : Iota), Eq (∀ (B C : Iota), para a B a C → coll a B C) True % 35.32/35.56 Clause #105 (by clausification #[104]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), para a a_1 a C → coll a a_1 C) True % 35.32/35.56 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 % 35.32/35.56 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) % 35.32/35.56 Clause #112 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll B a C) True % 35.32/35.56 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a_1 a C) True % 35.32/35.56 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 % 35.32/35.56 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) % 35.32/35.56 Clause #116 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (B C : Iota), coll a B C → coll a C B) True % 35.32/35.56 Clause #117 (by clausification #[116]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), coll a a_1 C → coll a C a_1) True % 35.32/35.56 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 % 35.32/35.56 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) % 35.32/35.56 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 % 35.32/35.56 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 % 35.32/35.56 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 % 35.39/35.62 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 % 35.39/35.62 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) % 35.39/35.62 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)) % 35.39/35.62 Clause #152 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B C D : Iota), para a B C D → para a B D C) True % 35.39/35.62 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 % 35.39/35.62 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 % 35.39/35.62 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 % 35.39/35.62 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) % 35.39/35.62 Clause #157 (by clausification #[42]): ∀ (a : Iota), Eq (∀ (B P Q : Iota), And (eqangle P a P B Q a Q B) (coll P Q B) → cyclic a B P Q) True % 35.39/35.62 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), Eq (∀ (P Q : Iota), And (eqangle P a P a_1 Q a Q a_1) (coll P Q a_1) → cyclic a a_1 P Q) True % 35.39/35.62 Clause #159 (by clausification #[158]): ∀ (a a_1 a_2 : Iota), Eq (∀ (Q : Iota), And (eqangle a a_1 a a_2 Q a_1 Q a_2) (coll a Q a_2) → cyclic a_1 a_2 a Q) True % 35.39/35.62 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 a_3 : Iota), Eq (And (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) (coll a a_3 a_2) → cyclic a_1 a_2 a a_3) True % 35.39/35.62 Clause #161 (by clausification #[160]): ∀ (a a_1 a_2 a_3 : Iota), % 35.39/35.62 Or (Eq (And (eqangle a a_1 a a_2 a_3 a_1 a_3 a_2) (coll a a_3 a_2)) False) (Eq (cyclic a_1 a_2 a a_3) True) % 35.39/35.62 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 a_3 : Iota), % 35.39/35.62 Or (Eq (cyclic a a_1 a_2 a_3) True) % 35.39/35.62 (Or (Eq (eqangle a_2 a a_2 a_1 a_3 a a_3 a_1) False) (Eq (coll a_2 a_3 a_1) False)) % 35.39/35.62 Clause #170 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic B a C D) True % 35.39/35.62 Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a_1 a C D) True % 35.39/35.62 Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a_1 a a_2 D) True % 35.39/35.62 Clause #173 (by clausification #[172]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a_1 a a_2 a_3) True % 35.39/35.62 Clause #174 (by clausification #[173]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a_1 a a_2 a_3) True) % 35.39/35.62 Clause #175 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a C B D) True % 35.39/35.62 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a C a_1 D) True % 35.39/35.62 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a a_2 a_1 D) True % 35.39/35.62 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a a_2 a_1 a_3) True % 35.39/35.62 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a a_2 a_1 a_3) True) % 35.39/35.62 Clause #180 (by clausification #[13]): ∀ (a : Iota), Eq (∀ (B C D : Iota), cyclic a B C D → cyclic a B D C) True % 35.39/35.62 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), Eq (∀ (C D : Iota), cyclic a a_1 C D → cyclic a a_1 D C) True % 35.39/35.62 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D : Iota), cyclic a a_1 a_2 D → cyclic a a_1 D a_2) True % 35.39/35.62 Clause #183 (by clausification #[182]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3 → cyclic a a_1 a_3 a_2) True % 35.39/35.62 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) False) (Eq (cyclic a a_1 a_3 a_2) True) % 35.39/35.62 Clause #261 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp a B D C) True % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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) % 35.39/35.67 Clause #266 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B C D : Iota), perp a B C D → perp C D a B) True % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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) % 35.39/35.67 Clause #284 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (B C D E : Iota), And (cyclic a B C D) (cyclic a B C E) → cyclic B C D E) True % 35.39/35.67 Clause #285 (by clausification #[284]): ∀ (a a_1 : Iota), Eq (∀ (C D E : Iota), And (cyclic a a_1 C D) (cyclic a a_1 C E) → cyclic a_1 C D E) True % 35.39/35.67 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 : Iota), Eq (∀ (D E : Iota), And (cyclic a a_1 a_2 D) (cyclic a a_1 a_2 E) → cyclic a_1 a_2 D E) True % 35.39/35.67 Clause #287 (by clausification #[286]): ∀ (a a_1 a_2 a_3 : Iota), Eq (∀ (E : Iota), And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 E) → cyclic a_1 a_2 a_3 E) True % 35.39/35.67 Clause #288 (by clausification #[287]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4) → cyclic a_1 a_2 a_3 a_4) True % 35.39/35.67 Clause #289 (by clausification #[288]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.39/35.67 Or (Eq (And (cyclic a a_1 a_2 a_3) (cyclic a a_1 a_2 a_4)) False) (Eq (cyclic a_1 a_2 a_3 a_4) True) % 35.39/35.67 Clause #290 (by clausification #[289]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.39/35.67 Or (Eq (cyclic a a_1 a_2 a_3) True) (Or (Eq (cyclic a_4 a a_1 a_2) False) (Eq (cyclic a_4 a a_1 a_3) False)) % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.39/35.67 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) % 35.39/35.67 Clause #305 (by clausification #[304]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.39/35.67 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)) % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.39/35.67 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 % 35.44/35.73 Clause #348 (by clausification #[347]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #349 (by clausification #[348]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #350 (by clausification #[349]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #351 (by clausification #[350]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #352 (by clausification #[351]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.44/35.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) % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.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) % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.73 Clause #437 (by clausification #[436]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #438 (by clausification #[437]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #439 (by clausification #[438]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #440 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.44/35.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 % 35.44/35.73 Clause #441 (by clausification #[440]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.44/35.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) % 35.44/35.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 % 35.44/35.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 % 35.44/35.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 % 35.44/35.73 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 % 35.53/35.78 Clause #492 (by clausification #[491]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.53/35.78 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 % 35.53/35.78 Clause #493 (by clausification #[492]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.53/35.78 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 % 35.53/35.78 Clause #494 (by clausification #[493]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.53/35.78 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 % 35.53/35.78 Clause #495 (by clausification #[494]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.53/35.78 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 % 35.53/35.78 Clause #496 (by clausification #[495]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.53/35.78 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) % 35.53/35.78 Clause #604 (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 % 35.53/35.78 Clause #605 (by clausification #[604]): ∀ (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 % 35.53/35.78 Clause #606 (by clausification #[605]): ∀ (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 % 35.53/35.78 Clause #607 (by clausification #[606]): ∀ (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 % 35.53/35.78 Clause #608 (by clausification #[607]): ∀ (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 % 35.53/35.78 Clause #609 (by clausification #[608]): ∀ (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 % 35.53/35.78 Clause #610 (by clausification #[609]): ∀ (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) % 35.53/35.78 Clause #611 (by clausification #[94]): Eq % 35.53/35.78 (∀ (A B C O G D E F NWPNT1 : Iota), % 35.53/35.78 And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And (And (And (And (And (circle O A B C) (perp G C A B)) (coll G A B)) (circle O C D NWPNT1)) (coll D C G)) % 35.53/35.78 (perp E D A C)) % 35.53/35.78 (coll E A C)) % 35.53/35.78 (perp F D B C)) % 35.53/35.78 (coll F B C) → % 35.53/35.78 cyclic A E F B) % 35.53/35.78 False % 35.53/35.78 Clause #612 (by clausification #[611]): ∀ (a : Iota), % 35.53/35.78 Eq % 35.53/35.78 (Not % 35.53/35.78 (∀ (B C O G D E F NWPNT1 : Iota), % 35.53/35.78 And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And (And (And (circle O (skS.0 5 a) B C) (perp G C (skS.0 5 a) B)) (coll G (skS.0 5 a) B)) % 35.53/35.78 (circle O C D NWPNT1)) % 35.53/35.78 (coll D C G)) % 35.53/35.78 (perp E D (skS.0 5 a) C)) % 35.53/35.78 (coll E (skS.0 5 a) C)) % 35.53/35.78 (perp F D B C)) % 35.53/35.78 (coll F B C) → % 35.53/35.78 cyclic (skS.0 5 a) E F B)) % 35.53/35.78 True % 35.53/35.78 Clause #613 (by clausification #[612]): ∀ (a : Iota), % 35.53/35.78 Eq % 35.53/35.78 (∀ (B C O G D E F NWPNT1 : Iota), % 35.53/35.78 And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And (And (And (circle O (skS.0 5 a) B C) (perp G C (skS.0 5 a) B)) (coll G (skS.0 5 a) B)) % 35.53/35.78 (circle O C D NWPNT1)) % 35.53/35.78 (coll D C G)) % 35.53/35.78 (perp E D (skS.0 5 a) C)) % 35.53/35.78 (coll E (skS.0 5 a) C)) % 35.53/35.78 (perp F D B C)) % 35.53/35.78 (coll F B C) → % 35.53/35.78 cyclic (skS.0 5 a) E F B) % 35.53/35.78 False % 35.53/35.78 Clause #614 (by clausification #[613]): ∀ (a a_1 : Iota), % 35.53/35.78 Eq % 35.53/35.78 (Not % 35.53/35.78 (∀ (C O G D E F NWPNT1 : Iota), % 35.53/35.78 And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And % 35.53/35.78 (And (And (circle O (skS.0 5 a) (skS.0 6 a a_1) C) (perp G C (skS.0 5 a) (skS.0 6 a a_1))) % 35.53/35.78 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.53/35.78 (circle O C D NWPNT1)) % 35.53/35.78 (coll D C G)) % 35.53/35.78 (perp E D (skS.0 5 a) C)) % 35.53/35.78 (coll E (skS.0 5 a) C)) % 35.57/35.83 (perp F D (skS.0 6 a a_1) C)) % 35.57/35.83 (coll F (skS.0 6 a a_1) C) → % 35.57/35.83 cyclic (skS.0 5 a) E F (skS.0 6 a a_1))) % 35.57/35.83 True % 35.57/35.83 Clause #615 (by clausification #[614]): ∀ (a a_1 : Iota), % 35.57/35.83 Eq % 35.57/35.83 (∀ (C O G D E F NWPNT1 : Iota), % 35.57/35.83 And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And (And (circle O (skS.0 5 a) (skS.0 6 a a_1) C) (perp G C (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (circle O C D NWPNT1)) % 35.57/35.83 (coll D C G)) % 35.57/35.83 (perp E D (skS.0 5 a) C)) % 35.57/35.83 (coll E (skS.0 5 a) C)) % 35.57/35.83 (perp F D (skS.0 6 a a_1) C)) % 35.57/35.83 (coll F (skS.0 6 a a_1) C) → % 35.57/35.83 cyclic (skS.0 5 a) E F (skS.0 6 a a_1)) % 35.57/35.83 False % 35.57/35.83 Clause #616 (by clausification #[615]): ∀ (a a_1 a_2 : Iota), % 35.57/35.83 Eq % 35.57/35.83 (Not % 35.57/35.83 (∀ (O G D E F NWPNT1 : Iota), % 35.57/35.83 And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And (circle O (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.57/35.83 (perp G (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (circle O (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.57/35.83 (coll D (skS.0 7 a a_1 a_2) G)) % 35.57/35.83 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.57/35.83 cyclic (skS.0 5 a) E F (skS.0 6 a a_1))) % 35.57/35.83 True % 35.57/35.83 Clause #617 (by clausification #[616]): ∀ (a a_1 a_2 : Iota), % 35.57/35.83 Eq % 35.57/35.83 (∀ (O G D E F NWPNT1 : Iota), % 35.57/35.83 And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And (circle O (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.57/35.83 (perp G (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (circle O (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.57/35.83 (coll D (skS.0 7 a a_1 a_2) G)) % 35.57/35.83 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.57/35.83 cyclic (skS.0 5 a) E F (skS.0 6 a a_1)) % 35.57/35.83 False % 35.57/35.83 Clause #618 (by clausification #[617]): ∀ (a a_1 a_2 a_3 : Iota), % 35.57/35.83 Eq % 35.57/35.83 (Not % 35.57/35.83 (∀ (G D E F NWPNT1 : Iota), % 35.57/35.83 And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.57/35.83 (perp G (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.57/35.83 (coll D (skS.0 7 a a_1 a_2) G)) % 35.57/35.83 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.57/35.83 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.57/35.83 cyclic (skS.0 5 a) E F (skS.0 6 a a_1))) % 35.57/35.83 True % 35.57/35.83 Clause #619 (by clausification #[618]): ∀ (a a_1 a_2 a_3 : Iota), % 35.57/35.83 Eq % 35.57/35.83 (∀ (G D E F NWPNT1 : Iota), % 35.57/35.83 And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And % 35.57/35.83 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.57/35.83 (perp G (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (coll G (skS.0 5 a) (skS.0 6 a a_1))) % 35.57/35.83 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.61/35.89 (coll D (skS.0 7 a a_1 a_2) G)) % 35.61/35.89 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.61/35.89 cyclic (skS.0 5 a) E F (skS.0 6 a a_1)) % 35.61/35.89 False % 35.61/35.89 Clause #620 (by clausification #[619]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.61/35.89 Eq % 35.61/35.89 (Not % 35.61/35.89 (∀ (D E F NWPNT1 : Iota), % 35.61/35.89 And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.61/35.89 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.61/35.89 (coll D (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.61/35.89 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.61/35.89 cyclic (skS.0 5 a) E F (skS.0 6 a a_1))) % 35.61/35.89 True % 35.61/35.89 Clause #621 (by clausification #[620]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.61/35.89 Eq % 35.61/35.89 (∀ (D E F NWPNT1 : Iota), % 35.61/35.89 And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.61/35.89 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) D NWPNT1)) % 35.61/35.89 (coll D (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.61/35.89 (perp E D (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (perp F D (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.61/35.89 cyclic (skS.0 5 a) E F (skS.0 6 a a_1)) % 35.61/35.89 False % 35.61/35.89 Clause #622 (by clausification #[621]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.61/35.89 Eq % 35.61/35.89 (Not % 35.61/35.89 (∀ (E F NWPNT1 : Iota), % 35.61/35.89 And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.61/35.89 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.61/35.89 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.61/35.89 (perp E (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (perp F (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.61/35.89 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.61/35.89 cyclic (skS.0 5 a) E F (skS.0 6 a a_1))) % 35.61/35.89 True % 35.61/35.89 Clause #623 (by clausification #[622]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 35.61/35.89 Eq % 35.61/35.89 (∀ (E F NWPNT1 : Iota), % 35.61/35.89 And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And % 35.61/35.89 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.61/35.89 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.61/35.89 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.67/35.93 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.67/35.93 (perp E (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll E (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (perp F (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.67/35.93 cyclic (skS.0 5 a) E F (skS.0 6 a a_1)) % 35.67/35.93 False % 35.67/35.93 Clause #624 (by clausification #[623]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.67/35.93 Eq % 35.67/35.93 (Not % 35.67/35.93 (∀ (F NWPNT1 : Iota), % 35.67/35.93 And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.67/35.93 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.67/35.93 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.67/35.93 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.67/35.93 (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (perp F (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.67/35.93 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) F (skS.0 6 a a_1))) % 35.67/35.93 True % 35.67/35.93 Clause #625 (by clausification #[624]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 35.67/35.93 Eq % 35.67/35.93 (∀ (F NWPNT1 : Iota), % 35.67/35.93 And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.67/35.93 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.67/35.93 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.67/35.93 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.67/35.93 (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (perp F (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll F (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.67/35.93 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) F (skS.0 6 a a_1)) % 35.67/35.93 False % 35.67/35.93 Clause #626 (by clausification #[625]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.67/35.93 Eq % 35.67/35.93 (Not % 35.67/35.93 (∀ (NWPNT1 : Iota), % 35.67/35.93 And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And % 35.67/35.93 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.67/35.93 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.67/35.93 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.67/35.93 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.67/35.93 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.67/35.93 (skS.0 7 a a_1 a_2))) % 35.67/35.93 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/35.99 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/35.99 (skS.0 7 a a_1 a_2))) % 35.73/35.99 (coll (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.73/35.99 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 35.73/35.99 (skS.0 6 a a_1))) % 35.73/35.99 True % 35.73/35.99 Clause #627 (by clausification #[626]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/35.99 Eq % 35.73/35.99 (∀ (NWPNT1 : Iota), % 35.73/35.99 And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/35.99 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) NWPNT1)) % 35.73/35.99 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.73/35.99 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.73/35.99 (skS.0 7 a a_1 a_2))) % 35.73/35.99 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/35.99 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/35.99 (skS.0 7 a a_1 a_2))) % 35.73/35.99 (coll (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.73/35.99 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 35.73/35.99 (skS.0 6 a a_1)) % 35.73/35.99 False % 35.73/35.99 Clause #628 (by clausification #[627]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 35.73/35.99 Eq % 35.73/35.99 (Not % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/35.99 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.73/35.99 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 35.73/35.99 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.73/35.99 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.73/35.99 (skS.0 7 a a_1 a_2))) % 35.73/35.99 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/35.99 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/35.99 (skS.0 7 a a_1 a_2))) % 35.73/35.99 (coll (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.73/35.99 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 35.73/35.99 (skS.0 6 a a_1))) % 35.73/35.99 True % 35.73/35.99 Clause #629 (by clausification #[628]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 35.73/35.99 Eq % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And % 35.73/35.99 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/35.99 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/35.99 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.73/35.99 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 35.73/35.99 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.73/35.99 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.73/36.04 (skS.0 7 a a_1 a_2))) % 35.73/36.04 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/36.04 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/36.04 (skS.0 7 a a_1 a_2))) % 35.73/36.04 (coll (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) → % 35.73/36.04 cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1)) % 35.73/36.04 False % 35.73/36.04 Clause #630 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 35.73/36.04 Eq % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/36.04 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/36.04 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/36.04 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.73/36.04 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 35.73/36.04 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.73/36.04 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) % 35.73/36.04 (skS.0 7 a a_1 a_2))) % 35.73/36.04 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/36.04 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/36.04 (skS.0 7 a a_1 a_2))) % 35.73/36.04 (coll (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2))) % 35.73/36.04 True % 35.73/36.04 Clause #631 (by clausification #[629]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/36.04 Eq (cyclic (skS.0 5 a) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1)) % 35.73/36.04 False % 35.73/36.04 Clause #633 (by clausification #[630]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 35.73/36.04 Eq % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And % 35.73/36.04 (And (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 5 a) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/36.04 (perp (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 7 a a_1 a_2) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/36.04 (coll (skS.0 9 a a_1 a_2 a_3 a_4) (skS.0 5 a) (skS.0 6 a a_1))) % 35.73/36.04 (circle (skS.0 8 a a_1 a_2 a_3) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.73/36.04 (skS.0 13 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 35.73/36.04 (coll (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 7 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4))) % 35.73/36.04 (perp (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/36.04 (coll (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 5 a) (skS.0 7 a a_1 a_2))) % 35.73/36.04 (perp (skS.0 12 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) (skS.0 6 a a_1) % 35.73/36.04 (skS.0 7 a a_1 a_2))) % 35.73/36.04 True % 35.73/36.04 Clause #883 (by clausification #[633]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/36.04 Eq % 35.73/36.04 (perp (skS.0 12 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) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.73/36.04 True % 35.73/36.04 Clause #885 (by superposition #[883, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/36.04 Or (Eq True False) % 35.73/36.04 (Eq % 35.73/36.04 (perp (skS.0 12 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) (skS.0 7 a a_1 a_2) % 35.73/36.04 (skS.0 6 a a_1)) % 35.73/36.04 True) % 35.73/36.04 Clause #886 (by superposition #[883, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/36.04 Or (Eq True False) % 35.73/36.04 (Eq % 35.73/36.04 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 35.73/36.04 (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 35.73/36.04 True) % 35.73/36.04 Clause #1669 (by clausification #[886]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.73/36.04 Eq % 35.73/36.04 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 12 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)) % 35.73/36.04 True % 35.73/36.04 Clause #1670 (by superposition #[1669, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq % 35.87/36.10 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.87/36.10 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 35.87/36.10 True) % 35.87/36.10 Clause #1681 (by clausification #[1670]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 35.87/36.10 True % 35.87/36.10 Clause #1682 (by superposition #[1681, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq % 35.87/36.10 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) % 35.87/36.10 (skS.0 7 a a_1 a_2)) % 35.87/36.10 True) % 35.87/36.10 Clause #1692 (by clausification #[1682]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2)) % 35.87/36.10 True % 35.87/36.10 Clause #1693 (by superposition #[1692, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq % 35.87/36.10 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) % 35.87/36.10 (skS.0 6 a a_1)) % 35.87/36.10 True) % 35.87/36.10 Clause #1704 (by clausification #[1693]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1)) % 35.87/36.10 True % 35.87/36.10 Clause #1705 (by superposition #[1704, 270]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq % 35.87/36.10 (perp (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) % 35.87/36.10 (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 35.87/36.10 True) % 35.87/36.10 Clause #1715 (by clausification #[1705]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 10 a a_1 a_2 a_3 a_4 a_5) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 35.87/36.10 True % 35.87/36.10 Clause #1716 (by superposition #[1715, 265]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq % 35.87/36.10 (perp (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 12 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 35.87/36.10 (skS.0 10 a a_1 a_2 a_3 a_4 a_5)) % 35.87/36.10 True) % 35.87/36.10 Clause #1726 (by clausification #[1716]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 12 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)) % 35.87/36.10 True % 35.87/36.10 Clause #1727 (by superposition #[1726, 305]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 35.87/36.10 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4) True) % 35.87/36.10 (Or (Eq True False) % 35.87/36.10 (Eq (perp (skS.0 12 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 10 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False)) % 35.87/36.10 Clause #1736 (by clausification #[885]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 35.87/36.10 Eq % 35.87/36.10 (perp (skS.0 12 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) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1)) % 35.87/36.10 True % 35.87/36.10 Clause #1757 (by clausification #[1727]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 35.87/36.10 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4) True) % 35.87/36.10 (Eq (perp (skS.0 12 a a_1 a_2 a_5 a_6 a_7 a_8 a_9) (skS.0 10 a a_1 a_2 a_5 a_6 a_7) a_3 a_4) False) % 35.87/36.10 Clause #1759 (by superposition #[1757, 1736]): ∀ (a a_1 a_2 : Iota), % 35.87/36.10 Or (Eq (para (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1)) True) (Eq False True) % 35.87/36.10 Clause #1760 (by clausification #[1759]): ∀ (a a_1 a_2 : Iota), Eq (para (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1)) True % 35.87/36.10 Clause #1765 (by superposition #[1760, 610]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4) True) % 35.87/36.10 Clause #1796 (by clausification #[1765]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.87/36.10 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4 (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4) True % 35.87/36.10 Clause #1804 (by superposition #[1796, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.87/36.10 Or (Eq True False) % 35.87/36.10 (Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4 a_3 a_4) True) % 35.87/36.10 Clause #1808 (by clausification #[1804]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Eq (eqangle (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) (skS.0 7 a a_1 a_2) (skS.0 6 a a_1) a_3 a_4 a_3 a_4) True % 35.91/36.15 Clause #1814 (by superposition #[1808, 441]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Or (Eq True False) % 35.91/36.15 (Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True) % 35.91/36.15 Clause #1820 (by clausification #[1814]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Eq (eqangle a a_1 a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True % 35.91/36.15 Clause #1824 (by superposition #[1820, 352]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Or (Eq True False) % 35.91/36.15 (Eq (eqangle a a_1 a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True) % 35.91/36.15 Clause #1833 (by clausification #[1824]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Eq (eqangle a a_1 a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True % 35.91/36.15 Clause #1840 (by superposition #[1833, 496]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Or (Eq True False) % 35.91/36.15 (Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True) % 35.91/36.15 Clause #1845 (by clausification #[1840]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 35.91/36.15 Eq (eqangle a a_1 (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3) a_1 a (skS.0 7 a_2 a_3 a_4) (skS.0 6 a_2 a_3)) True % 35.91/36.15 Clause #1849 (by superposition #[1845, 359]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a_1 a) True) % 35.91/36.15 Clause #1858 (by clausification #[1849]): ∀ (a a_1 : Iota), Eq (para a a_1 a_1 a) True % 35.91/36.15 Clause #1868 (by superposition #[1858, 156]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (para a a_1 a a_1) True) % 35.91/36.15 Clause #1888 (by clausification #[1868]): ∀ (a a_1 : Iota), Eq (para a a_1 a a_1) True % 35.91/36.15 Clause #1889 (by superposition #[1888, 107]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a_1) True) % 35.91/36.15 Clause #1893 (by superposition #[1888, 610]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True) % 35.91/36.15 Clause #1906 (by clausification #[1889]): ∀ (a a_1 : Iota), Eq (coll a a_1 a_1) True % 35.91/36.15 Clause #1917 (by superposition #[1906, 115]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a_1 a) True) % 35.91/36.15 Clause #1926 (by clausification #[1917]): ∀ (a a_1 : Iota), Eq (coll a a_1 a) True % 35.91/36.15 Clause #1941 (by superposition #[1926, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (coll a a a_1) True) % 35.91/36.15 Clause #1950 (by clausification #[1941]): ∀ (a a_1 : Iota), Eq (coll a a a_1) True % 35.91/36.15 Clause #1965 (by superposition #[1950, 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)) % 35.91/36.15 Clause #2071 (by clausification #[1893]): ∀ (a a_1 a_2 a_3 : Iota), Eq (eqangle a a_1 a_2 a_3 a a_1 a_2 a_3) True % 35.91/36.15 Clause #2072 (by superposition #[2071, 162]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Or (Eq True False) (Eq (coll a_2 a_2 a_1) False)) % 35.91/36.15 Clause #2080 (by clausification #[1965]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 35.91/36.15 Clause #2086 (by superposition #[2080, 1950]): ∀ (a a_1 a_2 : Iota), Or (Eq (coll a a_1 a_2) True) (Eq False True) % 35.91/36.15 Clause #2087 (by clausification #[2086]): ∀ (a a_1 a_2 : Iota), Eq (coll a a_1 a_2) True % 35.91/36.15 Clause #2132 (by clausification #[2072]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq (coll a_2 a_2 a_1) False) % 35.91/36.15 Clause #2133 (by forward demodulation #[2132, 2087]): ∀ (a a_1 a_2 : Iota), Or (Eq (cyclic a a_1 a_2 a_2) True) (Eq True False) % 35.91/36.15 Clause #2134 (by clausification #[2133]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_2) True % 35.91/36.15 Clause #2136 (by superposition #[2134, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_2 a_1) True) % 35.91/36.15 Clause #2141 (by clausification #[2136]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_2 a_1) True % 35.91/36.15 Clause #2143 (by superposition #[2141, 184]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a_1 a_2) True) % 35.91/36.15 Clause #2149 (by clausification #[2143]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a_1 a_2) True % 35.91/36.15 Clause #2150 (by superposition #[2149, 174]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a_1 a a_2) True) % 35.91/36.19 Clause #2155 (by clausification #[2150]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a_1 a a_2) True % 35.91/36.19 Clause #2156 (by superposition #[2155, 179]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (cyclic a a a_1 a_2) True) % 35.91/36.19 Clause #2161 (by clausification #[2156]): ∀ (a a_1 a_2 : Iota), Eq (cyclic a a a_1 a_2) True % 35.91/36.19 Clause #2163 (by superposition #[2161, 290]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Or (Eq True False) (Eq (cyclic a a a_1 a_3) False)) % 35.91/36.19 Clause #2475 (by clausification #[2163]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq (cyclic a a a_1 a_3) False) % 35.91/36.19 Clause #2479 (by superposition #[2475, 2161]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cyclic a a_1 a_2 a_3) True) (Eq False True) % 35.91/36.19 Clause #2480 (by clausification #[2479]): ∀ (a a_1 a_2 a_3 : Iota), Eq (cyclic a a_1 a_2 a_3) True % 35.91/36.19 Clause #2486 (by superposition #[2480, 631]): Eq True False % 35.91/36.19 Clause #2488 (by clausification #[2486]): False % 35.91/36.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------