%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU326+1 : TPTP v9.2.0. Released v3.3.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 08:01:23 PM UTC 2025 % Result : Theorem 15.09s 15.30s % Output : Proof 15.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SEU326+1 : TPTP v9.2.0. Released v3.3.0. % 0.13/0.13 % Command : duper %s % 0.14/0.35 % Computer : n015.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 03:57:23 EDT 2025 % 0.21/0.35 % CPUTime : % 15.09/15.30 SZS status Theorem for theBenchmark.p % 15.09/15.30 SZS output start Proof for theBenchmark.p % 15.09/15.30 Clause #17 (by assumption #[]): Eq (∀ (A B : Iota), element B (powerset (powerset A)) → element (complements_of_subsets A B) (powerset (powerset A))) % 15.09/15.30 True % 15.09/15.30 Clause #21 (by assumption #[]): Eq (∀ (A B : Iota), element B (powerset (powerset A)) → Eq (complements_of_subsets A (complements_of_subsets A B)) B) % 15.09/15.30 True % 15.09/15.30 Clause #24 (by assumption #[]): Eq (∀ (A : Iota), Exists fun B => And (element B (powerset A)) (empty B)) True % 15.09/15.30 Clause #26 (by assumption #[]): Eq % 15.09/15.30 (Not % 15.09/15.30 (∀ (A B : Iota), % 15.09/15.30 element B (powerset (powerset A)) → % 15.09/15.30 And (Not (And (Ne B empty_set) (Eq (complements_of_subsets A B) empty_set))) % 15.09/15.30 (Not (And (Ne (complements_of_subsets A B) empty_set) (Eq B empty_set))))) % 15.09/15.30 True % 15.09/15.30 Clause #30 (by assumption #[]): Eq % 15.09/15.30 (∀ (A B : Iota), % 15.09/15.30 element B (powerset (powerset A)) → Not (And (Ne B empty_set) (Eq (complements_of_subsets A B) empty_set))) % 15.09/15.30 True % 15.09/15.30 Clause #33 (by assumption #[]): Eq (∀ (A : Iota), empty A → Eq A empty_set) True % 15.09/15.30 Clause #55 (by clausification #[33]): ∀ (a : Iota), Eq (empty a → Eq a empty_set) True % 15.09/15.30 Clause #56 (by clausification #[55]): ∀ (a : Iota), Or (Eq (empty a) False) (Eq (Eq a empty_set) True) % 15.09/15.30 Clause #57 (by clausification #[56]): ∀ (a : Iota), Or (Eq (empty a) False) (Eq a empty_set) % 15.09/15.30 Clause #118 (by clausification #[17]): ∀ (a : Iota), % 15.09/15.30 Eq (∀ (B : Iota), element B (powerset (powerset a)) → element (complements_of_subsets a B) (powerset (powerset a))) % 15.09/15.30 True % 15.09/15.30 Clause #119 (by clausification #[118]): ∀ (a a_1 : Iota), % 15.09/15.30 Eq (element a (powerset (powerset a_1)) → element (complements_of_subsets a_1 a) (powerset (powerset a_1))) True % 15.09/15.30 Clause #120 (by clausification #[119]): ∀ (a a_1 : Iota), % 15.09/15.30 Or (Eq (element a (powerset (powerset a_1))) False) % 15.09/15.30 (Eq (element (complements_of_subsets a_1 a) (powerset (powerset a_1))) True) % 15.09/15.30 Clause #135 (by clausification #[24]): ∀ (a : Iota), Eq (Exists fun B => And (element B (powerset a)) (empty B)) True % 15.09/15.30 Clause #136 (by clausification #[135]): ∀ (a a_1 : Iota), Eq (And (element (skS.0 1 a a_1) (powerset a)) (empty (skS.0 1 a a_1))) True % 15.09/15.30 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), Eq (empty (skS.0 1 a a_1)) True % 15.09/15.30 Clause #138 (by clausification #[136]): ∀ (a a_1 : Iota), Eq (element (skS.0 1 a a_1) (powerset a)) True % 15.09/15.30 Clause #139 (by superposition #[137, 57]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (skS.0 1 a a_1) empty_set) % 15.09/15.30 Clause #146 (by clausification #[139]): ∀ (a a_1 : Iota), Eq (skS.0 1 a a_1) empty_set % 15.09/15.30 Clause #148 (by forward demodulation #[138, 146]): ∀ (a : Iota), Eq (element empty_set (powerset a)) True % 15.09/15.30 Clause #150 (by superposition #[148, 120]): ∀ (a : Iota), Or (Eq True False) (Eq (element (complements_of_subsets a empty_set) (powerset (powerset a))) True) % 15.09/15.30 Clause #202 (by clausification #[150]): ∀ (a : Iota), Eq (element (complements_of_subsets a empty_set) (powerset (powerset a))) True % 15.09/15.30 Clause #231 (by clausification #[21]): ∀ (a : Iota), % 15.09/15.30 Eq (∀ (B : Iota), element B (powerset (powerset a)) → Eq (complements_of_subsets a (complements_of_subsets a B)) B) % 15.09/15.30 True % 15.09/15.30 Clause #232 (by clausification #[231]): ∀ (a a_1 : Iota), % 15.09/15.30 Eq (element a (powerset (powerset a_1)) → Eq (complements_of_subsets a_1 (complements_of_subsets a_1 a)) a) True % 15.09/15.30 Clause #233 (by clausification #[232]): ∀ (a a_1 : Iota), % 15.09/15.30 Or (Eq (element a (powerset (powerset a_1))) False) % 15.09/15.30 (Eq (Eq (complements_of_subsets a_1 (complements_of_subsets a_1 a)) a) True) % 15.09/15.30 Clause #234 (by clausification #[233]): ∀ (a a_1 : Iota), % 15.09/15.30 Or (Eq (element a (powerset (powerset a_1))) False) (Eq (complements_of_subsets a_1 (complements_of_subsets a_1 a)) a) % 15.09/15.30 Clause #236 (by superposition #[234, 148]): ∀ (a : Iota), Or (Eq (complements_of_subsets a (complements_of_subsets a empty_set)) empty_set) (Eq False True) % 15.09/15.30 Clause #240 (by clausification #[236]): ∀ (a : Iota), Eq (complements_of_subsets a (complements_of_subsets a empty_set)) empty_set % 15.09/15.30 Clause #282 (by clausification #[26]): Eq % 15.09/15.30 (∀ (A B : Iota), % 15.09/15.30 element B (powerset (powerset A)) → % 15.18/15.33 And (Not (And (Ne B empty_set) (Eq (complements_of_subsets A B) empty_set))) % 15.18/15.33 (Not (And (Ne (complements_of_subsets A B) empty_set) (Eq B empty_set)))) % 15.18/15.33 False % 15.18/15.33 Clause #283 (by clausification #[282]): ∀ (a : Iota), % 15.18/15.33 Eq % 15.18/15.33 (Not % 15.18/15.33 (∀ (B : Iota), % 15.18/15.33 element B (powerset (powerset (skS.0 4 a))) → % 15.18/15.33 And (Not (And (Ne B empty_set) (Eq (complements_of_subsets (skS.0 4 a) B) empty_set))) % 15.18/15.33 (Not (And (Ne (complements_of_subsets (skS.0 4 a) B) empty_set) (Eq B empty_set))))) % 15.18/15.33 True % 15.18/15.33 Clause #284 (by clausification #[283]): ∀ (a : Iota), % 15.18/15.33 Eq % 15.18/15.33 (∀ (B : Iota), % 15.18/15.33 element B (powerset (powerset (skS.0 4 a))) → % 15.18/15.33 And (Not (And (Ne B empty_set) (Eq (complements_of_subsets (skS.0 4 a) B) empty_set))) % 15.18/15.33 (Not (And (Ne (complements_of_subsets (skS.0 4 a) B) empty_set) (Eq B empty_set)))) % 15.18/15.33 False % 15.18/15.33 Clause #285 (by clausification #[284]): ∀ (a a_1 : Iota), % 15.18/15.33 Eq % 15.18/15.33 (Not % 15.18/15.33 (element (skS.0 5 a a_1) (powerset (powerset (skS.0 4 a))) → % 15.18/15.33 And % 15.18/15.33 (Not (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set))) % 15.18/15.33 (Not % 15.18/15.33 (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set))))) % 15.18/15.33 True % 15.18/15.33 Clause #286 (by clausification #[285]): ∀ (a a_1 : Iota), % 15.18/15.33 Eq % 15.18/15.33 (element (skS.0 5 a a_1) (powerset (powerset (skS.0 4 a))) → % 15.18/15.33 And (Not (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set))) % 15.18/15.33 (Not (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set)))) % 15.18/15.33 False % 15.18/15.33 Clause #287 (by clausification #[286]): ∀ (a a_1 : Iota), Eq (element (skS.0 5 a a_1) (powerset (powerset (skS.0 4 a)))) True % 15.18/15.33 Clause #288 (by clausification #[286]): ∀ (a a_1 : Iota), % 15.18/15.33 Eq % 15.18/15.33 (And (Not (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set))) % 15.18/15.33 (Not (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set)))) % 15.18/15.33 False % 15.18/15.33 Clause #303 (by clausification #[30]): ∀ (a : Iota), % 15.18/15.33 Eq % 15.18/15.33 (∀ (B : Iota), % 15.18/15.33 element B (powerset (powerset a)) → Not (And (Ne B empty_set) (Eq (complements_of_subsets a B) empty_set))) % 15.18/15.33 True % 15.18/15.33 Clause #304 (by clausification #[303]): ∀ (a a_1 : Iota), % 15.18/15.33 Eq (element a (powerset (powerset a_1)) → Not (And (Ne a empty_set) (Eq (complements_of_subsets a_1 a) empty_set))) % 15.18/15.33 True % 15.18/15.33 Clause #305 (by clausification #[304]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (element a (powerset (powerset a_1))) False) % 15.18/15.33 (Eq (Not (And (Ne a empty_set) (Eq (complements_of_subsets a_1 a) empty_set))) True) % 15.18/15.33 Clause #306 (by clausification #[305]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (element a (powerset (powerset a_1))) False) % 15.18/15.33 (Eq (And (Ne a empty_set) (Eq (complements_of_subsets a_1 a) empty_set)) False) % 15.18/15.33 Clause #307 (by clausification #[306]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (element a (powerset (powerset a_1))) False) % 15.18/15.33 (Or (Eq (Ne a empty_set) False) (Eq (Eq (complements_of_subsets a_1 a) empty_set) False)) % 15.18/15.33 Clause #308 (by clausification #[307]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (element a (powerset (powerset a_1))) False) % 15.18/15.33 (Or (Eq (Eq (complements_of_subsets a_1 a) empty_set) False) (Eq a empty_set)) % 15.18/15.33 Clause #309 (by clausification #[308]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (element a (powerset (powerset a_1))) False) % 15.18/15.33 (Or (Eq a empty_set) (Ne (complements_of_subsets a_1 a) empty_set)) % 15.18/15.33 Clause #312 (by superposition #[309, 202]): ∀ (a : Iota), % 15.18/15.33 Or (Eq (complements_of_subsets a empty_set) empty_set) % 15.18/15.33 (Or (Ne (complements_of_subsets a (complements_of_subsets a empty_set)) empty_set) (Eq False True)) % 15.18/15.33 Clause #313 (by superposition #[309, 287]): ∀ (a a_1 : Iota), % 15.18/15.33 Or (Eq (skS.0 5 a a_1) empty_set) % 15.18/15.33 (Or (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq False True)) % 15.18/15.33 Clause #318 (by clausification #[312]): ∀ (a : Iota), % 15.18/15.33 Or (Eq (complements_of_subsets a empty_set) empty_set) % 15.18/15.33 (Ne (complements_of_subsets a (complements_of_subsets a empty_set)) empty_set) % 15.18/15.36 Clause #319 (by forward demodulation #[318, 240]): ∀ (a : Iota), Or (Eq (complements_of_subsets a empty_set) empty_set) (Ne empty_set empty_set) % 15.18/15.36 Clause #320 (by eliminate resolved literals #[319]): ∀ (a : Iota), Eq (complements_of_subsets a empty_set) empty_set % 15.18/15.36 Clause #518 (by clausification #[288]): ∀ (a a_1 : Iota), % 15.18/15.36 Or % 15.18/15.36 (Eq (Not (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set))) % 15.18/15.36 False) % 15.18/15.36 (Eq (Not (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set))) % 15.18/15.36 False) % 15.18/15.36 Clause #519 (by clausification #[518]): ∀ (a a_1 : Iota), % 15.18/15.36 Or % 15.18/15.36 (Eq (Not (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set))) % 15.18/15.36 False) % 15.18/15.36 (Eq (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set)) True) % 15.18/15.36 Clause #520 (by clausification #[519]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (And (Ne (skS.0 5 a a_1) empty_set) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set)) True) % 15.18/15.36 (Eq (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set)) True) % 15.18/15.36 Clause #521 (by clausification #[520]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set)) True) % 15.18/15.36 (Eq (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) True) % 15.18/15.36 Clause #522 (by clausification #[520]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (And (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set)) True) % 15.18/15.36 (Eq (Ne (skS.0 5 a a_1) empty_set) True) % 15.18/15.36 Clause #523 (by clausification #[521]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) True) % 15.18/15.36 (Eq (Eq (skS.0 5 a a_1) empty_set) True) % 15.18/15.36 Clause #525 (by clausification #[523]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (Eq (skS.0 5 a a_1) empty_set) True) (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) % 15.18/15.36 Clause #526 (by clausification #[525]): ∀ (a a_1 : Iota), Or (Eq (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) (Eq (skS.0 5 a a_1) empty_set) % 15.18/15.36 Clause #587 (by clausification #[313]): ∀ (a a_1 : Iota), Or (Eq (skS.0 5 a a_1) empty_set) (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) % 15.18/15.36 Clause #588 (by forward contextual literal cutting #[587, 526]): ∀ (a a_1 : Iota), Eq (skS.0 5 a a_1) empty_set % 15.18/15.36 Clause #779 (by clausification #[522]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (Ne (skS.0 5 a a_1) empty_set) True) % 15.18/15.36 (Eq (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) True) % 15.18/15.36 Clause #1655 (by clausification #[779]): ∀ (a a_1 : Iota), % 15.18/15.36 Or (Eq (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) True) (Ne (skS.0 5 a a_1) empty_set) % 15.18/15.36 Clause #1656 (by clausification #[1655]): ∀ (a a_1 : Iota), Or (Ne (skS.0 5 a a_1) empty_set) (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) % 15.18/15.36 Clause #1657 (by forward demodulation #[1656, 588]): ∀ (a a_1 : Iota), Or (Ne empty_set empty_set) (Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set) % 15.18/15.36 Clause #1658 (by eliminate resolved literals #[1657]): ∀ (a a_1 : Iota), Ne (complements_of_subsets (skS.0 4 a) (skS.0 5 a a_1)) empty_set % 15.18/15.36 Clause #1659 (by forward demodulation #[1658, 588]): ∀ (a : Iota), Ne (complements_of_subsets (skS.0 4 a) empty_set) empty_set % 15.18/15.36 Clause #1660 (by forward demodulation #[1659, 320]): Ne empty_set empty_set % 15.18/15.36 Clause #1661 (by eliminate resolved literals #[1660]): False % 15.18/15.36 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------