%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM849+2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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:57:26 PM UTC 2025 % Result : Theorem 18.18s 18.33s % Output : Proof 18.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : NUM849+2 : TPTP v9.2.0. Released v4.1.0. % 0.08/0.15 % Command : duper %s % 0.15/0.37 % Computer : n004.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:45:38 EDT 2025 % 0.15/0.37 % CPUTime : % 18.18/18.33 SZS status Theorem for theBenchmark.p % 18.18/18.33 SZS output start Proof for theBenchmark.p % 18.18/18.33 Clause #0 (by assumption #[]): Eq % 18.18/18.33 (Not % 18.18/18.33 (∀ (Vd454 : Iota), % 18.18/18.33 Eq (vmul (vmul vd448 vd449) Vd454) (vmul vd448 (vmul vd449 Vd454)) → % 18.18/18.33 Eq (vmul (vmul vd448 vd449) (vsucc Vd454)) (vmul vd448 (vmul vd449 (vsucc Vd454))))) % 18.18/18.33 True % 18.18/18.33 Clause #2 (by assumption #[]): Eq % 18.18/18.33 (∀ (Vd451 : Iota), % 18.18/18.33 Eq (vmul (vmul vd448 vd449) Vd451) (vmul vd448 (vmul vd449 Vd451)) → % 18.18/18.33 Eq (vplus (vmul vd448 (vmul vd449 Vd451)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 Vd451) vd449))) % 18.18/18.33 True % 18.18/18.33 Clause #7 (by assumption #[]): Eq (∀ (Vd418 Vd419 : Iota), Eq (vmul Vd418 Vd419) (vmul Vd419 Vd418)) True % 18.18/18.33 Clause #8 (by assumption #[]): Eq (∀ (Vd408 Vd409 : Iota), Eq (vmul (vsucc Vd408) Vd409) (vplus (vmul Vd408 Vd409) Vd409)) True % 18.18/18.33 Clause #15 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (Vd419 : Iota), Eq (vmul a Vd419) (vmul Vd419 a)) True % 18.18/18.33 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Eq (Eq (vmul a a_1) (vmul a_1 a)) True % 18.18/18.33 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Eq (vmul a a_1) (vmul a_1 a) % 18.18/18.33 Clause #20 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (Vd409 : Iota), Eq (vmul (vsucc a) Vd409) (vplus (vmul a Vd409) Vd409)) True % 18.18/18.33 Clause #21 (by clausification #[20]): ∀ (a a_1 : Iota), Eq (Eq (vmul (vsucc a) a_1) (vplus (vmul a a_1) a_1)) True % 18.18/18.33 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), Eq (vmul (vsucc a) a_1) (vplus (vmul a a_1) a_1) % 18.18/18.33 Clause #26 (by superposition #[22, 17]): ∀ (a a_1 : Iota), Eq (vmul (vsucc a) a_1) (vplus (vmul a_1 a) a_1) % 18.18/18.33 Clause #30 (by clausification #[0]): Eq % 18.18/18.33 (∀ (Vd454 : Iota), % 18.18/18.33 Eq (vmul (vmul vd448 vd449) Vd454) (vmul vd448 (vmul vd449 Vd454)) → % 18.18/18.33 Eq (vmul (vmul vd448 vd449) (vsucc Vd454)) (vmul vd448 (vmul vd449 (vsucc Vd454)))) % 18.18/18.33 False % 18.18/18.33 Clause #31 (by clausification #[30]): ∀ (a : Iota), % 18.18/18.33 Eq % 18.18/18.33 (Not % 18.18/18.33 (Eq (vmul (vmul vd448 vd449) (skS.0 0 a)) (vmul vd448 (vmul vd449 (skS.0 0 a))) → % 18.18/18.33 Eq (vmul (vmul vd448 vd449) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a)))))) % 18.18/18.33 True % 18.18/18.33 Clause #32 (by clausification #[31]): ∀ (a : Iota), % 18.18/18.33 Eq % 18.18/18.33 (Eq (vmul (vmul vd448 vd449) (skS.0 0 a)) (vmul vd448 (vmul vd449 (skS.0 0 a))) → % 18.18/18.33 Eq (vmul (vmul vd448 vd449) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a))))) % 18.18/18.33 False % 18.18/18.33 Clause #33 (by clausification #[32]): ∀ (a : Iota), Eq (Eq (vmul (vmul vd448 vd449) (skS.0 0 a)) (vmul vd448 (vmul vd449 (skS.0 0 a)))) True % 18.18/18.33 Clause #34 (by clausification #[32]): ∀ (a : Iota), Eq (Eq (vmul (vmul vd448 vd449) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a))))) False % 18.18/18.33 Clause #35 (by clausification #[33]): ∀ (a : Iota), Eq (vmul (vmul vd448 vd449) (skS.0 0 a)) (vmul vd448 (vmul vd449 (skS.0 0 a))) % 18.18/18.33 Clause #36 (by forward demodulation #[35, 17]): ∀ (a : Iota), Eq (vmul (vmul vd449 vd448) (skS.0 0 a)) (vmul vd448 (vmul vd449 (skS.0 0 a))) % 18.18/18.33 Clause #38 (by superposition #[36, 26]): ∀ (a : Iota), % 18.18/18.33 Eq (vmul (vsucc (skS.0 0 a)) (vmul vd449 vd448)) (vplus (vmul vd448 (vmul vd449 (skS.0 0 a))) (vmul vd449 vd448)) % 18.18/18.33 Clause #61 (by clausification #[2]): ∀ (a : Iota), % 18.18/18.33 Eq % 18.18/18.33 (Eq (vmul (vmul vd448 vd449) a) (vmul vd448 (vmul vd449 a)) → % 18.18/18.33 Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 a) vd449))) % 18.18/18.33 True % 18.18/18.33 Clause #62 (by clausification #[61]): ∀ (a : Iota), % 18.18/18.33 Or (Eq (Eq (vmul (vmul vd448 vd449) a) (vmul vd448 (vmul vd449 a))) False) % 18.18/18.33 (Eq (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 a) vd449))) True) % 18.18/18.33 Clause #63 (by clausification #[62]): ∀ (a : Iota), % 18.18/18.33 Or (Eq (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 a) vd449))) True) % 18.18/18.33 (Ne (vmul (vmul vd448 vd449) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.33 Clause #64 (by clausification #[63]): ∀ (a : Iota), % 18.18/18.33 Or (Ne (vmul (vmul vd448 vd449) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.33 (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 a) vd449))) % 18.18/18.33 Clause #65 (by forward demodulation #[64, 17]): ∀ (a : Iota), % 18.18/18.36 Or (Ne (vmul (vmul vd449 vd448) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.36 (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd448 vd449)) (vmul vd448 (vplus (vmul vd449 a) vd449))) % 18.18/18.36 Clause #66 (by forward demodulation #[65, 17]): ∀ (a : Iota), % 18.18/18.36 Or (Ne (vmul (vmul vd449 vd448) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.36 (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd449 vd448)) (vmul vd448 (vplus (vmul vd449 a) vd449))) % 18.18/18.36 Clause #67 (by forward demodulation #[66, 26]): ∀ (a : Iota), % 18.18/18.36 Or (Ne (vmul (vmul vd449 vd448) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.36 (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd449 vd448)) (vmul vd448 (vmul (vsucc a) vd449))) % 18.18/18.36 Clause #68 (by forward demodulation #[67, 17]): ∀ (a : Iota), % 18.18/18.36 Or (Ne (vmul (vmul vd449 vd448) a) (vmul vd448 (vmul vd449 a))) % 18.18/18.36 (Eq (vplus (vmul vd448 (vmul vd449 a)) (vmul vd449 vd448)) (vmul vd448 (vmul vd449 (vsucc a)))) % 18.18/18.36 Clause #69 (by superposition #[68, 36]): ∀ (a : Iota), % 18.18/18.36 Or (Ne (vmul vd448 (vmul vd449 (skS.0 0 a))) (vmul vd448 (vmul vd449 (skS.0 0 a)))) % 18.18/18.36 (Eq (vplus (vmul vd448 (vmul vd449 (skS.0 0 a))) (vmul vd449 vd448)) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a))))) % 18.18/18.36 Clause #218 (by clausification #[34]): ∀ (a : Iota), Ne (vmul (vmul vd448 vd449) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a)))) % 18.18/18.36 Clause #219 (by forward demodulation #[218, 17]): ∀ (a : Iota), Ne (vmul (vmul vd449 vd448) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a)))) % 18.18/18.36 Clause #239 (by forward demodulation #[38, 17]): ∀ (a : Iota), % 18.18/18.36 Eq (vmul (vmul vd449 vd448) (vsucc (skS.0 0 a))) (vplus (vmul vd448 (vmul vd449 (skS.0 0 a))) (vmul vd449 vd448)) % 18.18/18.36 Clause #265 (by eliminate resolved literals #[69]): ∀ (a : Iota), % 18.18/18.36 Eq (vplus (vmul vd448 (vmul vd449 (skS.0 0 a))) (vmul vd449 vd448)) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a)))) % 18.18/18.36 Clause #266 (by superposition #[265, 239]): ∀ (a : Iota), Eq (vmul (vmul vd449 vd448) (vsucc (skS.0 0 a))) (vmul vd448 (vmul vd449 (vsucc (skS.0 0 a)))) % 18.18/18.36 Clause #5082 (by forward contextual literal cutting #[266, 219]): False % 18.18/18.36 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------