%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM952_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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 149.20s 149.39s % Output : Proof 149.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM952_5 : TPTP v9.2.0. Released v6.0.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n014.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:26:23 EDT 2025 % 0.13/0.34 % CPUTime : % 149.20/149.39 SZS status Theorem for theBenchmark.p % 149.20/149.39 SZS output start Proof for theBenchmark.p % 149.20/149.39 Clause #0 (by assumption #[]): Eq % 149.20/149.39 (Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 149.20/149.39 True % 149.20/149.39 Clause #1 (by assumption #[]): Eq % 149.20/149.39 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 149.20/149.39 (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min))) % 149.20/149.39 True % 149.20/149.39 Clause #4 (by assumption #[]): Eq % 149.20/149.39 (∀ (B1 : Type), % 149.20/149.39 And (monoid_mult B1) (number B1) → % 149.20/149.39 ∀ (W : int), % 149.20/149.39 Eq (power_power B1 (number_number_of B1 W) (number_number_of nat (bit0 (bit1 pls)))) % 149.20/149.39 (times_times B1 (number_number_of B1 W) (number_number_of B1 W))) % 149.20/149.39 True % 149.20/149.39 Clause #9 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit1 K1) L) (plus_plus int (bit0 (times_times int K1 L)) L)) True % 149.20/149.39 Clause #24 (by assumption #[]): Eq (Eq (bit0 pls) pls) True % 149.20/149.39 Clause #25 (by assumption #[]): Eq (∀ (W : int), Eq (times_times int pls W) pls) True % 149.20/149.39 Clause #26 (by assumption #[]): Eq (∀ (L K1 : int), Eq (times_times int (bit0 K1) L) (bit0 (times_times int K1 L))) True % 149.20/149.39 Clause #46 (by assumption #[]): Eq (∀ (L K1 : int), Eq (plus_plus int (bit0 K1) (bit1 L)) (bit1 (plus_plus int K1 L))) True % 149.20/149.39 Clause #69 (by assumption #[]): Eq (∀ (K1 : int), Eq (number_number_of int K1) K1) True % 149.20/149.39 Clause #77 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int K1 pls) K1) True % 149.20/149.39 Clause #78 (by assumption #[]): Eq (∀ (K1 : int), Eq (plus_plus int pls K1) K1) True % 149.20/149.39 Clause #96 (by assumption #[]): Eq (∀ (A : Type), number_ring A → Eq (one_one A) (number_number_of A (bit1 pls))) True % 149.20/149.39 Clause #98 (by assumption #[]): Eq (monoid_mult int) True % 149.20/149.39 Clause #101 (by assumption #[]): Eq (number_ring int) True % 149.20/149.39 Clause #104 (by assumption #[]): Eq (number int) True % 149.20/149.39 Clause #112 (by assumption #[]): Eq % 149.20/149.39 (Not % 149.20/149.39 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)))) % 149.20/149.39 True % 149.20/149.39 Clause #113 (by clausification #[0]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (number_number_of int min)) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 149.20/149.39 Clause #114 (by forward demodulation #[1, 113]): Eq % 149.20/149.39 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 149.20/149.39 True % 149.20/149.39 Clause #119 (by clausification #[24]): Eq (bit0 pls) pls % 149.20/149.39 Clause #129 (by clausification #[69]): ∀ (a : int), Eq (Eq (number_number_of int a) a) True % 149.20/149.39 Clause #130 (by clausification #[129]): ∀ (a : int), Eq (number_number_of int a) a % 149.20/149.39 Clause #131 (by backward demodulation #[130, 113]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int)) % 149.20/149.39 Clause #132 (by backward demodulation #[130, 114]): Eq % 149.20/149.39 (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) % 149.20/149.39 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 149.20/149.39 True % 149.20/149.39 Clause #136 (by clausification #[4]): ∀ (a : Type), % 149.20/149.39 Eq % 149.20/149.39 (And (monoid_mult a) (number a) → % 149.20/149.39 ∀ (W : int), % 149.20/149.39 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 149.20/149.39 (times_times a (number_number_of a W) (number_number_of a W))) % 149.20/149.39 True % 149.20/149.39 Clause #137 (by clausification #[136]): ∀ (a : Type), % 149.20/149.39 Or (Eq (And (monoid_mult a) (number a)) False) % 149.20/149.39 (Eq % 149.20/149.39 (∀ (W : int), % 149.20/149.39 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 149.20/149.39 (times_times a (number_number_of a W) (number_number_of a W))) % 149.20/149.39 True) % 149.20/149.39 Clause #138 (by clausification #[137]): ∀ (a : Type), % 149.24/149.41 Or % 149.24/149.41 (Eq % 149.24/149.41 (∀ (W : int), % 149.24/149.41 Eq (power_power a (number_number_of a W) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.41 (times_times a (number_number_of a W) (number_number_of a W))) % 149.24/149.41 True) % 149.24/149.41 (Or (Eq (monoid_mult a) False) (Eq (number a) False)) % 149.24/149.41 Clause #139 (by clausification #[138]): ∀ (a : Type) (a_1 : int), % 149.24/149.41 Or (Eq (monoid_mult a) False) % 149.24/149.41 (Or (Eq (number a) False) % 149.24/149.41 (Eq % 149.24/149.41 (Eq (power_power a (number_number_of a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.41 (times_times a (number_number_of a a_1) (number_number_of a a_1))) % 149.24/149.41 True)) % 149.24/149.41 Clause #140 (by clausification #[139]): ∀ (a : Type) (a_1 : int), % 149.24/149.41 Or (Eq (monoid_mult a) False) % 149.24/149.41 (Or (Eq (number a) False) % 149.24/149.41 (Eq (power_power a (number_number_of a a_1) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.41 (times_times a (number_number_of a a_1) (number_number_of a a_1)))) % 149.24/149.41 Clause #141 (by superposition #[140, 98]): ∀ (a : int), % 149.24/149.41 Or (Eq (number int) False) % 149.24/149.41 (Or % 149.24/149.41 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.41 (times_times int (number_number_of int a) (number_number_of int a))) % 149.24/149.41 (Eq False True)) % 149.24/149.41 Clause #145 (by clausification #[25]): ∀ (a : int), Eq (Eq (times_times int pls a) pls) True % 149.24/149.41 Clause #146 (by clausification #[145]): ∀ (a : int), Eq (times_times int pls a) pls % 149.24/149.41 Clause #156 (by clausification #[78]): ∀ (a : int), Eq (Eq (plus_plus int pls a) a) True % 149.24/149.41 Clause #157 (by clausification #[156]): ∀ (a : int), Eq (plus_plus int pls a) a % 149.24/149.41 Clause #158 (by clausification #[77]): ∀ (a : int), Eq (Eq (plus_plus int a pls) a) True % 149.24/149.41 Clause #159 (by clausification #[158]): ∀ (a : int), Eq (plus_plus int a pls) a % 149.24/149.41 Clause #185 (by clausification #[96]): ∀ (a : Type), Eq (number_ring a → Eq (one_one a) (number_number_of a (bit1 pls))) True % 149.24/149.41 Clause #186 (by clausification #[185]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (Eq (one_one a) (number_number_of a (bit1 pls))) True) % 149.24/149.41 Clause #187 (by clausification #[186]): ∀ (a : Type), Or (Eq (number_ring a) False) (Eq (one_one a) (number_number_of a (bit1 pls))) % 149.24/149.41 Clause #188 (by superposition #[187, 101]): Or (Eq (one_one int) (number_number_of int (bit1 pls))) (Eq False True) % 149.24/149.41 Clause #189 (by clausification #[188]): Eq (one_one int) (number_number_of int (bit1 pls)) % 149.24/149.41 Clause #190 (by superposition #[189, 130]): Eq (one_one int) (bit1 pls) % 149.24/149.41 Clause #226 (by clausification #[9]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit1 K1) a) (plus_plus int (bit0 (times_times int K1 a)) a)) True % 149.24/149.41 Clause #227 (by clausification #[226]): ∀ (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 % 149.24/149.41 Clause #228 (by clausification #[227]): ∀ (a a_1 : int), Eq (times_times int (bit1 a) a_1) (plus_plus int (bit0 (times_times int a a_1)) a_1) % 149.24/149.41 Clause #230 (by superposition #[228, 146]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int (bit0 pls) a) % 149.24/149.41 Clause #231 (by forward demodulation #[230, 119]): ∀ (a : int), Eq (times_times int (bit1 pls) a) (plus_plus int pls a) % 149.24/149.41 Clause #232 (by forward demodulation #[231, 157]): ∀ (a : int), Eq (times_times int (bit1 pls) a) a % 149.24/149.41 Clause #370 (by clausification #[26]): ∀ (a : int), Eq (∀ (K1 : int), Eq (times_times int (bit0 K1) a) (bit0 (times_times int K1 a))) True % 149.24/149.41 Clause #371 (by clausification #[370]): ∀ (a a_1 : int), Eq (Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1))) True % 149.24/149.41 Clause #372 (by clausification #[371]): ∀ (a a_1 : int), Eq (times_times int (bit0 a) a_1) (bit0 (times_times int a a_1)) % 149.24/149.41 Clause #388 (by superposition #[372, 232]): ∀ (a : int), Eq (times_times int (bit0 (bit1 pls)) a) (bit0 a) % 149.24/149.41 Clause #410 (by superposition #[388, 372]): ∀ (a : int), Eq (times_times int (bit0 (bit0 (bit1 pls))) a) (bit0 (bit0 a)) % 149.24/149.41 Clause #606 (by clausification #[46]): ∀ (a : int), Eq (∀ (K1 : int), Eq (plus_plus int (bit0 K1) (bit1 a)) (bit1 (plus_plus int K1 a))) True % 149.24/149.41 Clause #607 (by clausification #[606]): ∀ (a a_1 : int), Eq (Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1))) True % 149.24/149.43 Clause #608 (by clausification #[607]): ∀ (a a_1 : int), Eq (plus_plus int (bit0 a) (bit1 a_1)) (bit1 (plus_plus int a a_1)) % 149.24/149.43 Clause #1586 (by clausification #[112]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (one_one int))) % 149.24/149.43 False % 149.24/149.43 Clause #1587 (by forward demodulation #[1586, 190]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (one_one int)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1588 (by forward demodulation #[1587, 190]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (number_number_of int (bit0 (bit0 (bit1 pls)))) m) (bit1 pls)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1589 (by forward demodulation #[1588, 130]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1590 (by forward demodulation #[1589, 410]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1591 (by forward demodulation #[1590, 608]): Eq % 149.24/149.43 (dvd_dvd int (bit1 (plus_plus int (bit0 m) pls)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1592 (by forward demodulation #[1591, 159]): Eq (dvd_dvd int (bit1 (bit0 m)) (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 False % 149.24/149.43 Clause #1600 (by forward demodulation #[131, 190]): Eq (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls)) % 149.24/149.43 Clause #1601 (by backward demodulation #[1600, 1592]): Eq (dvd_dvd int (bit1 (bit0 m)) (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) % 149.24/149.43 False % 149.24/149.43 Clause #1609 (by forward demodulation #[132, 190]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) % 149.24/149.43 (plus_plus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) (bit1 pls))) % 149.24/149.43 True % 149.24/149.43 Clause #1610 (by forward demodulation #[1609, 1600]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (one_one int)) % 149.24/149.43 (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) % 149.24/149.43 True % 149.24/149.43 Clause #1611 (by forward demodulation #[1610, 190]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (times_times int (bit0 (bit0 (bit1 pls))) m) (bit1 pls)) % 149.24/149.43 (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) % 149.24/149.43 True % 149.24/149.43 Clause #1612 (by forward demodulation #[1611, 410]): Eq % 149.24/149.43 (dvd_dvd int (plus_plus int (bit0 (bit0 m)) (bit1 pls)) % 149.24/149.43 (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) % 149.24/149.43 True % 149.24/149.43 Clause #1613 (by forward demodulation #[1612, 608]): Eq % 149.24/149.43 (dvd_dvd int (bit1 (plus_plus int (bit0 m) pls)) % 149.24/149.43 (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) % 149.24/149.43 True % 149.24/149.43 Clause #1614 (by forward demodulation #[1613, 159]): Eq (dvd_dvd int (bit1 (bit0 m)) (minus_minus int (power_power int s (number_number_of nat (bit0 (bit1 pls)))) min)) True % 149.24/149.43 Clause #1746 (by clausification #[141]): ∀ (a : int), % 149.24/149.43 Or (Eq (number int) False) % 149.24/149.43 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.43 (times_times int (number_number_of int a) (number_number_of int a))) % 149.24/149.43 Clause #1747 (by forward demodulation #[1746, 104]): ∀ (a : int), % 149.24/149.43 Or (Eq True False) % 149.24/149.43 (Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 149.24/149.43 (times_times int (number_number_of int a) (number_number_of int a))) % 149.24/149.43 Clause #1748 (by clausification #[1747]): ∀ (a : int), % 149.40/149.59 Eq (power_power int (number_number_of int a) (number_number_of nat (bit0 (bit1 pls)))) % 149.40/149.59 (times_times int (number_number_of int a) (number_number_of int a)) % 149.40/149.59 Clause #1749 (by forward demodulation #[1748, 130]): ∀ (a : int), % 149.40/149.59 Eq (power_power int a (number_number_of nat (bit0 (bit1 pls)))) % 149.40/149.59 (times_times int (number_number_of int a) (number_number_of int a)) % 149.40/149.59 Clause #1750 (by forward demodulation #[1749, 130]): ∀ (a : int), % 149.40/149.59 Eq (power_power int a (number_number_of nat (bit0 (bit1 pls)))) (times_times int (number_number_of int a) a) % 149.40/149.59 Clause #1751 (by forward demodulation #[1750, 130]): ∀ (a : int), Eq (power_power int a (number_number_of nat (bit0 (bit1 pls)))) (times_times int a a) % 149.40/149.59 Clause #1753 (by superposition #[1751, 1614]): Eq (dvd_dvd int (bit1 (bit0 m)) (minus_minus int (times_times int s s) min)) True % 149.40/149.59 Clause #27324 (by forward demodulation #[1601, 1751]): Eq (dvd_dvd int (bit1 (bit0 m)) (minus_minus int (times_times int s s) min)) False % 149.40/149.59 Clause #30351 (by superposition #[1753, 27324]): Eq False True % 149.40/149.59 Clause #30353 (by clausification #[30351]): False % 149.40/149.59 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------