%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM617+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:50 PM UTC 2025 % Result : Theorem 10.80s 11.00s % Output : Proof 10.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : NUM617+3 : TPTP v9.2.0. Released v4.0.0. % 0.13/0.15 % Command : duper %s % 0.15/0.37 % Computer : n016.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 300 % 0.15/0.37 % DateTime : Fri Oct 3 07:44:53 EDT 2025 % 0.15/0.38 % CPUTime : % 10.80/11.00 SZS status Theorem for theBenchmark.p % 10.80/11.00 SZS output start Proof for theBenchmark.p % 10.80/11.00 Clause #99 (by assumption #[]): Eq (And (∀ (W0 : Iota), aElementOf0 W0 xQ → aElementOf0 W0 szNzAzT0) (aSubsetOf0 xQ szNzAzT0)) True % 10.80/11.00 Clause #105 (by assumption #[]): Eq (And (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xQ) (aSubsetOf0 xP xQ)) True % 10.80/11.00 Clause #111 (by assumption #[]): Eq (And (And (And (aElement0 xx) (aElementOf0 xx xQ)) (Ne xx (szmzizndt0 xQ))) (aElementOf0 xx xP)) True % 10.80/11.00 Clause #112 (by assumption #[]): Eq (Not (aElementOf0 xx szNzAzT0)) True % 10.80/11.00 Clause #127 (by clausification #[112]): Eq (aElementOf0 xx szNzAzT0) False % 10.80/11.00 Clause #811 (by clausification #[99]): Eq (∀ (W0 : Iota), aElementOf0 W0 xQ → aElementOf0 W0 szNzAzT0) True % 10.80/11.00 Clause #814 (by clausification #[811]): ∀ (a : Iota), Eq (aElementOf0 a xQ → aElementOf0 a szNzAzT0) True % 10.80/11.00 Clause #815 (by clausification #[814]): ∀ (a : Iota), Or (Eq (aElementOf0 a xQ) False) (Eq (aElementOf0 a szNzAzT0) True) % 10.80/11.00 Clause #1640 (by clausification #[105]): Eq (∀ (W0 : Iota), aElementOf0 W0 xP → aElementOf0 W0 xQ) True % 10.80/11.00 Clause #1641 (by clausification #[1640]): ∀ (a : Iota), Eq (aElementOf0 a xP → aElementOf0 a xQ) True % 10.80/11.00 Clause #1642 (by clausification #[1641]): ∀ (a : Iota), Or (Eq (aElementOf0 a xP) False) (Eq (aElementOf0 a xQ) True) % 10.80/11.00 Clause #2288 (by clausification #[111]): Eq (aElementOf0 xx xP) True % 10.80/11.00 Clause #2291 (by superposition #[2288, 1642]): Or (Eq True False) (Eq (aElementOf0 xx xQ) True) % 10.80/11.00 Clause #2292 (by clausification #[2291]): Eq (aElementOf0 xx xQ) True % 10.80/11.00 Clause #2293 (by superposition #[2292, 815]): Or (Eq True False) (Eq (aElementOf0 xx szNzAzT0) True) % 10.80/11.00 Clause #2296 (by clausification #[2293]): Eq (aElementOf0 xx szNzAzT0) True % 10.80/11.00 Clause #2297 (by superposition #[2296, 127]): Eq True False % 10.80/11.00 Clause #2333 (by clausification #[2297]): False % 10.80/11.00 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------