%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM925^2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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 133.96s 134.19s % Output : Proof 134.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NUM925^2 : TPTP v9.2.0. Released v5.3.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n031.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:05:08 EDT 2025 % 0.13/0.34 % CPUTime : % 133.96/134.19 SZS status Theorem for theBenchmark.p % 133.96/134.19 SZS output start Proof for theBenchmark.p % 133.96/134.19 Clause #18 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 133.96/134.19 Clause #25 (by assumption #[]): Eq (Eq (number_number_of_int (bit1 pls)) one_one_int) True % 133.96/134.19 Clause #60 (by assumption #[]): Eq (∀ (Z_2 W : int), Eq (plus_plus_int Z_2 W) (plus_plus_int W Z_2)) True % 133.96/134.19 Clause #90 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 133.96/134.19 Clause #159 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of_int K) K) True % 133.96/134.19 Clause #205 (by assumption #[]): Eq (∀ (N_27 : nat) (A_75 : int), Ne A_75 zero_zero_int → Ne (power_power_int A_75 N_27) zero_zero_int) True % 133.96/134.19 Clause #414 (by assumption #[]): Eq (Not (ord_less_eq_int one_one_int zero_zero_int)) True % 133.96/134.19 Clause #439 (by assumption #[]): Eq % 133.96/134.19 (∀ (W Z_2 : int), % 133.96/134.19 Iff (ord_less_eq_int W Z_2) (Exists fun N_1 => Eq Z_2 (plus_plus_int W (semiri1621563631at_int N_1)))) % 133.96/134.19 True % 133.96/134.19 Clause #481 (by assumption #[]): Eq (∀ (K : int), Eq (succ K) (plus_plus_int K one_one_int)) True % 133.96/134.19 Clause #593 (by assumption #[]): Eq % 133.96/134.19 (Not % 133.96/134.19 (Ne % 133.96/134.19 (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 133.96/134.19 zero_zero_int)) % 133.96/134.19 True % 133.96/134.19 Clause #622 (by clausification #[90]): Eq pls zero_zero_int % 133.96/134.19 Clause #643 (by clausification #[414]): Eq (ord_less_eq_int one_one_int zero_zero_int) False % 133.96/134.19 Clause #644 (by forward demodulation #[643, 622]): Eq (ord_less_eq_int one_one_int pls) False % 133.96/134.19 Clause #745 (by clausification #[25]): Eq (number_number_of_int (bit1 pls)) one_one_int % 133.96/134.19 Clause #770 (by clausification #[159]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 133.96/134.19 Clause #771 (by clausification #[770]): ∀ (a : int), Eq (number_number_of_int a) a % 133.96/134.19 Clause #775 (by superposition #[771, 745]): Eq (bit1 pls) one_one_int % 133.96/134.19 Clause #796 (by clausification #[18]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 133.96/134.19 Clause #797 (by forward demodulation #[796, 775]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 133.96/134.19 Clause #2074 (by clausification #[60]): ∀ (a : int), Eq (∀ (W : int), Eq (plus_plus_int a W) (plus_plus_int W a)) True % 133.96/134.19 Clause #2075 (by clausification #[2074]): ∀ (a a_1 : int), Eq (Eq (plus_plus_int a a_1) (plus_plus_int a_1 a)) True % 133.96/134.19 Clause #2076 (by clausification #[2075]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 133.96/134.19 Clause #7979 (by clausification #[205]): ∀ (a : nat), Eq (∀ (A_75 : int), Ne A_75 zero_zero_int → Ne (power_power_int A_75 a) zero_zero_int) True % 133.96/134.19 Clause #7980 (by clausification #[7979]): ∀ (a : int) (a_1 : nat), Eq (Ne a zero_zero_int → Ne (power_power_int a a_1) zero_zero_int) True % 133.96/134.19 Clause #7981 (by clausification #[7980]): ∀ (a : int) (a_1 : nat), Or (Eq (Ne a zero_zero_int) False) (Eq (Ne (power_power_int a a_1) zero_zero_int) True) % 133.96/134.19 Clause #7982 (by clausification #[7981]): ∀ (a : int) (a_1 : nat), Or (Eq (Ne (power_power_int a a_1) zero_zero_int) True) (Eq a zero_zero_int) % 133.96/134.19 Clause #7983 (by clausification #[7982]): ∀ (a : int) (a_1 : nat), Or (Eq a zero_zero_int) (Ne (power_power_int a a_1) zero_zero_int) % 133.96/134.19 Clause #7984 (by forward demodulation #[7983, 622]): ∀ (a : int) (a_1 : nat), Or (Eq a pls) (Ne (power_power_int a a_1) zero_zero_int) % 133.96/134.19 Clause #7985 (by forward demodulation #[7984, 622]): ∀ (a : int) (a_1 : nat), Or (Eq a pls) (Ne (power_power_int a a_1) pls) % 133.96/134.19 Clause #18297 (by clausification #[439]): ∀ (a : int), % 133.96/134.19 Eq % 133.96/134.19 (∀ (Z_2 : int), % 133.96/134.19 Iff (ord_less_eq_int a Z_2) (Exists fun N_1 => Eq Z_2 (plus_plus_int a (semiri1621563631at_int N_1)))) % 133.96/134.19 True % 133.96/134.19 Clause #18298 (by clausification #[18297]): ∀ (a a_1 : int), % 133.96/134.19 Eq (Iff (ord_less_eq_int a a_1) (Exists fun N_1 => Eq a_1 (plus_plus_int a (semiri1621563631at_int N_1)))) True % 133.96/134.19 Clause #18299 (by clausification #[18298]): ∀ (a a_1 : int), % 133.96/134.19 Or (Eq (ord_less_eq_int a a_1) True) % 133.96/134.19 (Eq (Exists fun N_1 => Eq a_1 (plus_plus_int a (semiri1621563631at_int N_1))) False) % 133.96/134.19 Clause #18301 (by clausification #[18299]): ∀ (a a_1 : int) (a_2 : nat), % 134.28/134.48 Or (Eq (ord_less_eq_int a a_1) True) (Eq (Eq a_1 (plus_plus_int a (semiri1621563631at_int a_2))) False) % 134.28/134.48 Clause #18302 (by clausification #[18301]): ∀ (a a_1 : int) (a_2 : nat), % 134.28/134.48 Or (Eq (ord_less_eq_int a a_1) True) (Ne a_1 (plus_plus_int a (semiri1621563631at_int a_2))) % 134.28/134.48 Clause #18303 (by destructive equality resolution #[18302]): ∀ (a : int) (a_1 : nat), Eq (ord_less_eq_int a (plus_plus_int a (semiri1621563631at_int a_1))) True % 134.28/134.48 Clause #18332 (by superposition #[18303, 2076]): ∀ (a : int) (a_1 : nat), Eq (ord_less_eq_int a (plus_plus_int (semiri1621563631at_int a_1) a)) True % 134.28/134.48 Clause #23102 (by clausification #[481]): ∀ (a : int), Eq (Eq (succ a) (plus_plus_int a one_one_int)) True % 134.28/134.48 Clause #23103 (by clausification #[23102]): ∀ (a : int), Eq (succ a) (plus_plus_int a one_one_int) % 134.28/134.48 Clause #23140 (by superposition #[23103, 18332]): ∀ (a : nat), Eq (ord_less_eq_int one_one_int (succ (semiri1621563631at_int a))) True % 134.28/134.48 Clause #23163 (by superposition #[23103, 2076]): ∀ (a : int), Eq (plus_plus_int one_one_int a) (succ a) % 134.28/134.48 Clause #37905 (by clausification #[593]): Eq % 134.28/134.48 (Ne (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 134.28/134.48 zero_zero_int) % 134.28/134.48 False % 134.28/134.48 Clause #37906 (by clausification #[37905]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 134.28/134.48 zero_zero_int % 134.28/134.48 Clause #37907 (by forward demodulation #[37906, 775]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 one_one_int))) % 134.28/134.48 zero_zero_int % 134.28/134.48 Clause #37908 (by forward demodulation #[37907, 797]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (plus_plus_nat one_one_nat one_one_nat)) % 134.28/134.48 zero_zero_int % 134.28/134.48 Clause #37909 (by forward demodulation #[37908, 23163]): Eq (power_power_int (succ (semiri1621563631at_int n)) (plus_plus_nat one_one_nat one_one_nat)) zero_zero_int % 134.28/134.48 Clause #37910 (by forward demodulation #[37909, 622]): Eq (power_power_int (succ (semiri1621563631at_int n)) (plus_plus_nat one_one_nat one_one_nat)) pls % 134.28/134.48 Clause #37922 (by superposition #[37910, 7985]): Or (Eq (succ (semiri1621563631at_int n)) pls) (Ne pls pls) % 134.28/134.48 Clause #37955 (by eliminate resolved literals #[37922]): Eq (succ (semiri1621563631at_int n)) pls % 134.28/134.48 Clause #37958 (by superposition #[37955, 23140]): Eq (ord_less_eq_int one_one_int pls) True % 134.28/134.48 Clause #38026 (by superposition #[37958, 644]): Eq True False % 134.28/134.48 Clause #38120 (by clausification #[38026]): False % 134.28/134.48 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------