%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM925+2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n013.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 173.66s 173.87s % Output : Proof 173.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM925+2 : TPTP v9.2.0. Released v5.3.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n013.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 07:46:23 EDT 2025 % 0.13/0.35 % CPUTime : % 173.66/173.87 SZS status Theorem for theBenchmark.p % 173.66/173.87 SZS output start Proof for theBenchmark.p % 173.66/173.87 Clause #5 (by assumption #[]): Eq % 173.66/173.87 (hBOOL % 173.66/173.87 (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int zero_zero_int) % 173.66/173.87 (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n)))) % 173.66/173.87 True % 173.66/173.87 Clause #30 (by assumption #[]): Eq (Eq (number_number_of_int (bit1 pls)) one_one_int) True % 173.66/173.87 Clause #65 (by assumption #[]): Eq (∀ (Z_2 W : Iota), Eq (hAPP_int_int (plus_plus_int Z_2) W) (hAPP_int_int (plus_plus_int W) Z_2)) True % 173.66/173.87 Clause #76 (by assumption #[]): Eq (Not (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) zero_zero_int))) True % 173.66/173.87 Clause #95 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 173.66/173.87 Clause #164 (by assumption #[]): Eq (∀ (K : Iota), Eq (number_number_of_int K) K) True % 173.66/173.87 Clause #210 (by assumption #[]): Eq (∀ (N_23 A_62 : Iota), Ne A_62 zero_zero_int → Ne (hAPP_nat_int (power_power_int A_62) N_23) zero_zero_int) True % 173.66/173.87 Clause #486 (by assumption #[]): Eq (∀ (K : Iota), Eq (succ K) (hAPP_int_int (plus_plus_int K) one_one_int)) True % 173.66/173.87 Clause #598 (by assumption #[]): Eq % 173.66/173.87 (Not % 173.66/173.87 (Ne % 173.66/173.87 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 173.66/173.87 (number_number_of_nat (bit0 (bit1 pls)))) % 173.66/173.87 zero_zero_int)) % 173.66/173.87 True % 173.66/173.87 Clause #606 (by clausification #[95]): Eq pls zero_zero_int % 173.66/173.87 Clause #624 (by forward demodulation #[5, 606]): Eq % 173.66/173.87 (hBOOL % 173.66/173.87 (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) % 173.66/173.87 (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n)))) % 173.66/173.87 True % 173.66/173.87 Clause #655 (by clausification #[30]): Eq (number_number_of_int (bit1 pls)) one_one_int % 173.66/173.87 Clause #666 (by clausification #[164]): ∀ (a : Iota), Eq (Eq (number_number_of_int a) a) True % 173.66/173.87 Clause #667 (by clausification #[666]): ∀ (a : Iota), Eq (number_number_of_int a) a % 173.66/173.87 Clause #668 (by superposition #[667, 655]): Eq (bit1 pls) one_one_int % 173.66/173.87 Clause #726 (by clausification #[76]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) zero_zero_int)) False % 173.66/173.87 Clause #727 (by forward demodulation #[726, 606]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls)) False % 173.66/173.87 Clause #2427 (by clausification #[486]): ∀ (a : Iota), Eq (Eq (succ a) (hAPP_int_int (plus_plus_int a) one_one_int)) True % 173.66/173.87 Clause #2428 (by clausification #[2427]): ∀ (a : Iota), Eq (succ a) (hAPP_int_int (plus_plus_int a) one_one_int) % 173.66/173.87 Clause #2671 (by clausification #[65]): ∀ (a : Iota), Eq (∀ (W : Iota), Eq (hAPP_int_int (plus_plus_int a) W) (hAPP_int_int (plus_plus_int W) a)) True % 173.66/173.87 Clause #2672 (by clausification #[2671]): ∀ (a a_1 : Iota), Eq (Eq (hAPP_int_int (plus_plus_int a) a_1) (hAPP_int_int (plus_plus_int a_1) a)) True % 173.66/173.87 Clause #2673 (by clausification #[2672]): ∀ (a a_1 : Iota), Eq (hAPP_int_int (plus_plus_int a) a_1) (hAPP_int_int (plus_plus_int a_1) a) % 173.66/173.87 Clause #2676 (by superposition #[2673, 2428]): ∀ (a : Iota), Eq (succ a) (hAPP_int_int (plus_plus_int one_one_int) a) % 173.66/173.87 Clause #2690 (by backward demodulation #[2676, 624]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) (succ (hAPP_nat_int semiri1621563631at_int n)))) True % 173.66/173.87 Clause #13475 (by clausification #[210]): ∀ (a : Iota), % 173.66/173.87 Eq (∀ (A_62 : Iota), Ne A_62 zero_zero_int → Ne (hAPP_nat_int (power_power_int A_62) a) zero_zero_int) True % 173.66/173.87 Clause #13476 (by clausification #[13475]): ∀ (a a_1 : Iota), Eq (Ne a zero_zero_int → Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True % 173.66/173.87 Clause #13477 (by clausification #[13476]): ∀ (a a_1 : Iota), Or (Eq (Ne a zero_zero_int) False) (Eq (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True) % 173.66/173.87 Clause #13478 (by clausification #[13477]): ∀ (a a_1 : Iota), Or (Eq (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) True) (Eq a zero_zero_int) % 173.66/173.87 Clause #13479 (by clausification #[13478]): ∀ (a a_1 : Iota), Or (Eq a zero_zero_int) (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) % 173.66/173.87 Clause #13480 (by forward demodulation #[13479, 606]): ∀ (a a_1 : Iota), Or (Eq a pls) (Ne (hAPP_nat_int (power_power_int a) a_1) zero_zero_int) % 173.90/174.12 Clause #13481 (by forward demodulation #[13480, 606]): ∀ (a a_1 : Iota), Or (Eq a pls) (Ne (hAPP_nat_int (power_power_int a) a_1) pls) % 173.90/174.12 Clause #38108 (by clausification #[598]): Eq % 173.90/174.12 (Ne % 173.90/174.12 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 173.90/174.12 (number_number_of_nat (bit0 (bit1 pls)))) % 173.90/174.12 zero_zero_int) % 173.90/174.12 False % 173.90/174.12 Clause #38109 (by clausification #[38108]): Eq % 173.90/174.12 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 173.90/174.12 (number_number_of_nat (bit0 (bit1 pls)))) % 173.90/174.12 zero_zero_int % 173.90/174.12 Clause #38110 (by forward demodulation #[38109, 668]): Eq % 173.90/174.12 (hAPP_nat_int (power_power_int (hAPP_int_int (plus_plus_int one_one_int) (hAPP_nat_int semiri1621563631at_int n))) % 173.90/174.12 (number_number_of_nat (bit0 one_one_int))) % 173.90/174.12 zero_zero_int % 173.90/174.12 Clause #38111 (by forward demodulation #[38110, 2676]): Eq % 173.90/174.12 (hAPP_nat_int (power_power_int (succ (hAPP_nat_int semiri1621563631at_int n))) % 173.90/174.12 (number_number_of_nat (bit0 one_one_int))) % 173.90/174.12 zero_zero_int % 173.90/174.12 Clause #38112 (by forward demodulation #[38111, 606]): Eq % 173.90/174.12 (hAPP_nat_int (power_power_int (succ (hAPP_nat_int semiri1621563631at_int n))) % 173.90/174.12 (number_number_of_nat (bit0 one_one_int))) % 173.90/174.12 pls % 173.90/174.12 Clause #38126 (by superposition #[38112, 13481]): Or (Eq (succ (hAPP_nat_int semiri1621563631at_int n)) pls) (Ne pls pls) % 173.90/174.12 Clause #38269 (by eliminate resolved literals #[38126]): Eq (succ (hAPP_nat_int semiri1621563631at_int n)) pls % 173.90/174.12 Clause #38270 (by backward demodulation #[38269, 2690]): Eq (hBOOL (hAPP_int_bool (hAPP_i1948725293t_bool ord_less_int pls) pls)) True % 173.90/174.12 Clause #38833 (by superposition #[38270, 727]): Eq True False % 173.90/174.12 Clause #38887 (by clausification #[38833]): False % 173.90/174.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------