%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM624+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:51 PM UTC 2025 % Result : Theorem 76.59s 76.84s % Output : Proof 76.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM624+3 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.14 % Command : duper %s % 0.15/0.35 % Computer : n001.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 07:40:38 EDT 2025 % 0.15/0.35 % CPUTime : % 76.59/76.84 SZS status Theorem for theBenchmark.p % 76.59/76.84 SZS output start Proof for theBenchmark.p % 76.59/76.84 Clause #34 (by assumption #[]): Eq % 76.59/76.84 (∀ (W0 W1 : Iota), % 76.59/76.84 And (aElementOf0 W0 szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 W0 W1) (sdtlseqdt0 W1 W0) → Eq W0 W1) % 76.59/76.84 True % 76.59/76.84 Clause #99 (by assumption #[]): Eq (And (∀ (W0 : Iota), aElementOf0 W0 xQ → aElementOf0 W0 szNzAzT0) (aSubsetOf0 xQ szNzAzT0)) True % 76.59/76.84 Clause #101 (by assumption #[]): Eq (And (And (aElementOf0 xp xQ) (∀ (W0 : Iota), aElementOf0 W0 xQ → sdtlseqdt0 xp W0)) (Eq xp (szmzizndt0 xQ))) True % 76.59/76.84 Clause #103 (by assumption #[]): Eq (aElementOf0 xp xQ) True % 76.59/76.84 Clause #114 (by assumption #[]): Eq (∀ (W0 : Iota), aElementOf0 W0 (sdtlpdtrp0 xN xm) → sdtlseqdt0 xx W0) True % 76.59/76.84 Clause #117 (by assumption #[]): Eq (And (aElementOf0 xp (sdtlpdtrp0 xN xm)) (aElementOf0 xx xQ)) True % 76.59/76.84 Clause #119 (by assumption #[]): Eq (Not (Eq xp xx)) True % 76.59/76.84 Clause #186 (by clausification #[119]): Eq (Eq xp xx) False % 76.59/76.84 Clause #187 (by clausification #[186]): Ne xp xx % 76.59/76.84 Clause #188 (by clausification #[114]): ∀ (a : Iota), Eq (aElementOf0 a (sdtlpdtrp0 xN xm) → sdtlseqdt0 xx a) True % 76.59/76.84 Clause #189 (by clausification #[188]): ∀ (a : Iota), Or (Eq (aElementOf0 a (sdtlpdtrp0 xN xm)) False) (Eq (sdtlseqdt0 xx a) True) % 76.59/76.84 Clause #417 (by clausification #[34]): ∀ (a : Iota), % 76.59/76.84 Eq % 76.59/76.84 (∀ (W1 : Iota), % 76.59/76.84 And (aElementOf0 a szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 a W1) (sdtlseqdt0 W1 a) → Eq a W1) % 76.59/76.84 True % 76.59/76.84 Clause #418 (by clausification #[417]): ∀ (a a_1 : Iota), % 76.59/76.84 Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0) → And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) % 76.59/76.84 True % 76.59/76.84 Clause #419 (by clausification #[418]): ∀ (a a_1 : Iota), % 76.59/76.84 Or (Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0)) False) % 76.59/76.84 (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 76.59/76.84 Clause #420 (by clausification #[419]): ∀ (a a_1 : Iota), % 76.59/76.84 Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 76.59/76.84 (Or (Eq (aElementOf0 a szNzAzT0) False) (Eq (aElementOf0 a_1 szNzAzT0) False)) % 76.59/76.84 Clause #421 (by clausification #[420]): ∀ (a a_1 : Iota), % 76.59/76.84 Or (Eq (aElementOf0 a szNzAzT0) False) % 76.59/76.84 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 76.59/76.84 (Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a)) False) (Eq (Eq a a_1) True))) % 76.59/76.84 Clause #422 (by clausification #[421]): ∀ (a a_1 : Iota), % 76.59/76.84 Or (Eq (aElementOf0 a szNzAzT0) False) % 76.59/76.84 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 76.59/76.84 (Or (Eq (Eq a a_1) True) (Or (Eq (sdtlseqdt0 a a_1) False) (Eq (sdtlseqdt0 a_1 a) False)))) % 76.59/76.84 Clause #423 (by clausification #[422]): ∀ (a a_1 : Iota), % 76.59/76.84 Or (Eq (aElementOf0 a szNzAzT0) False) % 76.59/76.84 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 76.59/76.84 (Or (Eq (sdtlseqdt0 a a_1) False) (Or (Eq (sdtlseqdt0 a_1 a) False) (Eq a a_1)))) % 76.59/76.84 Clause #780 (by clausification #[99]): Eq (∀ (W0 : Iota), aElementOf0 W0 xQ → aElementOf0 W0 szNzAzT0) True % 76.59/76.84 Clause #782 (by clausification #[780]): ∀ (a : Iota), Eq (aElementOf0 a xQ → aElementOf0 a szNzAzT0) True % 76.59/76.84 Clause #783 (by clausification #[782]): ∀ (a : Iota), Or (Eq (aElementOf0 a xQ) False) (Eq (aElementOf0 a szNzAzT0) True) % 76.59/76.84 Clause #784 (by superposition #[783, 103]): Or (Eq (aElementOf0 xp szNzAzT0) True) (Eq False True) % 76.59/76.84 Clause #801 (by clausification #[784]): Eq (aElementOf0 xp szNzAzT0) True % 76.59/76.84 Clause #810 (by superposition #[801, 423]): ∀ (a : Iota), % 76.59/76.84 Or (Eq True False) % 76.59/76.84 (Or (Eq (aElementOf0 a szNzAzT0) False) % 76.59/76.84 (Or (Eq (sdtlseqdt0 xp a) False) (Or (Eq (sdtlseqdt0 a xp) False) (Eq xp a)))) % 76.59/76.84 Clause #1115 (by clausification #[117]): Eq (aElementOf0 xx xQ) True % 76.59/76.84 Clause #1116 (by clausification #[117]): Eq (aElementOf0 xp (sdtlpdtrp0 xN xm)) True % 76.59/76.84 Clause #1117 (by superposition #[1115, 783]): Or (Eq True False) (Eq (aElementOf0 xx szNzAzT0) True) % 76.59/76.84 Clause #1118 (by clausification #[1117]): Eq (aElementOf0 xx szNzAzT0) True % 76.59/76.84 Clause #1167 (by superposition #[1116, 189]): Or (Eq True False) (Eq (sdtlseqdt0 xx xp) True) % 76.59/76.84 Clause #1168 (by clausification #[1167]): Eq (sdtlseqdt0 xx xp) True % 76.59/76.84 Clause #2154 (by clausification #[101]): Eq (And (aElementOf0 xp xQ) (∀ (W0 : Iota), aElementOf0 W0 xQ → sdtlseqdt0 xp W0)) True % 76.74/76.92 Clause #2159 (by clausification #[2154]): Eq (∀ (W0 : Iota), aElementOf0 W0 xQ → sdtlseqdt0 xp W0) True % 76.74/76.92 Clause #2160 (by clausification #[2159]): ∀ (a : Iota), Eq (aElementOf0 a xQ → sdtlseqdt0 xp a) True % 76.74/76.92 Clause #2161 (by clausification #[2160]): ∀ (a : Iota), Or (Eq (aElementOf0 a xQ) False) (Eq (sdtlseqdt0 xp a) True) % 76.74/76.92 Clause #2163 (by superposition #[2161, 1115]): Or (Eq (sdtlseqdt0 xp xx) True) (Eq False True) % 76.74/76.92 Clause #2165 (by clausification #[2163]): Eq (sdtlseqdt0 xp xx) True % 76.74/76.92 Clause #16252 (by clausification #[810]): ∀ (a : Iota), % 76.74/76.92 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xp a) False) (Or (Eq (sdtlseqdt0 a xp) False) (Eq xp a))) % 76.74/76.92 Clause #16266 (by superposition #[16252, 1118]): Or (Eq (sdtlseqdt0 xp xx) False) (Or (Eq (sdtlseqdt0 xx xp) False) (Or (Eq xp xx) (Eq False True))) % 76.74/76.92 Clause #16296 (by clausification #[16266]): Or (Eq (sdtlseqdt0 xp xx) False) (Or (Eq (sdtlseqdt0 xx xp) False) (Eq xp xx)) % 76.74/76.92 Clause #16297 (by forward demodulation #[16296, 1168]): Or (Eq (sdtlseqdt0 xp xx) False) (Or (Eq True False) (Eq xp xx)) % 76.74/76.92 Clause #16298 (by clausification #[16297]): Or (Eq (sdtlseqdt0 xp xx) False) (Eq xp xx) % 76.74/76.92 Clause #16299 (by forward contextual literal cutting #[16298, 187]): Eq (sdtlseqdt0 xp xx) False % 76.74/76.92 Clause #16300 (by superposition #[16299, 2165]): Eq False True % 76.74/76.92 Clause #16301 (by clausification #[16300]): False % 76.74/76.92 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------