%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU196+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:05 PM UTC 2025 % Result : Theorem 59.02s 59.21s % Output : Proof 59.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.14 % Problem : SEU196+1 : TPTP v9.2.0. Released v3.3.0. % 0.14/0.15 % Command : duper %s % 0.15/0.36 % Computer : n007.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Fri Oct 3 04:33:53 EDT 2025 % 0.15/0.37 % CPUTime : % 59.02/59.21 SZS status Theorem for theBenchmark.p % 59.02/59.21 SZS output start Proof for theBenchmark.p % 59.02/59.21 Clause #3 (by assumption #[]): Eq (∀ (A B : Iota), relation A → relation (relation_dom_restriction A B)) True % 59.02/59.21 Clause #20 (by assumption #[]): Eq % 59.02/59.21 (∀ (A : Iota), % 59.02/59.21 relation A → % 59.02/59.21 ∀ (B : Iota), % 59.02/59.21 relation B → % 59.02/59.21 subset A B → And (subset (relation_dom A) (relation_dom B)) (subset (relation_rng A) (relation_rng B))) % 59.02/59.21 True % 59.02/59.21 Clause #27 (by assumption #[]): Eq (∀ (A B : Iota), relation B → subset (relation_dom_restriction B A) B) True % 59.02/59.21 Clause #29 (by assumption #[]): Eq (Not (∀ (A B : Iota), relation B → subset (relation_rng (relation_dom_restriction B A)) (relation_rng B))) True % 59.02/59.21 Clause #50 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (B : Iota), relation a → relation (relation_dom_restriction a B)) True % 59.02/59.21 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), Eq (relation a → relation (relation_dom_restriction a a_1)) True % 59.02/59.21 Clause #52 (by clausification #[51]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (relation (relation_dom_restriction a a_1)) True) % 59.02/59.21 Clause #87 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (B : Iota), relation B → subset (relation_dom_restriction B a) B) True % 59.02/59.21 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), Eq (relation a → subset (relation_dom_restriction a a_1) a) True % 59.02/59.21 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Or (Eq (relation a) False) (Eq (subset (relation_dom_restriction a a_1) a) True) % 59.02/59.21 Clause #202 (by clausification #[20]): ∀ (a : Iota), % 59.02/59.21 Eq % 59.02/59.21 (relation a → % 59.02/59.21 ∀ (B : Iota), % 59.02/59.21 relation B → % 59.02/59.21 subset a B → And (subset (relation_dom a) (relation_dom B)) (subset (relation_rng a) (relation_rng B))) % 59.02/59.21 True % 59.02/59.21 Clause #203 (by clausification #[202]): ∀ (a : Iota), % 59.02/59.21 Or (Eq (relation a) False) % 59.02/59.21 (Eq % 59.02/59.21 (∀ (B : Iota), % 59.02/59.21 relation B → % 59.02/59.21 subset a B → And (subset (relation_dom a) (relation_dom B)) (subset (relation_rng a) (relation_rng B))) % 59.02/59.21 True) % 59.02/59.21 Clause #204 (by clausification #[203]): ∀ (a a_1 : Iota), % 59.02/59.21 Or (Eq (relation a) False) % 59.02/59.21 (Eq % 59.02/59.21 (relation a_1 → % 59.02/59.21 subset a a_1 → And (subset (relation_dom a) (relation_dom a_1)) (subset (relation_rng a) (relation_rng a_1))) % 59.02/59.21 True) % 59.02/59.21 Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota), % 59.02/59.21 Or (Eq (relation a) False) % 59.02/59.21 (Or (Eq (relation a_1) False) % 59.02/59.21 (Eq (subset a a_1 → And (subset (relation_dom a) (relation_dom a_1)) (subset (relation_rng a) (relation_rng a_1))) % 59.02/59.21 True)) % 59.02/59.21 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 59.02/59.21 Or (Eq (relation a) False) % 59.02/59.21 (Or (Eq (relation a_1) False) % 59.02/59.21 (Or (Eq (subset a a_1) False) % 59.02/59.21 (Eq (And (subset (relation_dom a) (relation_dom a_1)) (subset (relation_rng a) (relation_rng a_1))) True))) % 59.02/59.21 Clause #207 (by clausification #[206]): ∀ (a a_1 : Iota), % 59.02/59.21 Or (Eq (relation a) False) % 59.02/59.21 (Or (Eq (relation a_1) False) (Or (Eq (subset a a_1) False) (Eq (subset (relation_rng a) (relation_rng a_1)) True))) % 59.02/59.21 Clause #264 (by clausification #[29]): Eq (∀ (A B : Iota), relation B → subset (relation_rng (relation_dom_restriction B A)) (relation_rng B)) False % 59.02/59.21 Clause #265 (by clausification #[264]): ∀ (a : Iota), % 59.02/59.21 Eq (Not (∀ (B : Iota), relation B → subset (relation_rng (relation_dom_restriction B (skS.0 7 a))) (relation_rng B))) % 59.02/59.21 True % 59.02/59.21 Clause #266 (by clausification #[265]): ∀ (a : Iota), % 59.02/59.21 Eq (∀ (B : Iota), relation B → subset (relation_rng (relation_dom_restriction B (skS.0 7 a))) (relation_rng B)) False % 59.02/59.21 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), % 59.02/59.21 Eq % 59.02/59.21 (Not % 59.02/59.21 (relation (skS.0 8 a a_1) → % 59.02/59.21 subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) (skS.0 7 a))) (relation_rng (skS.0 8 a a_1)))) % 59.02/59.21 True % 59.02/59.21 Clause #268 (by clausification #[267]): ∀ (a a_1 : Iota), % 59.02/59.21 Eq % 59.02/59.21 (relation (skS.0 8 a a_1) → % 59.02/59.21 subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) (skS.0 7 a))) (relation_rng (skS.0 8 a a_1))) % 59.02/59.21 False % 59.02/59.21 Clause #269 (by clausification #[268]): ∀ (a a_1 : Iota), Eq (relation (skS.0 8 a a_1)) True % 59.02/59.21 Clause #270 (by clausification #[268]): ∀ (a a_1 : Iota), % 59.08/59.29 Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) (skS.0 7 a))) (relation_rng (skS.0 8 a a_1))) False % 59.08/59.29 Clause #271 (by superposition #[269, 52]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (relation (relation_dom_restriction (skS.0 8 a a_1) a_2)) True) % 59.08/59.29 Clause #274 (by superposition #[269, 89]): ∀ (a a_1 a_2 : Iota), % 59.08/59.29 Or (Eq True False) (Eq (subset (relation_dom_restriction (skS.0 8 a a_1) a_2) (skS.0 8 a a_1)) True) % 59.08/59.29 Clause #354 (by clausification #[271]): ∀ (a a_1 a_2 : Iota), Eq (relation (relation_dom_restriction (skS.0 8 a a_1) a_2)) True % 59.08/59.29 Clause #359 (by superposition #[354, 207]): ∀ (a a_1 a_2 a_3 : Iota), % 59.08/59.29 Or (Eq True False) % 59.08/59.29 (Or (Eq (relation a) False) % 59.08/59.29 (Or (Eq (subset (relation_dom_restriction (skS.0 8 a_1 a_2) a_3) a) False) % 59.08/59.29 (Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a_1 a_2) a_3)) (relation_rng a)) True))) % 59.08/59.29 Clause #580 (by clausification #[274]): ∀ (a a_1 a_2 : Iota), Eq (subset (relation_dom_restriction (skS.0 8 a a_1) a_2) (skS.0 8 a a_1)) True % 59.08/59.29 Clause #749 (by clausification #[359]): ∀ (a a_1 a_2 a_3 : Iota), % 59.08/59.29 Or (Eq (relation a) False) % 59.08/59.29 (Or (Eq (subset (relation_dom_restriction (skS.0 8 a_1 a_2) a_3) a) False) % 59.08/59.29 (Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a_1 a_2) a_3)) (relation_rng a)) True)) % 59.08/59.29 Clause #752 (by superposition #[749, 269]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 59.08/59.29 Or (Eq (subset (relation_dom_restriction (skS.0 8 a a_1) a_2) (skS.0 8 a_3 a_4)) False) % 59.08/59.29 (Or % 59.08/59.29 (Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) a_2)) (relation_rng (skS.0 8 a_3 a_4))) True) % 59.08/59.29 (Eq False True)) % 59.08/59.29 Clause #8317 (by clausification #[752]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 59.08/59.29 Or (Eq (subset (relation_dom_restriction (skS.0 8 a a_1) a_2) (skS.0 8 a_3 a_4)) False) % 59.08/59.29 (Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) a_2)) (relation_rng (skS.0 8 a_3 a_4))) True) % 59.08/59.29 Clause #8318 (by superposition #[8317, 580]): ∀ (a a_1 a_2 : Iota), % 59.08/59.29 Or (Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) a_2)) (relation_rng (skS.0 8 a a_1))) True) % 59.08/59.29 (Eq False True) % 59.08/59.29 Clause #8319 (by clausification #[8318]): ∀ (a a_1 a_2 : Iota), % 59.08/59.29 Eq (subset (relation_rng (relation_dom_restriction (skS.0 8 a a_1) a_2)) (relation_rng (skS.0 8 a a_1))) True % 59.08/59.29 Clause #8320 (by superposition #[8319, 270]): Eq True False % 59.08/59.29 Clause #8322 (by clausification #[8320]): False % 59.08/59.29 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------