%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM932_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 7.99s 8.18s % Output : Proof 7.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM932_5 : TPTP v9.2.0. Released v6.0.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n008.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 08:56:53 EDT 2025 % 0.14/0.34 % CPUTime : % 7.99/8.18 SZS status Theorem for theBenchmark.p % 7.99/8.18 SZS output start Proof for theBenchmark.p % 7.99/8.18 Clause #0 (by assumption #[]): Eq (ord_less_eq int m (zero_zero int)) True % 7.99/8.18 Clause #8 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit1 K) L1) (plus_plus int (bit0 (times_times int K L1)) L1)) True % 7.99/8.18 Clause #10 (by assumption #[]): Eq (∀ (L1 K : int), Eq (plus_plus int (bit0 K) (bit1 L1)) (bit1 (plus_plus int K L1))) True % 7.99/8.18 Clause #13 (by assumption #[]): Eq (∀ (K3 : int), Iff (ord_less_eq int (bit0 K3) pls) (ord_less_eq int K3 pls)) True % 7.99/8.18 Clause #25 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 7.99/8.18 Clause #26 (by assumption #[]): Eq (∀ (L K3 : int), Iff (ord_less_eq int (bit1 K3) (bit1 L)) (ord_less_eq int K3 L)) True % 7.99/8.18 Clause #29 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 7.99/8.18 Clause #30 (by assumption #[]): Eq (∀ (L1 K : int), Eq (times_times int (bit0 K) L1) (bit0 (times_times int K L1))) True % 7.99/8.18 Clause #43 (by assumption #[]): Eq (Eq pls (zero_zero int)) True % 7.99/8.18 Clause #45 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of int K) K) True % 7.99/8.18 Clause #50 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int K pls) K) True % 7.99/8.18 Clause #51 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int pls K) K) True % 7.99/8.18 Clause #67 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 7.99/8.18 Clause #113 (by assumption #[]): Eq % 7.99/8.18 (Not % 7.99/8.18 (ord_less_eq int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.99/8.18 (one_one int))) % 7.99/8.18 True % 7.99/8.18 Clause #121 (by clausification #[25]): Eq (bit0 pls) pls % 7.99/8.18 Clause #122 (by clausification #[43]): Eq pls (zero_zero int) % 7.99/8.18 Clause #123 (by backward demodulation #[122, 0]): Eq (ord_less_eq int m pls) True % 7.99/8.18 Clause #135 (by clausification #[45]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 7.99/8.18 Clause #136 (by clausification #[135]): ∀ (a : int), Eq (number_number_of int a) a % 7.99/8.18 Clause #148 (by clausification #[29]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 7.99/8.18 Clause #149 (by clausification #[148]): ∀ (a : int), Eq (times_times int pls a) pls % 7.99/8.18 Clause #151 (by clausification #[51]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 7.99/8.18 Clause #152 (by clausification #[151]): ∀ (a : int), Eq (plus_plus int pls a) a % 7.99/8.18 Clause #160 (by clausification #[50]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 7.99/8.18 Clause #161 (by clausification #[160]): ∀ (a : int), Eq (plus_plus int a pls) a % 7.99/8.18 Clause #162 (by clausification #[67]): Eq (one_one int) (number_number_of int (bit1 pls)) % 7.99/8.18 Clause #163 (by superposition #[162, 136]): Eq (one_one int) (bit1 pls) % 7.99/8.18 Clause #184 (by clausification #[8]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit1 K) a) (plus_plus int (bit0 (times_times int K a)) a)) True % 7.99/8.18 Clause #185 (by clausification #[184]): ∀ (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 % 7.99/8.18 Clause #186 (by clausification #[185]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 7.99/8.18 Clause #188 (by superposition #[186, 149]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 7.99/8.18 Clause #191 (by forward demodulation #[188, 121]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 7.99/8.18 Clause #192 (by forward demodulation #[191, 152]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 7.99/8.18 Clause #218 (by clausification #[10]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit0 K) (bit1 a)) (bit1 (plus_plus int K a))) True % 7.99/8.18 Clause #219 (by clausification #[218]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 7.99/8.18 Clause #220 (by clausification #[219]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 7.99/8.18 Clause #269 (by clausification #[13]): ∀ (a : int), Eq (Iff (ord_less_eq int (bit0 a) pls) (ord_less_eq int a pls)) True % 7.99/8.18 Clause #270 (by clausification #[269]): ∀ (a : int), Or (Eq (ord_less_eq int (bit0 a) pls) True) (Eq (ord_less_eq int a pls) False) % 7.99/8.18 Clause #273 (by superposition #[270, 123]): Or (Eq (ord_less_eq int (bit0 m) pls) True) (Eq False True) % 7.99/8.19 Clause #274 (by clausification #[273]): Eq (ord_less_eq int (bit0 m) pls) True % 7.99/8.19 Clause #391 (by clausification #[26]): ∀ (a : int), Eq (∀ (K3 : int), Iff (ord_less_eq int (bit1 K3) (bit1 a)) (ord_less_eq int K3 a)) True % 7.99/8.19 Clause #392 (by clausification #[391]): ∀ (a a_1 : int), Eq (Iff (ord_less_eq int (bit1 a) (bit1 a_1)) (ord_less_eq int a a_1)) True % 7.99/8.19 Clause #393 (by clausification #[392]): ∀ (a a_1 : int), Or (Eq (ord_less_eq int (bit1 a) (bit1 a_1)) True) (Eq (ord_less_eq int a a_1) False) % 7.99/8.19 Clause #401 (by superposition #[393, 274]): Or (Eq (ord_less_eq int (bit1 (bit0 m)) (bit1 pls)) True) (Eq False True) % 7.99/8.19 Clause #455 (by clausification #[30]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit0 K) a) (bit0 (times_times int K a))) True % 7.99/8.19 Clause #456 (by clausification #[455]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 7.99/8.19 Clause #457 (by clausification #[456]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 7.99/8.19 Clause #472 (by superposition #[457, 192]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 7.99/8.19 Clause #479 (by superposition #[472, 457]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 7.99/8.19 Clause #585 (by clausification #[401]): Eq (ord_less_eq int (bit1 (bit0 m)) (bit1 pls)) True % 7.99/8.19 Clause #1569 (by clausification #[113]): Eq % 7.99/8.19 (ord_less_eq int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.99/8.19 (one_one int)) % 7.99/8.19 False % 7.99/8.19 Clause #1570 (by forward demodulation #[1569, 163]): Eq % 7.99/8.19 (ord_less_eq int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.99/8.19 (bit1 pls)) % 7.99/8.19 False % 7.99/8.19 Clause #1571 (by forward demodulation #[1570, 163]): Eq % 7.99/8.19 (ord_less_eq int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) % 7.99/8.19 (bit1 pls)) % 7.99/8.19 False % 7.99/8.19 Clause #1572 (by forward demodulation #[1571, 136]): Eq (ord_less_eq int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) (bit1 pls)) False % 7.99/8.19 Clause #1573 (by forward demodulation #[1572, 479]): Eq (ord_less_eq int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) (bit1 pls)) False % 7.99/8.19 Clause #1574 (by forward demodulation #[1573, 220]): Eq (ord_less_eq int (bit1 (plus_plus int (bit0 m) pls)) (bit1 pls)) False % 7.99/8.19 Clause #1575 (by forward demodulation #[1574, 161]): Eq (ord_less_eq int (bit1 (bit0 m)) (bit1 pls)) False % 7.99/8.19 Clause #1576 (by superposition #[1575, 585]): Eq False True % 7.99/8.19 Clause #1577 (by clausification #[1576]): False % 7.99/8.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------