%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM848+2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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 34.70s 34.87s % Output : Proof 34.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NUM848+2 : TPTP v9.2.0. Released v4.1.0. % 0.03/0.12 % Command : duper %s % 0.12/0.32 % Computer : n014.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Fri Oct 3 08:44:38 EDT 2025 % 0.12/0.33 % CPUTime : % 34.70/34.87 SZS status Theorem for theBenchmark.p % 34.70/34.87 SZS output start Proof for theBenchmark.p % 34.70/34.87 Clause #0 (by assumption #[]): Eq % 34.70/34.87 (Not % 34.70/34.87 (Eq (vplus (vmul vd436 vd437) (vplus (vmul vd436 vd439) vd436)) % 34.70/34.87 (vplus (vmul vd436 vd437) (vmul vd436 (vsucc vd439))))) % 34.70/34.87 True % 34.70/34.87 Clause #8 (by assumption #[]): Eq % 34.70/34.87 (∀ (Vd396 Vd397 : Iota), % 34.70/34.87 And (Eq (vmul Vd396 (vsucc Vd397)) (vplus (vmul Vd396 Vd397) Vd396)) (Eq (vmul Vd396 v1) Vd396)) % 34.70/34.87 True % 34.70/34.87 Clause #31 (by clausification #[0]): Eq % 34.70/34.87 (Eq (vplus (vmul vd436 vd437) (vplus (vmul vd436 vd439) vd436)) (vplus (vmul vd436 vd437) (vmul vd436 (vsucc vd439)))) % 34.70/34.87 False % 34.70/34.87 Clause #32 (by clausification #[31]): Ne (vplus (vmul vd436 vd437) (vplus (vmul vd436 vd439) vd436)) (vplus (vmul vd436 vd437) (vmul vd436 (vsucc vd439))) % 34.70/34.87 Clause #482 (by clausification #[8]): ∀ (a : Iota), Eq (∀ (Vd397 : Iota), And (Eq (vmul a (vsucc Vd397)) (vplus (vmul a Vd397) a)) (Eq (vmul a v1) a)) True % 34.70/34.87 Clause #483 (by clausification #[482]): ∀ (a a_1 : Iota), Eq (And (Eq (vmul a (vsucc a_1)) (vplus (vmul a a_1) a)) (Eq (vmul a v1) a)) True % 34.70/34.87 Clause #485 (by clausification #[483]): ∀ (a a_1 : Iota), Eq (Eq (vmul a (vsucc a_1)) (vplus (vmul a a_1) a)) True % 34.70/34.87 Clause #18449 (by clausification #[485]): ∀ (a a_1 : Iota), Eq (vmul a (vsucc a_1)) (vplus (vmul a a_1) a) % 34.70/34.87 Clause #18451 (by backward positive simplify reflect #[18449, 32]): False % 34.70/34.87 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------