%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU219+3 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:09 PM UTC 2025 % Result : Theorem 77.05s 77.26s % Output : Proof 77.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.09 % Problem : SEU219+3 : TPTP v9.2.0. Released v3.2.0. % 0.06/0.10 % Command : duper %s % 0.09/0.30 % Computer : n021.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Fri Oct 3 06:22:53 EDT 2025 % 0.09/0.30 % CPUTime : % 77.05/77.26 SZS status Theorem for theBenchmark.p % 77.05/77.26 SZS output start Proof for theBenchmark.p % 77.05/77.26 Clause #4 (by assumption #[]): Eq (∀ (A : Iota), And (relation A) (function A) → one_to_one A → Eq (function_inverse A) (relation_inverse A)) True % 77.05/77.26 Clause #32 (by assumption #[]): Eq % 77.05/77.26 (∀ (A : Iota), % 77.05/77.26 relation A → % 77.05/77.26 And (Eq (relation_rng A) (relation_dom (relation_inverse A))) % 77.05/77.26 (Eq (relation_dom A) (relation_rng (relation_inverse A)))) % 77.05/77.26 True % 77.05/77.26 Clause #35 (by assumption #[]): Eq % 77.05/77.26 (Not % 77.05/77.26 (∀ (A : Iota), % 77.05/77.26 And (relation A) (function A) → % 77.05/77.26 one_to_one A → % 77.05/77.26 And (Eq (relation_rng A) (relation_dom (function_inverse A))) % 77.05/77.26 (Eq (relation_dom A) (relation_rng (function_inverse A))))) % 77.05/77.26 True % 77.05/77.26 Clause #93 (by clausification #[4]): ∀ (a : Iota), Eq (And (relation a) (function a) → one_to_one a → Eq (function_inverse a) (relation_inverse a)) True % 77.05/77.26 Clause #94 (by clausification #[93]): ∀ (a : Iota), % 77.05/77.26 Or (Eq (And (relation a) (function a)) False) (Eq (one_to_one a → Eq (function_inverse a) (relation_inverse a)) True) % 77.05/77.26 Clause #95 (by clausification #[94]): ∀ (a : Iota), % 77.05/77.26 Or (Eq (one_to_one a → Eq (function_inverse a) (relation_inverse a)) True) % 77.05/77.26 (Or (Eq (relation a) False) (Eq (function a) False)) % 77.05/77.26 Clause #96 (by clausification #[95]): ∀ (a : Iota), % 77.05/77.26 Or (Eq (relation a) False) % 77.05/77.26 (Or (Eq (function a) False) (Or (Eq (one_to_one a) False) (Eq (Eq (function_inverse a) (relation_inverse a)) True))) % 77.05/77.26 Clause #97 (by clausification #[96]): ∀ (a : Iota), % 77.05/77.26 Or (Eq (relation a) False) % 77.05/77.26 (Or (Eq (function a) False) (Or (Eq (one_to_one a) False) (Eq (function_inverse a) (relation_inverse a)))) % 77.05/77.26 Clause #359 (by clausification #[32]): ∀ (a : Iota), % 77.05/77.26 Eq % 77.05/77.26 (relation a → % 77.05/77.26 And (Eq (relation_rng a) (relation_dom (relation_inverse a))) % 77.05/77.26 (Eq (relation_dom a) (relation_rng (relation_inverse a)))) % 77.05/77.26 True % 77.05/77.26 Clause #360 (by clausification #[359]): ∀ (a : Iota), % 77.05/77.26 Or (Eq (relation a) False) % 77.05/77.26 (Eq % 77.05/77.26 (And (Eq (relation_rng a) (relation_dom (relation_inverse a))) % 77.05/77.26 (Eq (relation_dom a) (relation_rng (relation_inverse a)))) % 77.05/77.26 True) % 77.05/77.26 Clause #361 (by clausification #[360]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Eq (relation_dom a) (relation_rng (relation_inverse a))) True) % 77.05/77.26 Clause #362 (by clausification #[360]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (Eq (relation_rng a) (relation_dom (relation_inverse a))) True) % 77.05/77.26 Clause #363 (by clausification #[361]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (relation_dom a) (relation_rng (relation_inverse a))) % 77.05/77.26 Clause #404 (by clausification #[35]): Eq % 77.05/77.26 (∀ (A : Iota), % 77.05/77.26 And (relation A) (function A) → % 77.05/77.26 one_to_one A → % 77.05/77.26 And (Eq (relation_rng A) (relation_dom (function_inverse A))) % 77.05/77.26 (Eq (relation_dom A) (relation_rng (function_inverse A)))) % 77.05/77.26 False % 77.05/77.26 Clause #405 (by clausification #[404]): ∀ (a : Iota), % 77.05/77.26 Eq % 77.05/77.26 (Not % 77.05/77.26 (And (relation (skS.0 11 a)) (function (skS.0 11 a)) → % 77.05/77.26 one_to_one (skS.0 11 a) → % 77.05/77.26 And (Eq (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.05/77.26 (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))))) % 77.05/77.26 True % 77.05/77.26 Clause #406 (by clausification #[405]): ∀ (a : Iota), % 77.05/77.26 Eq % 77.05/77.26 (And (relation (skS.0 11 a)) (function (skS.0 11 a)) → % 77.05/77.26 one_to_one (skS.0 11 a) → % 77.05/77.26 And (Eq (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.05/77.26 (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a))))) % 77.05/77.26 False % 77.05/77.26 Clause #407 (by clausification #[406]): ∀ (a : Iota), Eq (And (relation (skS.0 11 a)) (function (skS.0 11 a))) True % 77.05/77.26 Clause #408 (by clausification #[406]): ∀ (a : Iota), % 77.05/77.26 Eq % 77.05/77.26 (one_to_one (skS.0 11 a) → % 77.05/77.26 And (Eq (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.05/77.26 (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a))))) % 77.05/77.26 False % 77.05/77.26 Clause #409 (by clausification #[407]): ∀ (a : Iota), Eq (function (skS.0 11 a)) True % 77.05/77.26 Clause #410 (by clausification #[407]): ∀ (a : Iota), Eq (relation (skS.0 11 a)) True % 77.10/77.30 Clause #416 (by superposition #[410, 97]): ∀ (a : Iota), % 77.10/77.30 Or (Eq True False) % 77.10/77.30 (Or (Eq (function (skS.0 11 a)) False) % 77.10/77.30 (Or (Eq (one_to_one (skS.0 11 a)) False) (Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a))))) % 77.10/77.30 Clause #420 (by superposition #[410, 363]): ∀ (a : Iota), Or (Eq True False) (Eq (relation_dom (skS.0 11 a)) (relation_rng (relation_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #526 (by clausification #[362]): ∀ (a : Iota), Or (Eq (relation a) False) (Eq (relation_rng a) (relation_dom (relation_inverse a))) % 77.10/77.30 Clause #533 (by superposition #[526, 410]): ∀ (a : Iota), Or (Eq (relation_rng (skS.0 11 a)) (relation_dom (relation_inverse (skS.0 11 a)))) (Eq False True) % 77.10/77.30 Clause #1268 (by clausification #[420]): ∀ (a : Iota), Eq (relation_dom (skS.0 11 a)) (relation_rng (relation_inverse (skS.0 11 a))) % 77.10/77.30 Clause #1281 (by clausification #[533]): ∀ (a : Iota), Eq (relation_rng (skS.0 11 a)) (relation_dom (relation_inverse (skS.0 11 a))) % 77.10/77.30 Clause #1543 (by clausification #[408]): ∀ (a : Iota), Eq (one_to_one (skS.0 11 a)) True % 77.10/77.30 Clause #1544 (by clausification #[408]): ∀ (a : Iota), % 77.10/77.30 Eq % 77.10/77.30 (And (Eq (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.10/77.30 (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a))))) % 77.10/77.30 False % 77.10/77.30 Clause #1579 (by clausification #[416]): ∀ (a : Iota), % 77.10/77.30 Or (Eq (function (skS.0 11 a)) False) % 77.10/77.30 (Or (Eq (one_to_one (skS.0 11 a)) False) (Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #1580 (by forward demodulation #[1579, 409]): ∀ (a : Iota), % 77.10/77.30 Or (Eq True False) % 77.10/77.30 (Or (Eq (one_to_one (skS.0 11 a)) False) (Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #1581 (by clausification #[1580]): ∀ (a : Iota), % 77.10/77.30 Or (Eq (one_to_one (skS.0 11 a)) False) (Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a))) % 77.10/77.30 Clause #1582 (by superposition #[1581, 1543]): ∀ (a : Iota), Or (Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a))) (Eq False True) % 77.10/77.30 Clause #1623 (by clausification #[1582]): ∀ (a : Iota), Eq (function_inverse (skS.0 11 a)) (relation_inverse (skS.0 11 a)) % 77.10/77.30 Clause #6685 (by clausification #[1544]): ∀ (a : Iota), % 77.10/77.30 Or (Eq (Eq (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) False) % 77.10/77.30 (Eq (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))) False) % 77.10/77.30 Clause #6686 (by clausification #[6685]): ∀ (a : Iota), % 77.10/77.30 Or (Eq (Eq (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))) False) % 77.10/77.30 (Ne (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #6687 (by clausification #[6686]): ∀ (a : Iota), % 77.10/77.30 Or (Ne (relation_rng (skS.0 11 a)) (relation_dom (function_inverse (skS.0 11 a)))) % 77.10/77.30 (Ne (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #6688 (by forward demodulation #[6687, 1623]): ∀ (a : Iota), % 77.10/77.30 Or (Ne (relation_rng (skS.0 11 a)) (relation_dom (relation_inverse (skS.0 11 a)))) % 77.10/77.30 (Ne (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #6689 (by forward demodulation #[6688, 1281]): ∀ (a : Iota), % 77.10/77.30 Or (Ne (relation_rng (skS.0 11 a)) (relation_rng (skS.0 11 a))) % 77.10/77.30 (Ne (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a)))) % 77.10/77.30 Clause #6690 (by eliminate resolved literals #[6689]): ∀ (a : Iota), Ne (relation_dom (skS.0 11 a)) (relation_rng (function_inverse (skS.0 11 a))) % 77.10/77.30 Clause #6691 (by forward demodulation #[6690, 1623]): ∀ (a : Iota), Ne (relation_dom (skS.0 11 a)) (relation_rng (relation_inverse (skS.0 11 a))) % 77.10/77.30 Clause #6692 (by forward demodulation #[6691, 1268]): ∀ (a : Iota), Ne (relation_dom (skS.0 11 a)) (relation_dom (skS.0 11 a)) % 77.10/77.30 Clause #6693 (by eliminate resolved literals #[6692]): False % 77.10/77.30 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------