%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM547+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:56:42 PM UTC 2025 % Result : Theorem 252.08s 252.31s % Output : Proof 252.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : NUM547+3 : TPTP v9.2.0. Released v4.0.0. % 0.08/0.14 % Command : duper %s % 0.13/0.35 % Computer : n028.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 07:35:38 EDT 2025 % 0.13/0.35 % CPUTime : % 252.08/252.31 SZS status Theorem for theBenchmark.p % 252.08/252.31 SZS output start Proof for theBenchmark.p % 252.08/252.31 Clause #62 (by assumption #[]): Eq % 252.08/252.31 (And % 252.08/252.31 (And % 252.08/252.31 (And % 252.08/252.31 (And % 252.08/252.31 (And % 252.08/252.31 (And (aSet0 (slbdtsldtrb0 xS xk)) % 252.08/252.31 (∀ (W0 : Iota), % 252.08/252.31 And % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 252.08/252.31 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk) → % 252.08/252.31 aElementOf0 W0 (slbdtsldtrb0 xS xk)))) % 252.08/252.31 (aSet0 (slbdtsldtrb0 xT xk))) % 252.08/252.31 (∀ (W0 : Iota), % 252.08/252.31 And % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xT xk) → % 252.08/252.31 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xT)) (aSubsetOf0 W0 xT)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xT)) (aSubsetOf0 W0 xT)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk) → % 252.08/252.31 aElementOf0 W0 (slbdtsldtrb0 xT xk)))) % 252.08/252.31 (∀ (W0 : Iota), aElementOf0 W0 (slbdtsldtrb0 xS xk) → aElementOf0 W0 (slbdtsldtrb0 xT xk))) % 252.08/252.31 (aSubsetOf0 (slbdtsldtrb0 xS xk) (slbdtsldtrb0 xT xk))) % 252.08/252.31 (Not % 252.08/252.31 ((∀ (W0 : Iota), % 252.08/252.31 And % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 252.08/252.31 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk) → % 252.08/252.31 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 252.08/252.31 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0)))) % 252.08/252.31 True % 252.08/252.31 Clause #64 (by assumption #[]): Eq % 252.08/252.31 (Not % 252.08/252.31 (Exists fun W0 => % 252.08/252.31 Or % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk)))) % 252.08/252.31 True % 252.08/252.31 Clause #862 (by clausification #[62]): Eq % 252.08/252.31 (Not % 252.08/252.31 ((∀ (W0 : Iota), % 252.08/252.31 And % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 252.08/252.31 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk) → % 252.08/252.31 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 252.08/252.31 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0))) % 252.08/252.31 True % 252.08/252.31 Clause #864 (by clausification #[862]): Eq % 252.08/252.31 ((∀ (W0 : Iota), % 252.08/252.31 And % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 252.08/252.31 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk) → % 252.08/252.31 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 252.08/252.31 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0)) % 252.08/252.31 False % 252.08/252.31 Clause #866 (by clausification #[864]): Eq (Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0)) False % 252.08/252.31 Clause #881 (by clausification #[64]): Eq % 252.08/252.31 (Exists fun W0 => % 252.08/252.31 Or % 252.08/252.31 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 252.08/252.31 (Eq (sbrdtbr0 W0) xk)) % 252.08/252.31 (aElementOf0 W0 (slbdtsldtrb0 xS xk))) % 252.08/252.31 False % 252.08/252.31 Clause #882 (by clausification #[881]): ∀ (a : Iota), % 252.08/252.31 Eq % 252.08/252.31 (Or % 252.08/252.31 (And (Or (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) % 252.08/252.31 (Eq (sbrdtbr0 a) xk)) % 252.08/252.31 (aElementOf0 a (slbdtsldtrb0 xS xk))) % 252.39/252.61 False % 252.39/252.61 Clause #883 (by clausification #[882]): ∀ (a : Iota), Eq (aElementOf0 a (slbdtsldtrb0 xS xk)) False % 252.39/252.61 Clause #63999 (by clausification #[866]): Eq (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) False % 252.39/252.61 Clause #64001 (by clausification #[63999]): Eq (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk)) True % 252.39/252.61 Clause #64002 (by clausification #[64001]): ∀ (a : Iota), Eq (aElementOf0 (skS.0 11 a) (slbdtsldtrb0 xS xk)) True % 252.39/252.61 Clause #64003 (by superposition #[64002, 883]): Eq True False % 252.39/252.61 Clause #64004 (by clausification #[64003]): False % 252.39/252.61 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------