%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM388+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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 7.91s 8.11s % Output : Proof 7.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM388+1 : TPTP v9.2.0. Released v3.2.0. % 0.04/0.13 % Command : duper %s % 0.13/0.34 % Computer : n015.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 07:44:53 EDT 2025 % 0.13/0.35 % CPUTime : % 7.91/8.11 SZS status Theorem for theBenchmark.p % 7.91/8.11 SZS output start Proof for theBenchmark.p % 7.91/8.11 Clause #2 (by assumption #[]): Eq (∀ (A : Iota), ordinal A → And (epsilon_transitive A) (epsilon_connected A)) True % 7.91/8.11 Clause #6 (by assumption #[]): Eq (∀ (A : Iota), Iff (epsilon_transitive A) (∀ (B : Iota), in B A → subset B A)) True % 7.91/8.11 Clause #23 (by assumption #[]): Eq % 7.91/8.11 (Not % 7.91/8.11 (∀ (A : Iota), % 7.91/8.11 ordinal A → ∀ (B : Iota), ordinal B → ∀ (C : Iota), epsilon_transitive C → And (in C A) (in A B) → in C B)) % 7.91/8.11 True % 7.91/8.11 Clause #25 (by assumption #[]): Eq (∀ (A B : Iota), element A B → Or (empty B) (in A B)) True % 7.91/8.11 Clause #26 (by assumption #[]): Eq (∀ (A B : Iota), Iff (element A (powerset B)) (subset A B)) True % 7.91/8.11 Clause #27 (by assumption #[]): Eq (∀ (A B C : Iota), And (in A B) (element B (powerset C)) → element A C) True % 7.91/8.11 Clause #30 (by assumption #[]): Eq (∀ (A B : Iota), Not (And (in A B) (empty B))) True % 7.91/8.11 Clause #55 (by clausification #[2]): ∀ (a : Iota), Eq (ordinal a → And (epsilon_transitive a) (epsilon_connected a)) True % 7.91/8.11 Clause #56 (by clausification #[55]): ∀ (a : Iota), Or (Eq (ordinal a) False) (Eq (And (epsilon_transitive a) (epsilon_connected a)) True) % 7.91/8.11 Clause #58 (by clausification #[56]): ∀ (a : Iota), Or (Eq (ordinal a) False) (Eq (epsilon_transitive a) True) % 7.91/8.11 Clause #68 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (B C : Iota), And (in a B) (element B (powerset C)) → element a C) True % 7.91/8.11 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), And (in a a_1) (element a_1 (powerset C)) → element a C) True % 7.91/8.11 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 : Iota), Eq (And (in a a_1) (element a_1 (powerset a_2)) → element a a_2) True % 7.91/8.11 Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), Or (Eq (And (in a a_1) (element a_1 (powerset a_2))) False) (Eq (element a a_2) True) % 7.91/8.11 Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 : Iota), Or (Eq (element a a_1) True) (Or (Eq (in a a_2) False) (Eq (element a_2 (powerset a_1)) False)) % 7.91/8.11 Clause #89 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (epsilon_transitive a) (∀ (B : Iota), in B a → subset B a)) True % 7.91/8.11 Clause #91 (by clausification #[89]): ∀ (a : Iota), Or (Eq (epsilon_transitive a) False) (Eq (∀ (B : Iota), in B a → subset B a) True) % 7.91/8.11 Clause #99 (by clausification #[91]): ∀ (a a_1 : Iota), Or (Eq (epsilon_transitive a) False) (Eq (in a_1 a → subset a_1 a) True) % 7.91/8.11 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), Or (Eq (epsilon_transitive a) False) (Or (Eq (in a_1 a) False) (Eq (subset a_1 a) True)) % 7.91/8.11 Clause #113 (by clausification #[30]): ∀ (a : Iota), Eq (∀ (B : Iota), Not (And (in a B) (empty B))) True % 7.91/8.11 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Eq (Not (And (in a a_1) (empty a_1))) True % 7.91/8.11 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), Eq (And (in a a_1) (empty a_1)) False % 7.91/8.11 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Or (Eq (in a a_1) False) (Eq (empty a_1) False) % 7.91/8.11 Clause #139 (by clausification #[25]): ∀ (a : Iota), Eq (∀ (B : Iota), element a B → Or (empty B) (in a B)) True % 7.91/8.11 Clause #140 (by clausification #[139]): ∀ (a a_1 : Iota), Eq (element a a_1 → Or (empty a_1) (in a a_1)) True % 7.91/8.11 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Eq (Or (empty a_1) (in a a_1)) True) % 7.91/8.11 Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota), Or (Eq (element a a_1) False) (Or (Eq (empty a_1) True) (Eq (in a a_1) True)) % 7.91/8.11 Clause #148 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (element a (powerset B)) (subset a B)) True % 7.91/8.11 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), Eq (Iff (element a (powerset a_1)) (subset a a_1)) True % 7.91/8.11 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), Or (Eq (element a (powerset a_1)) True) (Eq (subset a a_1) False) % 7.91/8.11 Clause #182 (by clausification #[23]): Eq % 7.91/8.11 (∀ (A : Iota), % 7.91/8.11 ordinal A → ∀ (B : Iota), ordinal B → ∀ (C : Iota), epsilon_transitive C → And (in C A) (in A B) → in C B) % 7.91/8.11 False % 7.91/8.11 Clause #183 (by clausification #[182]): ∀ (a : Iota), % 7.97/8.14 Eq % 7.97/8.14 (Not % 7.97/8.14 (ordinal (skS.0 13 a) → % 7.97/8.14 ∀ (B : Iota), % 7.97/8.14 ordinal B → ∀ (C : Iota), epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) B) → in C B)) % 7.97/8.14 True % 7.97/8.14 Clause #184 (by clausification #[183]): ∀ (a : Iota), % 7.97/8.14 Eq % 7.97/8.14 (ordinal (skS.0 13 a) → % 7.97/8.14 ∀ (B : Iota), % 7.97/8.14 ordinal B → ∀ (C : Iota), epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) B) → in C B) % 7.97/8.14 False % 7.97/8.14 Clause #186 (by clausification #[184]): ∀ (a : Iota), % 7.97/8.14 Eq % 7.97/8.14 (∀ (B : Iota), % 7.97/8.14 ordinal B → ∀ (C : Iota), epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) B) → in C B) % 7.97/8.14 False % 7.97/8.14 Clause #196 (by clausification #[186]): ∀ (a a_1 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (Not % 7.97/8.14 (ordinal (skS.0 14 a a_1) → % 7.97/8.14 ∀ (C : Iota), % 7.97/8.14 epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → in C (skS.0 14 a a_1))) % 7.97/8.14 True % 7.97/8.14 Clause #197 (by clausification #[196]): ∀ (a a_1 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (ordinal (skS.0 14 a a_1) → % 7.97/8.14 ∀ (C : Iota), % 7.97/8.14 epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → in C (skS.0 14 a a_1)) % 7.97/8.14 False % 7.97/8.14 Clause #198 (by clausification #[197]): ∀ (a a_1 : Iota), Eq (ordinal (skS.0 14 a a_1)) True % 7.97/8.14 Clause #199 (by clausification #[197]): ∀ (a a_1 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (∀ (C : Iota), % 7.97/8.14 epsilon_transitive C → And (in C (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → in C (skS.0 14 a a_1)) % 7.97/8.14 False % 7.97/8.14 Clause #201 (by superposition #[198, 58]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (epsilon_transitive (skS.0 14 a a_1)) True) % 7.97/8.14 Clause #220 (by clausification #[201]): ∀ (a a_1 : Iota), Eq (epsilon_transitive (skS.0 14 a a_1)) True % 7.97/8.14 Clause #222 (by superposition #[220, 100]): ∀ (a a_1 a_2 : Iota), % 7.97/8.14 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)) % 7.97/8.14 Clause #229 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (Not % 7.97/8.14 (epsilon_transitive (skS.0 15 a a_1 a_2) → % 7.97/8.14 And (in (skS.0 15 a a_1 a_2) (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → % 7.97/8.14 in (skS.0 15 a a_1 a_2) (skS.0 14 a a_1))) % 7.97/8.14 True % 7.97/8.14 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (epsilon_transitive (skS.0 15 a a_1 a_2) → % 7.97/8.14 And (in (skS.0 15 a a_1 a_2) (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → % 7.97/8.14 in (skS.0 15 a a_1 a_2) (skS.0 14 a a_1)) % 7.97/8.14 False % 7.97/8.14 Clause #232 (by clausification #[230]): ∀ (a a_1 a_2 : Iota), % 7.97/8.14 Eq % 7.97/8.14 (And (in (skS.0 15 a a_1 a_2) (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1)) → % 7.97/8.14 in (skS.0 15 a a_1 a_2) (skS.0 14 a a_1)) % 7.97/8.14 False % 7.97/8.14 Clause #373 (by clausification #[222]): ∀ (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) % 7.97/8.14 Clause #378 (by clausification #[232]): ∀ (a a_1 a_2 : Iota), Eq (And (in (skS.0 15 a a_1 a_2) (skS.0 13 a)) (in (skS.0 13 a) (skS.0 14 a a_1))) True % 7.97/8.14 Clause #379 (by clausification #[232]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 15 a a_1 a_2) (skS.0 14 a a_1)) False % 7.97/8.14 Clause #380 (by clausification #[378]): ∀ (a a_1 : Iota), Eq (in (skS.0 13 a) (skS.0 14 a a_1)) True % 7.97/8.14 Clause #381 (by clausification #[378]): ∀ (a a_1 a_2 : Iota), Eq (in (skS.0 15 a a_1 a_2) (skS.0 13 a)) True % 7.97/8.14 Clause #382 (by superposition #[380, 373]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (subset (skS.0 13 a) (skS.0 14 a a_1)) True) % 7.97/8.14 Clause #386 (by superposition #[380, 116]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (empty (skS.0 14 a a_1)) False) % 7.97/8.14 Clause #388 (by clausification #[386]): ∀ (a a_1 : Iota), Eq (empty (skS.0 14 a a_1)) False % 7.97/8.14 Clause #395 (by clausification #[382]): ∀ (a a_1 : Iota), Eq (subset (skS.0 13 a) (skS.0 14 a a_1)) True % 7.97/8.14 Clause #396 (by superposition #[395, 150]): ∀ (a a_1 : Iota), Or (Eq (element (skS.0 13 a) (powerset (skS.0 14 a a_1))) True) (Eq True False) % 7.97/8.14 Clause #400 (by superposition #[381, 72]): ∀ (a a_1 a_2 a_3 : Iota), % 7.97/8.14 Or (Eq (element (skS.0 15 a a_1 a_2) a_3) True) (Or (Eq True False) (Eq (element (skS.0 13 a) (powerset a_3)) False)) % 7.97/8.14 Clause #407 (by clausification #[396]): ∀ (a a_1 : Iota), Eq (element (skS.0 13 a) (powerset (skS.0 14 a a_1))) True % 7.97/8.15 Clause #530 (by clausification #[400]): ∀ (a a_1 a_2 a_3 : Iota), % 7.97/8.15 Or (Eq (element (skS.0 15 a a_1 a_2) a_3) True) (Eq (element (skS.0 13 a) (powerset a_3)) False) % 7.97/8.15 Clause #531 (by superposition #[530, 407]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (element (skS.0 15 a a_1 a_2) (skS.0 14 a a_3)) True) (Eq False True) % 7.97/8.15 Clause #535 (by clausification #[531]): ∀ (a a_1 a_2 a_3 : Iota), Eq (element (skS.0 15 a a_1 a_2) (skS.0 14 a a_3)) True % 7.97/8.15 Clause #536 (by superposition #[535, 142]): ∀ (a a_1 a_2 a_3 : Iota), % 7.97/8.15 Or (Eq True False) (Or (Eq (empty (skS.0 14 a a_1)) True) (Eq (in (skS.0 15 a a_2 a_3) (skS.0 14 a a_1)) True)) % 7.97/8.15 Clause #720 (by clausification #[536]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (empty (skS.0 14 a a_1)) True) (Eq (in (skS.0 15 a a_2 a_3) (skS.0 14 a a_1)) True) % 7.97/8.15 Clause #721 (by forward demodulation #[720, 388]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq False True) (Eq (in (skS.0 15 a a_1 a_2) (skS.0 14 a a_3)) True) % 7.97/8.15 Clause #722 (by clausification #[721]): ∀ (a a_1 a_2 a_3 : Iota), Eq (in (skS.0 15 a a_1 a_2) (skS.0 14 a a_3)) True % 7.97/8.15 Clause #723 (by superposition #[722, 379]): Eq True False % 7.97/8.15 Clause #730 (by clausification #[723]): False % 7.97/8.15 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------