%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM925_2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:57:35 PM UTC 2025 % Result : Theorem 174.47s 174.69s % Output : Proof 174.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM925_2 : TPTP v9.2.0. Released v5.3.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n008.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 : Fri Oct 3 08:59:38 EDT 2025 % 0.13/0.35 % CPUTime : % 174.47/174.69 SZS status Theorem for theBenchmark.p % 174.47/174.69 SZS output start Proof for theBenchmark.p % 174.47/174.69 Clause #0 (by assumption #[]): Eq % 174.47/174.69 (hBOOL % 174.47/174.69 (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int zero_zero_int) % 174.47/174.69 (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n)))) % 174.47/174.69 True % 174.47/174.69 Clause #9 (by assumption #[]): Eq (Eq (hAPP_nat_real (power_power_real zero_zero_real) (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_real) True % 174.47/174.69 Clause #25 (by assumption #[]): Eq (Eq (number_number_of_int (bit1 pls)) one_one_int) True % 174.47/174.69 Clause #37 (by assumption #[]): Eq (Eq (hAPP_nat_int semiri1621563631at_int one_one_nat) one_one_int) True % 174.47/174.69 Clause #41 (by assumption #[]): Eq (Eq (hAPP_nat_int semiri1621563631at_int zero_zero_nat) zero_zero_int) True % 174.47/174.69 Clause #60 (by assumption #[]): Eq (∀ (Z_2 W : int), Eq (hAPP_int_int (plus_plus_int Z_2) W) (hAPP_int_int (plus_plus_int W) Z_2)) True % 174.47/174.69 Clause #71 (by assumption #[]): Eq (Not (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) zero_zero_int))) True % 174.47/174.69 Clause #90 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 174.47/174.69 Clause #123 (by assumption #[]): Eq % 174.47/174.69 (∀ (A_66 : real), % 174.47/174.69 Not % 174.47/174.69 (hBOOL % 174.47/174.69 (hAPP_real_bool % 174.47/174.69 (hAPP_r1134773055l_bool ord_less_real % 174.47/174.69 (hAPP_nat_real (power_power_real A_66) (number_number_of_nat (bit0 (bit1 pls))))) % 174.47/174.69 zero_zero_real))) % 174.47/174.69 True % 174.47/174.69 Clause #159 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of_int K) K) True % 174.47/174.69 Clause #198 (by assumption #[]): Eq % 174.47/174.69 (∀ (Xa Ya : nat) (P_1 : bool), % 174.47/174.69 And % 174.47/174.69 (hBOOL P_1 → % 174.47/174.69 Eq (hAPP_nat_int semiri1621563631at_int Xa) % 174.47/174.69 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 Xa) Ya))) % 174.47/174.69 (Not (hBOOL P_1) → % 174.47/174.69 Eq (hAPP_nat_int semiri1621563631at_int Ya) % 174.47/174.69 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 Xa) Ya)))) % 174.47/174.69 True % 174.47/174.69 Clause #202 (by assumption #[]): Eq (Ne one_one_int zero_zero_int) True % 174.47/174.69 Clause #205 (by assumption #[]): Eq (∀ (N_23 : nat) (A_62 : int), Ne A_62 zero_zero_int → Ne (hAPP_nat_int (power_power_int A_62) N_23) zero_zero_int) % 174.47/174.69 True % 174.47/174.69 Clause #481 (by assumption #[]): Eq (∀ (K : int), Eq (succ K) (hAPP_int_int (plus_plus_int K) one_one_int)) True % 174.47/174.69 Clause #590 (by assumption #[]): Eq (∀ (X Y : nat), Eq (hAPP_nat_nat (if_nat fTrue X) Y) X) True % 174.47/174.69 Clause #592 (by assumption #[]): Eq (∀ (P : bool), Or (Eq P fTrue) (Eq P fFalse)) True % 174.47/174.69 Clause #593 (by assumption #[]): Eq % 174.47/174.69 (Not % 174.47/174.69 (Ne % 174.47/174.69 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 174.47/174.69 (number_number_of_nat (bit0 (bit1 pls)))) % 174.47/174.69 zero_zero_int)) % 174.47/174.69 True % 174.47/174.69 Clause #595 (by clausification #[202]): Ne one_one_int zero_zero_int % 174.47/174.69 Clause #599 (by clausification #[90]): Eq pls zero_zero_int % 174.47/174.69 Clause #600 (by backward demodulation #[599, 595]): Ne one_one_int pls % 174.47/174.69 Clause #601 (by backward demodulation #[599, 0]): Eq % 174.47/174.69 (hBOOL % 174.47/174.69 (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) % 174.47/174.69 (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n)))) % 174.47/174.69 True % 174.47/174.69 Clause #626 (by clausification #[37]): Eq (hAPP_nat_int semiri1621563631at_int one_one_nat) one_one_int % 174.47/174.70 Clause #648 (by clausification #[25]): Eq (number_number_of_int (bit1 pls)) one_one_int % 174.47/174.70 Clause #656 (by clausification #[159]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 174.47/174.70 Clause #657 (by clausification #[656]): ∀ (a : int), Eq (number_number_of_int a) a % 174.47/174.70 Clause #658 (by superposition #[657, 648]): Eq (bit1 pls) one_one_int % 174.47/174.70 Clause #675 (by clausification #[41]): Eq (hAPP_nat_int semiri1621563631at_int zero_zero_nat) zero_zero_int % 174.47/174.70 Clause #676 (by forward demodulation #[675, 599]): Eq (hAPP_nat_int semiri1621563631at_int zero_zero_nat) pls % 174.47/174.70 Clause #680 (by clausification #[9]): Eq (hAPP_nat_real (power_power_real zero_zero_real) (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_real % 174.47/174.70 Clause #681 (by forward demodulation #[680, 658]): Eq (hAPP_nat_real (power_power_real zero_zero_real) (number_number_of_nat (bit0 one_one_int))) zero_zero_real % 174.47/174.70 Clause #716 (by clausification #[71]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) zero_zero_int)) False % 174.55/174.72 Clause #717 (by forward demodulation #[716, 599]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls)) False % 174.55/174.72 Clause #1624 (by clausification #[481]): ∀ (a : int), Eq (Eq (succ a) (hAPP_int_int (plus_plus_int a) one_one_int)) True % 174.55/174.72 Clause #1625 (by clausification #[1624]): ∀ (a : int), Eq (succ a) (hAPP_int_int (plus_plus_int a) one_one_int) % 174.55/174.72 Clause #1789 (by clausification #[60]): ∀ (a : int), Eq (∀ (W : int), Eq (hAPP_int_int (plus_plus_int a) W) (hAPP_int_int (plus_plus_int W) a)) True % 174.55/174.72 Clause #1790 (by clausification #[1789]): ∀ (a a_1 : int), Eq (Eq (hAPP_int_int (plus_plus_int a) a_1) (hAPP_int_int (plus_plus_int a_1) a)) True % 174.55/174.72 Clause #1791 (by clausification #[1790]): ∀ (a a_1 : int), Eq (hAPP_int_int (plus_plus_int a) a_1) (hAPP_int_int (plus_plus_int a_1) a) % 174.55/174.72 Clause #1794 (by superposition #[1791, 1625]): ∀ (a : int), Eq (succ a) (hAPP_int_int (plus_plus_int one_one_int) a) % 174.55/174.72 Clause #3156 (by clausification #[123]): ∀ (a : real), % 174.55/174.72 Eq % 174.55/174.72 (Not % 174.55/174.72 (hBOOL % 174.55/174.72 (hAPP_real_bool % 174.55/174.72 (hAPP_r1134773055l_bool ord_less_real % 174.55/174.72 (hAPP_nat_real (power_power_real a) (number_number_of_nat (bit0 (bit1 pls))))) % 174.55/174.72 zero_zero_real))) % 174.55/174.72 True % 174.55/174.72 Clause #3157 (by clausification #[3156]): ∀ (a : real), % 174.55/174.72 Eq % 174.55/174.72 (hBOOL % 174.55/174.72 (hAPP_real_bool % 174.55/174.72 (hAPP_r1134773055l_bool ord_less_real % 174.55/174.72 (hAPP_nat_real (power_power_real a) (number_number_of_nat (bit0 (bit1 pls))))) % 174.55/174.72 zero_zero_real)) % 174.55/174.72 False % 174.55/174.72 Clause #3158 (by forward demodulation #[3157, 658]): ∀ (a : real), % 174.55/174.72 Eq % 174.55/174.72 (hBOOL % 174.55/174.72 (hAPP_real_bool % 174.55/174.72 (hAPP_r1134773055l_bool ord_less_real % 174.55/174.72 (hAPP_nat_real (power_power_real a) (number_number_of_nat (bit0 one_one_int)))) % 174.55/174.72 zero_zero_real)) % 174.55/174.72 False % 174.55/174.72 Clause #3160 (by superposition #[3158, 681]): Eq (hBOOL (hAPP_real_bool (hAPP_r1134773055l_bool ord_less_real zero_zero_real) zero_zero_real)) False % 174.55/174.72 Clause #5866 (by clausification #[198]): ∀ (a : nat), % 174.55/174.72 Eq % 174.55/174.72 (∀ (Ya : nat) (P_1 : bool), % 174.55/174.72 And % 174.55/174.72 (hBOOL P_1 → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 a) Ya))) % 174.55/174.72 (Not (hBOOL P_1) → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int Ya) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 a) Ya)))) % 174.55/174.72 True % 174.55/174.72 Clause #5867 (by clausification #[5866]): ∀ (a a_1 : nat), % 174.55/174.72 Eq % 174.55/174.72 (∀ (P_1 : bool), % 174.55/174.72 And % 174.55/174.72 (hBOOL P_1 → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 a) a_1))) % 174.55/174.72 (Not (hBOOL P_1) → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a_1) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat P_1 a) a_1)))) % 174.55/174.72 True % 174.55/174.72 Clause #5868 (by clausification #[5867]): ∀ (a : bool) (a_1 a_2 : nat), % 174.55/174.72 Eq % 174.55/174.72 (And % 174.55/174.72 (hBOOL a → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a_1) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a a_1) a_2))) % 174.55/174.72 (Not (hBOOL a) → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a_2) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a a_1) a_2)))) % 174.55/174.72 True % 174.55/174.72 Clause #5869 (by clausification #[5868]): ∀ (a : bool) (a_1 a_2 : nat), % 174.55/174.72 Eq % 174.55/174.72 (Not (hBOOL a) → % 174.55/174.72 Eq (hAPP_nat_int semiri1621563631at_int a_1) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a a_2) a_1))) % 174.55/174.72 True % 174.55/174.72 Clause #5871 (by clausification #[5869]): ∀ (a : bool) (a_1 a_2 : nat), % 174.55/174.72 Or (Eq (Not (hBOOL a)) False) % 174.55/174.72 (Eq % 174.55/174.72 (Eq (hAPP_nat_int semiri1621563631at_int a_1) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a a_2) a_1))) % 174.55/174.72 True) % 174.55/174.72 Clause #5872 (by clausification #[5871]): ∀ (a : nat) (a_1 : bool) (a_2 : nat), % 174.55/174.72 Or % 174.55/174.72 (Eq % 174.55/174.72 (Eq (hAPP_nat_int semiri1621563631at_int a) % 174.55/174.72 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a_1 a_2) a))) % 174.55/174.72 True) % 174.55/174.72 (Eq (hBOOL a_1) True) % 174.55/174.72 Clause #5873 (by clausification #[5872]): ∀ (a : bool) (a_1 a_2 : nat), % 174.55/174.74 Or (Eq (hBOOL a) True) % 174.55/174.74 (Eq (hAPP_nat_int semiri1621563631at_int a_1) % 174.55/174.74 (hAPP_nat_int semiri1621563631at_int (hAPP_nat_nat (if_nat a a_2) a_1))) % 174.55/174.74 Clause #6054 (by clausification #[205]): ∀ (a : nat), Eq (∀ (A_62 : int), Ne A_62 zero_zero_int → Ne (hAPP_nat_int (power_power_int A_62) a) zero_zero_int) True % 174.55/174.74 Clause #6055 (by clausification #[6054]): ∀ (a : int) (a_1 : nat), Eq (Ne a zero_zero_int → Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True % 174.55/174.74 Clause #6056 (by clausification #[6055]): ∀ (a : int) (a_1 : nat), % 174.55/174.74 Or (Eq (Ne a zero_zero_int) False) (Eq (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True) % 174.55/174.74 Clause #6057 (by clausification #[6056]): ∀ (a : int) (a_1 : nat), Or (Eq (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True) (Eq a zero_zero_int) % 174.55/174.74 Clause #6058 (by clausification #[6057]): ∀ (a : int) (a_1 : nat), Or (Eq a zero_zero_int) (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) % 174.55/174.74 Clause #6059 (by forward demodulation #[6058, 599]): ∀ (a : int) (a_1 : nat), Or (Eq a pls) (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) % 174.55/174.74 Clause #6060 (by forward demodulation #[6059, 599]): ∀ (a : int) (a_1 : nat), Or (Eq a pls) (Ne (hAPP_nat_int (power_power_int a) a_1) pls) % 174.55/174.74 Clause #6277 (by clausification #[590]): ∀ (a : nat), Eq (∀ (Y : nat), Eq (hAPP_nat_nat (if_nat fTrue a) Y) a) True % 174.55/174.74 Clause #6278 (by clausification #[6277]): ∀ (a a_1 : nat), Eq (Eq (hAPP_nat_nat (if_nat fTrue a) a_1) a) True % 174.55/174.74 Clause #6279 (by clausification #[6278]): ∀ (a a_1 : nat), Eq (hAPP_nat_nat (if_nat fTrue a) a_1) a % 174.55/174.74 Clause #6280 (by superposition #[6279, 5873]): ∀ (a a_1 : nat), % 174.55/174.74 Or (Eq (hBOOL fTrue) True) (Eq (hAPP_nat_int semiri1621563631at_int a) (hAPP_nat_int semiri1621563631at_int a_1)) % 174.55/174.74 Clause #6282 (by superposition #[6280, 676]): ∀ (a : nat), Or (Eq (hBOOL fTrue) True) (Eq (hAPP_nat_int semiri1621563631at_int a) pls) % 174.55/174.74 Clause #6331 (by superposition #[6282, 626]): Or (Eq (hBOOL fTrue) True) (Eq pls one_one_int) % 174.55/174.74 Clause #6357 (by forward contextual literal cutting #[6331, 600]): Eq (hBOOL fTrue) True % 174.55/174.74 Clause #11965 (by clausification #[592]): ∀ (a : bool), Eq (Or (Eq a fTrue) (Eq a fFalse)) True % 174.55/174.74 Clause #11966 (by clausification #[11965]): ∀ (a : bool), Or (Eq (Eq a fTrue) True) (Eq (Eq a fFalse) True) % 174.55/174.74 Clause #11967 (by clausification #[11966]): ∀ (a : bool), Or (Eq (Eq a fFalse) True) (Eq a fTrue) % 174.55/174.74 Clause #11968 (by clausification #[11967]): ∀ (a : bool), Or (Eq a fTrue) (Eq a fFalse) % 174.55/174.74 Clause #11970 (by superposition #[11968, 6357]): ∀ (a : bool), Or (Eq a fFalse) (Eq (hBOOL a) True) % 174.55/174.74 Clause #12261 (by superposition #[11970, 717]): Or (Eq (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls) fFalse) (Eq True False) % 174.55/174.74 Clause #12288 (by superposition #[11970, 3160]): Or (Eq (hAPP_real_bool (hAPP_r1134773055l_bool ord_less_real zero_zero_real) zero_zero_real) fFalse) (Eq True False) % 174.55/174.74 Clause #18138 (by clausification #[12288]): Eq (hAPP_real_bool (hAPP_r1134773055l_bool ord_less_real zero_zero_real) zero_zero_real) fFalse % 174.55/174.74 Clause #18139 (by backward demodulation #[18138, 3160]): Eq (hBOOL fFalse) False % 174.55/174.74 Clause #20921 (by clausification #[12261]): Eq (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls) fFalse % 174.55/174.74 Clause #50465 (by clausification #[593]): Eq % 174.55/174.74 (Ne % 174.55/174.74 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 174.55/174.74 (number_number_of_nat (bit0 (bit1 pls)))) % 174.55/174.74 zero_zero_int) % 174.55/174.74 False % 174.55/174.74 Clause #50466 (by clausification #[50465]): Eq % 174.55/174.74 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 174.55/174.74 (number_number_of_nat (bit0 (bit1 pls)))) % 174.55/174.74 zero_zero_int % 174.55/174.74 Clause #50467 (by forward demodulation #[50466, 658]): Eq % 174.55/174.74 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 174.55/174.74 (number_number_of_nat (bit0 one_one_int))) % 174.55/174.74 zero_zero_int % 174.55/174.74 Clause #50468 (by forward demodulation #[50467, 1794]): Eq % 174.55/174.74 (hAPP_nat_int (power_power_int (succ (hAPP_nat_int semiri1621563631at_int n))) % 174.55/174.74 (number_number_of_nat (bit0 one_one_int))) % 174.85/175.05 zero_zero_int % 174.85/175.05 Clause #50469 (by forward demodulation #[50468, 599]): Eq % 174.85/175.05 (hAPP_nat_int (power_power_int (succ (hAPP_nat_int semiri1621563631at_int n))) % 174.85/175.05 (number_number_of_nat (bit0 one_one_int))) % 174.85/175.05 pls % 174.85/175.05 Clause #50483 (by superposition #[50469, 6060]): Or (Eq (succ (hAPP_nat_int semiri1621563631at_int n)) pls) (Ne pls pls) % 174.85/175.05 Clause #50501 (by eliminate resolved literals #[50483]): Eq (succ (hAPP_nat_int semiri1621563631at_int n)) pls % 174.85/175.05 Clause #50603 (by forward demodulation #[601, 1794]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) (succ (hAPP_nat_int semiri1621563631at_int n)))) True % 174.85/175.05 Clause #50604 (by forward demodulation #[50603, 50501]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls)) True % 174.85/175.05 Clause #50605 (by forward demodulation #[50604, 20921]): Eq (hBOOL fFalse) True % 174.85/175.05 Clause #50606 (by superposition #[50605, 18139]): Eq True False % 174.85/175.05 Clause #50691 (by clausification #[50606]): False % 174.85/175.05 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------