%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET019+4 : TPTP v9.2.0. Released v2.2.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 07:59:23 PM UTC 2025 % Result : Theorem 66.69s 67.00s % Output : Proof 66.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.24 % Problem : SET019+4 : TPTP v9.2.0. Released v2.2.0. % 0.07/0.25 % Command : duper %s % 0.12/0.44 % Computer : n007.cluster.edu % 0.12/0.44 % Model : x86_64 x86_64 % 0.12/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.44 % Memory : 8042.1875MB % 0.12/0.44 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.44 % CPULimit : 300 % 0.12/0.44 % WCLimit : 300 % 0.12/0.44 % DateTime : Thu Oct 2 14:04:23 EDT 2025 % 0.12/0.44 % CPUTime : % 66.69/67.00 SZS status Theorem for theBenchmark.p % 66.69/67.00 SZS output start Proof for theBenchmark.p % 66.69/67.00 Clause #1 (by assumption #[]): Eq (∀ (A B : Iota), Iff (equal_set A B) (And (subset A B) (subset B A))) True % 66.69/67.00 Clause #11 (by assumption #[]): Eq (Not (∀ (A B : Iota), And (subset A B) (subset B A) → equal_set A B)) True % 66.69/67.00 Clause #14 (by clausification #[11]): Eq (∀ (A B : Iota), And (subset A B) (subset B A) → equal_set A B) False % 66.69/67.00 Clause #15 (by clausification #[14]): ∀ (a : Iota), Eq (Not (∀ (B : Iota), And (subset (skS.0 0 a) B) (subset B (skS.0 0 a)) → equal_set (skS.0 0 a) B)) True % 66.69/67.00 Clause #16 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (B : Iota), And (subset (skS.0 0 a) B) (subset B (skS.0 0 a)) → equal_set (skS.0 0 a) B) False % 66.69/67.00 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), % 66.69/67.00 Eq % 66.69/67.00 (Not % 66.69/67.00 (And (subset (skS.0 0 a) (skS.0 1 a a_1)) (subset (skS.0 1 a a_1) (skS.0 0 a)) → % 66.69/67.00 equal_set (skS.0 0 a) (skS.0 1 a a_1))) % 66.69/67.00 True % 66.69/67.00 Clause #18 (by clausification #[17]): ∀ (a a_1 : Iota), % 66.69/67.00 Eq % 66.69/67.00 (And (subset (skS.0 0 a) (skS.0 1 a a_1)) (subset (skS.0 1 a a_1) (skS.0 0 a)) → % 66.69/67.00 equal_set (skS.0 0 a) (skS.0 1 a a_1)) % 66.69/67.00 False % 66.69/67.00 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (And (subset (skS.0 0 a) (skS.0 1 a a_1)) (subset (skS.0 1 a a_1) (skS.0 0 a))) True % 66.69/67.00 Clause #20 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (equal_set (skS.0 0 a) (skS.0 1 a a_1)) False % 66.69/67.00 Clause #21 (by clausification #[19]): ∀ (a a_1 : Iota), Eq (subset (skS.0 1 a a_1) (skS.0 0 a)) True % 66.69/67.00 Clause #22 (by clausification #[19]): ∀ (a a_1 : Iota), Eq (subset (skS.0 0 a) (skS.0 1 a a_1)) True % 66.69/67.00 Clause #38 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (equal_set a B) (And (subset a B) (subset B a))) True % 66.69/67.00 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), Eq (Iff (equal_set a a_1) (And (subset a a_1) (subset a_1 a))) True % 66.69/67.00 Clause #40 (by clausification #[39]): ∀ (a a_1 : Iota), Or (Eq (equal_set a a_1) True) (Eq (And (subset a a_1) (subset a_1 a)) False) % 66.69/67.00 Clause #42 (by clausification #[40]): ∀ (a a_1 : Iota), Or (Eq (equal_set a a_1) True) (Or (Eq (subset a a_1) False) (Eq (subset a_1 a) False)) % 66.69/67.00 Clause #294 (by superposition #[22, 42]): ∀ (a a_1 : Iota), % 66.69/67.00 Or (Eq (equal_set (skS.0 0 a) (skS.0 1 a a_1)) True) % 66.69/67.00 (Or (Eq (subset (skS.0 1 a a_1) (skS.0 0 a)) False) (Eq False True)) % 66.69/67.00 Clause #22120 (by clausification #[294]): ∀ (a a_1 : Iota), Or (Eq (equal_set (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq (subset (skS.0 1 a a_1) (skS.0 0 a)) False) % 66.69/67.00 Clause #22121 (by forward demodulation #[22120, 21]): ∀ (a a_1 : Iota), Or (Eq (equal_set (skS.0 0 a) (skS.0 1 a a_1)) True) (Eq True False) % 66.69/67.00 Clause #22122 (by clausification #[22121]): ∀ (a a_1 : Iota), Eq (equal_set (skS.0 0 a) (skS.0 1 a a_1)) True % 66.69/67.00 Clause #22123 (by superposition #[22122, 20]): Eq True False % 66.69/67.00 Clause #22124 (by clausification #[22123]): False % 66.69/67.00 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------