%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM557+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:43 PM UTC 2025 % Result : Theorem 5.55s 5.72s % Output : Proof 5.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM557+3 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n010.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 08:22:23 EDT 2025 % 0.13/0.34 % CPUTime : % 5.55/5.72 SZS status Theorem for theBenchmark.p % 5.55/5.72 SZS output start Proof for theBenchmark.p % 5.55/5.72 Clause #62 (by assumption #[]): Eq % 5.55/5.72 (And % 5.55/5.72 (And % 5.55/5.72 (And % 5.55/5.72 (And % 5.55/5.72 (And % 5.55/5.72 (And (aSet0 (slbdtsldtrb0 xS xk)) % 5.55/5.72 (∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xS xk)))) % 5.55/5.72 (aSet0 (slbdtsldtrb0 xT xk))) % 5.55/5.72 (∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xT xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xT)) (aSubsetOf0 W0 xT)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xT)) (aSubsetOf0 W0 xT)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xT xk)))) % 5.55/5.72 (∀ (W0 : Iota), aElementOf0 W0 (slbdtsldtrb0 xS xk) → aElementOf0 W0 (slbdtsldtrb0 xT xk))) % 5.55/5.72 (aSubsetOf0 (slbdtsldtrb0 xS xk) (slbdtsldtrb0 xT xk))) % 5.55/5.72 (Not % 5.55/5.72 ((∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 5.55/5.72 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0)))) % 5.55/5.72 True % 5.55/5.72 Clause #70 (by assumption #[]): Eq (And (And (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xS) (aSubsetOf0 xP xS)) (Eq (sbrdtbr0 xP) xk)) True % 5.55/5.72 Clause #71 (by assumption #[]): Eq % 5.55/5.72 (Not % 5.55/5.72 (Or (And (Or (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xS) (aSubsetOf0 xP xS)) (Eq (sbrdtbr0 xP) xk)) % 5.55/5.72 (aElementOf0 xP (slbdtsldtrb0 xS xk)))) % 5.55/5.72 True % 5.55/5.72 Clause #911 (by clausification #[62]): Eq % 5.55/5.72 (Not % 5.55/5.72 ((∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 5.55/5.72 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0))) % 5.55/5.72 True % 5.55/5.72 Clause #913 (by clausification #[911]): Eq % 5.55/5.72 ((∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xS xk))) → % 5.55/5.72 Or (Not (Exists fun W0 => aElementOf0 W0 (slbdtsldtrb0 xS xk))) (Eq (slbdtsldtrb0 xS xk) slcrc0)) % 5.55/5.72 False % 5.55/5.72 Clause #914 (by clausification #[913]): Eq % 5.55/5.72 (∀ (W0 : Iota), % 5.55/5.72 And % 5.55/5.72 (aElementOf0 W0 (slbdtsldtrb0 xS xk) → % 5.55/5.72 And (And (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk)) % 5.55/5.72 (And (Or (And (aSet0 W0) (∀ (W1 : Iota), aElementOf0 W1 W0 → aElementOf0 W1 xS)) (aSubsetOf0 W0 xS)) % 5.55/5.72 (Eq (sbrdtbr0 W0) xk) → % 5.55/5.72 aElementOf0 W0 (slbdtsldtrb0 xS xk))) % 5.55/5.72 True % 5.55/5.72 Clause #916 (by clausification #[914]): ∀ (a : Iota), % 5.55/5.72 Eq % 5.55/5.72 (And % 5.55/5.73 (aElementOf0 a (slbdtsldtrb0 xS xk) → % 5.55/5.73 And (And (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) % 5.55/5.73 (Eq (sbrdtbr0 a) xk)) % 5.55/5.73 (And (Or (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) % 5.55/5.73 (Eq (sbrdtbr0 a) xk) → % 5.55/5.73 aElementOf0 a (slbdtsldtrb0 xS xk))) % 5.55/5.73 True % 5.55/5.73 Clause #917 (by clausification #[916]): ∀ (a : Iota), % 5.55/5.73 Eq % 5.55/5.73 (And (Or (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) % 5.55/5.73 (Eq (sbrdtbr0 a) xk) → % 5.55/5.73 aElementOf0 a (slbdtsldtrb0 xS xk)) % 5.55/5.73 True % 5.55/5.73 Clause #919 (by clausification #[917]): ∀ (a : Iota), % 5.55/5.73 Or % 5.55/5.73 (Eq % 5.55/5.73 (And (Or (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) % 5.55/5.73 (Eq (sbrdtbr0 a) xk)) % 5.55/5.73 False) % 5.55/5.73 (Eq (aElementOf0 a (slbdtsldtrb0 xS xk)) True) % 5.55/5.73 Clause #920 (by clausification #[919]): ∀ (a : Iota), % 5.55/5.73 Or (Eq (aElementOf0 a (slbdtsldtrb0 xS xk)) True) % 5.55/5.73 (Or (Eq (Or (And (aSet0 a) (∀ (W1 : Iota), aElementOf0 W1 a → aElementOf0 W1 xS)) (aSubsetOf0 a xS)) False) % 5.55/5.74 (Eq (Eq (sbrdtbr0 a) xk) False)) % 5.55/5.74 Clause #921 (by clausification #[920]): ∀ (a : Iota), % 5.55/5.74 Or (Eq (aElementOf0 a (slbdtsldtrb0 xS xk)) True) (Or (Eq (Eq (sbrdtbr0 a) xk) False) (Eq (aSubsetOf0 a xS) False)) % 5.55/5.74 Clause #923 (by clausification #[921]): ∀ (a : Iota), Or (Eq (aElementOf0 a (slbdtsldtrb0 xS xk)) True) (Or (Eq (aSubsetOf0 a xS) False) (Ne (sbrdtbr0 a) xk)) % 5.55/5.74 Clause #1040 (by clausification #[70]): Eq (Eq (sbrdtbr0 xP) xk) True % 5.55/5.74 Clause #1041 (by clausification #[70]): Eq (And (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xS) (aSubsetOf0 xP xS)) True % 5.55/5.74 Clause #1042 (by clausification #[1040]): Eq (sbrdtbr0 xP) xk % 5.55/5.74 Clause #1043 (by clausification #[1041]): Eq (aSubsetOf0 xP xS) True % 5.55/5.74 Clause #1045 (by superposition #[1043, 923]): Or (Eq (aElementOf0 xP (slbdtsldtrb0 xS xk)) True) (Or (Eq True False) (Ne (sbrdtbr0 xP) xk)) % 5.55/5.74 Clause #1048 (by clausification #[1045]): Or (Eq (aElementOf0 xP (slbdtsldtrb0 xS xk)) True) (Ne (sbrdtbr0 xP) xk) % 5.55/5.74 Clause #1049 (by forward demodulation #[1048, 1042]): Or (Eq (aElementOf0 xP (slbdtsldtrb0 xS xk)) True) (Ne xk xk) % 5.55/5.74 Clause #1050 (by eliminate resolved literals #[1049]): Eq (aElementOf0 xP (slbdtsldtrb0 xS xk)) True % 5.55/5.74 Clause #1076 (by clausification #[71]): Eq % 5.55/5.74 (Or (And (Or (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xS) (aSubsetOf0 xP xS)) (Eq (sbrdtbr0 xP) xk)) % 5.55/5.74 (aElementOf0 xP (slbdtsldtrb0 xS xk))) % 5.55/5.74 False % 5.55/5.74 Clause #1077 (by clausification #[1076]): Eq (aElementOf0 xP (slbdtsldtrb0 xS xk)) False % 5.55/5.74 Clause #1079 (by superposition #[1077, 1050]): Eq False True % 5.55/5.74 Clause #1080 (by clausification #[1079]): False % 5.55/5.74 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------