%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM576+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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:45 PM UTC 2025 % Result : Theorem 31.49s 31.66s % Output : Proof 31.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM576+1 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n009.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:14:53 EDT 2025 % 0.13/0.34 % CPUTime : % 31.49/31.66 SZS status Theorem for theBenchmark.p % 31.49/31.66 SZS output start Proof for theBenchmark.p % 31.49/31.66 Clause #34 (by assumption #[]): Eq % 31.49/31.66 (∀ (W0 W1 : Iota), % 31.49/31.66 And (aElementOf0 W0 szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 W0 W1) (sdtlseqdt0 W1 W0) → Eq W0 W1) % 31.49/31.66 True % 31.49/31.66 Clause #36 (by assumption #[]): Eq % 31.49/31.66 (∀ (W0 W1 : Iota), % 31.49/31.66 And (aElementOf0 W0 szNzAzT0) (aElementOf0 W1 szNzAzT0) → Or (sdtlseqdt0 W0 W1) (sdtlseqdt0 (szszuzczcdt0 W1) W0)) % 31.49/31.66 True % 31.49/31.66 Clause #82 (by assumption #[]): Eq (And (aElementOf0 xi szNzAzT0) (aElementOf0 xj szNzAzT0)) True % 31.49/31.66 Clause #83 (by assumption #[]): Eq (Not (Ne xi xj → Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj))) True % 31.49/31.66 Clause #243 (by clausification #[82]): Eq (aElementOf0 xj szNzAzT0) True % 31.49/31.66 Clause #244 (by clausification #[82]): Eq (aElementOf0 xi szNzAzT0) True % 31.49/31.66 Clause #408 (by clausification #[34]): ∀ (a : Iota), % 31.49/31.66 Eq % 31.49/31.66 (∀ (W1 : Iota), % 31.49/31.66 And (aElementOf0 a szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 a W1) (sdtlseqdt0 W1 a) → Eq a W1) % 31.49/31.66 True % 31.49/31.66 Clause #409 (by clausification #[408]): ∀ (a a_1 : Iota), % 31.49/31.66 Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0) → And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) % 31.49/31.66 True % 31.49/31.66 Clause #410 (by clausification #[409]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0)) False) % 31.49/31.66 (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 31.49/31.66 Clause #411 (by clausification #[410]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 31.49/31.66 (Or (Eq (aElementOf0 a szNzAzT0) False) (Eq (aElementOf0 a_1 szNzAzT0) False)) % 31.49/31.66 Clause #412 (by clausification #[411]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 31.49/31.66 (Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a)) False) (Eq (Eq a a_1) True))) % 31.49/31.66 Clause #413 (by clausification #[412]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 31.49/31.66 (Or (Eq (Eq a a_1) True) (Or (Eq (sdtlseqdt0 a a_1) False) (Eq (sdtlseqdt0 a_1 a) False)))) % 31.49/31.66 Clause #414 (by clausification #[413]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 31.49/31.66 (Or (Eq (sdtlseqdt0 a a_1) False) (Or (Eq (sdtlseqdt0 a_1 a) False) (Eq a a_1)))) % 31.49/31.66 Clause #418 (by superposition #[414, 244]): ∀ (a : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (sdtlseqdt0 xi a) False) (Or (Eq (sdtlseqdt0 a xi) False) (Or (Eq xi a) (Eq False True)))) % 31.49/31.66 Clause #536 (by clausification #[36]): ∀ (a : Iota), % 31.49/31.66 Eq % 31.49/31.66 (∀ (W1 : Iota), % 31.49/31.66 And (aElementOf0 a szNzAzT0) (aElementOf0 W1 szNzAzT0) → Or (sdtlseqdt0 a W1) (sdtlseqdt0 (szszuzczcdt0 W1) a)) % 31.49/31.66 True % 31.49/31.66 Clause #537 (by clausification #[536]): ∀ (a a_1 : Iota), % 31.49/31.66 Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0) → Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) % 31.49/31.66 True % 31.49/31.66 Clause #538 (by clausification #[537]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0)) False) % 31.49/31.66 (Eq (Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) True) % 31.49/31.66 Clause #539 (by clausification #[538]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) True) % 31.49/31.66 (Or (Eq (aElementOf0 a szNzAzT0) False) (Eq (aElementOf0 a_1 szNzAzT0) False)) % 31.49/31.66 Clause #540 (by clausification #[539]): ∀ (a a_1 : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 31.49/31.66 (Or (Eq (sdtlseqdt0 a a_1) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a_1) a) True))) % 31.49/31.66 Clause #543 (by superposition #[540, 243]): ∀ (a : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (sdtlseqdt0 xj a) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 a) xj) True) (Eq False True))) % 31.49/31.66 Clause #544 (by superposition #[540, 244]): ∀ (a : Iota), % 31.49/31.66 Or (Eq (aElementOf0 a szNzAzT0) False) % 31.49/31.66 (Or (Eq (sdtlseqdt0 xi a) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 a) xi) True) (Eq False True))) % 31.49/31.66 Clause #1482 (by clausification #[83]): Eq (Ne xi xj → Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj)) False % 31.53/31.70 Clause #1483 (by clausification #[1482]): Eq (Ne xi xj) True % 31.53/31.70 Clause #1484 (by clausification #[1482]): Eq (Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj)) False % 31.53/31.70 Clause #1485 (by clausification #[1483]): Ne xi xj % 31.53/31.70 Clause #1634 (by clausification #[1484]): Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) False % 31.53/31.70 Clause #1635 (by clausification #[1484]): Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) False % 31.53/31.70 Clause #3620 (by clausification #[418]): ∀ (a : Iota), % 31.53/31.70 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xi a) False) (Or (Eq (sdtlseqdt0 a xi) False) (Eq xi a))) % 31.53/31.70 Clause #3623 (by superposition #[3620, 243]): Or (Eq (sdtlseqdt0 xi xj) False) (Or (Eq (sdtlseqdt0 xj xi) False) (Or (Eq xi xj) (Eq False True))) % 31.53/31.70 Clause #6225 (by clausification #[543]): ∀ (a : Iota), % 31.53/31.70 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xj a) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a) xj) True)) % 31.53/31.70 Clause #6229 (by superposition #[6225, 244]): Or (Eq (sdtlseqdt0 xj xi) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) True) (Eq False True)) % 31.53/31.70 Clause #6262 (by clausification #[544]): ∀ (a : Iota), % 31.53/31.70 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xi a) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a) xi) True)) % 31.53/31.70 Clause #6265 (by superposition #[6262, 243]): Or (Eq (sdtlseqdt0 xi xj) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) True) (Eq False True)) % 31.53/31.70 Clause #6303 (by clausification #[6229]): Or (Eq (sdtlseqdt0 xj xi) True) (Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) True) % 31.53/31.70 Clause #6304 (by superposition #[6303, 1634]): Or (Eq (sdtlseqdt0 xj xi) True) (Eq True False) % 31.53/31.70 Clause #6337 (by clausification #[6304]): Eq (sdtlseqdt0 xj xi) True % 31.53/31.70 Clause #6376 (by clausification #[6265]): Or (Eq (sdtlseqdt0 xi xj) True) (Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) True) % 31.53/31.70 Clause #6377 (by superposition #[6376, 1635]): Or (Eq (sdtlseqdt0 xi xj) True) (Eq True False) % 31.53/31.70 Clause #6378 (by clausification #[6377]): Eq (sdtlseqdt0 xi xj) True % 31.53/31.70 Clause #6909 (by clausification #[3623]): Or (Eq (sdtlseqdt0 xi xj) False) (Or (Eq (sdtlseqdt0 xj xi) False) (Eq xi xj)) % 31.53/31.70 Clause #6910 (by forward demodulation #[6909, 6337]): Or (Eq (sdtlseqdt0 xi xj) False) (Or (Eq True False) (Eq xi xj)) % 31.53/31.70 Clause #6911 (by clausification #[6910]): Or (Eq (sdtlseqdt0 xi xj) False) (Eq xi xj) % 31.53/31.70 Clause #6912 (by forward contextual literal cutting #[6911, 1485]): Eq (sdtlseqdt0 xi xj) False % 31.53/31.70 Clause #6913 (by superposition #[6912, 6378]): Eq False True % 31.53/31.70 Clause #6914 (by clausification #[6913]): False % 31.53/31.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------