%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SWW498_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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:22 PM UTC 2025 % Result : Theorem 102.61s 102.83s % Output : Proof 102.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW498_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n025.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 11:24:38 EDT 2025 % 0.13/0.35 % CPUTime : % 102.61/102.83 SZS status Theorem for theBenchmark.p % 102.61/102.83 SZS output start Proof for theBenchmark.p % 102.61/102.83 Clause #1 (by assumption #[]): Eq % 102.61/102.83 (ord_less_eq real % 102.61/102.83 (power_power real (abs_abs real (times_times real (number_number_of real (bit0 (bit1 pls))) x)) % 102.61/102.83 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real (one_one real) (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True % 102.61/102.83 Clause #11 (by assumption #[]): Eq % 102.61/102.83 (∀ (X : real), % 102.61/102.83 Eq % 102.61/102.83 (times_times real (number_number_of real (bit0 (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real X (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 (power_power real (times_times real (number_number_of real (bit0 (bit1 pls))) X) % 102.61/102.83 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True % 102.61/102.83 Clause #57 (by assumption #[]): Eq % 102.61/102.83 (∀ (A : Type), % 102.61/102.83 linordered_idom A → % 102.61/102.83 ∀ (A1 : A), % 102.61/102.83 Eq (power_power A (abs_abs A A1) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power A A1 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True % 102.61/102.83 Clause #77 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_1 A → ∀ (B A1 : A), Eq (times_times A A1 B) (times_times A B A1)) True % 102.61/102.83 Clause #92 (by assumption #[]): Eq (∀ (A : Type), monoid_mult A → ∀ (N : nat), Eq (power_power A (one_one A) N) (one_one A)) True % 102.61/102.83 Clause #107 (by assumption #[]): Eq (linordered_idom real) True % 102.61/102.83 Clause #108 (by assumption #[]): Eq (comm_semiring_1 real) True % 102.61/102.83 Clause #110 (by assumption #[]): Eq (monoid_mult real) True % 102.61/102.83 Clause #124 (by assumption #[]): Eq % 102.61/102.83 (Not % 102.61/102.83 (ord_less_eq real % 102.61/102.83 (times_times real (number_number_of real (bit0 (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real x (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 (one_one real))) % 102.61/102.83 True % 102.61/102.83 Clause #212 (by clausification #[11]): ∀ (a : real), % 102.61/102.83 Eq % 102.61/102.83 (Eq % 102.61/102.83 (times_times real (number_number_of real (bit0 (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real a (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 (power_power real (times_times real (number_number_of real (bit0 (bit1 pls))) a) % 102.61/102.83 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True % 102.61/102.83 Clause #213 (by clausification #[212]): ∀ (a : real), % 102.61/102.83 Eq % 102.61/102.83 (times_times real (number_number_of real (bit0 (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real a (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 (power_power real (times_times real (number_number_of real (bit0 (bit1 pls))) a) % 102.61/102.83 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 Clause #758 (by clausification #[57]): ∀ (a : Type), % 102.61/102.83 Eq % 102.61/102.83 (linordered_idom a → % 102.61/102.83 ∀ (A1 : a), % 102.61/102.83 Eq (power_power a (abs_abs a A1) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power a A1 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True % 102.61/102.83 Clause #759 (by clausification #[758]): ∀ (a : Type), % 102.61/102.83 Or (Eq (linordered_idom a) False) % 102.61/102.83 (Eq % 102.61/102.83 (∀ (A1 : a), % 102.61/102.83 Eq (power_power a (abs_abs a A1) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power a A1 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True) % 102.61/102.83 Clause #760 (by clausification #[759]): ∀ (a : Type) (a_1 : a), % 102.61/102.83 Or (Eq (linordered_idom a) False) % 102.61/102.83 (Eq % 102.61/102.83 (Eq (power_power a (abs_abs a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power a a_1 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 True) % 102.61/102.83 Clause #761 (by clausification #[760]): ∀ (a : Type) (a_1 : a), % 102.61/102.83 Or (Eq (linordered_idom a) False) % 102.61/102.83 (Eq (power_power a (abs_abs a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power a a_1 (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 Clause #762 (by superposition #[761, 107]): ∀ (a : real), % 102.61/102.83 Or % 102.61/102.83 (Eq (power_power real (abs_abs real a) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.83 (power_power real a (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.83 (Eq False True) % 102.61/102.83 Clause #1243 (by clausification #[77]): ∀ (a : Type), Eq (comm_semiring_1 a → ∀ (B A1 : a), Eq (times_times a A1 B) (times_times a B A1)) True % 102.61/102.83 Clause #1244 (by clausification #[1243]): ∀ (a : Type), Or (Eq (comm_semiring_1 a) False) (Eq (∀ (B A1 : a), Eq (times_times a A1 B) (times_times a B A1)) True) % 102.61/102.83 Clause #1245 (by clausification #[1244]): ∀ (a : Type) (a_1 : a), % 102.61/102.83 Or (Eq (comm_semiring_1 a) False) (Eq (∀ (A1 : a), Eq (times_times a A1 a_1) (times_times a a_1 A1)) True) % 102.61/102.89 Clause #1246 (by clausification #[1245]): ∀ (a : Type) (a_1 a_2 : a), % 102.61/102.89 Or (Eq (comm_semiring_1 a) False) (Eq (Eq (times_times a a_1 a_2) (times_times a a_2 a_1)) True) % 102.61/102.89 Clause #1247 (by clausification #[1246]): ∀ (a : Type) (a_1 a_2 : a), Or (Eq (comm_semiring_1 a) False) (Eq (times_times a a_1 a_2) (times_times a a_2 a_1)) % 102.61/102.89 Clause #1250 (by superposition #[1247, 108]): ∀ (a a_1 : real), Or (Eq (times_times real a a_1) (times_times real a_1 a)) (Eq False True) % 102.61/102.89 Clause #1427 (by clausification #[92]): ∀ (a : Type), Eq (monoid_mult a → ∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True % 102.61/102.89 Clause #1428 (by clausification #[1427]): ∀ (a : Type), Or (Eq (monoid_mult a) False) (Eq (∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True) % 102.61/102.89 Clause #1429 (by clausification #[1428]): ∀ (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) % 102.61/102.89 Clause #1430 (by clausification #[1429]): ∀ (a : Type) (a_1 : nat), Or (Eq (monoid_mult a) False) (Eq (power_power a (one_one a) a_1) (one_one a)) % 102.61/102.89 Clause #1432 (by superposition #[1430, 110]): ∀ (a : nat), Or (Eq (power_power real (one_one real) a) (one_one real)) (Eq False True) % 102.61/102.89 Clause #1447 (by clausification #[1432]): ∀ (a : nat), Eq (power_power real (one_one real) a) (one_one real) % 102.61/102.89 Clause #1449 (by backward demodulation #[1447, 1]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (power_power real (abs_abs real (times_times real (number_number_of real (bit0 (bit1 pls))) x)) % 102.61/102.89 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (one_one real)) % 102.61/102.89 True % 102.61/102.89 Clause #1451 (by clausification #[124]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (times_times real (number_number_of real (bit0 (bit0 (bit1 pls)))) % 102.61/102.89 (power_power real x (number_number_of nat (bit0 (bit1 pls))))) % 102.61/102.89 (one_one real)) % 102.61/102.89 False % 102.61/102.89 Clause #1452 (by forward demodulation #[1451, 213]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (power_power real (times_times real (number_number_of real (bit0 (bit1 pls))) x) % 102.61/102.89 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (one_one real)) % 102.61/102.89 False % 102.61/102.89 Clause #1474 (by clausification #[1250]): ∀ (a a_1 : real), Eq (times_times real a a_1) (times_times real a_1 a) % 102.61/102.89 Clause #1481 (by superposition #[1474, 1452]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (power_power real (times_times real x (number_number_of real (bit0 (bit1 pls)))) % 102.61/102.89 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (one_one real)) % 102.61/102.89 False % 102.61/102.89 Clause #4429 (by clausification #[762]): ∀ (a : real), % 102.61/102.89 Eq (power_power real (abs_abs real a) (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (power_power real a (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 Clause #10915 (by forward demodulation #[1449, 4429]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (power_power real (times_times real (number_number_of real (bit0 (bit1 pls))) x) % 102.61/102.89 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (one_one real)) % 102.61/102.89 True % 102.61/102.89 Clause #10916 (by forward demodulation #[10915, 1474]): Eq % 102.61/102.89 (ord_less_eq real % 102.61/102.89 (power_power real (times_times real x (number_number_of real (bit0 (bit1 pls)))) % 102.61/102.89 (number_number_of nat (bit0 (bit1 pls)))) % 102.61/102.89 (one_one real)) % 102.61/102.89 True % 102.61/102.89 Clause #11331 (by superposition #[1481, 10916]): Eq True False % 102.61/102.89 Clause #11332 (by clausification #[11331]): False % 102.61/102.89 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------