%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM954_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:39 PM UTC 2025 % Result : Theorem 9.28s 9.44s % Output : Proof 9.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM954_5 : TPTP v9.2.0. Released v6.0.0. % 0.04/0.14 % Command : duper %s % 0.14/0.35 % Computer : n008.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:34:23 EDT 2025 % 0.14/0.35 % CPUTime : % 9.28/9.44 SZS status Theorem for theBenchmark.p % 9.28/9.44 SZS output start Proof for theBenchmark.p % 9.28/9.44 Clause #0 (by assumption #[]): Eq % 9.28/9.44 (Eq (twoSqu196287499sum2sq (product_Pair int int s (one_one int))) % 9.28/9.44 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.28/9.44 t)) % 9.28/9.44 True % 9.28/9.44 Clause #6 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit1 K1) L) (plus_plus int (bit0 (times_times int K1 L)) L)) True % 9.28/9.44 Clause #8 (by assumption #[]): Eq (∀ (L K1 : int), Eq (plus_plus int (bit0 K1) (bit1 L)) (bit1 (plus_plus int K1 L))) True % 9.28/9.44 Clause #24 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 9.28/9.44 Clause #25 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 9.28/9.44 Clause #26 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit0 K1) L) (bit0 (times_times int K1 L))) True % 9.28/9.44 Clause #31 (by assumption #[]): Eq (∀ (K1 : int), Eq (number_number_of int K1) K1) True % 9.28/9.44 Clause #32 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int K1 pls) K1) True % 9.28/9.44 Clause #33 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int pls K1) K1) True % 9.28/9.44 Clause #48 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 9.28/9.44 Clause #58 (by assumption #[]): Eq % 9.28/9.44 (∀ (X : int), % 9.28/9.44 Iff (twoSqu1567020053sum2sq X) % 9.28/9.44 (Exists fun A3 => Exists fun B2 => Eq (twoSqu196287499sum2sq (product_Pair int int A3 B2)) X)) % 9.28/9.44 True % 9.28/9.44 Clause #111 (by assumption #[]): Eq % 9.28/9.44 (Not % 9.28/9.44 (twoSqu1567020053sum2sq % 9.28/9.44 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.28/9.44 t))) % 9.28/9.44 True % 9.28/9.44 Clause #112 (by clausification #[0]): Eq (twoSqu196287499sum2sq (product_Pair int int s (one_one int))) % 9.28/9.44 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) t) % 9.28/9.44 Clause #121 (by clausification #[24]): Eq (bit0 pls) pls % 9.28/9.44 Clause #135 (by clausification #[31]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 9.28/9.44 Clause #136 (by clausification #[135]): ∀ (a : int), Eq (number_number_of int a) a % 9.28/9.44 Clause #137 (by backward demodulation #[136, 112]): Eq (twoSqu196287499sum2sq (product_Pair int int s (one_one int))) % 9.28/9.44 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) t) % 9.28/9.44 Clause #145 (by clausification #[48]): Eq (one_one int) (number_number_of int (bit1 pls)) % 9.28/9.44 Clause #146 (by superposition #[145, 136]): Eq (one_one int) (bit1 pls) % 9.28/9.44 Clause #149 (by clausification #[33]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 9.28/9.44 Clause #150 (by clausification #[149]): ∀ (a : int), Eq (plus_plus int pls a) a % 9.28/9.44 Clause #155 (by clausification #[32]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 9.28/9.44 Clause #156 (by clausification #[155]): ∀ (a : int), Eq (plus_plus int a pls) a % 9.28/9.44 Clause #166 (by clausification #[6]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit1 K1) a) (plus_plus int (bit0 (times_times int K1 a)) a)) True % 9.28/9.44 Clause #167 (by clausification #[166]): ∀ (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.28/9.44 Clause #168 (by clausification #[167]): ∀ (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.28/9.44 Clause #170 (by clausification #[25]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 9.28/9.44 Clause #171 (by clausification #[170]): ∀ (a : int), Eq (times_times int pls a) pls % 9.28/9.44 Clause #172 (by superposition #[171, 168]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 9.28/9.44 Clause #173 (by forward demodulation #[172, 121]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 9.28/9.44 Clause #174 (by forward demodulation #[173, 150]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 9.28/9.44 Clause #193 (by clausification #[8]): ∀ (a : int), Eq (∀ (K1 : int), Eq (plus_plus int (bit0 K1) (bit1 a)) (bit1 (plus_plus int K1 a))) True % 9.28/9.44 Clause #194 (by clausification #[193]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 9.28/9.44 Clause #195 (by clausification #[194]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 9.28/9.46 Clause #392 (by clausification #[26]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit0 K1) a) (bit0 (times_times int K1 a))) True % 9.28/9.46 Clause #393 (by clausification #[392]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 9.28/9.46 Clause #394 (by clausification #[393]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 9.28/9.46 Clause #425 (by superposition #[394, 174]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 9.28/9.46 Clause #443 (by superposition #[425, 394]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 9.28/9.46 Clause #891 (by clausification #[58]): ∀ (a : int), % 9.28/9.46 Eq % 9.28/9.46 (Iff (twoSqu1567020053sum2sq a) % 9.28/9.46 (Exists fun A3 => Exists fun B2 => Eq (twoSqu196287499sum2sq (product_Pair int int A3 B2)) a)) % 9.28/9.46 True % 9.28/9.46 Clause #892 (by clausification #[891]): ∀ (a : int), % 9.28/9.46 Or (Eq (twoSqu1567020053sum2sq a) True) % 9.28/9.46 (Eq (Exists fun A3 => Exists fun B2 => Eq (twoSqu196287499sum2sq (product_Pair int int A3 B2)) a) False) % 9.28/9.46 Clause #894 (by clausification #[892]): ∀ (a a_1 : int), % 9.28/9.46 Or (Eq (twoSqu1567020053sum2sq a) True) % 9.28/9.46 (Eq (Exists fun B2 => Eq (twoSqu196287499sum2sq (product_Pair int int a_1 B2)) a) False) % 9.28/9.46 Clause #895 (by clausification #[894]): ∀ (a a_1 a_2 : int), % 9.28/9.46 Or (Eq (twoSqu1567020053sum2sq a) True) (Eq (Eq (twoSqu196287499sum2sq (product_Pair int int a_1 a_2)) a) False) % 9.28/9.46 Clause #896 (by clausification #[895]): ∀ (a a_1 a_2 : int), % 9.28/9.46 Or (Eq (twoSqu1567020053sum2sq a) True) (Ne (twoSqu196287499sum2sq (product_Pair int int a_1 a_2)) a) % 9.28/9.46 Clause #897 (by destructive equality resolution #[896]): ∀ (a a_1 : int), Eq (twoSqu1567020053sum2sq (twoSqu196287499sum2sq (product_Pair int int a a_1))) True % 9.28/9.46 Clause #1585 (by clausification #[111]): Eq % 9.28/9.46 (twoSqu1567020053sum2sq % 9.28/9.46 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 9.28/9.46 t)) % 9.28/9.46 False % 9.28/9.46 Clause #1586 (by forward demodulation #[1585, 146]): Eq % 9.28/9.46 (twoSqu1567020053sum2sq % 9.28/9.46 (times_times int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) t)) % 9.28/9.46 False % 9.28/9.46 Clause #1587 (by forward demodulation #[1586, 136]): Eq (twoSqu1567020053sum2sq (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t)) % 9.28/9.46 False % 9.28/9.46 Clause #1588 (by forward demodulation #[1587, 443]): Eq (twoSqu1567020053sum2sq (times_times int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) t)) False % 9.28/9.46 Clause #1589 (by forward demodulation #[1588, 195]): Eq (twoSqu1567020053sum2sq (times_times int (bit1 (plus_plus int (bit0 m) pls)) t)) False % 9.28/9.46 Clause #1590 (by forward demodulation #[1589, 156]): Eq (twoSqu1567020053sum2sq (times_times int (bit1 (bit0 m)) t)) False % 9.28/9.46 Clause #1617 (by forward demodulation #[137, 146]): Eq (twoSqu196287499sum2sq (product_Pair int int s (bit1 pls))) % 9.28/9.46 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) t) % 9.28/9.46 Clause #1618 (by forward demodulation #[1617, 146]): Eq (twoSqu196287499sum2sq (product_Pair int int s (bit1 pls))) % 9.28/9.46 (times_times int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) t) % 9.28/9.46 Clause #1619 (by forward demodulation #[1618, 443]): Eq (twoSqu196287499sum2sq (product_Pair int int s (bit1 pls))) % 9.28/9.46 (times_times int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) t) % 9.28/9.46 Clause #1620 (by forward demodulation #[1619, 195]): Eq (twoSqu196287499sum2sq (product_Pair int int s (bit1 pls))) (times_times int (bit1 (plus_plus int (bit0 m) pls)) t) % 9.28/9.46 Clause #1621 (by forward demodulation #[1620, 156]): Eq (twoSqu196287499sum2sq (product_Pair int int s (bit1 pls))) (times_times int (bit1 (bit0 m)) t) % 9.28/9.46 Clause #1622 (by superposition #[1621, 897]): Eq (twoSqu1567020053sum2sq (times_times int (bit1 (bit0 m)) t)) True % 9.28/9.46 Clause #1623 (by superposition #[1622, 1590]): Eq True False % 9.28/9.46 Clause #1625 (by clausification #[1623]): False % 9.28/9.46 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------