%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW490_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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 8.18s 8.40s % Output : Proof 8.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.14 % Problem : SWW490_5 : TPTP v9.2.0. Released v6.0.0. % 0.12/0.15 % Command : duper %s % 0.15/0.37 % Computer : n020.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.38 % CPULimit : 300 % 0.15/0.38 % WCLimit : 300 % 0.15/0.38 % DateTime : Thu Oct 2 11:08:23 EDT 2025 % 0.15/0.38 % CPUTime : % 8.18/8.40 SZS status Theorem for theBenchmark.p % 8.18/8.40 SZS output start Proof for theBenchmark.p % 8.18/8.40 Clause #0 (by assumption #[]): Eq % 8.18/8.40 (∀ (A : Type), % 8.18/8.40 comm_semiring_0 A → ∀ (H : A), Eq (fundam296178794t_poly A (zero_zero (poly A)) H) (zero_zero (poly A))) % 8.18/8.40 True % 8.18/8.40 Clause #9 (by assumption #[]): Eq (∀ (A : Type), zero A → Eq (degree A (zero_zero (poly A))) (zero_zero nat)) True % 8.18/8.40 Clause #97 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_0 A → zero A) True % 8.18/8.40 Clause #129 (by assumption #[]): Eq (Not (Eq (degree a (fundam296178794t_poly a (zero_zero (poly a)) h)) (degree a (zero_zero (poly a))))) True % 8.18/8.40 Clause #130 (by assumption #[]): Eq (comm_semiring_0 a) True % 8.18/8.40 Clause #131 (by clausification #[0]): ∀ (a : Type), % 8.18/8.40 Eq (comm_semiring_0 a → ∀ (H : a), Eq (fundam296178794t_poly a (zero_zero (poly a)) H) (zero_zero (poly a))) True % 8.18/8.40 Clause #132 (by clausification #[131]): ∀ (a : Type), % 8.18/8.40 Or (Eq (comm_semiring_0 a) False) % 8.18/8.40 (Eq (∀ (H : a), Eq (fundam296178794t_poly a (zero_zero (poly a)) H) (zero_zero (poly a))) True) % 8.18/8.40 Clause #133 (by clausification #[132]): ∀ (a : Type) (a_1 : a), % 8.18/8.40 Or (Eq (comm_semiring_0 a) False) % 8.18/8.40 (Eq (Eq (fundam296178794t_poly a (zero_zero (poly a)) a_1) (zero_zero (poly a))) True) % 8.18/8.40 Clause #134 (by clausification #[133]): ∀ (a : Type) (a_1 : a), % 8.18/8.40 Or (Eq (comm_semiring_0 a) False) (Eq (fundam296178794t_poly a (zero_zero (poly a)) a_1) (zero_zero (poly a))) % 8.18/8.40 Clause #135 (by superposition #[134, 130]): ∀ (a_1 : a), Or (Eq (fundam296178794t_poly a (zero_zero (poly a)) a_1) (zero_zero (poly a))) (Eq False True) % 8.18/8.40 Clause #146 (by clausification #[97]): ∀ (a : Type), Eq (comm_semiring_0 a → zero a) True % 8.18/8.40 Clause #147 (by clausification #[146]): ∀ (a : Type), Or (Eq (comm_semiring_0 a) False) (Eq (zero a) True) % 8.18/8.40 Clause #148 (by superposition #[147, 130]): Or (Eq (zero a) True) (Eq False True) % 8.18/8.40 Clause #157 (by clausification #[148]): Eq (zero a) True % 8.18/8.40 Clause #291 (by clausification #[9]): ∀ (a : Type), Eq (zero a → Eq (degree a (zero_zero (poly a))) (zero_zero nat)) True % 8.18/8.40 Clause #292 (by clausification #[291]): ∀ (a : Type), Or (Eq (zero a) False) (Eq (Eq (degree a (zero_zero (poly a))) (zero_zero nat)) True) % 8.18/8.40 Clause #293 (by clausification #[292]): ∀ (a : Type), Or (Eq (zero a) False) (Eq (degree a (zero_zero (poly a))) (zero_zero nat)) % 8.18/8.40 Clause #295 (by superposition #[293, 157]): Or (Eq (degree a (zero_zero (poly a))) (zero_zero nat)) (Eq False True) % 8.18/8.40 Clause #574 (by clausification #[295]): Eq (degree a (zero_zero (poly a))) (zero_zero nat) % 8.18/8.40 Clause #3394 (by clausification #[129]): Eq (Eq (degree a (fundam296178794t_poly a (zero_zero (poly a)) h)) (degree a (zero_zero (poly a)))) False % 8.18/8.40 Clause #3395 (by clausification #[3394]): Ne (degree a (fundam296178794t_poly a (zero_zero (poly a)) h)) (degree a (zero_zero (poly a))) % 8.18/8.40 Clause #3396 (by forward demodulation #[3395, 574]): Ne (degree a (fundam296178794t_poly a (zero_zero (poly a)) h)) (zero_zero nat) % 8.18/8.40 Clause #3527 (by clausification #[135]): ∀ (a_1 : a), Eq (fundam296178794t_poly a (zero_zero (poly a)) a_1) (zero_zero (poly a)) % 8.18/8.40 Clause #3528 (by backward demodulation #[3527, 3396]): Ne (degree a (zero_zero (poly a))) (zero_zero nat) % 8.18/8.40 Clause #3531 (by forward demodulation #[3528, 574]): Ne (zero_zero nat) (zero_zero nat) % 8.18/8.40 Clause #3532 (by eliminate resolved literals #[3531]): False % 8.18/8.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------