%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM940_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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.21s 7.37s % Output : Proof 7.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM940_5 : TPTP v9.2.0. Released v6.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n025.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:24:38 EDT 2025 % 0.13/0.34 % CPUTime : % 7.21/7.37 SZS status Theorem for theBenchmark.p % 7.21/7.37 SZS output start Proof for theBenchmark.p % 7.21/7.37 Clause #0 (by assumption #[]): Eq % 7.21/7.37 (Not % 7.21/7.37 (Or % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int)) % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls)))))) % 7.21/7.37 True % 7.21/7.37 Clause #1 (by assumption #[]): Eq % 7.21/7.37 (Or % 7.21/7.37 (Or % 7.21/7.37 (Eq % 7.21/7.37 (legendre (number_number_of int min) % 7.21/7.37 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.37 (one_one int)) % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int))) % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls))))) % 7.21/7.37 True % 7.21/7.37 Clause #6 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (times_times int (bit1 K1) L1) (plus_plus int (bit0 (times_times int K1 L1)) L1)) True % 7.21/7.37 Clause #9 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (plus_plus int (bit0 K1) (bit1 L1)) (bit1 (plus_plus int K1 L1))) True % 7.21/7.37 Clause #25 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 7.21/7.37 Clause #26 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 7.21/7.37 Clause #27 (by assumption #[]): Eq (∀ (L1 K1 : int), Eq (times_times int (bit0 K1) L1) (bit0 (times_times int K1 L1))) True % 7.21/7.37 Clause #46 (by assumption #[]): Eq (∀ (K1 : int), Eq (number_number_of int K1) K1) True % 7.21/7.37 Clause #49 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int K1 pls) K1) True % 7.21/7.37 Clause #50 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int pls K1) K1) True % 7.21/7.37 Clause #65 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 7.21/7.37 Clause #116 (by assumption #[]): Eq % 7.21/7.37 (Not % 7.21/7.37 (Eq % 7.21/7.37 (legendre (number_number_of int min) % 7.21/7.37 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.37 (one_one int))) % 7.21/7.37 True % 7.21/7.37 Clause #117 (by clausification #[0]): Eq % 7.21/7.37 (Or % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int)) % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls))))) % 7.21/7.37 False % 7.21/7.37 Clause #118 (by clausification #[117]): Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls)))) % 7.21/7.37 False % 7.21/7.37 Clause #119 (by clausification #[117]): Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int)) % 7.21/7.37 False % 7.21/7.37 Clause #120 (by clausification #[1]): Or % 7.21/7.37 (Eq % 7.21/7.37 (Or % 7.21/7.37 (Eq % 7.21/7.37 (legendre (number_number_of int min) % 7.21/7.37 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.37 (one_one int)) % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int))) % 7.21/7.37 True) % 7.21/7.37 (Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls)))) % 7.21/7.37 True) % 7.21/7.37 Clause #121 (by clausification #[120]): Or % 7.21/7.37 (Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (number_number_of int (bit0 (bit1 pls)))) % 7.21/7.37 True) % 7.21/7.37 (Or % 7.21/7.37 (Eq % 7.21/7.37 (Eq % 7.21/7.37 (legendre (number_number_of int min) % 7.21/7.37 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.37 (one_one int)) % 7.21/7.37 True) % 7.21/7.37 (Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.37 (one_one int)) % 7.21/7.37 True)) % 7.21/7.37 Clause #122 (by clausification #[121]): Or % 7.21/7.37 (Eq % 7.21/7.37 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.38 (number_number_of int (bit0 (bit1 pls)))) % 7.21/7.38 True) % 7.21/7.38 (Or % 7.21/7.38 (Eq % 7.21/7.38 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.38 (one_one int)) % 7.21/7.38 True) % 7.21/7.38 (Eq % 7.21/7.38 (legendre (number_number_of int min) % 7.21/7.38 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.38 (one_one int))) % 7.21/7.38 Clause #123 (by superposition #[122, 118]): Or % 7.21/7.38 (Eq % 7.21/7.38 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.38 (one_one int)) % 7.21/7.38 True) % 7.21/7.38 (Or % 7.21/7.38 (Eq % 7.21/7.38 (legendre (number_number_of int min) % 7.21/7.38 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.38 (one_one int)) % 7.21/7.38 (Eq True False)) % 7.21/7.38 Clause #134 (by clausification #[25]): Eq (bit0 pls) pls % 7.21/7.38 Clause #156 (by clausification #[46]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 7.21/7.38 Clause #157 (by clausification #[156]): ∀ (a : int), Eq (number_number_of int a) a % 7.21/7.38 Clause #163 (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 % 7.21/7.38 Clause #164 (by clausification #[163]): ∀ (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.21/7.38 Clause #165 (by clausification #[164]): ∀ (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.21/7.38 Clause #174 (by clausification #[50]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 7.21/7.38 Clause #175 (by clausification #[174]): ∀ (a : int), Eq (plus_plus int pls a) a % 7.21/7.38 Clause #176 (by clausification #[49]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 7.21/7.38 Clause #177 (by clausification #[176]): ∀ (a : int), Eq (plus_plus int a pls) a % 7.21/7.38 Clause #194 (by clausification #[26]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 7.21/7.38 Clause #195 (by clausification #[194]): ∀ (a : int), Eq (times_times int pls a) pls % 7.21/7.38 Clause #196 (by superposition #[195, 165]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 7.21/7.38 Clause #204 (by clausification #[65]): Eq (one_one int) (number_number_of int (bit1 pls)) % 7.21/7.38 Clause #205 (by superposition #[204, 157]): Eq (one_one int) (bit1 pls) % 7.21/7.38 Clause #225 (by clausification #[9]): ∀ (a : int), Eq (∀ (K1 : int), Eq (plus_plus int (bit0 K1) (bit1 a)) (bit1 (plus_plus int K1 a))) True % 7.21/7.38 Clause #226 (by clausification #[225]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 7.21/7.38 Clause #227 (by clausification #[226]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 7.21/7.38 Clause #424 (by clausification #[27]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit0 K1) a) (bit0 (times_times int K1 a))) True % 7.21/7.38 Clause #425 (by clausification #[424]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 7.21/7.38 Clause #426 (by clausification #[425]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 7.21/7.38 Clause #752 (by forward demodulation #[196, 134]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 7.21/7.38 Clause #753 (by forward demodulation #[752, 175]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 7.21/7.38 Clause #758 (by superposition #[753, 426]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 7.21/7.38 Clause #772 (by superposition #[758, 426]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 7.21/7.38 Clause #1484 (by clausification #[116]): Eq % 7.21/7.38 (Eq % 7.21/7.38 (legendre (number_number_of int min) % 7.21/7.38 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.38 (one_one int)) % 7.21/7.38 False % 7.21/7.38 Clause #1485 (by clausification #[1484]): Ne % 7.21/7.38 (legendre (number_number_of int min) % 7.21/7.38 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int) % 7.21/7.40 Clause #1486 (by forward demodulation #[1485, 205]): Ne % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls))) % 7.21/7.40 (one_one int) % 7.21/7.40 Clause #1487 (by forward demodulation #[1486, 157]): Ne (legendre (number_number_of int min) (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls))) % 7.21/7.40 (one_one int) % 7.21/7.40 Clause #1488 (by forward demodulation #[1487, 772]): Ne (legendre (number_number_of int min) (plus_plus int (bit0 (bit0 m)) (bit1 pls))) (one_one int) % 7.21/7.40 Clause #1489 (by forward demodulation #[1488, 227]): Ne (legendre (number_number_of int min) (bit1 (plus_plus int (bit0 m) pls))) (one_one int) % 7.21/7.40 Clause #1490 (by forward demodulation #[1489, 177]): Ne (legendre (number_number_of int min) (bit1 (bit0 m))) (one_one int) % 7.21/7.40 Clause #1491 (by forward demodulation #[1490, 157]): Ne (legendre min (bit1 (bit0 m))) (one_one int) % 7.21/7.40 Clause #1492 (by forward demodulation #[1491, 205]): Ne (legendre min (bit1 (bit0 m))) (bit1 pls) % 7.21/7.40 Clause #1500 (by forward demodulation #[119, 205]): Eq % 7.21/7.40 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.40 (bit1 pls)) % 7.21/7.40 False % 7.21/7.40 Clause #1501 (by forward demodulation #[1500, 205]): Eq % 7.21/7.40 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) % 7.21/7.40 (bit1 pls)) % 7.21/7.40 False % 7.21/7.40 Clause #1502 (by forward demodulation #[1501, 157]): Eq (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) (bit1 pls)) False % 7.21/7.40 Clause #1503 (by forward demodulation #[1502, 772]): Eq (dvd_dvd int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) (bit1 pls)) False % 7.21/7.40 Clause #1504 (by forward demodulation #[1503, 227]): Eq (dvd_dvd int (bit1 (plus_plus int (bit0 m) pls)) (bit1 pls)) False % 7.21/7.40 Clause #1505 (by forward demodulation #[1504, 177]): Eq (dvd_dvd int (bit1 (bit0 m)) (bit1 pls)) False % 7.21/7.40 Clause #1519 (by clausification #[123]): Or % 7.21/7.40 (Eq % 7.21/7.40 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.40 (one_one int)) % 7.21/7.40 True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1520 (by forward demodulation #[1519, 205]): Or % 7.21/7.40 (Eq % 7.21/7.40 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.21/7.40 (bit1 pls)) % 7.21/7.40 True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1521 (by forward demodulation #[1520, 205]): Or % 7.21/7.40 (Eq % 7.21/7.40 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) % 7.21/7.40 (bit1 pls)) % 7.21/7.40 True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1522 (by forward demodulation #[1521, 157]): Or (Eq (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) (bit1 pls)) True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1523 (by forward demodulation #[1522, 772]): Or (Eq (dvd_dvd int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) (bit1 pls)) True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1524 (by forward demodulation #[1523, 227]): Or (Eq (dvd_dvd int (bit1 (plus_plus int (bit0 m) pls)) (bit1 pls)) True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.40 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.40 (one_one int)) % 7.21/7.40 Clause #1525 (by forward demodulation #[1524, 177]): Or (Eq (dvd_dvd int (bit1 (bit0 m)) (bit1 pls)) True) % 7.21/7.40 (Eq % 7.21/7.40 (legendre (number_number_of int min) % 7.21/7.41 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.41 (one_one int)) % 7.21/7.41 Clause #1526 (by forward demodulation #[1525, 1505]): Or (Eq False True) % 7.21/7.41 (Eq % 7.21/7.41 (legendre (number_number_of int min) % 7.21/7.41 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.41 (one_one int)) % 7.21/7.41 Clause #1527 (by clausification #[1526]): Eq % 7.21/7.41 (legendre (number_number_of int min) % 7.21/7.41 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.21/7.41 (one_one int) % 7.21/7.41 Clause #1528 (by forward demodulation #[1527, 205]): Eq % 7.21/7.41 (legendre (number_number_of int min) % 7.21/7.41 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls))) % 7.21/7.41 (one_one int) % 7.21/7.41 Clause #1529 (by forward demodulation #[1528, 157]): Eq (legendre (number_number_of int min) (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls))) % 7.21/7.41 (one_one int) % 7.21/7.41 Clause #1530 (by forward demodulation #[1529, 772]): Eq (legendre (number_number_of int min) (plus_plus int (bit0 (bit0 m)) (bit1 pls))) (one_one int) % 7.21/7.41 Clause #1531 (by forward demodulation #[1530, 227]): Eq (legendre (number_number_of int min) (bit1 (plus_plus int (bit0 m) pls))) (one_one int) % 7.21/7.41 Clause #1532 (by forward demodulation #[1531, 177]): Eq (legendre (number_number_of int min) (bit1 (bit0 m))) (one_one int) % 7.21/7.41 Clause #1533 (by forward demodulation #[1532, 157]): Eq (legendre min (bit1 (bit0 m))) (one_one int) % 7.21/7.41 Clause #1534 (by forward demodulation #[1533, 205]): Eq (legendre min (bit1 (bit0 m))) (bit1 pls) % 7.21/7.41 Clause #1535 (by forward contextual literal cutting #[1534, 1492]): False % 7.21/7.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------