%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU137+2 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:00:56 PM UTC 2025 % Result : Theorem 17.81s 17.98s % Output : Proof 17.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU137+2 : TPTP v9.2.0. Released v3.3.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n008.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 05:52:38 EDT 2025 % 0.13/0.34 % CPUTime : % 17.81/17.98 SZS status Theorem for theBenchmark.p % 17.81/17.98 SZS output start Proof for theBenchmark.p % 17.81/17.98 Clause #21 (by assumption #[]): Eq (∀ (A B : Iota), subset A B → Eq (set_union2 A B) B) True % 17.81/17.98 Clause #33 (by assumption #[]): Eq (∀ (A B : Iota), Eq (set_union2 A (set_difference B A)) (set_union2 A B)) True % 17.81/17.98 Clause #38 (by assumption #[]): Eq (Not (∀ (A B : Iota), subset A B → Eq B (set_union2 A (set_difference B A)))) True % 17.81/17.98 Clause #273 (by clausification #[21]): ∀ (a : Iota), Eq (∀ (B : Iota), subset a B → Eq (set_union2 a B) B) True % 17.81/17.98 Clause #274 (by clausification #[273]): ∀ (a a_1 : Iota), Eq (subset a a_1 → Eq (set_union2 a a_1) a_1) True % 17.81/17.98 Clause #275 (by clausification #[274]): ∀ (a a_1 : Iota), Or (Eq (subset a a_1) False) (Eq (Eq (set_union2 a a_1) a_1) True) % 17.81/17.98 Clause #276 (by clausification #[275]): ∀ (a a_1 : Iota), Or (Eq (subset a a_1) False) (Eq (set_union2 a a_1) a_1) % 17.81/17.98 Clause #366 (by clausification #[33]): ∀ (a : Iota), Eq (∀ (B : Iota), Eq (set_union2 a (set_difference B a)) (set_union2 a B)) True % 17.81/17.98 Clause #367 (by clausification #[366]): ∀ (a a_1 : Iota), Eq (Eq (set_union2 a (set_difference a_1 a)) (set_union2 a a_1)) True % 17.81/17.98 Clause #368 (by clausification #[367]): ∀ (a a_1 : Iota), Eq (set_union2 a (set_difference a_1 a)) (set_union2 a a_1) % 17.81/17.98 Clause #442 (by clausification #[38]): Eq (∀ (A B : Iota), subset A B → Eq B (set_union2 A (set_difference B A))) False % 17.81/17.98 Clause #443 (by clausification #[442]): ∀ (a : Iota), % 17.81/17.98 Eq (Not (∀ (B : Iota), subset (skS.0 8 a) B → Eq B (set_union2 (skS.0 8 a) (set_difference B (skS.0 8 a))))) True % 17.81/17.98 Clause #444 (by clausification #[443]): ∀ (a : Iota), % 17.81/17.98 Eq (∀ (B : Iota), subset (skS.0 8 a) B → Eq B (set_union2 (skS.0 8 a) (set_difference B (skS.0 8 a)))) False % 17.81/17.98 Clause #445 (by clausification #[444]): ∀ (a a_1 : Iota), % 17.81/17.98 Eq % 17.81/17.98 (Not % 17.81/17.98 (subset (skS.0 8 a) (skS.0 9 a a_1) → % 17.81/17.98 Eq (skS.0 9 a a_1) (set_union2 (skS.0 8 a) (set_difference (skS.0 9 a a_1) (skS.0 8 a))))) % 17.81/17.98 True % 17.81/17.98 Clause #446 (by clausification #[445]): ∀ (a a_1 : Iota), % 17.81/17.98 Eq % 17.81/17.98 (subset (skS.0 8 a) (skS.0 9 a a_1) → % 17.81/17.98 Eq (skS.0 9 a a_1) (set_union2 (skS.0 8 a) (set_difference (skS.0 9 a a_1) (skS.0 8 a)))) % 17.81/17.98 False % 17.81/17.98 Clause #447 (by clausification #[446]): ∀ (a a_1 : Iota), Eq (subset (skS.0 8 a) (skS.0 9 a a_1)) True % 17.81/17.98 Clause #448 (by clausification #[446]): ∀ (a a_1 : Iota), Eq (Eq (skS.0 9 a a_1) (set_union2 (skS.0 8 a) (set_difference (skS.0 9 a a_1) (skS.0 8 a)))) False % 17.81/17.98 Clause #453 (by superposition #[447, 276]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (set_union2 (skS.0 8 a) (skS.0 9 a a_1)) (skS.0 9 a a_1)) % 17.81/17.98 Clause #5785 (by clausification #[448]): ∀ (a a_1 : Iota), Ne (skS.0 9 a a_1) (set_union2 (skS.0 8 a) (set_difference (skS.0 9 a a_1) (skS.0 8 a))) % 17.81/17.98 Clause #5786 (by forward demodulation #[5785, 368]): ∀ (a a_1 : Iota), Ne (skS.0 9 a a_1) (set_union2 (skS.0 8 a) (skS.0 9 a a_1)) % 17.81/17.98 Clause #5951 (by clausification #[453]): ∀ (a a_1 : Iota), Eq (set_union2 (skS.0 8 a) (skS.0 9 a a_1)) (skS.0 9 a a_1) % 17.81/17.98 Clause #5952 (by forward contextual literal cutting #[5951, 5786]): False % 17.81/17.98 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------