%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM994_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:42 PM UTC 2025 % Result : Theorem 8.89s 9.09s % Output : Proof 8.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM994_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n007.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 07:52:53 EDT 2025 % 0.14/0.35 % CPUTime : % 8.89/9.09 SZS status Theorem for theBenchmark.p % 8.89/9.09 SZS output start Proof for theBenchmark.p % 8.89/9.09 Clause #2 (by assumption #[]): Eq (∀ (K : int), Iff (ord_less_eq int pls (bit0 K)) (ord_less_eq int pls K)) True % 8.89/9.09 Clause #29 (by assumption #[]): Eq (∀ (L1 K3 : int), Eq (times_times int (bit0 K3) L1) (bit0 (times_times int K3 L1))) True % 8.89/9.09 Clause #33 (by assumption #[]): Eq (∀ (K3 : int), Eq (number_number_of int K3) K3) True % 8.89/9.09 Clause #36 (by assumption #[]): Eq (Eq pls (zero_zero int)) True % 8.89/9.09 Clause #42 (by assumption #[]): Eq (∀ (A : Type), ordere142940540dd_abs A → ∀ (A1 : A), ord_less_eq A (zero_zero A) (abs_abs A A1)) True % 8.89/9.09 Clause #46 (by assumption #[]): Eq (∀ (A : Type), number_ring A → ∀ (A1 : A), Eq (times_times A (number_number_of A (bit1 pls)) A1) A1) True % 8.89/9.09 Clause #93 (by assumption #[]): Eq (ordere142940540dd_abs int) True % 8.89/9.09 Clause #108 (by assumption #[]): Eq (number_ring int) True % 8.89/9.09 Clause #122 (by assumption #[]): Eq % 8.89/9.09 (Not % 8.89/9.09 (And (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int v))) % 8.89/9.09 (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))))) % 8.89/9.09 True % 8.89/9.09 Clause #137 (by clausification #[2]): ∀ (a : int), Eq (Iff (ord_less_eq int pls (bit0 a)) (ord_less_eq int pls a)) True % 8.89/9.09 Clause #138 (by clausification #[137]): ∀ (a : int), Or (Eq (ord_less_eq int pls (bit0 a)) True) (Eq (ord_less_eq int pls a) False) % 8.89/9.09 Clause #156 (by clausification #[36]): Eq pls (zero_zero int) % 8.89/9.09 Clause #190 (by clausification #[33]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 8.89/9.09 Clause #191 (by clausification #[190]): ∀ (a : int), Eq (number_number_of int a) a % 8.89/9.09 Clause #461 (by clausification #[29]): ∀ (a : int), Eq (∀ (K3 : int), Eq (times_times int (bit0 K3) a) (bit0 (times_times int K3 a))) True % 8.89/9.09 Clause #462 (by clausification #[461]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 8.89/9.09 Clause #463 (by clausification #[462]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 8.89/9.09 Clause #522 (by clausification #[42]): ∀ (a : Type), Eq (ordere142940540dd_abs a → ∀ (A1 : a), ord_less_eq a (zero_zero a) (abs_abs a A1)) True % 8.89/9.09 Clause #523 (by clausification #[522]): ∀ (a : Type), Or (Eq (ordere142940540dd_abs a) False) (Eq (∀ (A1 : a), ord_less_eq a (zero_zero a) (abs_abs a A1)) True) % 8.89/9.09 Clause #524 (by clausification #[523]): ∀ (a : Type) (a_1 : a), Or (Eq (ordere142940540dd_abs a) False) (Eq (ord_less_eq a (zero_zero a) (abs_abs a a_1)) True) % 8.89/9.09 Clause #525 (by superposition #[524, 93]): ∀ (a : int), Or (Eq (ord_less_eq int (zero_zero int) (abs_abs int a)) True) (Eq False True) % 8.89/9.09 Clause #534 (by clausification #[525]): ∀ (a : int), Eq (ord_less_eq int (zero_zero int) (abs_abs int a)) True % 8.89/9.09 Clause #535 (by forward demodulation #[534, 156]): ∀ (a : int), Eq (ord_less_eq int pls (abs_abs int a)) True % 8.89/9.09 Clause #536 (by superposition #[535, 138]): ∀ (a : int), Or (Eq (ord_less_eq int pls (bit0 (abs_abs int a))) True) (Eq True False) % 8.89/9.09 Clause #548 (by clausification #[536]): ∀ (a : int), Eq (ord_less_eq int pls (bit0 (abs_abs int a))) True % 8.89/9.09 Clause #676 (by clausification #[46]): ∀ (a : Type), Eq (number_ring a → ∀ (A1 : a), Eq (times_times a (number_number_of a (bit1 pls)) A1) A1) True % 8.89/9.09 Clause #677 (by clausification #[676]): ∀ (a : Type), % 8.89/9.09 Or (Eq (number_ring a) False) (Eq (∀ (A1 : a), Eq (times_times a (number_number_of a (bit1 pls)) A1) A1) True) % 8.89/9.09 Clause #678 (by clausification #[677]): ∀ (a : Type) (a_1 : a), % 8.89/9.09 Or (Eq (number_ring a) False) (Eq (Eq (times_times a (number_number_of a (bit1 pls)) a_1) a_1) True) % 8.89/9.09 Clause #679 (by clausification #[678]): ∀ (a : Type) (a_1 : a), Or (Eq (number_ring a) False) (Eq (times_times a (number_number_of a (bit1 pls)) a_1) a_1) % 8.89/9.09 Clause #680 (by superposition #[679, 108]): ∀ (a : int), Or (Eq (times_times int (number_number_of int (bit1 pls)) a) a) (Eq False True) % 8.89/9.09 Clause #681 (by clausification #[680]): ∀ (a : int), Eq (times_times int (number_number_of int (bit1 pls)) a) a % 8.89/9.09 Clause #682 (by forward demodulation #[681, 191]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 8.94/9.11 Clause #683 (by superposition #[682, 463]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 8.94/9.11 Clause #1841 (by clausification #[122]): Eq % 8.94/9.11 (And (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int v))) % 8.94/9.11 (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w)))) % 8.94/9.11 False % 8.94/9.11 Clause #1842 (by clausification #[1841]): Or % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int v))) % 8.94/9.11 False) % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) % 8.94/9.11 False) % 8.94/9.11 Clause #1843 (by forward demodulation #[1842, 191]): Or (Eq (ord_less_eq int (zero_zero int) (times_times int (bit0 (bit1 pls)) (abs_abs int v))) False) % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) % 8.94/9.11 False) % 8.94/9.11 Clause #1844 (by forward demodulation #[1843, 683]): Or (Eq (ord_less_eq int (zero_zero int) (bit0 (abs_abs int v))) False) % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) % 8.94/9.11 False) % 8.94/9.11 Clause #1845 (by forward demodulation #[1844, 156]): Or (Eq (ord_less_eq int pls (bit0 (abs_abs int v))) False) % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) % 8.94/9.11 False) % 8.94/9.11 Clause #1846 (by forward demodulation #[1845, 548]): Or (Eq True False) % 8.94/9.11 (Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) % 8.94/9.11 False) % 8.94/9.11 Clause #1847 (by clausification #[1846]): Eq (ord_less_eq int (zero_zero int) (times_times int (number_number_of int (bit0 (bit1 pls))) (abs_abs int w))) False % 8.94/9.11 Clause #1848 (by forward demodulation #[1847, 191]): Eq (ord_less_eq int (zero_zero int) (times_times int (bit0 (bit1 pls)) (abs_abs int w))) False % 8.94/9.11 Clause #1849 (by forward demodulation #[1848, 683]): Eq (ord_less_eq int (zero_zero int) (bit0 (abs_abs int w))) False % 8.94/9.11 Clause #1850 (by forward demodulation #[1849, 156]): Eq (ord_less_eq int pls (bit0 (abs_abs int w))) False % 8.94/9.11 Clause #1851 (by superposition #[1850, 548]): Eq False True % 8.94/9.11 Clause #1852 (by clausification #[1851]): False % 8.94/9.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------