%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU118+1 : TPTP v9.2.0. Released v3.2.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 08:00:53 PM UTC 2025 % Result : Theorem 7.97s 8.12s % Output : Proof 7.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU118+1 : TPTP v9.2.0. Released v3.2.0. % 0.13/0.13 % Command : duper %s % 0.14/0.33 % Computer : n006.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Fri Oct 3 06:18:53 EDT 2025 % 0.14/0.33 % CPUTime : % 7.97/8.12 SZS status Theorem for theBenchmark.p % 7.97/8.12 SZS output start Proof for theBenchmark.p % 7.97/8.12 Clause #3 (by assumption #[]): Eq (∀ (A : Iota), finite A → ∀ (B : Iota), element B (powerset A) → finite B) True % 7.97/8.12 Clause #6 (by assumption #[]): Eq % 7.97/8.12 (∀ (A B : Iota), % 7.97/8.12 preboolean B → Iff (Eq B (finite_subsets A)) (∀ (C : Iota), Iff (in C B) (And (subset C A) (finite C)))) % 7.97/8.12 True % 7.97/8.12 Clause #7 (by assumption #[]): Eq (∀ (A : Iota), preboolean (finite_subsets A)) True % 7.97/8.12 Clause #23 (by assumption #[]): Eq (∀ (A B : Iota), in A B → element A B) True % 7.97/8.12 Clause #25 (by assumption #[]): Eq (Not (∀ (A B : Iota), element B (powerset A) → finite A → element B (finite_subsets A))) True % 7.97/8.12 Clause #26 (by assumption #[]): Eq (∀ (A B : Iota), Iff (element A (powerset B)) (subset A B)) True % 7.97/8.12 Clause #32 (by clausification #[7]): ∀ (a : Iota), Eq (preboolean (finite_subsets a)) True % 7.97/8.12 Clause #70 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (B : Iota), in a B → element a B) True % 7.97/8.12 Clause #71 (by clausification #[70]): ∀ (a a_1 : Iota), Eq (in a a_1 → element a a_1) True % 7.97/8.12 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), Or (Eq (in a a_1) False) (Eq (element a a_1) True) % 7.97/8.12 Clause #73 (by clausification #[3]): ∀ (a : Iota), Eq (finite a → ∀ (B : Iota), element B (powerset a) → finite B) True % 7.97/8.12 Clause #74 (by clausification #[73]): ∀ (a : Iota), Or (Eq (finite a) False) (Eq (∀ (B : Iota), element B (powerset a) → finite B) True) % 7.97/8.12 Clause #75 (by clausification #[74]): ∀ (a a_1 : Iota), Or (Eq (finite a) False) (Eq (element a_1 (powerset a) → finite a_1) True) % 7.97/8.12 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), Or (Eq (finite a) False) (Or (Eq (element a_1 (powerset a)) False) (Eq (finite a_1) True)) % 7.97/8.12 Clause #93 (by clausification #[6]): ∀ (a : Iota), % 7.97/8.12 Eq % 7.97/8.12 (∀ (B : Iota), % 7.97/8.12 preboolean B → Iff (Eq B (finite_subsets a)) (∀ (C : Iota), Iff (in C B) (And (subset C a) (finite C)))) % 7.97/8.12 True % 7.97/8.12 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), % 7.97/8.12 Eq (preboolean a → Iff (Eq a (finite_subsets a_1)) (∀ (C : Iota), Iff (in C a) (And (subset C a_1) (finite C)))) True % 7.97/8.12 Clause #95 (by clausification #[94]): ∀ (a a_1 : Iota), % 7.97/8.12 Or (Eq (preboolean a) False) % 7.97/8.12 (Eq (Iff (Eq a (finite_subsets a_1)) (∀ (C : Iota), Iff (in C a) (And (subset C a_1) (finite C)))) True) % 7.97/8.12 Clause #97 (by clausification #[95]): ∀ (a a_1 : Iota), % 7.97/8.12 Or (Eq (preboolean a) False) % 7.97/8.12 (Or (Eq (Eq a (finite_subsets a_1)) False) (Eq (∀ (C : Iota), Iff (in C a) (And (subset C a_1) (finite C))) True)) % 7.97/8.12 Clause #111 (by clausification #[25]): Eq (∀ (A B : Iota), element B (powerset A) → finite A → element B (finite_subsets A)) False % 7.97/8.12 Clause #112 (by clausification #[111]): ∀ (a : Iota), % 7.97/8.12 Eq % 7.97/8.12 (Not (∀ (B : Iota), element B (powerset (skS.0 4 a)) → finite (skS.0 4 a) → element B (finite_subsets (skS.0 4 a)))) % 7.97/8.12 True % 7.97/8.12 Clause #113 (by clausification #[112]): ∀ (a : Iota), % 7.97/8.12 Eq (∀ (B : Iota), element B (powerset (skS.0 4 a)) → finite (skS.0 4 a) → element B (finite_subsets (skS.0 4 a))) % 7.97/8.12 False % 7.97/8.12 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), % 7.97/8.12 Eq % 7.97/8.12 (Not % 7.97/8.12 (element (skS.0 5 a a_1) (powerset (skS.0 4 a)) → % 7.97/8.12 finite (skS.0 4 a) → element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a)))) % 7.97/8.12 True % 7.97/8.12 Clause #115 (by clausification #[114]): ∀ (a a_1 : Iota), % 7.97/8.12 Eq % 7.97/8.12 (element (skS.0 5 a a_1) (powerset (skS.0 4 a)) → % 7.97/8.12 finite (skS.0 4 a) → element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) % 7.97/8.12 False % 7.97/8.12 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Eq (element (skS.0 5 a a_1) (powerset (skS.0 4 a))) True % 7.97/8.12 Clause #117 (by clausification #[115]): ∀ (a a_1 : Iota), Eq (finite (skS.0 4 a) → element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) False % 7.97/8.12 Clause #146 (by clausification #[26]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (element a (powerset B)) (subset a B)) True % 7.97/8.12 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), Eq (Iff (element a (powerset a_1)) (subset a a_1)) True % 7.97/8.12 Clause #149 (by clausification #[147]): ∀ (a a_1 : Iota), Or (Eq (element a (powerset a_1)) False) (Eq (subset a a_1) True) % 7.99/8.15 Clause #160 (by superposition #[149, 116]): ∀ (a a_1 : Iota), Or (Eq (subset (skS.0 5 a a_1) (skS.0 4 a)) True) (Eq False True) % 7.99/8.15 Clause #256 (by clausification #[97]): ∀ (a a_1 : Iota), % 7.99/8.15 Or (Eq (preboolean a) False) % 7.99/8.15 (Or (Eq (∀ (C : Iota), Iff (in C a) (And (subset C a_1) (finite C))) True) (Ne a (finite_subsets a_1))) % 7.99/8.15 Clause #257 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), % 7.99/8.15 Or (Eq (preboolean a) False) % 7.99/8.15 (Or (Ne a (finite_subsets a_1)) (Eq (Iff (in a_2 a) (And (subset a_2 a_1) (finite a_2))) True)) % 7.99/8.15 Clause #258 (by clausification #[257]): ∀ (a a_1 a_2 : Iota), % 7.99/8.15 Or (Eq (preboolean a) False) % 7.99/8.15 (Or (Ne a (finite_subsets a_1)) (Or (Eq (in a_2 a) True) (Eq (And (subset a_2 a_1) (finite a_2)) False))) % 7.99/8.15 Clause #260 (by clausification #[258]): ∀ (a a_1 a_2 : Iota), % 7.99/8.15 Or (Eq (preboolean a) False) % 7.99/8.15 (Or (Ne a (finite_subsets a_1)) (Or (Eq (in a_2 a) True) (Or (Eq (subset a_2 a_1) False) (Eq (finite a_2) False)))) % 7.99/8.15 Clause #261 (by destructive equality resolution #[260]): ∀ (a a_1 : Iota), % 7.99/8.15 Or (Eq (preboolean (finite_subsets a)) False) % 7.99/8.15 (Or (Eq (in a_1 (finite_subsets a)) True) (Or (Eq (subset a_1 a) False) (Eq (finite a_1) False))) % 7.99/8.15 Clause #262 (by forward demodulation #[261, 32]): ∀ (a a_1 : Iota), % 7.99/8.15 Or (Eq True False) (Or (Eq (in a (finite_subsets a_1)) True) (Or (Eq (subset a a_1) False) (Eq (finite a) False))) % 7.99/8.15 Clause #263 (by clausification #[262]): ∀ (a a_1 : Iota), Or (Eq (in a (finite_subsets a_1)) True) (Or (Eq (subset a a_1) False) (Eq (finite a) False)) % 7.99/8.15 Clause #309 (by clausification #[117]): ∀ (a : Iota), Eq (finite (skS.0 4 a)) True % 7.99/8.15 Clause #310 (by clausification #[117]): ∀ (a a_1 : Iota), Eq (element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) False % 7.99/8.15 Clause #311 (by superposition #[309, 76]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (element a (powerset (skS.0 4 a_1))) False) (Eq (finite a) True)) % 7.99/8.15 Clause #314 (by clausification #[311]): ∀ (a a_1 : Iota), Or (Eq (element a (powerset (skS.0 4 a_1))) False) (Eq (finite a) True) % 7.99/8.15 Clause #315 (by superposition #[314, 116]): ∀ (a a_1 : Iota), Or (Eq (finite (skS.0 5 a a_1)) True) (Eq False True) % 7.99/8.15 Clause #319 (by clausification #[315]): ∀ (a a_1 : Iota), Eq (finite (skS.0 5 a a_1)) True % 7.99/8.15 Clause #379 (by clausification #[160]): ∀ (a a_1 : Iota), Eq (subset (skS.0 5 a a_1) (skS.0 4 a)) True % 7.99/8.15 Clause #382 (by superposition #[379, 263]): ∀ (a a_1 : Iota), % 7.99/8.15 Or (Eq (in (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True) % 7.99/8.15 (Or (Eq True False) (Eq (finite (skS.0 5 a a_1)) False)) % 7.99/8.15 Clause #718 (by clausification #[382]): ∀ (a a_1 : Iota), Or (Eq (in (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True) (Eq (finite (skS.0 5 a a_1)) False) % 7.99/8.15 Clause #719 (by forward demodulation #[718, 319]): ∀ (a a_1 : Iota), Or (Eq (in (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True) (Eq True False) % 7.99/8.15 Clause #720 (by clausification #[719]): ∀ (a a_1 : Iota), Eq (in (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True % 7.99/8.15 Clause #723 (by superposition #[720, 72]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True) % 7.99/8.15 Clause #725 (by clausification #[723]): ∀ (a a_1 : Iota), Eq (element (skS.0 5 a a_1) (finite_subsets (skS.0 4 a))) True % 7.99/8.15 Clause #726 (by superposition #[725, 310]): Eq True False % 7.99/8.15 Clause #728 (by clausification #[726]): False % 7.99/8.15 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------