%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM942_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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 55.87s 56.04s % Output : Proof 55.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM942_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n019.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:56:53 EDT 2025 % 0.13/0.34 % CPUTime : % 55.87/56.04 SZS status Theorem for theBenchmark.p % 55.87/56.04 SZS output start Proof for theBenchmark.p % 55.87/56.04 Clause #0 (by assumption #[]): Eq (zprime (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) True % 55.87/56.04 Clause #4 (by assumption #[]): Eq % 55.87/56.04 (∀ (M : int), % 55.87/56.04 zprime (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) M) (one_one int)) → % 55.87/56.04 Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) M) (one_one int))) % 55.87/56.04 (one_one int)) % 55.87/56.04 True % 55.87/56.04 Clause #5 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit1 K1) L) (plus_plus int (bit0 (times_times int K1 L)) L)) True % 55.87/56.04 Clause #7 (by assumption #[]): Eq (∀ (L K1 : int), Eq (plus_plus int (bit0 K1) (bit1 L)) (bit1 (plus_plus int K1 L))) True % 55.87/56.04 Clause #22 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 55.87/56.04 Clause #23 (by assumption #[]): Eq (∀ (W1 : int), Eq (times_times int pls W1) pls) True % 55.87/56.04 Clause #24 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit0 K1) L) (bit0 (times_times int K1 L))) True % 55.87/56.04 Clause #36 (by assumption #[]): Eq (∀ (K1 : int), Eq (number_number_of int K1) K1) True % 55.87/56.04 Clause #37 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int K1 pls) K1) True % 55.87/56.04 Clause #38 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int pls K1) K1) True % 55.87/56.04 Clause #53 (by assumption #[]): Eq (Eq (one_one int) (number_number_of int (bit1 pls))) True % 55.87/56.04 Clause #71 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_1 A → ∀ (B A1 : A), Eq (times_times A A1 B) (times_times A B A1)) True % 55.87/56.04 Clause #79 (by assumption #[]): Eq (∀ (A : Type), comm_semiring_1 A → ∀ (C A1 : A), Eq (plus_plus A A1 C) (plus_plus A C A1)) True % 55.87/56.04 Clause #98 (by assumption #[]): Eq (comm_semiring_1 int) True % 55.87/56.04 Clause #111 (by assumption #[]): Eq % 55.87/56.04 (Not % 55.87/56.04 (Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 55.87/56.04 (one_one int))) % 55.87/56.04 True % 55.87/56.04 Clause #126 (by clausification #[22]): Eq (bit0 pls) pls % 55.87/56.04 Clause #139 (by clausification #[36]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 55.87/56.04 Clause #140 (by clausification #[139]): ∀ (a : int), Eq (number_number_of int a) a % 55.87/56.04 Clause #141 (by backward demodulation #[140, 0]): Eq (zprime (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int))) True % 55.87/56.04 Clause #143 (by clausification #[4]): ∀ (a : int), % 55.87/56.04 Eq % 55.87/56.04 (zprime (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int)) → % 55.87/56.04 Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 (one_one int)) % 55.87/56.04 True % 55.87/56.04 Clause #144 (by clausification #[143]): ∀ (a : int), % 55.87/56.04 Or % 55.87/56.04 (Eq (zprime (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 False) % 55.87/56.04 (Eq % 55.87/56.04 (Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 (one_one int)) % 55.87/56.04 True) % 55.87/56.04 Clause #145 (by clausification #[144]): ∀ (a : int), % 55.87/56.04 Or % 55.87/56.04 (Eq (zprime (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 False) % 55.87/56.04 (Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 (one_one int)) % 55.87/56.04 Clause #146 (by forward demodulation #[145, 140]): ∀ (a : int), % 55.87/56.04 Or (Eq (zprime (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) False) % 55.87/56.04 (Eq % 55.87/56.04 (legendre (number_number_of int min) % 55.87/56.04 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) a) (one_one int))) % 55.87/56.04 (one_one int)) % 55.87/56.04 Clause #147 (by forward demodulation #[146, 140]): ∀ (a : int), % 55.87/56.04 Or (Eq (zprime (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) False) % 55.87/56.04 (Eq (legendre (number_number_of int min) (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) % 55.87/56.07 (one_one int)) % 55.87/56.07 Clause #148 (by forward demodulation #[147, 140]): ∀ (a : int), % 55.87/56.07 Or (Eq (zprime (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) False) % 55.87/56.07 (Eq (legendre min (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) (one_one int)) % 55.87/56.07 Clause #149 (by clausification #[38]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 55.87/56.07 Clause #150 (by clausification #[149]): ∀ (a : int), Eq (plus_plus int pls a) a % 55.87/56.07 Clause #151 (by clausification #[37]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 55.87/56.07 Clause #152 (by clausification #[151]): ∀ (a : int), Eq (plus_plus int a pls) a % 55.87/56.07 Clause #153 (by clausification #[23]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 55.87/56.07 Clause #154 (by clausification #[153]): ∀ (a : int), Eq (times_times int pls a) pls % 55.87/56.07 Clause #161 (by clausification #[5]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit1 K1) a) (plus_plus int (bit0 (times_times int K1 a)) a)) True % 55.87/56.07 Clause #162 (by clausification #[161]): ∀ (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 % 55.87/56.07 Clause #163 (by clausification #[162]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 55.87/56.07 Clause #165 (by superposition #[163, 154]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 55.87/56.07 Clause #167 (by clausification #[53]): Eq (one_one int) (number_number_of int (bit1 pls)) % 55.87/56.07 Clause #168 (by superposition #[167, 140]): Eq (one_one int) (bit1 pls) % 55.87/56.07 Clause #173 (by backward demodulation #[168, 148]): ∀ (a : int), % 55.87/56.07 Or (Eq (zprime (plus_plus int (times_times int (bit0 (bit0 (one_one int))) a) (one_one int))) False) % 55.87/56.07 (Eq (legendre min (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) (one_one int)) % 55.87/56.07 Clause #187 (by clausification #[7]): ∀ (a : int), Eq (∀ (K1 : int), Eq (plus_plus int (bit0 K1) (bit1 a)) (bit1 (plus_plus int K1 a))) True % 55.87/56.07 Clause #188 (by clausification #[187]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 55.87/56.07 Clause #189 (by clausification #[188]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 55.87/56.07 Clause #192 (by superposition #[189, 168]): ∀ (a : int), Eq (plus_plus int (bit0 a) (one_one int)) (bit1 (plus_plus int a pls)) % 55.87/56.07 Clause #294 (by forward demodulation #[165, 168]): ∀ (a : int), Eq (times_times int (one_one int) a) (plus_plus int (bit0 pls) a) % 55.87/56.07 Clause #295 (by forward demodulation #[294, 126]): ∀ (a : int), Eq (times_times int (one_one int) a) (plus_plus int pls a) % 55.87/56.07 Clause #296 (by forward demodulation #[295, 150]): ∀ (a : int), Eq (times_times int (one_one int) a) a % 55.87/56.07 Clause #363 (by clausification #[24]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit0 K1) a) (bit0 (times_times int K1 a))) True % 55.87/56.07 Clause #364 (by clausification #[363]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 55.87/56.07 Clause #365 (by clausification #[364]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 55.87/56.07 Clause #392 (by superposition #[365, 296]): ∀ (a : int), Eq (times_times int (bit0 (one_one int)) a) (bit0 a) % 55.87/56.07 Clause #410 (by superposition #[392, 365]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (one_one int))) a) (bit0 (bit0 a)) % 55.87/56.07 Clause #940 (by clausification #[71]): ∀ (a : Type), Eq (comm_semiring_1 a → ∀ (B A1 : a), Eq (times_times a A1 B) (times_times a B A1)) True % 55.87/56.07 Clause #941 (by clausification #[940]): ∀ (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) % 55.87/56.07 Clause #942 (by clausification #[941]): ∀ (a : Type) (a_1 : a), % 55.87/56.07 Or (Eq (comm_semiring_1 a) False) (Eq (∀ (A1 : a), Eq (times_times a A1 a_1) (times_times a a_1 A1)) True) % 55.87/56.07 Clause #943 (by clausification #[942]): ∀ (a : Type) (a_1 a_2 : a), % 55.87/56.07 Or (Eq (comm_semiring_1 a) False) (Eq (Eq (times_times a a_1 a_2) (times_times a a_2 a_1)) True) % 55.87/56.09 Clause #944 (by clausification #[943]): ∀ (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)) % 55.87/56.09 Clause #946 (by superposition #[944, 98]): ∀ (a a_1 : int), Or (Eq (times_times int a a_1) (times_times int a_1 a)) (Eq False True) % 55.87/56.09 Clause #947 (by clausification #[946]): ∀ (a a_1 : int), Eq (times_times int a a_1) (times_times int a_1 a) % 55.87/56.09 Clause #1026 (by superposition #[947, 410]): ∀ (a : int), Eq (times_times int a (bit0 (bit0 (one_one int)))) (bit0 (bit0 a)) % 55.87/56.09 Clause #1029 (by superposition #[947, 365]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a_1 a)) % 55.87/56.09 Clause #1122 (by clausification #[79]): ∀ (a : Type), Eq (comm_semiring_1 a → ∀ (C A1 : a), Eq (plus_plus a A1 C) (plus_plus a C A1)) True % 55.87/56.09 Clause #1123 (by clausification #[1122]): ∀ (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) % 55.87/56.09 Clause #1124 (by clausification #[1123]): ∀ (a : Type) (a_1 : a), % 55.87/56.09 Or (Eq (comm_semiring_1 a) False) (Eq (∀ (A1 : a), Eq (plus_plus a A1 a_1) (plus_plus a a_1 A1)) True) % 55.87/56.09 Clause #1125 (by clausification #[1124]): ∀ (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) % 55.87/56.09 Clause #1126 (by clausification #[1125]): ∀ (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)) % 55.87/56.09 Clause #1128 (by superposition #[1126, 98]): ∀ (a a_1 : int), Or (Eq (plus_plus int a a_1) (plus_plus int a_1 a)) (Eq False True) % 55.87/56.09 Clause #1250 (by superposition #[1029, 365]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (times_times int (bit0 a_1) a) % 55.87/56.09 Clause #1272 (by superposition #[1250, 947]): ∀ (a a_1 : int), Eq (times_times int a (bit0 a_1)) (times_times int (bit0 a) a_1) % 55.87/56.09 Clause #1306 (by superposition #[1272, 947]): ∀ (a a_1 : int), Eq (times_times int a (bit0 a_1)) (times_times int a_1 (bit0 a)) % 55.87/56.09 Clause #1396 (by clausification #[111]): Eq % 55.87/56.09 (Eq % 55.87/56.09 (legendre (number_number_of int min) % 55.87/56.09 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 55.87/56.09 (one_one int)) % 55.87/56.09 False % 55.87/56.09 Clause #1397 (by clausification #[1396]): Ne % 55.87/56.09 (legendre (number_number_of int min) % 55.87/56.09 (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int))) % 55.87/56.09 (one_one int) % 55.87/56.09 Clause #1398 (by forward demodulation #[1397, 947]): Ne % 55.87/56.09 (legendre (number_number_of int min) % 55.87/56.09 (plus_plus int (times_times int m (number_number_of int (bit0 (bit0 (bit1 pls))))) (one_one int))) % 55.87/56.09 (one_one int) % 55.87/56.09 Clause #1399 (by forward demodulation #[1398, 140]): Ne (legendre (number_number_of int min) (plus_plus int (times_times int m (bit0 (bit0 (bit1 pls)))) (one_one int))) % 55.87/56.09 (one_one int) % 55.87/56.09 Clause #1400 (by forward demodulation #[1399, 168]): Ne (legendre (number_number_of int min) (plus_plus int (times_times int m (bit0 (bit0 (one_one int)))) (one_one int))) % 55.87/56.09 (one_one int) % 55.87/56.09 Clause #1401 (by forward demodulation #[1400, 140]): Ne (legendre min (plus_plus int (times_times int m (bit0 (bit0 (one_one int)))) (one_one int))) (one_one int) % 55.91/56.09 Clause #1402 (by clausification #[1128]): ∀ (a a_1 : int), Eq (plus_plus int a a_1) (plus_plus int a_1 a) % 55.91/56.09 Clause #1446 (by backward demodulation #[1026, 1401]): Ne (legendre min (plus_plus int (bit0 (bit0 m)) (one_one int))) (one_one int) % 55.91/56.09 Clause #1455 (by forward demodulation #[141, 1402]): Eq (zprime (plus_plus int (one_one int) (times_times int (bit0 (bit0 (bit1 pls))) m))) True % 55.91/56.09 Clause #1456 (by forward demodulation #[1455, 1272]): Eq (zprime (plus_plus int (one_one int) (times_times int (bit0 (bit1 pls)) (bit0 m)))) True % 55.91/56.09 Clause #1457 (by forward demodulation #[1456, 1306]): Eq (zprime (plus_plus int (one_one int) (times_times int m (bit0 (bit0 (bit1 pls)))))) True % 55.91/56.09 Clause #1458 (by forward demodulation #[1457, 168]): Eq (zprime (plus_plus int (one_one int) (times_times int m (bit0 (bit0 (one_one int)))))) True % 55.91/56.09 Clause #1459 (by forward demodulation #[1458, 1026]): Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 m)))) True % 55.98/56.16 Clause #1491 (by forward demodulation #[173, 1402]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (times_times int (bit0 (bit0 (one_one int))) a))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) (one_one int)) % 55.98/56.16 Clause #1492 (by forward demodulation #[1491, 410]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) a) (one_one int))) (one_one int)) % 55.98/56.16 Clause #1493 (by forward demodulation #[1492, 1402]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (one_one int) (times_times int (bit0 (bit0 (bit1 pls))) a))) (one_one int)) % 55.98/56.16 Clause #1494 (by forward demodulation #[1493, 1272]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (one_one int) (times_times int (bit0 (bit1 pls)) (bit0 a)))) (one_one int)) % 55.98/56.16 Clause #1495 (by forward demodulation #[1494, 1272]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (one_one int) (times_times int (bit1 pls) (bit0 (bit0 a))))) (one_one int)) % 55.98/56.16 Clause #1496 (by forward demodulation #[1495, 168]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (one_one int) (times_times int (one_one int) (bit0 (bit0 a))))) (one_one int)) % 55.98/56.16 Clause #1497 (by forward demodulation #[1496, 296]): ∀ (a : int), % 55.98/56.16 Or (Eq (zprime (plus_plus int (one_one int) (bit0 (bit0 a)))) False) % 55.98/56.16 (Eq (legendre min (plus_plus int (one_one int) (bit0 (bit0 a)))) (one_one int)) % 55.98/56.16 Clause #1498 (by superposition #[1497, 1459]): Or (Eq (legendre min (plus_plus int (one_one int) (bit0 (bit0 m)))) (one_one int)) (Eq False True) % 55.98/56.16 Clause #1551 (by forward demodulation #[192, 152]): ∀ (a : int), Eq (plus_plus int (bit0 a) (one_one int)) (bit1 a) % 55.98/56.16 Clause #1555 (by superposition #[1551, 1402]): ∀ (a : int), Eq (plus_plus int (one_one int) (bit0 a)) (bit1 a) % 55.98/56.16 Clause #2057 (by forward demodulation #[1446, 1551]): Ne (legendre min (bit1 (bit0 m))) (one_one int) % 55.98/56.16 Clause #13408 (by clausification #[1498]): Eq (legendre min (plus_plus int (one_one int) (bit0 (bit0 m)))) (one_one int) % 55.98/56.16 Clause #13409 (by forward demodulation #[13408, 1555]): Eq (legendre min (bit1 (bit0 m))) (one_one int) % 55.98/56.16 Clause #13410 (by forward contextual literal cutting #[13409, 2057]): False % 55.98/56.16 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------