%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM958_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n024.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:40 PM UTC 2025 % Result : Theorem 9.67s 9.90s % Output : Proof 9.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NUM958_5 : TPTP v9.2.0. Released v6.0.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n024.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:20:53 EDT 2025 % 0.13/0.34 % CPUTime : % 9.67/9.90 SZS status Theorem for theBenchmark.p % 9.67/9.90 SZS output start Proof for theBenchmark.p % 9.67/9.90 Clause #0 (by assumption #[]): Eq % 9.67/9.90 (Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.90 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.67/9.90 t)) % 9.67/9.90 True % 9.67/9.90 Clause #12 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit1 K) L1) (plus_plus int (bit0 (times_times int K L1)) L1)) True % 9.67/9.90 Clause #13 (by assumption #[]): Eq (∀ (A : Type), number_ring A → Eq (number_number_of A (bit1 pls)) (one_one A)) True % 9.67/9.90 Clause #18 (by assumption #[]): Eq (∀ (L1 K : int), Eq (plus_plus int (bit0 K) (bit1 L1)) (bit1 (plus_plus int K L1))) True % 9.67/9.90 Clause #28 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 9.67/9.90 Clause #32 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 9.67/9.90 Clause #33 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit0 K) L1) (bit0 (times_times int K L1))) True % 9.67/9.90 Clause #76 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of int K) K) True % 9.67/9.90 Clause #80 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int K pls) K) True % 9.67/9.90 Clause #81 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int pls K) K) True % 9.67/9.90 Clause #100 (by assumption #[]): Eq (number_ring int) True % 9.67/9.90 Clause #111 (by assumption #[]): Eq % 9.67/9.90 (Not % 9.67/9.90 (Eq % 9.67/9.90 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.67/9.90 t) % 9.67/9.90 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)))) % 9.67/9.90 True % 9.67/9.90 Clause #112 (by clausification #[0]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.90 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 9.67/9.90 Clause #117 (by clausification #[28]): Eq (bit0 pls) pls % 9.67/9.90 Clause #126 (by clausification #[76]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 9.67/9.90 Clause #127 (by clausification #[126]): ∀ (a : int), Eq (number_number_of int a) a % 9.67/9.90 Clause #128 (by backward demodulation #[127, 112]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.90 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) t) % 9.67/9.90 Clause #144 (by clausification #[81]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 9.67/9.90 Clause #145 (by clausification #[144]): ∀ (a : int), Eq (plus_plus int pls a) a % 9.67/9.90 Clause #146 (by clausification #[80]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 9.67/9.90 Clause #147 (by clausification #[146]): ∀ (a : int), Eq (plus_plus int a pls) a % 9.67/9.90 Clause #149 (by clausification #[32]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 9.67/9.90 Clause #150 (by clausification #[149]): ∀ (a : int), Eq (times_times int pls a) pls % 9.67/9.90 Clause #172 (by clausification #[13]): ∀ (a : Type), Eq (number_ring a → Eq (number_number_of a (bit1 pls)) (one_one a)) True % 9.67/9.90 Clause #173 (by clausification #[172]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (Eq (number_number_of a (bit1 pls)) (one_one a)) True) % 9.67/9.90 Clause #174 (by clausification #[173]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (number_number_of a (bit1 pls)) (one_one a)) % 9.67/9.90 Clause #175 (by superposition #[174, 100]): Or (Eq (number_number_of int (bit1 pls)) (one_one int)) (Eq False True) % 9.67/9.90 Clause #176 (by clausification #[175]): Eq (number_number_of int (bit1 pls)) (one_one int) % 9.67/9.90 Clause #177 (by superposition #[176, 127]): Eq (one_one int) (bit1 pls) % 9.67/9.90 Clause #266 (by clausification #[12]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit1 K) a) (plus_plus int (bit0 (times_times int K a)) a)) True % 9.67/9.90 Clause #267 (by clausification #[266]): ∀ (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 % 9.67/9.90 Clause #268 (by clausification #[267]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 9.67/9.90 Clause #270 (by superposition #[268, 150]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 9.67/9.91 Clause #271 (by forward demodulation #[270, 117]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 9.67/9.91 Clause #272 (by forward demodulation #[271, 145]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 9.67/9.91 Clause #352 (by clausification #[18]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit0 K) (bit1 a)) (bit1 (plus_plus int K a))) True % 9.67/9.91 Clause #353 (by clausification #[352]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 9.67/9.91 Clause #354 (by clausification #[353]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 9.67/9.91 Clause #459 (by clausification #[33]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit0 K) a) (bit0 (times_times int K a))) True % 9.67/9.91 Clause #460 (by clausification #[459]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 9.67/9.91 Clause #461 (by clausification #[460]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 9.67/9.91 Clause #489 (by superposition #[461, 272]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 9.67/9.91 Clause #498 (by superposition #[489, 461]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 9.67/9.91 Clause #1985 (by clausification #[111]): Eq % 9.67/9.91 (Eq % 9.67/9.91 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.67/9.91 t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 9.67/9.91 False % 9.67/9.91 Clause #1986 (by clausification #[1985]): Ne (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1987 (by forward demodulation #[1986, 177]): Ne (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1988 (by forward demodulation #[1987, 127]): Ne (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1989 (by forward demodulation #[1988, 498]): Ne (times_times int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1990 (by forward demodulation #[1989, 354]): Ne (times_times int (bit1 (plus_plus int (bit0 m) pls)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1991 (by forward demodulation #[1990, 147]): Ne (times_times int (bit1 (bit0 m)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 9.67/9.91 Clause #1992 (by forward demodulation #[1991, 177]): Ne (times_times int (bit1 (bit0 m)) t) % 9.67/9.91 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.91 Clause #1996 (by forward demodulation #[128, 177]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.91 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) t) % 9.67/9.91 Clause #1997 (by forward demodulation #[1996, 177]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.91 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t) % 9.67/9.91 Clause #1998 (by forward demodulation #[1997, 498]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.91 (times_times int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) t) % 9.67/9.91 Clause #1999 (by forward demodulation #[1998, 354]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.91 (times_times int (bit1 (plus_plus int (bit0 m) pls)) t) % 9.67/9.91 Clause #2000 (by forward demodulation #[1999, 147]): Eq (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 9.67/9.92 (times_times int (bit1 (bit0 m)) t) % 9.67/9.92 Clause #2001 (by forward contextual literal cutting #[2000, 1992]): False % 9.67/9.92 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------