%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM576+3 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:46 PM UTC 2025 % Result : Theorem 29.36s 29.58s % Output : Proof 29.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM576+3 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.13 % Command : duper %s % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 07:29:38 EDT 2025 % 0.12/0.34 % CPUTime : % 29.36/29.58 SZS status Theorem for theBenchmark.p % 29.36/29.58 SZS output start Proof for theBenchmark.p % 29.36/29.58 Clause #34 (by assumption #[]): Eq % 29.36/29.58 (∀ (W0 W1 : Iota), % 29.36/29.58 And (aElementOf0 W0 szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 W0 W1) (sdtlseqdt0 W1 W0) → Eq W0 W1) % 29.36/29.58 True % 29.36/29.58 Clause #36 (by assumption #[]): Eq % 29.36/29.58 (∀ (W0 W1 : Iota), % 29.36/29.58 And (aElementOf0 W0 szNzAzT0) (aElementOf0 W1 szNzAzT0) → Or (sdtlseqdt0 W0 W1) (sdtlseqdt0 (szszuzczcdt0 W1) W0)) % 29.36/29.58 True % 29.36/29.58 Clause #82 (by assumption #[]): Eq (And (aElementOf0 xi szNzAzT0) (aElementOf0 xj szNzAzT0)) True % 29.36/29.58 Clause #83 (by assumption #[]): Eq (Not (Ne xi xj → Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj))) True % 29.36/29.58 Clause #221 (by clausification #[82]): Eq (aElementOf0 xj szNzAzT0) True % 29.36/29.58 Clause #222 (by clausification #[82]): Eq (aElementOf0 xi szNzAzT0) True % 29.36/29.58 Clause #509 (by clausification #[34]): ∀ (a : Iota), % 29.36/29.58 Eq % 29.36/29.58 (∀ (W1 : Iota), % 29.36/29.58 And (aElementOf0 a szNzAzT0) (aElementOf0 W1 szNzAzT0) → And (sdtlseqdt0 a W1) (sdtlseqdt0 W1 a) → Eq a W1) % 29.36/29.58 True % 29.36/29.58 Clause #510 (by clausification #[509]): ∀ (a a_1 : Iota), % 29.36/29.58 Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0) → And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) % 29.36/29.58 True % 29.36/29.58 Clause #511 (by clausification #[510]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0)) False) % 29.36/29.58 (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 29.36/29.58 Clause #512 (by clausification #[511]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a) → Eq a a_1) True) % 29.36/29.58 (Or (Eq (aElementOf0 a szNzAzT0) False) (Eq (aElementOf0 a_1 szNzAzT0) False)) % 29.36/29.58 Clause #513 (by clausification #[512]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 29.36/29.58 (Or (Eq (And (sdtlseqdt0 a a_1) (sdtlseqdt0 a_1 a)) False) (Eq (Eq a a_1) True))) % 29.36/29.58 Clause #514 (by clausification #[513]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 29.36/29.58 (Or (Eq (Eq a a_1) True) (Or (Eq (sdtlseqdt0 a a_1) False) (Eq (sdtlseqdt0 a_1 a) False)))) % 29.36/29.58 Clause #515 (by clausification #[514]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 29.36/29.58 (Or (Eq (sdtlseqdt0 a a_1) False) (Or (Eq (sdtlseqdt0 a_1 a) False) (Eq a a_1)))) % 29.36/29.58 Clause #518 (by superposition #[515, 221]): ∀ (a : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (sdtlseqdt0 xj a) False) (Or (Eq (sdtlseqdt0 a xj) False) (Or (Eq xj a) (Eq False True)))) % 29.36/29.58 Clause #547 (by clausification #[36]): ∀ (a : Iota), % 29.36/29.58 Eq % 29.36/29.58 (∀ (W1 : Iota), % 29.36/29.58 And (aElementOf0 a szNzAzT0) (aElementOf0 W1 szNzAzT0) → Or (sdtlseqdt0 a W1) (sdtlseqdt0 (szszuzczcdt0 W1) a)) % 29.36/29.58 True % 29.36/29.58 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), % 29.36/29.58 Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0) → Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) % 29.36/29.58 True % 29.36/29.58 Clause #549 (by clausification #[548]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (And (aElementOf0 a szNzAzT0) (aElementOf0 a_1 szNzAzT0)) False) % 29.36/29.58 (Eq (Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) True) % 29.36/29.58 Clause #550 (by clausification #[549]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (Or (sdtlseqdt0 a a_1) (sdtlseqdt0 (szszuzczcdt0 a_1) a)) True) % 29.36/29.58 (Or (Eq (aElementOf0 a szNzAzT0) False) (Eq (aElementOf0 a_1 szNzAzT0) False)) % 29.36/29.58 Clause #551 (by clausification #[550]): ∀ (a a_1 : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (aElementOf0 a_1 szNzAzT0) False) % 29.36/29.58 (Or (Eq (sdtlseqdt0 a a_1) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a_1) a) True))) % 29.36/29.58 Clause #554 (by superposition #[551, 221]): ∀ (a : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (sdtlseqdt0 xj a) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 a) xj) True) (Eq False True))) % 29.36/29.58 Clause #555 (by superposition #[551, 222]): ∀ (a : Iota), % 29.36/29.58 Or (Eq (aElementOf0 a szNzAzT0) False) % 29.36/29.58 (Or (Eq (sdtlseqdt0 xi a) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 a) xi) True) (Eq False True))) % 29.36/29.58 Clause #1488 (by clausification #[83]): Eq (Ne xi xj → Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj)) False % 29.43/29.62 Clause #1489 (by clausification #[1488]): Eq (Ne xi xj) True % 29.43/29.62 Clause #1490 (by clausification #[1488]): Eq (Or (sdtlseqdt0 (szszuzczcdt0 xj) xi) (sdtlseqdt0 (szszuzczcdt0 xi) xj)) False % 29.43/29.62 Clause #1491 (by clausification #[1489]): Ne xi xj % 29.43/29.62 Clause #1666 (by clausification #[1490]): Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) False % 29.43/29.62 Clause #1667 (by clausification #[1490]): Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) False % 29.43/29.62 Clause #4114 (by clausification #[518]): ∀ (a : Iota), % 29.43/29.62 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xj a) False) (Or (Eq (sdtlseqdt0 a xj) False) (Eq xj a))) % 29.43/29.62 Clause #4118 (by superposition #[4114, 222]): Or (Eq (sdtlseqdt0 xj xi) False) (Or (Eq (sdtlseqdt0 xi xj) False) (Or (Eq xj xi) (Eq False True))) % 29.43/29.62 Clause #4151 (by clausification #[4118]): Or (Eq (sdtlseqdt0 xj xi) False) (Or (Eq (sdtlseqdt0 xi xj) False) (Eq xj xi)) % 29.43/29.62 Clause #4152 (by forward contextual literal cutting #[4151, 1491]): Or (Eq (sdtlseqdt0 xj xi) False) (Eq (sdtlseqdt0 xi xj) False) % 29.43/29.62 Clause #4760 (by clausification #[554]): ∀ (a : Iota), % 29.43/29.62 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xj a) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a) xj) True)) % 29.43/29.62 Clause #4764 (by superposition #[4760, 222]): Or (Eq (sdtlseqdt0 xj xi) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) True) (Eq False True)) % 29.43/29.62 Clause #4804 (by clausification #[555]): ∀ (a : Iota), % 29.43/29.62 Or (Eq (aElementOf0 a szNzAzT0) False) (Or (Eq (sdtlseqdt0 xi a) True) (Eq (sdtlseqdt0 (szszuzczcdt0 a) xi) True)) % 29.43/29.62 Clause #4807 (by superposition #[4804, 221]): Or (Eq (sdtlseqdt0 xi xj) True) (Or (Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) True) (Eq False True)) % 29.43/29.62 Clause #5090 (by clausification #[4807]): Or (Eq (sdtlseqdt0 xi xj) True) (Eq (sdtlseqdt0 (szszuzczcdt0 xj) xi) True) % 29.43/29.62 Clause #5091 (by superposition #[5090, 1667]): Or (Eq (sdtlseqdt0 xi xj) True) (Eq True False) % 29.43/29.62 Clause #5094 (by clausification #[5091]): Eq (sdtlseqdt0 xi xj) True % 29.43/29.62 Clause #5240 (by clausification #[4764]): Or (Eq (sdtlseqdt0 xj xi) True) (Eq (sdtlseqdt0 (szszuzczcdt0 xi) xj) True) % 29.43/29.62 Clause #5241 (by superposition #[5240, 1666]): Or (Eq (sdtlseqdt0 xj xi) True) (Eq True False) % 29.43/29.62 Clause #5248 (by clausification #[5241]): Eq (sdtlseqdt0 xj xi) True % 29.43/29.62 Clause #5250 (by backward demodulation #[5248, 4152]): Or (Eq True False) (Eq (sdtlseqdt0 xi xj) False) % 29.43/29.62 Clause #5252 (by clausification #[5250]): Eq (sdtlseqdt0 xi xj) False % 29.43/29.62 Clause #5253 (by superposition #[5252, 5094]): Eq False True % 29.43/29.62 Clause #5254 (by clausification #[5253]): False % 29.43/29.62 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------