%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWV617_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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:05:26 PM UTC 2025 % Result : Theorem 9.98s 10.15s % Output : Proof 9.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.11 % Problem : SWV617_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.13 % Command : duper %s % 0.12/0.34 % Computer : n010.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 : Thu Oct 2 12:33:23 EDT 2025 % 0.12/0.34 % CPUTime : % 9.98/10.15 SZS status Theorem for theBenchmark.p % 9.98/10.15 SZS output start Proof for theBenchmark.p % 9.98/10.15 Clause #3 (by assumption #[]): Eq (∀ (N : nat), Eq (power_power complex (fFT_Mirabelle_root N) N) (one_one complex)) True % 9.98/10.15 Clause #5 (by assumption #[]): Eq (∀ (A : Type), monoid_mult A → ∀ (N : nat), Eq (power_power A (one_one A) N) (one_one A)) True % 9.98/10.15 Clause #6 (by assumption #[]): Eq (∀ (A : Type), division_ring A → ∀ (A1 : A), Eq (inverse_divide A (zero_zero A) A1) (zero_zero A)) True % 9.98/10.15 Clause #9 (by assumption #[]): Eq (∀ (A : Type), group_add A → ∀ (A1 : A), Eq (minus_minus A A1 A1) (zero_zero A)) True % 9.98/10.15 Clause #110 (by assumption #[]): Eq (division_ring complex) True % 9.98/10.15 Clause #112 (by assumption #[]): Eq (monoid_mult complex) True % 9.98/10.15 Clause #114 (by assumption #[]): Eq (group_add complex) True % 9.98/10.15 Clause #122 (by assumption #[]): Eq % 9.98/10.15 (Not % 9.98/10.15 (Eq % 9.98/10.15 (inverse_divide complex % 9.98/10.15 (minus_minus complex (power_power complex (power_power complex (fFT_Mirabelle_root n) n) k) (one_one complex)) % 9.98/10.15 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.15 (zero_zero complex))) % 9.98/10.15 True % 9.98/10.15 Clause #126 (by clausification #[3]): ∀ (a : nat), Eq (Eq (power_power complex (fFT_Mirabelle_root a) a) (one_one complex)) True % 9.98/10.15 Clause #127 (by clausification #[126]): ∀ (a : nat), Eq (power_power complex (fFT_Mirabelle_root a) a) (one_one complex) % 9.98/10.15 Clause #140 (by clausification #[5]): ∀ (a : Type), Eq (monoid_mult a → ∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True % 9.98/10.15 Clause #141 (by clausification #[140]): ∀ (a : Type), Or (Eq (monoid_mult a) False) (Eq (∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True) % 9.98/10.15 Clause #142 (by clausification #[141]): ∀ (a : Type) (a_1 : nat), Or (Eq (monoid_mult a) False) (Eq (Eq (power_power a (one_one a) a_1) (one_one a)) True) % 9.98/10.15 Clause #143 (by clausification #[142]): ∀ (a : Type) (a_1 : nat), Or (Eq (monoid_mult a) False) (Eq (power_power a (one_one a) a_1) (one_one a)) % 9.98/10.15 Clause #144 (by superposition #[143, 112]): ∀ (a : nat), Or (Eq (power_power complex (one_one complex) a) (one_one complex)) (Eq False True) % 9.98/10.15 Clause #164 (by clausification #[6]): ∀ (a : Type), Eq (division_ring a → ∀ (A1 : a), Eq (inverse_divide a (zero_zero a) A1) (zero_zero a)) True % 9.98/10.15 Clause #165 (by clausification #[164]): ∀ (a : Type), % 9.98/10.15 Or (Eq (division_ring a) False) (Eq (∀ (A1 : a), Eq (inverse_divide a (zero_zero a) A1) (zero_zero a)) True) % 9.98/10.15 Clause #166 (by clausification #[165]): ∀ (a : Type) (a_1 : a), % 9.98/10.15 Or (Eq (division_ring a) False) (Eq (Eq (inverse_divide a (zero_zero a) a_1) (zero_zero a)) True) % 9.98/10.15 Clause #167 (by clausification #[166]): ∀ (a : Type) (a_1 : a), Or (Eq (division_ring a) False) (Eq (inverse_divide a (zero_zero a) a_1) (zero_zero a)) % 9.98/10.15 Clause #168 (by superposition #[167, 110]): ∀ (a : complex), Or (Eq (inverse_divide complex (zero_zero complex) a) (zero_zero complex)) (Eq False True) % 9.98/10.15 Clause #177 (by clausification #[144]): ∀ (a : nat), Eq (power_power complex (one_one complex) a) (one_one complex) % 9.98/10.15 Clause #261 (by clausification #[168]): ∀ (a : complex), Eq (inverse_divide complex (zero_zero complex) a) (zero_zero complex) % 9.98/10.15 Clause #262 (by clausification #[9]): ∀ (a : Type), Eq (group_add a → ∀ (A1 : a), Eq (minus_minus a A1 A1) (zero_zero a)) True % 9.98/10.15 Clause #263 (by clausification #[262]): ∀ (a : Type), Or (Eq (group_add a) False) (Eq (∀ (A1 : a), Eq (minus_minus a A1 A1) (zero_zero a)) True) % 9.98/10.15 Clause #264 (by clausification #[263]): ∀ (a : Type) (a_1 : a), Or (Eq (group_add a) False) (Eq (Eq (minus_minus a a_1 a_1) (zero_zero a)) True) % 9.98/10.15 Clause #265 (by clausification #[264]): ∀ (a : Type) (a_1 : a), Or (Eq (group_add a) False) (Eq (minus_minus a a_1 a_1) (zero_zero a)) % 9.98/10.15 Clause #266 (by superposition #[265, 114]): ∀ (a : complex), Or (Eq (minus_minus complex a a) (zero_zero complex)) (Eq False True) % 9.98/10.15 Clause #267 (by clausification #[266]): ∀ (a : complex), Eq (minus_minus complex a a) (zero_zero complex) % 9.98/10.15 Clause #2391 (by clausification #[122]): Eq % 9.98/10.15 (Eq % 9.98/10.15 (inverse_divide complex % 9.98/10.15 (minus_minus complex (power_power complex (power_power complex (fFT_Mirabelle_root n) n) k) (one_one complex)) % 9.98/10.16 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.16 (zero_zero complex)) % 9.98/10.16 False % 9.98/10.16 Clause #2392 (by clausification #[2391]): Ne % 9.98/10.16 (inverse_divide complex % 9.98/10.16 (minus_minus complex (power_power complex (power_power complex (fFT_Mirabelle_root n) n) k) (one_one complex)) % 9.98/10.16 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.16 (zero_zero complex) % 9.98/10.16 Clause #2393 (by forward demodulation #[2392, 127]): Ne % 9.98/10.16 (inverse_divide complex (minus_minus complex (power_power complex (one_one complex) k) (one_one complex)) % 9.98/10.16 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.16 (zero_zero complex) % 9.98/10.16 Clause #2394 (by forward demodulation #[2393, 177]): Ne % 9.98/10.16 (inverse_divide complex (minus_minus complex (one_one complex) (one_one complex)) % 9.98/10.16 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.16 (zero_zero complex) % 9.98/10.16 Clause #2395 (by forward demodulation #[2394, 267]): Ne % 9.98/10.16 (inverse_divide complex (zero_zero complex) % 9.98/10.16 (minus_minus complex (power_power complex (fFT_Mirabelle_root n) k) (one_one complex))) % 9.98/10.16 (zero_zero complex) % 9.98/10.16 Clause #2396 (by forward demodulation #[2395, 261]): Ne (zero_zero complex) (zero_zero complex) % 9.98/10.16 Clause #2397 (by eliminate resolved literals #[2396]): False % 9.98/10.16 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------