%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM394+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:56:25 PM UTC 2025 % Result : Theorem 10.49s 10.67s % Output : Proof 10.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM394+1 : TPTP v9.2.0. Released v3.2.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 08:23:08 EDT 2025 % 0.13/0.34 % CPUTime : % 10.49/10.67 SZS status Theorem for theBenchmark.p % 10.49/10.67 SZS output start Proof for theBenchmark.p % 10.49/10.67 Clause #2 (by assumption #[]): Eq (∀ (A : Iota), ordinal A → And (epsilon_transitive A) (epsilon_connected A)) True % 10.49/10.67 Clause #7 (by assumption #[]): Eq (∀ (A : Iota), Iff (epsilon_transitive A) (∀ (B : Iota), in B A → subset B A)) True % 10.49/10.67 Clause #13 (by assumption #[]): Eq (Exists fun A => And (And (epsilon_transitive A) (epsilon_connected A)) (ordinal A)) True % 10.49/10.67 Clause #23 (by assumption #[]): Eq (∀ (A B : Iota), And (ordinal A) (ordinal B) → Iff (ordinal_subset A B) (subset A B)) True % 10.49/10.67 Clause #24 (by assumption #[]): Eq (∀ (A B : Iota), And (ordinal A) (ordinal B) → ordinal_subset A A) True % 10.49/10.67 Clause #27 (by assumption #[]): Eq (∀ (A : Iota), ordinal A → ∀ (B : Iota), ordinal B → Not (And (And (Not (in A B)) (Ne A B)) (Not (in B A)))) True % 10.49/10.67 Clause #28 (by assumption #[]): Eq (Not (∀ (A : Iota), ordinal A → ∀ (B : Iota), ordinal B → Or (ordinal_subset A B) (in B A))) True % 10.49/10.67 Clause #62 (by clausification #[2]): ∀ (a : Iota), Eq (ordinal a → And (epsilon_transitive a) (epsilon_connected a)) True % 10.49/10.67 Clause #63 (by clausification #[62]): ∀ (a : Iota), Or (Eq (ordinal a) False) (Eq (And (epsilon_transitive a) (epsilon_connected a)) True) % 10.49/10.67 Clause #65 (by clausification #[63]): ∀ (a : Iota), Or (Eq (ordinal a) False) (Eq (epsilon_transitive a) True) % 10.49/10.67 Clause #67 (by clausification #[24]): ∀ (a : Iota), Eq (∀ (B : Iota), And (ordinal a) (ordinal B) → ordinal_subset a a) True % 10.49/10.67 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), Eq (And (ordinal a) (ordinal a_1) → ordinal_subset a a) True % 10.49/10.67 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), Or (Eq (And (ordinal a) (ordinal a_1)) False) (Eq (ordinal_subset a a) True) % 10.49/10.67 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), Or (Eq (ordinal_subset a a) True) (Or (Eq (ordinal a) False) (Eq (ordinal a_1) False)) % 10.49/10.67 Clause #110 (by clausification #[7]): ∀ (a : Iota), Eq (Iff (epsilon_transitive a) (∀ (B : Iota), in B a → subset B a)) True % 10.49/10.67 Clause #112 (by clausification #[110]): ∀ (a : Iota), Or (Eq (epsilon_transitive a) False) (Eq (∀ (B : Iota), in B a → subset B a) True) % 10.49/10.67 Clause #120 (by clausification #[112]): ∀ (a a_1 : Iota), Or (Eq (epsilon_transitive a) False) (Eq (in a_1 a → subset a_1 a) True) % 10.49/10.67 Clause #121 (by clausification #[120]): ∀ (a a_1 : Iota), Or (Eq (epsilon_transitive a) False) (Or (Eq (in a_1 a) False) (Eq (subset a_1 a) True)) % 10.49/10.67 Clause #125 (by clausification #[13]): ∀ (a : Iota), Eq (And (And (epsilon_transitive (skS.0 7 a)) (epsilon_connected (skS.0 7 a))) (ordinal (skS.0 7 a))) True % 10.49/10.67 Clause #126 (by clausification #[125]): ∀ (a : Iota), Eq (ordinal (skS.0 7 a)) True % 10.49/10.67 Clause #180 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (B : Iota), And (ordinal a) (ordinal B) → Iff (ordinal_subset a B) (subset a B)) True % 10.49/10.67 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), Eq (And (ordinal a) (ordinal a_1) → Iff (ordinal_subset a a_1) (subset a a_1)) True % 10.49/10.67 Clause #182 (by clausification #[181]): ∀ (a a_1 : Iota), Or (Eq (And (ordinal a) (ordinal a_1)) False) (Eq (Iff (ordinal_subset a a_1) (subset a a_1)) True) % 10.49/10.67 Clause #183 (by clausification #[182]): ∀ (a a_1 : Iota), % 10.49/10.67 Or (Eq (Iff (ordinal_subset a a_1) (subset a a_1)) True) (Or (Eq (ordinal a) False) (Eq (ordinal a_1) False)) % 10.49/10.67 Clause #184 (by clausification #[183]): ∀ (a a_1 : Iota), % 10.49/10.67 Or (Eq (ordinal a) False) % 10.49/10.67 (Or (Eq (ordinal a_1) False) (Or (Eq (ordinal_subset a a_1) True) (Eq (subset a a_1) False))) % 10.49/10.67 Clause #204 (by clausification #[28]): Eq (∀ (A : Iota), ordinal A → ∀ (B : Iota), ordinal B → Or (ordinal_subset A B) (in B A)) False % 10.49/10.67 Clause #205 (by clausification #[204]): ∀ (a : Iota), % 10.49/10.67 Eq (Not (ordinal (skS.0 13 a) → ∀ (B : Iota), ordinal B → Or (ordinal_subset (skS.0 13 a) B) (in B (skS.0 13 a)))) % 10.49/10.67 True % 10.49/10.67 Clause #206 (by clausification #[205]): ∀ (a : Iota), % 10.49/10.67 Eq (ordinal (skS.0 13 a) → ∀ (B : Iota), ordinal B → Or (ordinal_subset (skS.0 13 a) B) (in B (skS.0 13 a))) False % 10.49/10.67 Clause #207 (by clausification #[206]): ∀ (a : Iota), Eq (ordinal (skS.0 13 a)) True % 10.53/10.70 Clause #208 (by clausification #[206]): ∀ (a : Iota), Eq (∀ (B : Iota), ordinal B → Or (ordinal_subset (skS.0 13 a) B) (in B (skS.0 13 a))) False % 10.53/10.70 Clause #211 (by superposition #[207, 70]): ∀ (a a_1 : Iota), Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 13 a)) True) (Or (Eq True False) (Eq (ordinal a_1) False)) % 10.53/10.70 Clause #213 (by superposition #[207, 184]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq True False) % 10.53/10.70 (Or (Eq (ordinal a) False) (Or (Eq (ordinal_subset (skS.0 13 a_1) a) True) (Eq (subset (skS.0 13 a_1) a) False))) % 10.53/10.70 Clause #218 (by clausification #[27]): ∀ (a : Iota), Eq (ordinal a → ∀ (B : Iota), ordinal B → Not (And (And (Not (in a B)) (Ne a B)) (Not (in B a)))) True % 10.53/10.70 Clause #219 (by clausification #[218]): ∀ (a : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) (Eq (∀ (B : Iota), ordinal B → Not (And (And (Not (in a B)) (Ne a B)) (Not (in B a)))) True) % 10.53/10.70 Clause #220 (by clausification #[219]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) (Eq (ordinal a_1 → Not (And (And (Not (in a a_1)) (Ne a a_1)) (Not (in a_1 a)))) True) % 10.53/10.70 Clause #221 (by clausification #[220]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) (Eq (Not (And (And (Not (in a a_1)) (Ne a a_1)) (Not (in a_1 a)))) True)) % 10.53/10.70 Clause #222 (by clausification #[221]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) (Eq (And (And (Not (in a a_1)) (Ne a a_1)) (Not (in a_1 a))) False)) % 10.53/10.70 Clause #223 (by clausification #[222]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) (Or (Eq (And (Not (in a a_1)) (Ne a a_1)) False) (Eq (Not (in a_1 a)) False))) % 10.53/10.70 Clause #224 (by clausification #[223]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) % 10.53/10.70 (Or (Eq (Not (in a_1 a)) False) (Or (Eq (Not (in a a_1)) False) (Eq (Ne a a_1) False)))) % 10.53/10.70 Clause #225 (by clausification #[224]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) (Or (Eq (Not (in a a_1)) False) (Or (Eq (Ne a a_1) False) (Eq (in a_1 a) True)))) % 10.53/10.70 Clause #226 (by clausification #[225]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (ordinal a_1) False) (Or (Eq (Ne a a_1) False) (Or (Eq (in a_1 a) True) (Eq (in a a_1) True)))) % 10.53/10.70 Clause #227 (by clausification #[226]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) (Or (Eq (ordinal a_1) False) (Or (Eq (in a_1 a) True) (Or (Eq (in a a_1) True) (Eq a a_1)))) % 10.53/10.70 Clause #229 (by superposition #[227, 207]): ∀ (a a_1 : Iota), % 10.53/10.70 Or (Eq (ordinal a) False) % 10.53/10.70 (Or (Eq (in a (skS.0 13 a_1)) True) (Or (Eq (in (skS.0 13 a_1) a) True) (Or (Eq (skS.0 13 a_1) a) (Eq False True)))) % 10.53/10.70 Clause #395 (by clausification #[208]): ∀ (a a_1 : Iota), % 10.53/10.70 Eq % 10.53/10.70 (Not % 10.53/10.70 (ordinal (skS.0 14 a a_1) → Or (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) (in (skS.0 14 a a_1) (skS.0 13 a)))) % 10.53/10.70 True % 10.53/10.70 Clause #396 (by clausification #[395]): ∀ (a a_1 : Iota), % 10.53/10.70 Eq (ordinal (skS.0 14 a a_1) → Or (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) (in (skS.0 14 a a_1) (skS.0 13 a))) % 10.53/10.70 False % 10.53/10.70 Clause #397 (by clausification #[396]): ∀ (a a_1 : Iota), Eq (ordinal (skS.0 14 a a_1)) True % 10.53/10.70 Clause #398 (by clausification #[396]): ∀ (a a_1 : Iota), Eq (Or (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) (in (skS.0 14 a a_1) (skS.0 13 a))) False % 10.53/10.70 Clause #400 (by superposition #[397, 65]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (epsilon_transitive (skS.0 14 a a_1)) True) % 10.53/10.70 Clause #408 (by clausification #[400]): ∀ (a a_1 : Iota), Eq (epsilon_transitive (skS.0 14 a a_1)) True % 10.53/10.70 Clause #410 (by superposition #[408, 121]): ∀ (a a_1 a_2 : Iota), % 10.53/10.70 Or (Eq True False) (Or (Eq (in a (skS.0 14 a_1 a_2)) False) (Eq (subset a (skS.0 14 a_1 a_2)) True)) % 10.53/10.70 Clause #417 (by clausification #[211]): ∀ (a a_1 : Iota), Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 13 a)) True) (Eq (ordinal a_1) False) % 10.53/10.70 Clause #418 (by superposition #[417, 126]): ∀ (a : Iota), Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 13 a)) True) (Eq False True) % 10.53/10.70 Clause #419 (by clausification #[418]): ∀ (a : Iota), Eq (ordinal_subset (skS.0 13 a) (skS.0 13 a)) True % 10.53/10.70 Clause #443 (by clausification #[213]): ∀ (a a_1 : Iota), % 10.53/10.72 Or (Eq (ordinal a) False) (Or (Eq (ordinal_subset (skS.0 13 a_1) a) True) (Eq (subset (skS.0 13 a_1) a) False)) % 10.53/10.72 Clause #446 (by superposition #[443, 397]): ∀ (a a_1 a_2 : Iota), % 10.53/10.72 Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 14 a_1 a_2)) True) % 10.53/10.72 (Or (Eq (subset (skS.0 13 a) (skS.0 14 a_1 a_2)) False) (Eq False True)) % 10.53/10.72 Clause #476 (by clausification #[229]): ∀ (a a_1 : Iota), % 10.53/10.72 Or (Eq (ordinal a) False) % 10.53/10.72 (Or (Eq (in a (skS.0 13 a_1)) True) (Or (Eq (in (skS.0 13 a_1) a) True) (Eq (skS.0 13 a_1) a))) % 10.53/10.72 Clause #479 (by superposition #[476, 397]): ∀ (a a_1 a_2 : Iota), % 10.53/10.72 Or (Eq (in (skS.0 14 a a_1) (skS.0 13 a_2)) True) % 10.53/10.72 (Or (Eq (in (skS.0 13 a_2) (skS.0 14 a a_1)) True) (Or (Eq (skS.0 13 a_2) (skS.0 14 a a_1)) (Eq False True))) % 10.53/10.72 Clause #482 (by clausification #[410]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (skS.0 14 a_1 a_2)) False) (Eq (subset a (skS.0 14 a_1 a_2)) True) % 10.53/10.72 Clause #651 (by clausification #[398]): ∀ (a a_1 : Iota), Eq (in (skS.0 14 a a_1) (skS.0 13 a)) False % 10.53/10.72 Clause #652 (by clausification #[398]): ∀ (a a_1 : Iota), Eq (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) False % 10.53/10.72 Clause #760 (by clausification #[446]): ∀ (a a_1 a_2 : Iota), % 10.53/10.72 Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 14 a_1 a_2)) True) (Eq (subset (skS.0 13 a) (skS.0 14 a_1 a_2)) False) % 10.53/10.72 Clause #962 (by clausification #[479]): ∀ (a a_1 a_2 : Iota), % 10.53/10.72 Or (Eq (in (skS.0 14 a a_1) (skS.0 13 a_2)) True) % 10.53/10.72 (Or (Eq (in (skS.0 13 a_2) (skS.0 14 a a_1)) True) (Eq (skS.0 13 a_2) (skS.0 14 a a_1))) % 10.53/10.72 Clause #963 (by superposition #[962, 651]): ∀ (a a_1 : Iota), % 10.53/10.72 Or (Eq (in (skS.0 13 a) (skS.0 14 a a_1)) True) (Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Eq True False)) % 10.53/10.72 Clause #981 (by clausification #[963]): ∀ (a a_1 : Iota), Or (Eq (in (skS.0 13 a) (skS.0 14 a a_1)) True) (Eq (skS.0 13 a) (skS.0 14 a a_1)) % 10.53/10.72 Clause #982 (by superposition #[981, 482]): ∀ (a a_1 : Iota), % 10.53/10.72 Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Or (Eq True False) (Eq (subset (skS.0 13 a) (skS.0 14 a a_1)) True)) % 10.53/10.72 Clause #997 (by clausification #[982]): ∀ (a a_1 : Iota), Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Eq (subset (skS.0 13 a) (skS.0 14 a a_1)) True) % 10.53/10.72 Clause #998 (by superposition #[997, 760]): ∀ (a a_1 : Iota), % 10.53/10.72 Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Or (Eq (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) True) (Eq True False)) % 10.53/10.72 Clause #1000 (by clausification #[998]): ∀ (a a_1 : Iota), Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Eq (ordinal_subset (skS.0 13 a) (skS.0 14 a a_1)) True) % 10.53/10.72 Clause #1001 (by superposition #[1000, 652]): ∀ (a a_1 : Iota), Or (Eq (skS.0 13 a) (skS.0 14 a a_1)) (Eq True False) % 10.53/10.72 Clause #1002 (by clausification #[1001]): ∀ (a a_1 : Iota), Eq (skS.0 13 a) (skS.0 14 a a_1) % 10.53/10.72 Clause #1009 (by backward demodulation #[1002, 652]): ∀ (a : Iota), Eq (ordinal_subset (skS.0 13 a) (skS.0 13 a)) False % 10.53/10.72 Clause #1025 (by superposition #[1009, 419]): Eq False True % 10.53/10.72 Clause #1029 (by clausification #[1025]): False % 10.53/10.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------