%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM944_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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 7.08s 7.31s % Output : Proof 7.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.13 % Problem : NUM944_5 : TPTP v9.2.0. Released v6.0.0. % 0.02/0.14 % Command : duper %s % 0.13/0.35 % Computer : n026.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:35:38 EDT 2025 % 0.13/0.35 % CPUTime : % 7.08/7.31 SZS status Theorem for theBenchmark.p % 7.08/7.31 SZS output start Proof for theBenchmark.p % 7.08/7.31 Clause #0 (by assumption #[]): Eq % 7.08/7.31 (Eq % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int)) % 7.08/7.31 True % 7.08/7.31 Clause #1 (by assumption #[]): Eq % 7.08/7.31 (Not % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min)) → % 7.08/7.31 Ne % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int)) % 7.08/7.31 True % 7.08/7.31 Clause #6 (by assumption #[]): Eq (∀ (L K : int), Eq (times_times int (bit1 K) L) (plus_plus int (bit0 (times_times int K L)) L)) True % 7.08/7.31 Clause #8 (by assumption #[]): Eq (∀ (L K : int), Eq (plus_plus int (bit0 K) (bit1 L)) (bit1 (plus_plus int K L))) True % 7.08/7.31 Clause #9 (by assumption #[]): Eq (∀ (L K : int), Eq (plus_plus int (bit1 K) (bit0 L)) (bit1 (plus_plus int K L))) True % 7.08/7.31 Clause #24 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 7.08/7.31 Clause #25 (by assumption #[]): Eq (∀ (W1 : int), Eq (times_times int pls W1) pls) True % 7.08/7.31 Clause #26 (by assumption #[]): Eq (∀ (L K : int), Eq (times_times int (bit0 K) L) (bit0 (times_times int K L))) True % 7.08/7.31 Clause #37 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of int K) K) True % 7.08/7.31 Clause #38 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int K pls) K) True % 7.08/7.31 Clause #39 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus int pls K) K) True % 7.08/7.31 Clause #55 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 7.08/7.31 Clause #72 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_1 A → ∀ (B A1 : A), Eq (times_times A A1 B) (times_times A B A1)) True % 7.08/7.31 Clause #80 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_1 A → ∀ (C A1 : A), Eq (plus_plus A A1 C) (plus_plus A C A1)) True % 7.08/7.31 Clause #98 (by assumption #[]): Eq (comm_semiring_1 int) True % 7.08/7.31 Clause #111 (by assumption #[]): Eq % 7.08/7.31 (Not % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min))) % 7.08/7.31 True % 7.08/7.31 Clause #112 (by clausification #[0]): Eq % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int) % 7.08/7.31 Clause #113 (by clausification #[1]): Or % 7.08/7.31 (Eq % 7.08/7.31 (Not % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min))) % 7.08/7.31 False) % 7.08/7.31 (Eq % 7.08/7.31 (Ne % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int)) % 7.08/7.31 True) % 7.08/7.31 Clause #114 (by clausification #[113]): Or % 7.08/7.31 (Eq % 7.08/7.31 (Ne % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int)) % 7.08/7.31 True) % 7.08/7.31 (Eq % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min)) % 7.08/7.31 True) % 7.08/7.31 Clause #115 (by clausification #[114]): Or % 7.08/7.31 (Eq % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min)) % 7.08/7.31 True) % 7.08/7.31 (Ne % 7.08/7.31 (legendre (number_number_of int min) % 7.08/7.31 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 7.08/7.31 (one_one int)) % 7.08/7.31 Clause #116 (by forward demodulation #[115, 112]): Or % 7.08/7.31 (Eq % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min)) % 7.08/7.31 True) % 7.08/7.31 (Ne (one_one int) (one_one int)) % 7.08/7.31 Clause #117 (by eliminate resolved literals #[116]): Eq % 7.08/7.31 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.08/7.31 (number_number_of int min)) % 7.08/7.31 True % 7.08/7.31 Clause #121 (by clausification #[24]): Eq (bit0 pls) pls % 7.15/7.33 Clause #136 (by clausification #[37]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 7.15/7.33 Clause #137 (by clausification #[136]): ∀ (a : int), Eq (number_number_of int a) a % 7.15/7.33 Clause #139 (by backward demodulation #[137, 117]): Eq (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) min) True % 7.15/7.33 Clause #147 (by clausification #[39]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 7.15/7.33 Clause #148 (by clausification #[147]): ∀ (a : int), Eq (plus_plus int pls a) a % 7.15/7.33 Clause #149 (by clausification #[38]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 7.15/7.33 Clause #150 (by clausification #[149]): ∀ (a : int), Eq (plus_plus int a pls) a % 7.15/7.33 Clause #154 (by clausification #[25]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 7.15/7.33 Clause #155 (by clausification #[154]): ∀ (a : int), Eq (times_times int pls a) pls % 7.15/7.33 Clause #161 (by clausification #[55]): Eq (one_one int) (number_number_of int (bit1 pls)) % 7.15/7.33 Clause #162 (by superposition #[161, 137]): Eq (one_one int) (bit1 pls) % 7.15/7.33 Clause #167 (by clausification #[6]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit1 K) a) (plus_plus int (bit0 (times_times int K a)) a)) True % 7.15/7.33 Clause #168 (by clausification #[167]): ∀ (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.15/7.33 Clause #169 (by clausification #[168]): ∀ (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.15/7.33 Clause #171 (by superposition #[169, 155]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 7.15/7.33 Clause #175 (by forward demodulation #[171, 121]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 7.15/7.33 Clause #176 (by forward demodulation #[175, 148]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 7.15/7.33 Clause #195 (by clausification #[8]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit0 K) (bit1 a)) (bit1 (plus_plus int K a))) True % 7.15/7.33 Clause #196 (by clausification #[195]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 7.15/7.33 Clause #197 (by clausification #[196]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 7.15/7.33 Clause #222 (by clausification #[9]): ∀ (a : int), Eq (∀ (K : int), Eq (plus_plus int (bit1 K) (bit0 a)) (bit1 (plus_plus int K a))) True % 7.15/7.33 Clause #223 (by clausification #[222]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1))) True % 7.15/7.33 Clause #224 (by clausification #[223]): ∀ (a a_1 : int), Eq (plus_plus int (bit1 a) (bit0 a_1)) (bit1 (plus_plus int a a_1)) % 7.15/7.33 Clause #400 (by clausification #[26]): ∀ (a : int), Eq (∀ (K : int), Eq (times_times int (bit0 K) a) (bit0 (times_times int K a))) True % 7.15/7.33 Clause #401 (by clausification #[400]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 7.15/7.33 Clause #402 (by clausification #[401]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 7.15/7.33 Clause #435 (by superposition #[402, 176]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 7.15/7.33 Clause #461 (by superposition #[435, 402]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 7.15/7.33 Clause #998 (by clausification #[72]): ∀ (a : Type), Eq (comm_semiring_1 a → ∀ (B A1 : a), Eq (times_times a A1 B) (times_times a B A1)) True % 7.15/7.33 Clause #999 (by clausification #[998]): ∀ (a : Type), Or (Eq (comm_semiring_1 a) False) (Eq (∀ (B A1 : a), Eq (times_times a A1 B) (times_times a B A1)) True) % 7.15/7.33 Clause #1000 (by clausification #[999]): ∀ (a : Type) (a_1 : a), % 7.15/7.33 Or (Eq (comm_semiring_1 a) False) (Eq (∀ (A1 : a), Eq (times_times a A1 a_1) (times_times a a_1 A1)) True) % 7.15/7.33 Clause #1001 (by clausification #[1000]): ∀ (a : Type) (a_1 a_2 : a), % 7.15/7.33 Or (Eq (comm_semiring_1 a) False) (Eq (Eq (times_times a a_1 a_2) (times_times a a_2 a_1)) True) % 7.15/7.33 Clause #1002 (by clausification #[1001]): ∀ (a : Type) (a_1 a_2 : a), Or (Eq (comm_semiring_1 a) False) (Eq (times_times a a_1 a_2) (times_times a a_2 a_1)) % 7.15/7.35 Clause #1004 (by superposition #[1002, 98]): ∀ (a a_1 : int), Or (Eq (times_times int a a_1) (times_times int a_1 a)) (Eq False True) % 7.15/7.35 Clause #1005 (by clausification #[1004]): ∀ (a a_1 : int), Eq (times_times int a a_1) (times_times int a_1 a) % 7.15/7.35 Clause #1081 (by superposition #[1005, 461]): ∀ (a : int), Eq (times_times int a (bit0 (bit0 (bit1 pls)))) (bit0 (bit0 a)) % 7.15/7.35 Clause #1184 (by clausification #[80]): ∀ (a : Type), Eq (comm_semiring_1 a → ∀ (C A1 : a), Eq (plus_plus a A1 C) (plus_plus a C A1)) True % 7.15/7.35 Clause #1185 (by clausification #[1184]): ∀ (a : Type), Or (Eq (comm_semiring_1 a) False) (Eq (∀ (C A1 : a), Eq (plus_plus a A1 C) (plus_plus a C A1)) True) % 7.15/7.35 Clause #1186 (by clausification #[1185]): ∀ (a : Type) (a_1 : a), % 7.15/7.35 Or (Eq (comm_semiring_1 a) False) (Eq (∀ (A1 : a), Eq (plus_plus a A1 a_1) (plus_plus a a_1 A1)) True) % 7.15/7.35 Clause #1187 (by clausification #[1186]): ∀ (a : Type) (a_1 a_2 : a), Or (Eq (comm_semiring_1 a) False) (Eq (Eq (plus_plus a a_1 a_2) (plus_plus a a_2 a_1)) True) % 7.15/7.35 Clause #1188 (by clausification #[1187]): ∀ (a : Type) (a_1 a_2 : a), Or (Eq (comm_semiring_1 a) False) (Eq (plus_plus a a_1 a_2) (plus_plus a a_2 a_1)) % 7.15/7.35 Clause #1190 (by superposition #[1188, 98]): ∀ (a a_1 : int), Or (Eq (plus_plus int a a_1) (plus_plus int a_1 a)) (Eq False True) % 7.15/7.35 Clause #1378 (by clausification #[111]): Eq % 7.15/7.35 (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 7.15/7.35 (number_number_of int min)) % 7.15/7.35 False % 7.15/7.35 Clause #1379 (by forward demodulation #[1378, 137]): Eq (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) min) False % 7.15/7.35 Clause #1380 (by forward demodulation #[1379, 162]): Eq (quadRes (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) min) False % 7.15/7.35 Clause #1381 (by forward demodulation #[1380, 1005]): Eq (quadRes (plus_plus int (times_times int m (number_number_of int (bit0 (bit0 (bit1 pls))))) (bit1 pls)) min) False % 7.15/7.35 Clause #1382 (by forward demodulation #[1381, 137]): Eq (quadRes (plus_plus int (times_times int m (bit0 (bit0 (bit1 pls)))) (bit1 pls)) min) False % 7.15/7.35 Clause #1383 (by clausification #[1190]): ∀ (a a_1 : int), Eq (plus_plus int a a_1) (plus_plus int a_1 a) % 7.15/7.35 Clause #1427 (by forward demodulation #[139, 1383]): Eq (quadRes (plus_plus int (one_one int) (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m)) min) True % 7.15/7.35 Clause #1428 (by forward demodulation #[1427, 1005]): Eq (quadRes (plus_plus int (one_one int) (times_times int m (number_number_of int (bit0 (bit0 (bit1 pls)))))) min) True % 7.15/7.35 Clause #1429 (by forward demodulation #[1428, 137]): Eq (quadRes (plus_plus int (one_one int) (times_times int m (bit0 (bit0 (bit1 pls))))) min) True % 7.15/7.35 Clause #1430 (by forward demodulation #[1429, 162]): Eq (quadRes (plus_plus int (bit1 pls) (times_times int m (bit0 (bit0 (bit1 pls))))) min) True % 7.15/7.35 Clause #1451 (by backward demodulation #[1081, 1382]): Eq (quadRes (plus_plus int (bit0 (bit0 m)) (bit1 pls)) min) False % 7.15/7.35 Clause #1452 (by backward demodulation #[1081, 1430]): Eq (quadRes (plus_plus int (bit1 pls) (bit0 (bit0 m))) min) True % 7.15/7.35 Clause #1496 (by forward demodulation #[1452, 224]): Eq (quadRes (bit1 (plus_plus int pls (bit0 m))) min) True % 7.15/7.35 Clause #1497 (by forward demodulation #[1496, 148]): Eq (quadRes (bit1 (bit0 m)) min) True % 7.15/7.35 Clause #1498 (by forward demodulation #[1451, 197]): Eq (quadRes (bit1 (plus_plus int (bit0 m) pls)) min) False % 7.15/7.35 Clause #1499 (by forward demodulation #[1498, 150]): Eq (quadRes (bit1 (bit0 m)) min) False % 7.15/7.35 Clause #1500 (by superposition #[1499, 1497]): Eq False True % 7.15/7.35 Clause #1501 (by clausification #[1500]): False % 7.15/7.35 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------