%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM973_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:41 PM UTC 2025 % Result : Theorem 79.23s 79.45s % Output : Proof 79.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM973_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.35 % Computer : n014.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 07:21:08 EDT 2025 % 0.13/0.35 % CPUTime : % 79.23/79.45 SZS status Theorem for theBenchmark.p % 79.23/79.45 SZS output start Proof for theBenchmark.p % 79.23/79.45 Clause #0 (by assumption #[]): Eq (Eq t (one_one int)) True % 79.23/79.45 Clause #3 (by assumption #[]): Eq % 79.23/79.45 (∀ (B1 : Type), % 79.23/79.45 And (monoid_mult B1) (number B1) → % 79.23/79.45 ∀ (W : int), % 79.23/79.45 Eq (power_power B1 (number_number_of B1 W) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times B1 (number_number_of B1 W) (number_number_of B1 W))) % 79.23/79.45 True % 79.23/79.45 Clause #9 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (times_times int (bit1 K1) L1) (plus_plus int (bit0 (times_times int K1 L1)) L1)) True % 79.23/79.45 Clause #11 (by assumption #[]): Eq % 79.23/79.45 (Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 79.23/79.45 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 79.23/79.45 t)) % 79.23/79.45 True % 79.23/79.45 Clause #24 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 79.23/79.45 Clause #25 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 79.23/79.45 Clause #26 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (times_times int (bit0 K1) L1) (bit0 (times_times int K1 L1))) True % 79.23/79.45 Clause #36 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (plus_plus int (bit0 K1) (bit1 L1)) (bit1 (plus_plus int K1 L1))) True % 79.23/79.45 Clause #45 (by assumption #[]): Eq (∀ (K1 : int), Eq (number_number_of int K1) K1) True % 79.23/79.45 Clause #47 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int K1 pls) K1) True % 79.23/79.45 Clause #48 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int pls K1) K1) True % 79.23/79.45 Clause #62 (by assumption #[]): Eq (∀ (A : Type), number_ring A → ∀ (A1 : A), Eq (times_times A A1 (number_number_of A (bit1 pls))) A1) True % 79.23/79.45 Clause #65 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 79.23/79.45 Clause #80 (by assumption #[]): Eq (∀ (A : Type), monoid_mult A → ∀ (N : nat), Eq (power_power A (one_one A) N) (one_one A)) True % 79.23/79.45 Clause #102 (by assumption #[]): Eq (monoid_mult int) True % 79.23/79.45 Clause #105 (by assumption #[]): Eq (number_ring int) True % 79.23/79.45 Clause #107 (by assumption #[]): Eq (number int) True % 79.23/79.45 Clause #127 (by assumption #[]): Eq % 79.23/79.45 (Not % 79.23/79.45 (Exists fun X => % 79.23/79.45 Exists fun Y => % 79.23/79.45 Eq % 79.23/79.45 (plus_plus int (power_power int X (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (power_power int Y (number_number_of nat (bit0 (bit1 pls))))) % 79.23/79.45 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)))) % 79.23/79.45 True % 79.23/79.45 Clause #128 (by clausification #[0]): Eq t (one_one int) % 79.23/79.45 Clause #131 (by clausification #[3]): ∀ (a : Type), % 79.23/79.45 Eq % 79.23/79.45 (And (monoid_mult a) (number a) → % 79.23/79.45 ∀ (W : int), % 79.23/79.45 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times a (number_number_of a W) (number_number_of a W))) % 79.23/79.45 True % 79.23/79.45 Clause #132 (by clausification #[131]): ∀ (a : Type), % 79.23/79.45 Or (Eq (And (monoid_mult a) (number a)) False) % 79.23/79.45 (Eq % 79.23/79.45 (∀ (W : int), % 79.23/79.45 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times a (number_number_of a W) (number_number_of a W))) % 79.23/79.45 True) % 79.23/79.45 Clause #133 (by clausification #[132]): ∀ (a : Type), % 79.23/79.45 Or % 79.23/79.45 (Eq % 79.23/79.45 (∀ (W : int), % 79.23/79.45 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times a (number_number_of a W) (number_number_of a W))) % 79.23/79.45 True) % 79.23/79.45 (Or (Eq (monoid_mult a) False) (Eq (number a) False)) % 79.23/79.45 Clause #134 (by clausification #[133]): ∀ (a : Type) (a_1 : int), % 79.23/79.45 Or (Eq (monoid_mult a) False) % 79.23/79.45 (Or (Eq (number a) False) % 79.23/79.45 (Eq % 79.23/79.45 (Eq (power_power a (number_number_of a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times a (number_number_of a a_1) (number_number_of a a_1))) % 79.23/79.45 True)) % 79.23/79.45 Clause #135 (by clausification #[134]): ∀ (a : Type) (a_1 : int), % 79.23/79.45 Or (Eq (monoid_mult a) False) % 79.23/79.45 (Or (Eq (number a) False) % 79.23/79.45 (Eq (power_power a (number_number_of a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.45 (times_times a (number_number_of a a_1) (number_number_of a a_1)))) % 79.23/79.45 Clause #138 (by superposition #[135, 102]): ∀ (a : int), % 79.23/79.47 Or (Eq (number int) False) % 79.23/79.47 (Or % 79.23/79.47 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 79.23/79.47 (times_times int (number_number_of int a) (number_number_of int a))) % 79.23/79.47 (Eq False True)) % 79.23/79.47 Clause #148 (by clausification #[24]): Eq (bit0 pls) pls % 79.23/79.47 Clause #153 (by clausification #[45]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 79.23/79.47 Clause #154 (by clausification #[153]): ∀ (a : int), Eq (number_number_of int a) a % 79.23/79.47 Clause #165 (by clausification #[47]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 79.23/79.47 Clause #166 (by clausification #[165]): ∀ (a : int), Eq (plus_plus int a pls) a % 79.23/79.47 Clause #167 (by clausification #[25]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 79.23/79.47 Clause #168 (by clausification #[167]): ∀ (a : int), Eq (times_times int pls a) pls % 79.23/79.47 Clause #169 (by clausification #[48]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 79.23/79.47 Clause #170 (by clausification #[169]): ∀ (a : int), Eq (plus_plus int pls a) a % 79.23/79.47 Clause #179 (by clausification #[65]): Eq (one_one int) (number_number_of int (bit1 pls)) % 79.23/79.47 Clause #180 (by forward demodulation #[179, 128]): Eq t (number_number_of int (bit1 pls)) % 79.23/79.47 Clause #181 (by superposition #[180, 154]): Eq t (bit1 pls) % 79.23/79.47 Clause #206 (by clausification #[9]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit1 K1) a) (plus_plus int (bit0 (times_times int K1 a)) a)) True % 79.23/79.47 Clause #207 (by clausification #[206]): ∀ (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 % 79.23/79.47 Clause #208 (by clausification #[207]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 79.23/79.47 Clause #210 (by superposition #[208, 168]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 79.23/79.47 Clause #211 (by forward demodulation #[210, 181]): ∀ (a : int), Eq (times_times int t a) (plus_plus int (bit0 pls) a) % 79.23/79.47 Clause #212 (by forward demodulation #[211, 148]): ∀ (a : int), Eq (times_times int t a) (plus_plus int pls a) % 79.23/79.47 Clause #213 (by forward demodulation #[212, 170]): ∀ (a : int), Eq (times_times int t a) a % 79.23/79.47 Clause #239 (by clausification #[11]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 79.23/79.47 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 79.23/79.47 Clause #240 (by forward demodulation #[239, 128]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) t) % 79.23/79.47 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 79.23/79.47 Clause #241 (by forward demodulation #[240, 181]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 t))) t) % 79.23/79.47 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 79.23/79.47 Clause #242 (by forward demodulation #[241, 128]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 t))) t) % 79.23/79.47 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) t) t) % 79.23/79.47 Clause #243 (by forward demodulation #[242, 154]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 t))) t) % 79.23/79.47 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) t) t) % 79.23/79.47 Clause #244 (by forward demodulation #[243, 181]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 t))) t) % 79.23/79.47 (times_times int (plus_plus int (times_times int (bit0 (bit0 t)) m) t) t) % 79.23/79.47 Clause #394 (by clausification #[26]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit0 K1) a) (bit0 (times_times int K1 a))) True % 79.23/79.47 Clause #395 (by clausification #[394]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 79.23/79.47 Clause #396 (by clausification #[395]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 79.23/79.47 Clause #412 (by superposition #[396, 213]): ∀ (a : int), Eq (times_times int (bit0 t) a) (bit0 a) % 79.23/79.47 Clause #416 (by superposition #[412, 396]): ∀ (a : int), Eq (times_times int (bit0 (bit0 t)) a) (bit0 (bit0 a)) % 79.32/79.49 Clause #439 (by backward demodulation #[416, 244]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 t))) t) % 79.32/79.49 (times_times int (plus_plus int (bit0 (bit0 m)) t) t) % 79.32/79.49 Clause #589 (by clausification #[36]): ∀ (a : int), Eq (∀ (K1 : int), Eq (plus_plus int (bit0 K1) (bit1 a)) (bit1 (plus_plus int K1 a))) True % 79.32/79.49 Clause #590 (by clausification #[589]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 79.32/79.49 Clause #591 (by clausification #[590]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 79.32/79.49 Clause #593 (by superposition #[591, 181]): ∀ (a : int), Eq (plus_plus int (bit0 a) t) (bit1 (plus_plus int a pls)) % 79.32/79.49 Clause #598 (by forward demodulation #[593, 166]): ∀ (a : int), Eq (plus_plus int (bit0 a) t) (bit1 a) % 79.32/79.49 Clause #1155 (by clausification #[62]): ∀ (a : Type), Eq (number_ring a → ∀ (A1 : a), Eq (times_times a A1 (number_number_of a (bit1 pls))) A1) True % 79.32/79.49 Clause #1156 (by clausification #[1155]): ∀ (a : Type), % 79.32/79.49 Or (Eq (number_ring a) False) (Eq (∀ (A1 : a), Eq (times_times a A1 (number_number_of a (bit1 pls))) A1) True) % 79.32/79.49 Clause #1157 (by clausification #[1156]): ∀ (a : Type) (a_1 : a), % 79.32/79.49 Or (Eq (number_ring a) False) (Eq (Eq (times_times a a_1 (number_number_of a (bit1 pls))) a_1) True) % 79.32/79.49 Clause #1158 (by clausification #[1157]): ∀ (a : Type) (a_1 : a), Or (Eq (number_ring a) False) (Eq (times_times a a_1 (number_number_of a (bit1 pls))) a_1) % 79.32/79.49 Clause #1159 (by forward demodulation #[1158, 181]): ∀ (a : Type) (a_1 : a), Or (Eq (number_ring a) False) (Eq (times_times a a_1 (number_number_of a t)) a_1) % 79.32/79.49 Clause #1161 (by superposition #[1159, 105]): ∀ (a : int), Or (Eq (times_times int a (number_number_of int t)) a) (Eq False True) % 79.32/79.49 Clause #1162 (by clausification #[1161]): ∀ (a : int), Eq (times_times int a (number_number_of int t)) a % 79.32/79.49 Clause #1163 (by forward demodulation #[1162, 154]): ∀ (a : int), Eq (times_times int a t) a % 79.32/79.49 Clause #1549 (by clausification #[80]): ∀ (a : Type), Eq (monoid_mult a → ∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True % 79.32/79.49 Clause #1550 (by clausification #[1549]): ∀ (a : Type), Or (Eq (monoid_mult a) False) (Eq (∀ (N : nat), Eq (power_power a (one_one a) N) (one_one a)) True) % 79.32/79.49 Clause #1551 (by clausification #[1550]): ∀ (a : Type) (a_1 : nat), Or (Eq (monoid_mult a) False) (Eq (Eq (power_power a (one_one a) a_1) (one_one a)) True) % 79.32/79.49 Clause #1552 (by clausification #[1551]): ∀ (a : Type) (a_1 : nat), Or (Eq (monoid_mult a) False) (Eq (power_power a (one_one a) a_1) (one_one a)) % 79.32/79.49 Clause #1555 (by superposition #[1552, 102]): ∀ (a : nat), Or (Eq (power_power int (one_one int) a) (one_one int)) (Eq False True) % 79.32/79.49 Clause #1556 (by clausification #[1555]): ∀ (a : nat), Eq (power_power int (one_one int) a) (one_one int) % 79.32/79.49 Clause #1557 (by forward demodulation #[1556, 128]): ∀ (a : nat), Eq (power_power int t a) (one_one int) % 79.32/79.49 Clause #1558 (by forward demodulation #[1557, 128]): ∀ (a : nat), Eq (power_power int t a) t % 79.32/79.49 Clause #1832 (by clausification #[127]): Eq % 79.32/79.49 (Exists fun X => % 79.32/79.49 Exists fun Y => % 79.32/79.49 Eq % 79.32/79.49 (plus_plus int (power_power int X (number_number_of nat (bit0 (bit1 pls)))) % 79.32/79.49 (power_power int Y (number_number_of nat (bit0 (bit1 pls))))) % 79.32/79.49 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 79.32/79.49 False % 79.32/79.49 Clause #1833 (by clausification #[1832]): ∀ (a : int), % 79.32/79.49 Eq % 79.32/79.49 (Exists fun Y => % 79.32/79.49 Eq % 79.32/79.49 (plus_plus int (power_power int a (number_number_of nat (bit0 (bit1 pls)))) % 79.32/79.49 (power_power int Y (number_number_of nat (bit0 (bit1 pls))))) % 79.32/79.49 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 79.32/79.49 False % 79.32/79.49 Clause #1834 (by clausification #[1833]): ∀ (a a_1 : int), % 79.32/79.49 Eq % 79.32/79.49 (Eq % 79.32/79.49 (plus_plus int (power_power int a (number_number_of nat (bit0 (bit1 pls)))) % 79.32/79.49 (power_power int a_1 (number_number_of nat (bit0 (bit1 pls))))) % 79.32/79.49 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 79.35/79.51 False % 79.35/79.51 Clause #1835 (by clausification #[1834]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 (bit1 pls)))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 (bit1 pls))))) % 79.35/79.51 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 79.35/79.51 Clause #1836 (by forward demodulation #[1835, 181]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 (bit1 pls)))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 79.35/79.51 Clause #1837 (by forward demodulation #[1836, 181]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 79.35/79.51 Clause #1838 (by forward demodulation #[1837, 128]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) t) % 79.35/79.51 Clause #1839 (by forward demodulation #[1838, 154]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) t) % 79.35/79.51 Clause #1840 (by forward demodulation #[1839, 181]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (times_times int (bit0 (bit0 t)) m) t) % 79.35/79.51 Clause #1841 (by forward demodulation #[1840, 416]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (plus_plus int (bit0 (bit0 m)) t) % 79.35/79.51 Clause #1842 (by forward demodulation #[1841, 598]): ∀ (a a_1 : int), % 79.35/79.51 Ne % 79.35/79.51 (plus_plus int (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (power_power int a_1 (number_number_of nat (bit0 t)))) % 79.35/79.51 (bit1 (bit0 m)) % 79.35/79.51 Clause #1846 (by superposition #[1842, 1558]): ∀ (a : int), Ne (plus_plus int (power_power int a (number_number_of nat (bit0 t))) t) (bit1 (bit0 m)) % 79.35/79.51 Clause #1883 (by clausification #[138]): ∀ (a : int), % 79.35/79.51 Or (Eq (number int) False) % 79.35/79.51 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 79.35/79.51 (times_times int (number_number_of int a) (number_number_of int a))) % 79.35/79.51 Clause #1884 (by forward demodulation #[1883, 107]): ∀ (a : int), % 79.35/79.51 Or (Eq True False) % 79.35/79.51 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 79.35/79.51 (times_times int (number_number_of int a) (number_number_of int a))) % 79.35/79.51 Clause #1885 (by clausification #[1884]): ∀ (a : int), % 79.35/79.51 Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 79.35/79.51 (times_times int (number_number_of int a) (number_number_of int a)) % 79.35/79.51 Clause #1886 (by forward demodulation #[1885, 181]): ∀ (a : int), % 79.35/79.51 Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 t))) % 79.35/79.51 (times_times int (number_number_of int a) (number_number_of int a)) % 79.35/79.51 Clause #1887 (by forward demodulation #[1886, 154]): ∀ (a : int), % 79.35/79.51 Eq (power_power int a (number_number_of nat (bit0 t))) % 79.35/79.51 (times_times int (number_number_of int a) (number_number_of int a)) % 79.35/79.51 Clause #1888 (by forward demodulation #[1887, 154]): ∀ (a : int), Eq (power_power int a (number_number_of nat (bit0 t))) (times_times int (number_number_of int a) a) % 79.35/79.51 Clause #1889 (by forward demodulation #[1888, 154]): ∀ (a : int), Eq (power_power int a (number_number_of nat (bit0 t))) (times_times int a a) % 79.35/79.51 Clause #3590 (by forward demodulation #[439, 1889]): Eq (plus_plus int (times_times int s s) t) (times_times int (plus_plus int (bit0 (bit0 m)) t) t) % 79.35/79.51 Clause #3591 (by forward demodulation #[3590, 598]): Eq (plus_plus int (times_times int s s) t) (times_times int (bit1 (bit0 m)) t) % 79.37/79.58 Clause #3592 (by forward demodulation #[3591, 1163]): Eq (plus_plus int (times_times int s s) t) (bit1 (bit0 m)) % 79.37/79.58 Clause #14558 (by superposition #[1846, 1889]): ∀ (a : int), Ne (plus_plus int (times_times int a a) t) (bit1 (bit0 m)) % 79.37/79.58 Clause #14562 (by backward contextual literal cutting #[14558, 3592]): False % 79.37/79.58 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------