%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM924_2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:33 PM UTC 2025 % Result : Theorem 145.82s 146.10s % Output : Proof 146.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.10 % Problem : NUM924_2 : TPTP v9.2.0. Released v5.3.0. % 0.05/0.11 % Command : duper %s % 0.10/0.32 % Computer : n029.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Fri Oct 3 08:11:38 EDT 2025 % 0.10/0.33 % CPUTime : % 145.82/146.10 SZS status Theorem for theBenchmark.p % 145.82/146.10 SZS output start Proof for theBenchmark.p % 145.82/146.10 Clause #2 (by assumption #[]): Eq % 145.82/146.10 (ord_less_int % 145.82/146.10 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t) % 145.82/146.10 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 145.82/146.10 zero_zero_int)) % 145.82/146.10 True % 145.82/146.10 Clause #3 (by assumption #[]): Eq % 145.82/146.10 (Eq (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.10 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t)) % 145.82/146.10 True % 145.82/146.10 Clause #34 (by assumption #[]): Eq (∀ (K_1 : int), Eq (number_number_of_int K_1) K_1) True % 145.82/146.10 Clause #35 (by assumption #[]): Eq (∀ (Z W : int), Eq (times_times_int Z W) (times_times_int W Z)) True % 145.82/146.10 Clause #82 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 145.82/146.10 Clause #84 (by assumption #[]): Eq (∀ (K_1 L : int), Eq (times_times_int (bit0 K_1) L) (bit0 (times_times_int K_1 L))) True % 145.82/146.10 Clause #86 (by assumption #[]): Eq (∀ (Z : int), Eq (times_times_int Z one_one_int) Z) True % 145.82/146.10 Clause #87 (by assumption #[]): Eq (∀ (Z : int), Eq (times_times_int one_one_int Z) Z) True % 145.82/146.10 Clause #124 (by assumption #[]): Eq (∀ (X Y Z : int), Eq (plus_plus_int X (plus_plus_int Y Z)) (plus_plus_int Y (plus_plus_int X Z))) True % 145.82/146.10 Clause #146 (by assumption #[]): Eq % 145.82/146.10 (∀ (X_19 Y_11 : int), % 145.82/146.10 Not (ord_less_int (plus_plus_int (times_times_int X_19 X_19) (times_times_int Y_11 Y_11)) zero_zero_int)) % 145.82/146.10 True % 145.82/146.10 Clause #152 (by assumption #[]): Eq (∀ (K_1 L : int), Eq (times_times_int (bit1 K_1) L) (plus_plus_int (bit0 (times_times_int K_1 L)) L)) True % 145.82/146.10 Clause #163 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 145.82/146.10 Clause #172 (by assumption #[]): Eq (∀ (Z : int), Eq (plus_plus_int Z zero_zero_int) Z) True % 145.82/146.10 Clause #188 (by assumption #[]): Eq (∀ (A_50 : int), Eq (power_power_int A_50 (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int A_50 A_50)) True % 145.82/146.10 Clause #228 (by assumption #[]): Eq (Eq (number_number_of_int (bit1 pls)) one_one_int) True % 145.82/146.10 Clause #324 (by assumption #[]): Eq (∀ (A_38 : int), Eq (times_times_int zero_zero_int A_38) zero_zero_int) True % 145.82/146.10 Clause #642 (by clausification #[3]): Eq (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.10 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t) % 145.82/146.10 Clause #643 (by backward demodulation #[642, 2]): Eq % 145.82/146.10 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.10 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 145.82/146.10 zero_zero_int)) % 145.82/146.10 True % 145.82/146.10 Clause #648 (by clausification #[163]): Eq pls zero_zero_int % 145.82/146.10 Clause #694 (by clausification #[228]): Eq (number_number_of_int (bit1 pls)) one_one_int % 145.82/146.10 Clause #755 (by clausification #[34]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 145.82/146.10 Clause #756 (by clausification #[755]): ∀ (a : int), Eq (number_number_of_int a) a % 145.82/146.10 Clause #762 (by superposition #[756, 694]): Eq (bit1 pls) one_one_int % 145.82/146.10 Clause #922 (by clausification #[324]): ∀ (a : int), Eq (Eq (times_times_int zero_zero_int a) zero_zero_int) True % 145.82/146.10 Clause #923 (by clausification #[922]): ∀ (a : int), Eq (times_times_int zero_zero_int a) zero_zero_int % 145.82/146.10 Clause #924 (by forward demodulation #[923, 648]): ∀ (a : int), Eq (times_times_int pls a) zero_zero_int % 145.82/146.10 Clause #925 (by forward demodulation #[924, 648]): ∀ (a : int), Eq (times_times_int pls a) pls % 145.82/146.10 Clause #967 (by clausification #[172]): ∀ (a : int), Eq (Eq (plus_plus_int a zero_zero_int) a) True % 145.82/146.10 Clause #968 (by clausification #[967]): ∀ (a : int), Eq (plus_plus_int a zero_zero_int) a % 145.82/146.10 Clause #969 (by forward demodulation #[968, 648]): ∀ (a : int), Eq (plus_plus_int a pls) a % 145.82/146.10 Clause #1072 (by clausification #[87]): ∀ (a : int), Eq (Eq (times_times_int one_one_int a) a) True % 145.82/146.10 Clause #1073 (by clausification #[1072]): ∀ (a : int), Eq (times_times_int one_one_int a) a % 145.82/146.13 Clause #1074 (by clausification #[86]): ∀ (a : int), Eq (Eq (times_times_int a one_one_int) a) True % 145.82/146.13 Clause #1075 (by clausification #[1074]): ∀ (a : int), Eq (times_times_int a one_one_int) a % 145.82/146.13 Clause #1312 (by clausification #[35]): ∀ (a : int), Eq (∀ (W : int), Eq (times_times_int a W) (times_times_int W a)) True % 145.82/146.13 Clause #1313 (by clausification #[1312]): ∀ (a a_1 : int), Eq (Eq (times_times_int a a_1) (times_times_int a_1 a)) True % 145.82/146.13 Clause #1314 (by clausification #[1313]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int a_1 a) % 145.82/146.13 Clause #2741 (by clausification #[82]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 145.82/146.13 Clause #2742 (by forward demodulation #[2741, 762]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 145.82/146.13 Clause #2775 (by clausification #[84]): ∀ (a : int), Eq (∀ (L : int), Eq (times_times_int (bit0 a) L) (bit0 (times_times_int a L))) True % 145.82/146.13 Clause #2776 (by clausification #[2775]): ∀ (a a_1 : int), Eq (Eq (times_times_int (bit0 a) a_1) (bit0 (times_times_int a a_1))) True % 145.82/146.13 Clause #2777 (by clausification #[2776]): ∀ (a a_1 : int), Eq (times_times_int (bit0 a) a_1) (bit0 (times_times_int a a_1)) % 145.82/146.13 Clause #2788 (by superposition #[2777, 1073]): ∀ (a : int), Eq (times_times_int (bit0 one_one_int) a) (bit0 a) % 145.82/146.13 Clause #2790 (by superposition #[2777, 1314]): ∀ (a a_1 : int), Eq (times_times_int (bit0 a) a_1) (bit0 (times_times_int a_1 a)) % 145.82/146.13 Clause #2822 (by superposition #[2788, 2777]): ∀ (a : int), Eq (times_times_int (bit0 (bit0 one_one_int)) a) (bit0 (bit0 a)) % 145.82/146.13 Clause #3009 (by superposition #[2822, 1314]): ∀ (a : int), Eq (times_times_int a (bit0 (bit0 one_one_int))) (bit0 (bit0 a)) % 145.82/146.13 Clause #3263 (by superposition #[2790, 2777]): ∀ (a a_1 : int), Eq (times_times_int (bit0 a) a_1) (times_times_int (bit0 a_1) a) % 145.82/146.13 Clause #3279 (by superposition #[3263, 1314]): ∀ (a a_1 : int), Eq (times_times_int a (bit0 a_1)) (times_times_int (bit0 a) a_1) % 145.82/146.13 Clause #3324 (by backward demodulation #[3279, 2790]): ∀ (a a_1 : int), Eq (times_times_int a (bit0 a_1)) (bit0 (times_times_int a_1 a)) % 145.82/146.13 Clause #5190 (by clausification #[124]): ∀ (a : int), Eq (∀ (Y Z : int), Eq (plus_plus_int a (plus_plus_int Y Z)) (plus_plus_int Y (plus_plus_int a Z))) True % 145.82/146.13 Clause #5191 (by clausification #[5190]): ∀ (a a_1 : int), % 145.82/146.13 Eq (∀ (Z : int), Eq (plus_plus_int a (plus_plus_int a_1 Z)) (plus_plus_int a_1 (plus_plus_int a Z))) True % 145.82/146.13 Clause #5192 (by clausification #[5191]): ∀ (a a_1 a_2 : int), Eq (Eq (plus_plus_int a (plus_plus_int a_1 a_2)) (plus_plus_int a_1 (plus_plus_int a a_2))) True % 145.82/146.13 Clause #5193 (by clausification #[5192]): ∀ (a a_1 a_2 : int), Eq (plus_plus_int a (plus_plus_int a_1 a_2)) (plus_plus_int a_1 (plus_plus_int a a_2)) % 145.82/146.13 Clause #5204 (by superposition #[5193, 969]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 (plus_plus_int a pls)) % 145.82/146.13 Clause #5243 (by forward demodulation #[5204, 969]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 145.82/146.13 Clause #6266 (by clausification #[146]): ∀ (a : int), % 145.82/146.13 Eq % 145.82/146.13 (∀ (Y_11 : int), Not (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int Y_11 Y_11)) zero_zero_int)) % 145.82/146.13 True % 145.82/146.13 Clause #6267 (by clausification #[6266]): ∀ (a a_1 : int), % 145.82/146.13 Eq (Not (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) zero_zero_int)) True % 145.82/146.13 Clause #6268 (by clausification #[6267]): ∀ (a a_1 : int), Eq (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) zero_zero_int) False % 145.82/146.13 Clause #6269 (by forward demodulation #[6268, 648]): ∀ (a a_1 : int), Eq (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) pls) False % 145.82/146.13 Clause #6292 (by superposition #[6269, 1075]): ∀ (a : int), Eq (ord_less_int (plus_plus_int one_one_int (times_times_int a a)) pls) False % 145.82/146.13 Clause #6467 (by clausification #[152]): ∀ (a : int), Eq (∀ (L : int), Eq (times_times_int (bit1 a) L) (plus_plus_int (bit0 (times_times_int a L)) L)) True % 145.82/146.13 Clause #6468 (by clausification #[6467]): ∀ (a a_1 : int), Eq (Eq (times_times_int (bit1 a) a_1) (plus_plus_int (bit0 (times_times_int a a_1)) a_1)) True % 145.82/146.15 Clause #6469 (by clausification #[6468]): ∀ (a a_1 : int), Eq (times_times_int (bit1 a) a_1) (plus_plus_int (bit0 (times_times_int a a_1)) a_1) % 145.82/146.15 Clause #6470 (by forward demodulation #[6469, 3324]): ∀ (a a_1 : int), Eq (times_times_int (bit1 a) a_1) (plus_plus_int (times_times_int a_1 (bit0 a)) a_1) % 145.82/146.15 Clause #6494 (by superposition #[6470, 1073]): ∀ (a : int), Eq (times_times_int (bit1 a) one_one_int) (plus_plus_int (bit0 a) one_one_int) % 145.82/146.15 Clause #6508 (by forward demodulation #[6494, 1075]): ∀ (a : int), Eq (bit1 a) (plus_plus_int (bit0 a) one_one_int) % 145.82/146.15 Clause #6520 (by superposition #[6508, 5243]): ∀ (a : int), Eq (plus_plus_int one_one_int (bit0 a)) (bit1 a) % 145.82/146.15 Clause #7727 (by clausification #[188]): ∀ (a : int), Eq (Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int a a)) True % 145.82/146.15 Clause #7728 (by clausification #[7727]): ∀ (a : int), Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int a a) % 145.82/146.15 Clause #7729 (by forward demodulation #[7728, 762]): ∀ (a : int), Eq (power_power_int a (number_number_of_nat (bit0 one_one_int))) (times_times_int a a) % 145.82/146.15 Clause #7730 (by forward demodulation #[7729, 2742]): ∀ (a : int), Eq (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) (times_times_int a a) % 145.82/146.15 Clause #29699 (by forward demodulation #[643, 1314]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int % 145.82/146.15 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 145.82/146.15 True % 145.82/146.15 Clause #29700 (by forward demodulation #[29699, 5243]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int % 145.82/146.15 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)))) % 145.82/146.15 True % 145.82/146.15 Clause #29701 (by forward demodulation #[29700, 1314]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int % 145.82/146.15 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))))) % 145.82/146.15 True % 145.82/146.15 Clause #29702 (by forward demodulation #[29701, 756]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))))) % 145.82/146.15 True % 145.82/146.15 Clause #29703 (by forward demodulation #[29702, 762]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int)))))) % 145.82/146.15 True % 145.82/146.15 Clause #29704 (by forward demodulation #[29703, 3009]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int (plus_plus_int one_one_int (bit0 (bit0 m))))) % 145.82/146.15 True % 145.82/146.15 Clause #29705 (by forward demodulation #[29704, 6520]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int zero_zero_int (bit1 (bit0 m)))) % 145.82/146.15 True % 145.82/146.15 Clause #29706 (by forward demodulation #[29705, 648]): Eq % 145.82/146.15 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 145.82/146.15 (times_times_int pls (bit1 (bit0 m)))) % 145.82/146.15 True % 145.82/146.15 Clause #29707 (by forward demodulation #[29706, 925]): Eq (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) pls) True % 145.82/146.15 Clause #29708 (by forward demodulation #[29707, 5243]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls))))) pls) True % 145.82/146.15 Clause #29709 (by forward demodulation #[29708, 762]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (number_number_of_nat (bit0 one_one_int)))) pls) True % 145.82/146.15 Clause #29710 (by forward demodulation #[29709, 2742]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (plus_plus_nat one_one_nat one_one_nat))) pls) True % 146.05/146.33 Clause #29711 (by forward demodulation #[29710, 7730]): Eq (ord_less_int (plus_plus_int one_one_int (times_times_int s s)) pls) True % 146.05/146.33 Clause #29712 (by superposition #[29711, 6292]): Eq True False % 146.05/146.33 Clause #29740 (by clausification #[29712]): False % 146.05/146.33 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------