%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM934_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:38 PM UTC 2025 % Result : Theorem 76.53s 76.70s % Output : Proof 76.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NUM934_5 : TPTP v9.2.0. Released v6.0.0. % 0.12/0.13 % Command : duper %s % 0.13/0.35 % Computer : n016.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:25:23 EDT 2025 % 0.13/0.35 % CPUTime : % 76.53/76.70 SZS status Theorem for theBenchmark.p % 76.53/76.70 SZS output start Proof for theBenchmark.p % 76.53/76.70 Clause #0 (by assumption #[]): Eq (ord_less_eq int (one_one int) m) True % 76.53/76.70 Clause #7 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit1 K) L1) (plus_plus int (bit0 (times_times int K L1)) L1)) True % 76.53/76.70 Clause #9 (by assumption #[]): Eq (∀ (L1 K : int), Eq (plus_plus int (bit0 K) (bit1 L1)) (bit1 (plus_plus int K L1))) True % 76.53/76.70 Clause #23 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 76.53/76.70 Clause #30 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 76.53/76.70 Clause #31 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit0 K) L1) (bit0 (times_times int K L1))) True % 76.53/76.70 Clause #48 (by assumption #[]): Eq (∀ (L K3 : int), Iff (ord_less_eq int (bit1 K3) (bit0 L)) (ord_less int K3 L)) True % 76.53/76.70 Clause #49 (by assumption #[]): Eq (∀ (L K3 : int), Iff (ord_less int (bit0 K3) (bit1 L)) (ord_less_eq int K3 L)) True % 76.53/76.70 Clause #57 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of int K) K) True % 76.53/76.70 Clause #59 (by assumption #[]): Eq (∀ (Z1 W1 : int), Iff (ord_less_eq int (plus_plus int W1 (one_one int)) Z1) (ord_less int W1 Z1)) True % 76.53/76.70 Clause #60 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int K pls) K) True % 76.53/76.70 Clause #61 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int pls K) K) True % 76.53/76.70 Clause #78 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 76.53/76.70 Clause #104 (by assumption #[]): Eq % 76.53/76.70 (Not % 76.53/76.70 (ord_less int (number_number_of int (bit0 (bit1 pls))) % 76.53/76.70 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)))) % 76.53/76.70 True % 76.53/76.70 Clause #112 (by clausification #[23]): Eq (bit0 pls) pls % 76.53/76.70 Clause #122 (by clausification #[57]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 76.53/76.70 Clause #123 (by clausification #[122]): ∀ (a : int), Eq (number_number_of int a) a % 76.53/76.70 Clause #126 (by clausification #[61]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 76.53/76.70 Clause #127 (by clausification #[126]): ∀ (a : int), Eq (plus_plus int pls a) a % 76.53/76.70 Clause #128 (by clausification #[60]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 76.53/76.70 Clause #129 (by clausification #[128]): ∀ (a : int), Eq (plus_plus int a pls) a % 76.53/76.70 Clause #137 (by clausification #[78]): Eq (one_one int) (number_number_of int (bit1 pls)) % 76.53/76.70 Clause #138 (by superposition #[137, 123]): Eq (one_one int) (bit1 pls) % 76.53/76.70 Clause #139 (by backward demodulation #[138, 0]): Eq (ord_less_eq int (bit1 pls) m) True % 76.53/76.70 Clause #141 (by clausification #[30]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 76.53/76.70 Clause #142 (by clausification #[141]): ∀ (a : int), Eq (times_times int pls a) pls % 76.53/76.70 Clause #179 (by clausification #[7]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit1 K) a) (plus_plus int (bit0 (times_times int K a)) a)) True % 76.53/76.70 Clause #180 (by clausification #[179]): ∀ (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 % 76.53/76.70 Clause #181 (by clausification #[180]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 76.53/76.70 Clause #183 (by superposition #[181, 142]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 76.53/76.70 Clause #184 (by forward demodulation #[183, 112]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 76.53/76.70 Clause #185 (by forward demodulation #[184, 127]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 76.53/76.70 Clause #195 (by clausification #[9]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit0 K) (bit1 a)) (bit1 (plus_plus int K a))) True % 76.53/76.70 Clause #196 (by clausification #[195]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 76.53/76.70 Clause #197 (by clausification #[196]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 76.53/76.70 Clause #464 (by clausification #[31]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit0 K) a) (bit0 (times_times int K a))) True % 76.53/76.70 Clause #465 (by clausification #[464]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 76.55/76.80 Clause #466 (by clausification #[465]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 76.55/76.80 Clause #483 (by superposition #[466, 185]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 76.55/76.80 Clause #490 (by superposition #[483, 466]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 76.55/76.80 Clause #790 (by clausification #[48]): ∀ (a : int), Eq (∀ (K3 : int), Iff (ord_less_eq int (bit1 K3) (bit0 a)) (ord_less int K3 a)) True % 76.55/76.80 Clause #791 (by clausification #[790]): ∀ (a a_1 : int), Eq (Iff (ord_less_eq int (bit1 a) (bit0 a_1)) (ord_less int a a_1)) True % 76.55/76.80 Clause #792 (by clausification #[791]): ∀ (a a_1 : int), Or (Eq (ord_less_eq int (bit1 a) (bit0 a_1)) True) (Eq (ord_less int a a_1) False) % 76.55/76.80 Clause #833 (by clausification #[49]): ∀ (a : int), Eq (∀ (K3 : int), Iff (ord_less int (bit0 K3) (bit1 a)) (ord_less_eq int K3 a)) True % 76.55/76.80 Clause #834 (by clausification #[833]): ∀ (a a_1 : int), Eq (Iff (ord_less int (bit0 a) (bit1 a_1)) (ord_less_eq int a a_1)) True % 76.55/76.80 Clause #835 (by clausification #[834]): ∀ (a a_1 : int), Or (Eq (ord_less int (bit0 a) (bit1 a_1)) True) (Eq (ord_less_eq int a a_1) False) % 76.55/76.80 Clause #1112 (by clausification #[59]): ∀ (a : int), Eq (∀ (W1 : int), Iff (ord_less_eq int (plus_plus int W1 (one_one int)) a) (ord_less int W1 a)) True % 76.55/76.80 Clause #1113 (by clausification #[1112]): ∀ (a a_1 : int), Eq (Iff (ord_less_eq int (plus_plus int a (one_one int)) a_1) (ord_less int a a_1)) True % 76.55/76.80 Clause #1115 (by clausification #[1113]): ∀ (a a_1 : int), Or (Eq (ord_less_eq int (plus_plus int a (one_one int)) a_1) False) (Eq (ord_less int a a_1) True) % 76.55/76.80 Clause #1776 (by clausification #[104]): Eq % 76.55/76.80 (ord_less int (number_number_of int (bit0 (bit1 pls))) % 76.55/76.80 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 76.55/76.80 False % 76.55/76.80 Clause #1777 (by forward demodulation #[1776, 138]): Eq % 76.55/76.80 (ord_less int (number_number_of int (bit0 (bit1 pls))) % 76.55/76.80 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls))) % 76.55/76.80 False % 76.55/76.80 Clause #1778 (by forward demodulation #[1777, 123]): Eq % 76.55/76.80 (ord_less int (number_number_of int (bit0 (bit1 pls))) % 76.55/76.80 (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls))) % 76.55/76.80 False % 76.55/76.80 Clause #1779 (by forward demodulation #[1778, 490]): Eq (ord_less int (number_number_of int (bit0 (bit1 pls))) (plus_plus int (bit0 (bit0 m)) (bit1 pls))) False % 76.55/76.80 Clause #1780 (by forward demodulation #[1779, 197]): Eq (ord_less int (number_number_of int (bit0 (bit1 pls))) (bit1 (plus_plus int (bit0 m) pls))) False % 76.55/76.80 Clause #1781 (by forward demodulation #[1780, 129]): Eq (ord_less int (number_number_of int (bit0 (bit1 pls))) (bit1 (bit0 m))) False % 76.55/76.80 Clause #1782 (by forward demodulation #[1781, 123]): Eq (ord_less int (bit0 (bit1 pls)) (bit1 (bit0 m))) False % 76.55/76.80 Clause #16326 (by forward demodulation #[1115, 138]): ∀ (a a_1 : int), Or (Eq (ord_less_eq int (plus_plus int a (bit1 pls)) a_1) False) (Eq (ord_less int a a_1) True) % 76.55/76.80 Clause #16338 (by superposition #[16326, 127]): ∀ (a : int), Or (Eq (ord_less_eq int (bit1 pls) a) False) (Eq (ord_less int pls a) True) % 76.55/76.80 Clause #16350 (by superposition #[16338, 139]): Or (Eq (ord_less int pls m) True) (Eq False True) % 76.55/76.80 Clause #16396 (by clausification #[16350]): Eq (ord_less int pls m) True % 76.55/76.80 Clause #16401 (by superposition #[16396, 792]): Or (Eq (ord_less_eq int (bit1 pls) (bit0 m)) True) (Eq True False) % 76.55/76.80 Clause #16646 (by clausification #[16401]): Eq (ord_less_eq int (bit1 pls) (bit0 m)) True % 76.55/76.80 Clause #16650 (by superposition #[16646, 835]): Or (Eq (ord_less int (bit0 (bit1 pls)) (bit1 (bit0 m))) True) (Eq True False) % 76.55/76.80 Clause #18034 (by clausification #[16650]): Eq (ord_less int (bit0 (bit1 pls)) (bit1 (bit0 m))) True % 76.55/76.80 Clause #18035 (by superposition #[18034, 1782]): Eq True False % 76.55/76.80 Clause #18054 (by clausification #[18035]): False % 76.55/76.80 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------