%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : TOP024+1 : TPTP v9.2.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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 08:09:53 PM UTC 2025 % Result : Theorem 85.73s 85.89s % Output : Proof 85.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : TOP024+1 : TPTP v9.2.0. Released v3.4.0. % 0.12/0.13 % Command : duper %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 02:01:23 EDT 2025 % 0.14/0.34 % CPUTime : % 85.73/85.89 SZS status Theorem for theBenchmark.p % 85.73/85.89 SZS output start Proof for theBenchmark.p % 85.73/85.89 Clause #0 (by assumption #[]): Eq % 85.73/85.89 (Not % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 85.73/85.89 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → v1_tsp_2 B A → v1_tops_1 B A)) % 85.73/85.89 True % 85.73/85.89 Clause #23 (by assumption #[]): Eq % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 l1_pre_topc A → % 85.73/85.89 ∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → Iff (v1_tops_1 B A) (Eq (k6_pre_topc A B) (u1_struct_0 A))) % 85.73/85.89 True % 85.73/85.89 Clause #24 (by assumption #[]): Eq % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 85.73/85.89 ∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → % 85.73/85.89 Iff (v1_tsp_2 B A) (And (v1_tsp_1 B A) (Eq (k3_tex_4 A B) (u1_struct_0 A)))) % 85.73/85.89 True % 85.73/85.89 Clause #29 (by assumption #[]): Eq (∀ (A : Iota), l1_pre_topc A → l1_struct_0 A) True % 85.73/85.89 Clause #37 (by assumption #[]): Eq (∀ (A : Iota), And (v2_pre_topc A) (l1_pre_topc A) → v4_pre_topc (k2_pre_topc A) A) True % 85.73/85.89 Clause #53 (by assumption #[]): Eq (∀ (A : Iota), Iota → r1_tarski A A) True % 85.73/85.89 Clause #54 (by assumption #[]): Eq (∀ (A : Iota), l1_struct_0 A → Eq (k2_pre_topc A) (u1_struct_0 A)) True % 85.73/85.89 Clause #57 (by assumption #[]): Eq (∀ (A B : Iota), Iff (m1_subset_1 A (k1_zfmisc_1 B)) (r1_tarski A B)) True % 85.73/85.89 Clause #59 (by assumption #[]): Eq % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 l1_pre_topc A → % 85.73/85.89 ∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → % 85.73/85.89 And (v4_pre_topc B A → Eq (k6_pre_topc A B) B) % 85.73/85.89 (And (v2_pre_topc A) (Eq (k6_pre_topc A B) B) → v4_pre_topc B A)) % 85.73/85.89 True % 85.73/85.89 Clause #61 (by assumption #[]): Eq % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 85.73/85.89 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → Eq (k6_pre_topc A (k3_tex_4 A B)) (k6_pre_topc A B)) % 85.73/85.89 True % 85.73/85.89 Clause #73 (by clausification #[0]): Eq % 85.73/85.89 (∀ (A : Iota), % 85.73/85.89 And (And (Not (v3_struct_0 A)) (v2_pre_topc A)) (l1_pre_topc A) → % 85.73/85.89 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)) → v1_tsp_2 B A → v1_tops_1 B A) % 85.73/85.89 False % 85.73/85.89 Clause #74 (by clausification #[73]): ∀ (a : Iota), % 85.73/85.89 Eq % 85.73/85.89 (Not % 85.73/85.89 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a)) → % 85.73/85.89 ∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a))) → v1_tsp_2 B (skS.0 0 a) → v1_tops_1 B (skS.0 0 a))) % 85.73/85.89 True % 85.73/85.89 Clause #75 (by clausification #[74]): ∀ (a : Iota), % 85.73/85.89 Eq % 85.73/85.89 (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a)) → % 85.73/85.89 ∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a))) → v1_tsp_2 B (skS.0 0 a) → v1_tops_1 B (skS.0 0 a)) % 85.73/85.89 False % 85.73/85.89 Clause #76 (by clausification #[75]): ∀ (a : Iota), Eq (And (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) (l1_pre_topc (skS.0 0 a))) True % 85.73/85.89 Clause #77 (by clausification #[75]): ∀ (a : Iota), % 85.73/85.89 Eq % 85.73/85.89 (∀ (B : Iota), % 85.73/85.89 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a))) → v1_tsp_2 B (skS.0 0 a) → v1_tops_1 B (skS.0 0 a)) % 85.73/85.89 False % 85.73/85.89 Clause #78 (by clausification #[76]): ∀ (a : Iota), Eq (l1_pre_topc (skS.0 0 a)) True % 85.73/85.89 Clause #79 (by clausification #[76]): ∀ (a : Iota), Eq (And (Not (v3_struct_0 (skS.0 0 a))) (v2_pre_topc (skS.0 0 a))) True % 85.73/85.89 Clause #80 (by clausification #[29]): ∀ (a : Iota), Eq (l1_pre_topc a → l1_struct_0 a) True % 85.73/85.89 Clause #81 (by clausification #[80]): ∀ (a : Iota), Or (Eq (l1_pre_topc a) False) (Eq (l1_struct_0 a) True) % 85.73/85.89 Clause #82 (by superposition #[81, 78]): ∀ (a : Iota), Or (Eq (l1_struct_0 (skS.0 0 a)) True) (Eq False True) % 85.73/85.89 Clause #88 (by clausification #[53]): ∀ (a : Iota), Eq (Iota → r1_tarski a a) True % 85.73/85.89 Clause #89 (by clausification #[88]): ∀ (a : Iota), Iota → Eq (r1_tarski a a) True % 85.73/85.89 Clause #108 (by clausification #[37]): ∀ (a : Iota), Eq (And (v2_pre_topc a) (l1_pre_topc a) → v4_pre_topc (k2_pre_topc a) a) True % 85.73/85.89 Clause #109 (by clausification #[108]): ∀ (a : Iota), Or (Eq (And (v2_pre_topc a) (l1_pre_topc a)) False) (Eq (v4_pre_topc (k2_pre_topc a) a) True) % 85.74/85.91 Clause #110 (by clausification #[109]): ∀ (a : Iota), Or (Eq (v4_pre_topc (k2_pre_topc a) a) True) (Or (Eq (v2_pre_topc a) False) (Eq (l1_pre_topc a) False)) % 85.74/85.91 Clause #148 (by clausification #[54]): ∀ (a : Iota), Eq (l1_struct_0 a → Eq (k2_pre_topc a) (u1_struct_0 a)) True % 85.74/85.91 Clause #149 (by clausification #[148]): ∀ (a : Iota), Or (Eq (l1_struct_0 a) False) (Eq (Eq (k2_pre_topc a) (u1_struct_0 a)) True) % 85.74/85.91 Clause #150 (by clausification #[149]): ∀ (a : Iota), Or (Eq (l1_struct_0 a) False) (Eq (k2_pre_topc a) (u1_struct_0 a)) % 85.74/85.91 Clause #180 (by clausification #[82]): ∀ (a : Iota), Eq (l1_struct_0 (skS.0 0 a)) True % 85.74/85.91 Clause #183 (by superposition #[180, 150]): ∀ (a : Iota), Or (Eq True False) (Eq (k2_pre_topc (skS.0 0 a)) (u1_struct_0 (skS.0 0 a))) % 85.74/85.91 Clause #238 (by clausification #[57]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (m1_subset_1 a (k1_zfmisc_1 B)) (r1_tarski a B)) True % 85.74/85.91 Clause #239 (by clausification #[238]): ∀ (a a_1 : Iota), Eq (Iff (m1_subset_1 a (k1_zfmisc_1 a_1)) (r1_tarski a a_1)) True % 85.74/85.91 Clause #240 (by clausification #[239]): ∀ (a a_1 : Iota), Or (Eq (m1_subset_1 a (k1_zfmisc_1 a_1)) True) (Eq (r1_tarski a a_1) False) % 85.74/85.91 Clause #242 (by superposition #[240, 89]): ∀ (a : Iota), Or (Eq (m1_subset_1 a (k1_zfmisc_1 a)) True) (Eq False True) % 85.74/85.91 Clause #243 (by clausification #[242]): ∀ (a : Iota), Eq (m1_subset_1 a (k1_zfmisc_1 a)) True % 85.74/85.91 Clause #262 (by clausification #[77]): ∀ (a a_1 : Iota), % 85.74/85.91 Eq % 85.74/85.91 (Not % 85.74/85.91 (m1_subset_1 (skS.0 5 a a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a))) → % 85.74/85.91 v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a) → v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a))) % 85.74/85.91 True % 85.74/85.91 Clause #263 (by clausification #[262]): ∀ (a a_1 : Iota), % 85.74/85.91 Eq % 85.74/85.91 (m1_subset_1 (skS.0 5 a a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a))) → % 85.74/85.91 v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a) → v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) % 85.74/85.91 False % 85.74/85.91 Clause #264 (by clausification #[263]): ∀ (a a_1 : Iota), Eq (m1_subset_1 (skS.0 5 a a_1) (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) True % 85.74/85.91 Clause #265 (by clausification #[263]): ∀ (a a_1 : Iota), Eq (v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a) → v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) False % 85.74/85.91 Clause #378 (by clausification #[23]): ∀ (a : Iota), % 85.74/85.91 Eq % 85.74/85.91 (l1_pre_topc a → % 85.74/85.91 ∀ (B : Iota), % 85.74/85.91 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → Iff (v1_tops_1 B a) (Eq (k6_pre_topc a B) (u1_struct_0 a))) % 85.74/85.91 True % 85.74/85.91 Clause #379 (by clausification #[378]): ∀ (a : Iota), % 85.74/85.91 Or (Eq (l1_pre_topc a) False) % 85.74/85.91 (Eq % 85.74/85.91 (∀ (B : Iota), % 85.74/85.91 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → Iff (v1_tops_1 B a) (Eq (k6_pre_topc a B) (u1_struct_0 a))) % 85.74/85.91 True) % 85.74/85.91 Clause #380 (by clausification #[379]): ∀ (a a_1 : Iota), % 85.74/85.91 Or (Eq (l1_pre_topc a) False) % 85.74/85.91 (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → Iff (v1_tops_1 a_1 a) (Eq (k6_pre_topc a a_1) (u1_struct_0 a))) % 85.74/85.91 True) % 85.74/85.91 Clause #381 (by clausification #[380]): ∀ (a a_1 : Iota), % 85.74/85.91 Or (Eq (l1_pre_topc a) False) % 85.74/85.91 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.91 (Eq (Iff (v1_tops_1 a_1 a) (Eq (k6_pre_topc a a_1) (u1_struct_0 a))) True)) % 85.77/85.91 Clause #382 (by clausification #[381]): ∀ (a a_1 : Iota), % 85.77/85.91 Or (Eq (l1_pre_topc a) False) % 85.77/85.91 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.91 (Or (Eq (v1_tops_1 a_1 a) True) (Eq (Eq (k6_pre_topc a a_1) (u1_struct_0 a)) False))) % 85.77/85.91 Clause #384 (by clausification #[382]): ∀ (a a_1 : Iota), % 85.77/85.91 Or (Eq (l1_pre_topc a) False) % 85.77/85.91 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.91 (Or (Eq (v1_tops_1 a_1 a) True) (Ne (k6_pre_topc a a_1) (u1_struct_0 a)))) % 85.77/85.91 Clause #385 (by superposition #[384, 78]): ∀ (a a_1 : Iota), % 85.77/85.91 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.91 (Or (Eq (v1_tops_1 a (skS.0 0 a_1)) True) % 85.77/85.91 (Or (Ne (k6_pre_topc (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1))) (Eq False True))) % 85.77/85.91 Clause #395 (by clausification #[24]): ∀ (a : Iota), % 85.77/85.91 Eq % 85.77/85.91 (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a) → % 85.77/85.91 ∀ (B : Iota), % 85.77/85.91 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 Iff (v1_tsp_2 B a) (And (v1_tsp_1 B a) (Eq (k3_tex_4 a B) (u1_struct_0 a)))) % 85.77/85.94 True % 85.77/85.94 Clause #396 (by clausification #[395]): ∀ (a : Iota), % 85.77/85.94 Or (Eq (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a)) False) % 85.77/85.94 (Eq % 85.77/85.94 (∀ (B : Iota), % 85.77/85.94 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 Iff (v1_tsp_2 B a) (And (v1_tsp_1 B a) (Eq (k3_tex_4 a B) (u1_struct_0 a)))) % 85.77/85.94 True) % 85.77/85.94 Clause #397 (by clausification #[396]): ∀ (a : Iota), % 85.77/85.94 Or % 85.77/85.94 (Eq % 85.77/85.94 (∀ (B : Iota), % 85.77/85.94 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 Iff (v1_tsp_2 B a) (And (v1_tsp_1 B a) (Eq (k3_tex_4 a B) (u1_struct_0 a)))) % 85.77/85.94 True) % 85.77/85.94 (Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) (Eq (l1_pre_topc a) False)) % 85.77/85.94 Clause #398 (by clausification #[397]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) % 85.77/85.94 (Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Eq % 85.77/85.94 (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 Iff (v1_tsp_2 a_1 a) (And (v1_tsp_1 a_1 a) (Eq (k3_tex_4 a a_1) (u1_struct_0 a)))) % 85.77/85.94 True)) % 85.77/85.94 Clause #399 (by clausification #[398]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or % 85.77/85.94 (Eq % 85.77/85.94 (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 Iff (v1_tsp_2 a_1 a) (And (v1_tsp_1 a_1 a) (Eq (k3_tex_4 a a_1) (u1_struct_0 a)))) % 85.77/85.94 True) % 85.77/85.94 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v2_pre_topc a) False))) % 85.77/85.94 Clause #400 (by clausification #[399]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or (Eq (Not (v3_struct_0 a)) False) % 85.77/85.94 (Or (Eq (v2_pre_topc a) False) % 85.77/85.94 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.94 (Eq (Iff (v1_tsp_2 a_1 a) (And (v1_tsp_1 a_1 a) (Eq (k3_tex_4 a a_1) (u1_struct_0 a)))) True)))) % 85.77/85.94 Clause #401 (by clausification #[400]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or (Eq (v2_pre_topc a) False) % 85.77/85.94 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.94 (Or (Eq (Iff (v1_tsp_2 a_1 a) (And (v1_tsp_1 a_1 a) (Eq (k3_tex_4 a a_1) (u1_struct_0 a)))) True) % 85.77/85.94 (Eq (v3_struct_0 a) True)))) % 85.77/85.94 Clause #403 (by clausification #[401]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or (Eq (v2_pre_topc a) False) % 85.77/85.94 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.94 (Or (Eq (v3_struct_0 a) True) % 85.77/85.94 (Or (Eq (v1_tsp_2 a_1 a) False) (Eq (And (v1_tsp_1 a_1 a) (Eq (k3_tex_4 a a_1) (u1_struct_0 a))) True))))) % 85.77/85.94 Clause #567 (by clausification #[59]): ∀ (a : Iota), % 85.77/85.94 Eq % 85.77/85.94 (l1_pre_topc a → % 85.77/85.94 ∀ (B : Iota), % 85.77/85.94 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 And (v4_pre_topc B a → Eq (k6_pre_topc a B) B) % 85.77/85.94 (And (v2_pre_topc a) (Eq (k6_pre_topc a B) B) → v4_pre_topc B a)) % 85.77/85.94 True % 85.77/85.94 Clause #568 (by clausification #[567]): ∀ (a : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Eq % 85.77/85.94 (∀ (B : Iota), % 85.77/85.94 m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 And (v4_pre_topc B a → Eq (k6_pre_topc a B) B) % 85.77/85.94 (And (v2_pre_topc a) (Eq (k6_pre_topc a B) B) → v4_pre_topc B a)) % 85.77/85.94 True) % 85.77/85.94 Clause #569 (by clausification #[568]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Eq % 85.77/85.94 (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → % 85.77/85.94 And (v4_pre_topc a_1 a → Eq (k6_pre_topc a a_1) a_1) % 85.77/85.94 (And (v2_pre_topc a) (Eq (k6_pre_topc a a_1) a_1) → v4_pre_topc a_1 a)) % 85.77/85.94 True) % 85.77/85.94 Clause #570 (by clausification #[569]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.94 (Eq % 85.77/85.94 (And (v4_pre_topc a_1 a → Eq (k6_pre_topc a a_1) a_1) % 85.77/85.94 (And (v2_pre_topc a) (Eq (k6_pre_topc a a_1) a_1) → v4_pre_topc a_1 a)) % 85.77/85.94 True)) % 85.77/85.94 Clause #572 (by clausification #[570]): ∀ (a a_1 : Iota), % 85.77/85.94 Or (Eq (l1_pre_topc a) False) % 85.77/85.94 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.94 (Eq (v4_pre_topc a_1 a → Eq (k6_pre_topc a a_1) a_1) True)) % 85.77/85.94 Clause #581 (by clausification #[61]): ∀ (a : Iota), % 85.77/85.94 Eq % 85.77/85.94 (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a) → % 85.77/85.96 ∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → Eq (k6_pre_topc a (k3_tex_4 a B)) (k6_pre_topc a B)) % 85.77/85.96 True % 85.77/85.96 Clause #582 (by clausification #[581]): ∀ (a : Iota), % 85.77/85.96 Or (Eq (And (And (Not (v3_struct_0 a)) (v2_pre_topc a)) (l1_pre_topc a)) False) % 85.77/85.96 (Eq % 85.77/85.96 (∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → Eq (k6_pre_topc a (k3_tex_4 a B)) (k6_pre_topc a B)) % 85.77/85.96 True) % 85.77/85.96 Clause #583 (by clausification #[582]): ∀ (a : Iota), % 85.77/85.96 Or % 85.77/85.96 (Eq % 85.77/85.96 (∀ (B : Iota), m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 a)) → Eq (k6_pre_topc a (k3_tex_4 a B)) (k6_pre_topc a B)) % 85.77/85.96 True) % 85.77/85.96 (Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) (Eq (l1_pre_topc a) False)) % 85.77/85.96 Clause #584 (by clausification #[583]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (And (Not (v3_struct_0 a)) (v2_pre_topc a)) False) % 85.77/85.96 (Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → Eq (k6_pre_topc a (k3_tex_4 a a_1)) (k6_pre_topc a a_1)) % 85.77/85.96 True)) % 85.77/85.96 Clause #585 (by clausification #[584]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or % 85.77/85.96 (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a)) → Eq (k6_pre_topc a (k3_tex_4 a a_1)) (k6_pre_topc a a_1)) % 85.77/85.96 True) % 85.77/85.96 (Or (Eq (Not (v3_struct_0 a)) False) (Eq (v2_pre_topc a) False))) % 85.77/85.96 Clause #586 (by clausification #[585]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or (Eq (Not (v3_struct_0 a)) False) % 85.77/85.96 (Or (Eq (v2_pre_topc a) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.96 (Eq (Eq (k6_pre_topc a (k3_tex_4 a a_1)) (k6_pre_topc a a_1)) True)))) % 85.77/85.96 Clause #587 (by clausification #[586]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or (Eq (v2_pre_topc a) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.96 (Or (Eq (Eq (k6_pre_topc a (k3_tex_4 a a_1)) (k6_pre_topc a a_1)) True) (Eq (v3_struct_0 a) True)))) % 85.77/85.96 Clause #588 (by clausification #[587]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or (Eq (v2_pre_topc a) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.96 (Or (Eq (v3_struct_0 a) True) (Eq (k6_pre_topc a (k3_tex_4 a a_1)) (k6_pre_topc a a_1))))) % 85.77/85.96 Clause #589 (by superposition #[588, 78]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 85.77/85.96 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 85.77/85.96 (Or (Eq (k6_pre_topc (skS.0 0 a) (k3_tex_4 (skS.0 0 a) a_1)) (k6_pre_topc (skS.0 0 a) a_1)) (Eq False True)))) % 85.77/85.96 Clause #621 (by clausification #[79]): ∀ (a : Iota), Eq (v2_pre_topc (skS.0 0 a)) True % 85.77/85.96 Clause #622 (by clausification #[79]): ∀ (a : Iota), Eq (Not (v3_struct_0 (skS.0 0 a))) True % 85.77/85.96 Clause #623 (by superposition #[621, 110]): ∀ (a : Iota), % 85.77/85.96 Or (Eq (v4_pre_topc (k2_pre_topc (skS.0 0 a)) (skS.0 0 a)) True) % 85.77/85.96 (Or (Eq True False) (Eq (l1_pre_topc (skS.0 0 a)) False)) % 85.77/85.96 Clause #635 (by clausification #[622]): ∀ (a : Iota), Eq (v3_struct_0 (skS.0 0 a)) False % 85.77/85.96 Clause #671 (by clausification #[183]): ∀ (a : Iota), Eq (k2_pre_topc (skS.0 0 a)) (u1_struct_0 (skS.0 0 a)) % 85.77/85.96 Clause #713 (by clausification #[265]): ∀ (a a_1 : Iota), Eq (v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a)) True % 85.77/85.96 Clause #714 (by clausification #[265]): ∀ (a a_1 : Iota), Eq (v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) False % 85.77/85.96 Clause #728 (by clausification #[572]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.96 (Or (Eq (v4_pre_topc a_1 a) False) (Eq (Eq (k6_pre_topc a a_1) a_1) True))) % 85.77/85.96 Clause #729 (by clausification #[728]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (l1_pre_topc a) False) % 85.77/85.96 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.96 (Or (Eq (v4_pre_topc a_1 a) False) (Eq (k6_pre_topc a a_1) a_1))) % 85.77/85.96 Clause #730 (by superposition #[729, 78]): ∀ (a a_1 : Iota), % 85.77/85.96 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.96 (Or (Eq (v4_pre_topc a (skS.0 0 a_1)) False) (Or (Eq (k6_pre_topc (skS.0 0 a_1) a) a) (Eq False True))) % 85.77/85.99 Clause #911 (by clausification #[385]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Or (Eq (v1_tops_1 a (skS.0 0 a_1)) True) (Ne (k6_pre_topc (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1)))) % 85.77/85.99 Clause #912 (by superposition #[911, 264]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) True) % 85.77/85.99 (Or (Ne (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a))) (Eq False True)) % 85.77/85.99 Clause #942 (by clausification #[403]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (l1_pre_topc a) False) % 85.77/85.99 (Or (Eq (v2_pre_topc a) False) % 85.77/85.99 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 a) True) % 85.77/85.99 (Or (Eq (v1_tsp_2 a_1 a) False) (Eq (Eq (k3_tex_4 a a_1) (u1_struct_0 a)) True))))) % 85.77/85.99 Clause #944 (by clausification #[942]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (l1_pre_topc a) False) % 85.77/85.99 (Or (Eq (v2_pre_topc a) False) % 85.77/85.99 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 a))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 a) True) (Or (Eq (v1_tsp_2 a_1 a) False) (Eq (k3_tex_4 a a_1) (u1_struct_0 a)))))) % 85.77/85.99 Clause #945 (by superposition #[944, 78]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 85.77/85.99 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 85.77/85.99 (Or (Eq (v1_tsp_2 a_1 (skS.0 0 a)) False) % 85.77/85.99 (Or (Eq (k3_tex_4 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a))) (Eq False True))))) % 85.77/85.99 Clause #1009 (by clausification #[623]): ∀ (a : Iota), Or (Eq (v4_pre_topc (k2_pre_topc (skS.0 0 a)) (skS.0 0 a)) True) (Eq (l1_pre_topc (skS.0 0 a)) False) % 85.77/85.99 Clause #1010 (by forward demodulation #[1009, 671]): ∀ (a : Iota), Or (Eq (v4_pre_topc (u1_struct_0 (skS.0 0 a)) (skS.0 0 a)) True) (Eq (l1_pre_topc (skS.0 0 a)) False) % 85.77/85.99 Clause #1011 (by forward demodulation #[1010, 78]): ∀ (a : Iota), Or (Eq (v4_pre_topc (u1_struct_0 (skS.0 0 a)) (skS.0 0 a)) True) (Eq True False) % 85.77/85.99 Clause #1012 (by clausification #[1011]): ∀ (a : Iota), Eq (v4_pre_topc (u1_struct_0 (skS.0 0 a)) (skS.0 0 a)) True % 85.77/85.99 Clause #1180 (by clausification #[589]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 85.77/85.99 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 85.77/85.99 (Eq (k6_pre_topc (skS.0 0 a) (k3_tex_4 (skS.0 0 a) a_1)) (k6_pre_topc (skS.0 0 a) a_1)))) % 85.77/85.99 Clause #1181 (by forward demodulation #[1180, 621]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq True False) % 85.77/85.99 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 85.77/85.99 (Eq (k6_pre_topc (skS.0 0 a_1) (k3_tex_4 (skS.0 0 a_1) a)) (k6_pre_topc (skS.0 0 a_1) a)))) % 85.77/85.99 Clause #1182 (by clausification #[1181]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 85.77/85.99 (Eq (k6_pre_topc (skS.0 0 a_1) (k3_tex_4 (skS.0 0 a_1) a)) (k6_pre_topc (skS.0 0 a_1) a))) % 85.77/85.99 Clause #1183 (by forward demodulation #[1182, 635]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Or (Eq False True) (Eq (k6_pre_topc (skS.0 0 a_1) (k3_tex_4 (skS.0 0 a_1) a)) (k6_pre_topc (skS.0 0 a_1) a))) % 85.77/85.99 Clause #1184 (by clausification #[1183]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Eq (k6_pre_topc (skS.0 0 a_1) (k3_tex_4 (skS.0 0 a_1) a)) (k6_pre_topc (skS.0 0 a_1) a)) % 85.77/85.99 Clause #1185 (by superposition #[1184, 264]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (k6_pre_topc (skS.0 0 a) (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1))) (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1))) % 85.77/85.99 (Eq False True) % 85.77/85.99 Clause #1548 (by clausification #[730]): ∀ (a a_1 : Iota), % 85.77/85.99 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.77/85.99 (Or (Eq (v4_pre_topc a (skS.0 0 a_1)) False) (Eq (k6_pre_topc (skS.0 0 a_1) a) a)) % 85.77/85.99 Clause #1559 (by superposition #[1548, 243]): ∀ (a : Iota), % 85.77/85.99 Or (Eq (v4_pre_topc (u1_struct_0 (skS.0 0 a)) (skS.0 0 a)) False) % 85.77/85.99 (Or (Eq (k6_pre_topc (skS.0 0 a) (u1_struct_0 (skS.0 0 a))) (u1_struct_0 (skS.0 0 a))) (Eq False True)) % 85.86/86.04 Clause #2521 (by clausification #[912]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) True) % 85.86/86.04 (Ne (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a))) % 85.86/86.04 Clause #2693 (by clausification #[945]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (v2_pre_topc (skS.0 0 a)) False) % 85.86/86.04 (Or (Eq (m1_subset_1 a_1 (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a)))) False) % 85.86/86.04 (Or (Eq (v3_struct_0 (skS.0 0 a)) True) % 85.86/86.04 (Or (Eq (v1_tsp_2 a_1 (skS.0 0 a)) False) (Eq (k3_tex_4 (skS.0 0 a) a_1) (u1_struct_0 (skS.0 0 a)))))) % 85.86/86.04 Clause #2694 (by forward demodulation #[2693, 621]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq True False) % 85.86/86.04 (Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.86/86.04 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 85.86/86.04 (Or (Eq (v1_tsp_2 a (skS.0 0 a_1)) False) (Eq (k3_tex_4 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1)))))) % 85.86/86.04 Clause #2695 (by clausification #[2694]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.86/86.04 (Or (Eq (v3_struct_0 (skS.0 0 a_1)) True) % 85.86/86.04 (Or (Eq (v1_tsp_2 a (skS.0 0 a_1)) False) (Eq (k3_tex_4 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1))))) % 85.86/86.04 Clause #2696 (by forward demodulation #[2695, 635]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.86/86.04 (Or (Eq False True) % 85.86/86.04 (Or (Eq (v1_tsp_2 a (skS.0 0 a_1)) False) (Eq (k3_tex_4 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1))))) % 85.86/86.04 Clause #2697 (by clausification #[2696]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (m1_subset_1 a (k1_zfmisc_1 (u1_struct_0 (skS.0 0 a_1)))) False) % 85.86/86.04 (Or (Eq (v1_tsp_2 a (skS.0 0 a_1)) False) (Eq (k3_tex_4 (skS.0 0 a_1) a) (u1_struct_0 (skS.0 0 a_1)))) % 85.86/86.04 Clause #2698 (by superposition #[2697, 264]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a)) False) % 85.86/86.04 (Or (Eq (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a))) (Eq False True)) % 85.86/86.04 Clause #3324 (by clausification #[1185]): ∀ (a a_1 : Iota), % 85.86/86.04 Eq (k6_pre_topc (skS.0 0 a) (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1))) (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1)) % 85.86/86.04 Clause #4004 (by clausification #[1559]): ∀ (a : Iota), % 85.86/86.04 Or (Eq (v4_pre_topc (u1_struct_0 (skS.0 0 a)) (skS.0 0 a)) False) % 85.86/86.04 (Eq (k6_pre_topc (skS.0 0 a) (u1_struct_0 (skS.0 0 a))) (u1_struct_0 (skS.0 0 a))) % 85.86/86.04 Clause #4005 (by forward demodulation #[4004, 1012]): ∀ (a : Iota), Or (Eq True False) (Eq (k6_pre_topc (skS.0 0 a) (u1_struct_0 (skS.0 0 a))) (u1_struct_0 (skS.0 0 a))) % 85.86/86.04 Clause #4006 (by clausification #[4005]): ∀ (a : Iota), Eq (k6_pre_topc (skS.0 0 a) (u1_struct_0 (skS.0 0 a))) (u1_struct_0 (skS.0 0 a)) % 85.86/86.04 Clause #4687 (by clausification #[2698]): ∀ (a a_1 : Iota), % 85.86/86.04 Or (Eq (v1_tsp_2 (skS.0 5 a a_1) (skS.0 0 a)) False) % 85.86/86.04 (Eq (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a))) % 85.86/86.04 Clause #4688 (by superposition #[4687, 713]): ∀ (a a_1 : Iota), Or (Eq (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a))) (Eq False True) % 85.86/86.04 Clause #4691 (by clausification #[4688]): ∀ (a a_1 : Iota), Eq (k3_tex_4 (skS.0 0 a) (skS.0 5 a a_1)) (u1_struct_0 (skS.0 0 a)) % 85.86/86.04 Clause #4695 (by backward demodulation #[4691, 3324]): ∀ (a a_1 : Iota), Eq (k6_pre_topc (skS.0 0 a) (u1_struct_0 (skS.0 0 a))) (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1)) % 85.86/86.04 Clause #4702 (by forward demodulation #[4695, 4006]): ∀ (a a_1 : Iota), Eq (u1_struct_0 (skS.0 0 a)) (k6_pre_topc (skS.0 0 a) (skS.0 5 a a_1)) % 85.86/86.04 Clause #4709 (by backward contextual literal cutting #[4702, 2521]): ∀ (a a_1 : Iota), Eq (v1_tops_1 (skS.0 5 a a_1) (skS.0 0 a)) True % 85.86/86.04 Clause #4710 (by superposition #[4709, 714]): Eq True False % 85.86/86.04 Clause #4711 (by clausification #[4710]): False % 85.86/86.04 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------