%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP130^2 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:51:17 PM UTC 2025 % Result : Theorem 74.48s 74.65s % Output : Proof 74.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : ITP130^2 : TPTP v9.2.0. Released v7.5.0. % 0.13/0.14 % Command : duper %s % 0.14/0.36 % Computer : n024.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 300 % 0.14/0.36 % DateTime : Thu Oct 2 23:05:23 EDT 2025 % 0.14/0.36 % CPUTime : % 74.48/74.65 SZS status Theorem for theBenchmark.p % 74.48/74.65 SZS output start Proof for theBenchmark.p % 74.48/74.65 Clause #2 (by assumption #[]): Eq % 74.48/74.65 (∀ (A : Type), % 74.48/74.65 linordered_idom A → % 74.48/74.65 ∀ (X B : int) (W : nat), % 74.48/74.65 Eq (ord_less A (ring_1_of_int A X) (power_power A (ring_1_of_int A B) W)) % 74.48/74.65 (ord_less int X (power_power int B W))) % 74.48/74.65 True % 74.48/74.65 Clause #57 (by assumption #[]): Eq (ord_less int na (power_power int ya p)) True % 74.48/74.65 Clause #62 (by assumption #[]): Eq (Eq p (suc pm)) True % 74.48/74.65 Clause #265 (by assumption #[]): Eq (linordered_idom real) True % 74.48/74.65 Clause #275 (by assumption #[]): Eq (Not (ord_less real (ring_1_of_int real na) (power_power real (ring_1_of_int real ya) (suc pm)))) True % 74.48/74.65 Clause #284 (by clausification #[2]): ∀ (a : Type), % 74.48/74.65 Eq % 74.48/74.65 (linordered_idom a → % 74.48/74.65 ∀ (X B : int) (W : nat), % 74.48/74.65 Eq (ord_less a (ring_1_of_int a X) (power_power a (ring_1_of_int a B) W)) % 74.48/74.65 (ord_less int X (power_power int B W))) % 74.48/74.65 True % 74.48/74.65 Clause #285 (by clausification #[284]): ∀ (a : Type), % 74.48/74.65 Or (Eq (linordered_idom a) False) % 74.48/74.65 (Eq % 74.48/74.65 (∀ (X B : int) (W : nat), % 74.48/74.65 Eq (ord_less a (ring_1_of_int a X) (power_power a (ring_1_of_int a B) W)) % 74.48/74.65 (ord_less int X (power_power int B W))) % 74.48/74.65 True) % 74.48/74.65 Clause #286 (by clausification #[285]): ∀ (a : Type) (a_1 : int), % 74.48/74.65 Or (Eq (linordered_idom a) False) % 74.48/74.65 (Eq % 74.48/74.65 (∀ (B : int) (W : nat), % 74.48/74.65 Eq (ord_less a (ring_1_of_int a a_1) (power_power a (ring_1_of_int a B) W)) % 74.48/74.65 (ord_less int a_1 (power_power int B W))) % 74.48/74.65 True) % 74.48/74.65 Clause #287 (by clausification #[286]): ∀ (a : Type) (a_1 a_2 : int), % 74.48/74.65 Or (Eq (linordered_idom a) False) % 74.48/74.65 (Eq % 74.48/74.65 (∀ (W : nat), % 74.48/74.65 Eq (ord_less a (ring_1_of_int a a_1) (power_power a (ring_1_of_int a a_2) W)) % 74.48/74.65 (ord_less int a_1 (power_power int a_2 W))) % 74.48/74.65 True) % 74.48/74.65 Clause #288 (by clausification #[287]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : nat), % 74.48/74.65 Or (Eq (linordered_idom a) False) % 74.48/74.65 (Eq % 74.48/74.65 (Eq (ord_less a (ring_1_of_int a a_1) (power_power a (ring_1_of_int a a_2) a_3)) % 74.48/74.65 (ord_less int a_1 (power_power int a_2 a_3))) % 74.48/74.65 True) % 74.48/74.65 Clause #289 (by clausification #[288]): ∀ (a : Type) (a_1 a_2 : int) (a_3 : nat), % 74.48/74.65 Or (Eq (linordered_idom a) False) % 74.48/74.65 (Eq (ord_less a (ring_1_of_int a a_1) (power_power a (ring_1_of_int a a_2) a_3)) % 74.48/74.65 (ord_less int a_1 (power_power int a_2 a_3))) % 74.48/74.65 Clause #290 (by superposition #[289, 265]): ∀ (a a_1 : int) (a_2 : nat), % 74.48/74.65 Or % 74.48/74.65 (Eq (ord_less real (ring_1_of_int real a) (power_power real (ring_1_of_int real a_1) a_2)) % 74.48/74.65 (ord_less int a (power_power int a_1 a_2))) % 74.48/74.65 (Eq False True) % 74.48/74.65 Clause #324 (by clausification #[62]): Eq p (suc pm) % 74.48/74.65 Clause #21195 (by clausification #[275]): Eq (ord_less real (ring_1_of_int real na) (power_power real (ring_1_of_int real ya) (suc pm))) False % 74.48/74.65 Clause #21196 (by forward demodulation #[21195, 324]): Eq (ord_less real (ring_1_of_int real na) (power_power real (ring_1_of_int real ya) p)) False % 74.48/74.65 Clause #21313 (by clausification #[290]): ∀ (a a_1 : int) (a_2 : nat), % 74.48/74.65 Eq (ord_less real (ring_1_of_int real a) (power_power real (ring_1_of_int real a_1) a_2)) % 74.48/74.65 (ord_less int a (power_power int a_1 a_2)) % 74.48/74.65 Clause #21316 (by superposition #[21313, 21196]): Eq (ord_less int na (power_power int ya p)) False % 74.48/74.65 Clause #21391 (by superposition #[21316, 57]): Eq False True % 74.48/74.65 Clause #21398 (by clausification #[21391]): False % 74.48/74.65 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------