%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW488_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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 08:06:21 PM UTC 2025 % Result : Theorem 9.07s 9.27s % Output : Proof 9.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW488_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n005.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 : Thu Oct 2 11:21:38 EDT 2025 % 0.13/0.34 % CPUTime : % 9.07/9.27 SZS status Theorem for theBenchmark.p % 9.07/9.27 SZS output start Proof for theBenchmark.p % 9.07/9.27 Clause #0 (by assumption #[]): Eq % 9.07/9.27 (∀ (A : Type), % 9.07/9.27 comm_semiring_0 A → ∀ (H : A), Eq (fundam296178794t_poly A (zero_zero (poly1 A)) H) (zero_zero (poly1 A))) % 9.07/9.27 True % 9.07/9.27 Clause #1 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_0 A → ∀ (X : A), Eq (aa A A (poly A (zero_zero (poly1 A))) X) (zero_zero A)) True % 9.07/9.27 Clause #140 (by assumption #[]): Eq % 9.07/9.27 (Not % 9.07/9.27 (Eq (aa a a (poly a (fundam296178794t_poly a (zero_zero (poly1 a)) h)) x) % 9.07/9.27 (aa a a (poly a (zero_zero (poly1 a))) (plus_plus a h x)))) % 9.07/9.27 True % 9.07/9.27 Clause #141 (by assumption #[]): Eq (comm_semiring_0 a) True % 9.07/9.27 Clause #142 (by clausification #[0]): ∀ (a : Type), % 9.07/9.27 Eq (comm_semiring_0 a → ∀ (H : a), Eq (fundam296178794t_poly a (zero_zero (poly1 a)) H) (zero_zero (poly1 a))) True % 9.07/9.27 Clause #143 (by clausification #[142]): ∀ (a : Type), % 9.07/9.27 Or (Eq (comm_semiring_0 a) False) % 9.07/9.27 (Eq (∀ (H : a), Eq (fundam296178794t_poly a (zero_zero (poly1 a)) H) (zero_zero (poly1 a))) True) % 9.07/9.27 Clause #144 (by clausification #[143]): ∀ (a : Type) (a_1 : a), % 9.07/9.27 Or (Eq (comm_semiring_0 a) False) % 9.07/9.27 (Eq (Eq (fundam296178794t_poly a (zero_zero (poly1 a)) a_1) (zero_zero (poly1 a))) True) % 9.07/9.27 Clause #145 (by clausification #[144]): ∀ (a : Type) (a_1 : a), % 9.07/9.27 Or (Eq (comm_semiring_0 a) False) (Eq (fundam296178794t_poly a (zero_zero (poly1 a)) a_1) (zero_zero (poly1 a))) % 9.07/9.27 Clause #146 (by superposition #[145, 141]): ∀ (a_1 : a), Or (Eq (fundam296178794t_poly a (zero_zero (poly1 a)) a_1) (zero_zero (poly1 a))) (Eq False True) % 9.07/9.27 Clause #148 (by clausification #[1]): ∀ (a : Type), Eq (comm_semiring_0 a → ∀ (X : a), Eq (aa a a (poly a (zero_zero (poly1 a))) X) (zero_zero a)) True % 9.07/9.27 Clause #149 (by clausification #[148]): ∀ (a : Type), % 9.07/9.27 Or (Eq (comm_semiring_0 a) False) (Eq (∀ (X : a), Eq (aa a a (poly a (zero_zero (poly1 a))) X) (zero_zero a)) True) % 9.07/9.27 Clause #150 (by clausification #[149]): ∀ (a : Type) (a_1 : a), % 9.07/9.27 Or (Eq (comm_semiring_0 a) False) (Eq (Eq (aa a a (poly a (zero_zero (poly1 a))) a_1) (zero_zero a)) True) % 9.07/9.27 Clause #151 (by clausification #[150]): ∀ (a : Type) (a_1 : a), Or (Eq (comm_semiring_0 a) False) (Eq (aa a a (poly a (zero_zero (poly1 a))) a_1) (zero_zero a)) % 9.07/9.27 Clause #152 (by superposition #[151, 141]): ∀ (a_1 : a), Or (Eq (aa a a (poly a (zero_zero (poly1 a))) a_1) (zero_zero a)) (Eq False True) % 9.07/9.27 Clause #1046 (by clausification #[146]): ∀ (a_1 : a), Eq (fundam296178794t_poly a (zero_zero (poly1 a)) a_1) (zero_zero (poly1 a)) % 9.07/9.27 Clause #1589 (by clausification #[152]): ∀ (a_1 : a), Eq (aa a a (poly a (zero_zero (poly1 a))) a_1) (zero_zero a) % 9.07/9.27 Clause #2029 (by clausification #[140]): Eq % 9.07/9.27 (Eq (aa a a (poly a (fundam296178794t_poly a (zero_zero (poly1 a)) h)) x) % 9.07/9.27 (aa a a (poly a (zero_zero (poly1 a))) (plus_plus a h x))) % 9.07/9.27 False % 9.07/9.27 Clause #2030 (by clausification #[2029]): Ne (aa a a (poly a (fundam296178794t_poly a (zero_zero (poly1 a)) h)) x) % 9.07/9.27 (aa a a (poly a (zero_zero (poly1 a))) (plus_plus a h x)) % 9.07/9.27 Clause #2031 (by forward demodulation #[2030, 1046]): Ne (aa a a (poly a (zero_zero (poly1 a))) x) (aa a a (poly a (zero_zero (poly1 a))) (plus_plus a h x)) % 9.07/9.27 Clause #2032 (by forward demodulation #[2031, 1589]): Ne (zero_zero a) (aa a a (poly a (zero_zero (poly1 a))) (plus_plus a h x)) % 9.07/9.27 Clause #2033 (by forward demodulation #[2032, 1589]): Ne (zero_zero a) (zero_zero a) % 9.07/9.27 Clause #2034 (by eliminate resolved literals #[2033]): False % 9.07/9.27 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------