%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU604^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:02:01 PM UTC 2025 % Result : Theorem 5.24s 5.43s % Output : Proof 5.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU604^2 : TPTP v9.2.0. Released v3.7.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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 04:03:53 EDT 2025 % 0.13/0.34 % CPUTime : % 5.24/5.43 SZS status Theorem for theBenchmark.p % 5.24/5.43 SZS output start Proof for theBenchmark.p % 5.24/5.43 Clause #0 (by assumption #[]): Eq (Eq subsetI2 (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B)) True % 5.24/5.43 Clause #1 (by assumption #[]): Eq (Eq subsetE (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B)) True % 5.24/5.43 Clause #2 (by assumption #[]): Eq (Eq subsetemptysetimpeq (∀ (A : Iota), subset A emptyset → Eq A emptyset)) True % 5.24/5.43 Clause #3 (by assumption #[]): Eq (Eq setminusEL (∀ (A B Xx : Iota), in Xx (setminus A B) → in Xx A)) True % 5.24/5.43 Clause #4 (by assumption #[]): Eq (Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B))) True % 5.24/5.43 Clause #5 (by assumption #[]): Eq % 5.24/5.43 (Not % 5.24/5.43 (subsetI2 → % 5.24/5.43 subsetE → % 5.24/5.43 subsetemptysetimpeq → setminusEL → setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset)) % 5.24/5.43 True % 5.24/5.43 Clause #6 (by clausification #[2]): Eq subsetemptysetimpeq (∀ (A : Iota), subset A emptyset → Eq A emptyset) % 5.24/5.43 Clause #17 (by clausification #[0]): Eq subsetI2 (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B) % 5.24/5.43 Clause #28 (by clausification #[1]): Eq subsetE (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B) % 5.24/5.43 Clause #48 (by clausification #[3]): Eq setminusEL (∀ (A B Xx : Iota), in Xx (setminus A B) → in Xx A) % 5.24/5.43 Clause #52 (by clausification #[4]): Eq setminusER (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 5.24/5.43 Clause #81 (by clausification #[5]): Eq % 5.24/5.43 (subsetI2 → % 5.24/5.43 subsetE → subsetemptysetimpeq → setminusEL → setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) % 5.24/5.43 False % 5.24/5.43 Clause #82 (by clausification #[81]): Eq subsetI2 True % 5.24/5.43 Clause #83 (by clausification #[81]): Eq (subsetE → subsetemptysetimpeq → setminusEL → setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) % 5.24/5.43 False % 5.24/5.43 Clause #84 (by backward demodulation #[82, 17]): Eq True (∀ (A B : Iota), (∀ (Xx : Iota), in Xx A → in Xx B) → subset A B) % 5.24/5.43 Clause #87 (by clausification #[84]): ∀ (a : Iota), Eq (∀ (B : Iota), (∀ (Xx : Iota), in Xx a → in Xx B) → subset a B) True % 5.24/5.43 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), Eq ((∀ (Xx : Iota), in Xx a → in Xx a_1) → subset a a_1) True % 5.24/5.43 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Or (Eq (∀ (Xx : Iota), in Xx a → in Xx a_1) False) (Eq (subset a a_1) True) % 5.24/5.43 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), % 5.24/5.43 Or (Eq (subset a a_1) True) (Eq (Not (in (skS.0 13 a a_1 a_2) a → in (skS.0 13 a a_1 a_2) a_1)) True) % 5.24/5.43 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (in (skS.0 13 a a_1 a_2) a → in (skS.0 13 a a_1 a_2) a_1) False) % 5.24/5.43 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) True) (Eq (in (skS.0 13 a a_1 a_2) a) True) % 5.24/5.43 Clause #102 (by clausification #[83]): Eq subsetE True % 5.24/5.43 Clause #103 (by clausification #[83]): Eq (subsetemptysetimpeq → setminusEL → setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) False % 5.24/5.43 Clause #104 (by backward demodulation #[102, 28]): Eq True (∀ (A B Xx : Iota), subset A B → in Xx A → in Xx B) % 5.24/5.43 Clause #107 (by clausification #[104]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), subset a B → in Xx a → in Xx B) True % 5.24/5.43 Clause #108 (by clausification #[107]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), subset a a_1 → in Xx a → in Xx a_1) True % 5.24/5.43 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), Eq (subset a a_1 → in a_2 a → in a_2 a_1) True % 5.24/5.43 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) False) (Eq (in a_2 a → in a_2 a_1) True) % 5.24/5.43 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), Or (Eq (subset a a_1) False) (Or (Eq (in a_2 a) False) (Eq (in a_2 a_1) True)) % 5.24/5.43 Clause #113 (by clausification #[103]): Eq subsetemptysetimpeq True % 5.24/5.43 Clause #114 (by clausification #[103]): Eq (setminusEL → setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) False % 5.24/5.43 Clause #115 (by backward demodulation #[113, 6]): Eq True (∀ (A : Iota), subset A emptyset → Eq A emptyset) % 5.27/5.45 Clause #119 (by clausification #[115]): ∀ (a : Iota), Eq (subset a emptyset → Eq a emptyset) True % 5.27/5.45 Clause #120 (by clausification #[119]): ∀ (a : Iota), Or (Eq (subset a emptyset) False) (Eq (Eq a emptyset) True) % 5.27/5.45 Clause #121 (by clausification #[120]): ∀ (a : Iota), Or (Eq (subset a emptyset) False) (Eq a emptyset) % 5.27/5.45 Clause #123 (by clausification #[114]): Eq setminusEL True % 5.27/5.45 Clause #124 (by clausification #[114]): Eq (setminusER → ∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) False % 5.27/5.45 Clause #125 (by backward demodulation #[123, 48]): Eq True (∀ (A B Xx : Iota), in Xx (setminus A B) → in Xx A) % 5.27/5.45 Clause #128 (by clausification #[125]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (setminus a B) → in Xx a) True % 5.27/5.45 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (setminus a a_1) → in Xx a) True % 5.27/5.45 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), Eq (in a (setminus a_1 a_2) → in a a_1) True % 5.27/5.45 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (in a a_1) True) % 5.27/5.45 Clause #133 (by superposition #[131, 92]): ∀ (a a_1 a_2 a_3 : Iota), % 5.27/5.45 Or (Eq (in (skS.0 13 (setminus a a_1) a_2 a_3) a) True) (Or (Eq (subset (setminus a a_1) a_2) True) (Eq False True)) % 5.27/5.45 Clause #134 (by clausification #[124]): Eq setminusER True % 5.27/5.45 Clause #135 (by clausification #[124]): Eq (∀ (A B : Iota), subset A B → Eq (setminus A B) emptyset) False % 5.27/5.45 Clause #136 (by backward demodulation #[134, 52]): Eq True (∀ (A B Xx : Iota), in Xx (setminus A B) → Not (in Xx B)) % 5.27/5.45 Clause #142 (by clausification #[136]): ∀ (a : Iota), Eq (∀ (B Xx : Iota), in Xx (setminus a B) → Not (in Xx B)) True % 5.27/5.45 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), Eq (∀ (Xx : Iota), in Xx (setminus a a_1) → Not (in Xx a_1)) True % 5.27/5.45 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 : Iota), Eq (in a (setminus a_1 a_2) → Not (in a a_2)) True % 5.27/5.45 Clause #145 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (Not (in a a_2)) True) % 5.27/5.45 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (setminus a_1 a_2)) False) (Eq (in a a_2) False) % 5.27/5.45 Clause #147 (by superposition #[146, 92]): ∀ (a a_1 a_2 a_3 : Iota), % 5.27/5.45 Or (Eq (in (skS.0 13 (setminus a a_1) a_2 a_3) a_1) False) % 5.27/5.45 (Or (Eq (subset (setminus a a_1) a_2) True) (Eq False True)) % 5.27/5.45 Clause #148 (by clausification #[135]): ∀ (a : Iota), Eq (Not (∀ (B : Iota), subset (skS.0 14 a) B → Eq (setminus (skS.0 14 a) B) emptyset)) True % 5.27/5.45 Clause #149 (by clausification #[148]): ∀ (a : Iota), Eq (∀ (B : Iota), subset (skS.0 14 a) B → Eq (setminus (skS.0 14 a) B) emptyset) False % 5.27/5.45 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), % 5.27/5.45 Eq (Not (subset (skS.0 14 a) (skS.0 15 a a_1) → Eq (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset)) True % 5.27/5.45 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), Eq (subset (skS.0 14 a) (skS.0 15 a a_1) → Eq (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset) False % 5.27/5.45 Clause #152 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (subset (skS.0 14 a) (skS.0 15 a a_1)) True % 5.27/5.45 Clause #153 (by clausification #[151]): ∀ (a a_1 : Iota), Eq (Eq (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset) False % 5.27/5.45 Clause #154 (by superposition #[152, 111]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Or (Eq (in a (skS.0 14 a_1)) False) (Eq (in a (skS.0 15 a_1 a_2)) True)) % 5.27/5.45 Clause #169 (by clausification #[153]): ∀ (a a_1 : Iota), Ne (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset % 5.27/5.45 Clause #170 (by clausification #[154]): ∀ (a a_1 a_2 : Iota), Or (Eq (in a (skS.0 14 a_1)) False) (Eq (in a (skS.0 15 a_1 a_2)) True) % 5.27/5.45 Clause #177 (by clausification #[133]): ∀ (a a_1 a_2 a_3 : Iota), % 5.27/5.45 Or (Eq (in (skS.0 13 (setminus a a_1) a_2 a_3) a) True) (Eq (subset (setminus a a_1) a_2) True) % 5.27/5.45 Clause #180 (by superposition #[177, 170]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.27/5.45 Or (Eq (subset (setminus (skS.0 14 a) a_1) a_2) True) % 5.27/5.45 (Or (Eq True False) (Eq (in (skS.0 13 (setminus (skS.0 14 a) a_1) a_2 a_3) (skS.0 15 a a_4)) True)) % 5.27/5.46 Clause #208 (by clausification #[147]): ∀ (a a_1 a_2 a_3 : Iota), % 5.27/5.46 Or (Eq (in (skS.0 13 (setminus a a_1) a_2 a_3) a_1) False) (Eq (subset (setminus a a_1) a_2) True) % 5.27/5.46 Clause #267 (by clausification #[180]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.27/5.46 Or (Eq (subset (setminus (skS.0 14 a) a_1) a_2) True) % 5.27/5.46 (Eq (in (skS.0 13 (setminus (skS.0 14 a) a_1) a_2 a_3) (skS.0 15 a a_4)) True) % 5.27/5.46 Clause #269 (by superposition #[267, 208]): ∀ (a a_1 a_2 : Iota), % 5.27/5.46 Or (Eq (subset (setminus (skS.0 14 a) (skS.0 15 a a_1)) a_2) True) % 5.27/5.46 (Or (Eq True False) (Eq (subset (setminus (skS.0 14 a) (skS.0 15 a a_1)) a_2) True)) % 5.27/5.46 Clause #403 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), % 5.27/5.46 Or (Eq (subset (setminus (skS.0 14 a) (skS.0 15 a a_1)) a_2) True) % 5.27/5.46 (Eq (subset (setminus (skS.0 14 a) (skS.0 15 a a_1)) a_2) True) % 5.27/5.46 Clause #404 (by eliminate duplicate literals #[403]): ∀ (a a_1 a_2 : Iota), Eq (subset (setminus (skS.0 14 a) (skS.0 15 a a_1)) a_2) True % 5.27/5.46 Clause #405 (by superposition #[404, 121]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset) % 5.27/5.46 Clause #407 (by clausification #[405]): ∀ (a a_1 : Iota), Eq (setminus (skS.0 14 a) (skS.0 15 a a_1)) emptyset % 5.27/5.46 Clause #408 (by forward contextual literal cutting #[407, 169]): False % 5.27/5.46 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------