%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM924+2 : TPTP v9.2.0. Released v5.3.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:33 PM UTC 2025 % Result : Theorem 198.70s 198.86s % Output : Proof 198.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM924+2 : TPTP v9.2.0. Released v5.3.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 08:08:08 EDT 2025 % 0.13/0.34 % CPUTime : % 198.70/198.86 SZS status Theorem for theBenchmark.p % 198.70/198.86 SZS output start Proof for theBenchmark.p % 198.70/198.86 Clause #1 (by assumption #[]): Eq (is_int one_one_int) True % 198.70/198.86 Clause #4 (by assumption #[]): Eq (is_int zero_zero_int) True % 198.70/198.86 Clause #7 (by assumption #[]): Eq (∀ (B_1_1 : Iota), is_int B_1_1 → is_int (bit1 B_1_1)) True % 198.70/198.86 Clause #19 (by assumption #[]): Eq % 198.70/198.86 (ord_less_int % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t) % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 198.70/198.86 zero_zero_int)) % 198.70/198.86 True % 198.70/198.86 Clause #20 (by assumption #[]): Eq % 198.70/198.86 (Eq (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t)) % 198.70/198.86 True % 198.70/198.86 Clause #51 (by assumption #[]): Eq (∀ (K_1 : Iota), is_int K_1 → Eq (number_number_of_int K_1) K_1) True % 198.70/198.86 Clause #52 (by assumption #[]): Eq (∀ (Z W : Iota), Eq (times_times_int Z W) (times_times_int W Z)) True % 198.70/198.86 Clause #99 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 198.70/198.86 Clause #100 (by assumption #[]): Eq (∀ (W : Iota), Eq (times_times_int pls W) pls) True % 198.70/198.86 Clause #103 (by assumption #[]): Eq (∀ (Z : Iota), is_int Z → Eq (times_times_int Z one_one_int) Z) True % 198.70/198.86 Clause #142 (by assumption #[]): Eq (∀ (Z W : Iota), Eq (plus_plus_int Z W) (plus_plus_int W Z)) True % 198.70/198.86 Clause #163 (by assumption #[]): Eq % 198.70/198.86 (∀ (X_19 Y_11 : Iota), % 198.70/198.86 Not (ord_less_int (plus_plus_int (times_times_int X_19 X_19) (times_times_int Y_11 Y_11)) zero_zero_int)) % 198.70/198.86 True % 198.70/198.86 Clause #168 (by assumption #[]): Eq (Eq one_one_int (number_number_of_int (bit1 pls))) True % 198.70/198.86 Clause #180 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 198.70/198.86 Clause #205 (by assumption #[]): Eq (∀ (A_50 : Iota), Eq (power_power_int A_50 (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int A_50 A_50)) % 198.70/198.86 True % 198.70/198.86 Clause #709 (by clausification #[7]): ∀ (a : Iota), Eq (is_int a → is_int (bit1 a)) True % 198.70/198.86 Clause #710 (by clausification #[709]): ∀ (a : Iota), Or (Eq (is_int a) False) (Eq (is_int (bit1 a)) True) % 198.70/198.86 Clause #717 (by superposition #[710, 4]): Or (Eq (is_int (bit1 zero_zero_int)) True) (Eq False True) % 198.70/198.86 Clause #737 (by clausification #[180]): Eq pls zero_zero_int % 198.70/198.86 Clause #807 (by forward demodulation #[19, 737]): Eq % 198.70/198.86 (ord_less_int % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t) % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 198.70/198.86 pls)) % 198.70/198.86 True % 198.70/198.86 Clause #838 (by clausification #[20]): Eq (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) t) % 198.70/198.86 Clause #839 (by backward demodulation #[838, 807]): Eq % 198.70/198.86 (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) % 198.70/198.86 (times_times_int (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 198.70/198.86 pls)) % 198.70/198.86 True % 198.70/198.86 Clause #892 (by clausification #[717]): Eq (is_int (bit1 zero_zero_int)) True % 198.70/198.86 Clause #893 (by forward demodulation #[892, 737]): Eq (is_int (bit1 pls)) True % 198.70/198.86 Clause #1336 (by clausification #[168]): Eq one_one_int (number_number_of_int (bit1 pls)) % 198.70/198.86 Clause #2303 (by clausification #[51]): ∀ (a : Iota), Eq (is_int a → Eq (number_number_of_int a) a) True % 198.70/198.86 Clause #2304 (by clausification #[2303]): ∀ (a : Iota), Or (Eq (is_int a) False) (Eq (Eq (number_number_of_int a) a) True) % 198.70/198.86 Clause #2305 (by clausification #[2304]): ∀ (a : Iota), Or (Eq (is_int a) False) (Eq (number_number_of_int a) a) % 198.70/198.86 Clause #2325 (by superposition #[2305, 893]): Or (Eq (number_number_of_int (bit1 pls)) (bit1 pls)) (Eq False True) % 198.70/198.86 Clause #2437 (by clausification #[52]): ∀ (a : Iota), Eq (∀ (W : Iota), Eq (times_times_int a W) (times_times_int W a)) True % 198.70/198.86 Clause #2438 (by clausification #[2437]): ∀ (a a_1 : Iota), Eq (Eq (times_times_int a a_1) (times_times_int a_1 a)) True % 198.70/198.88 Clause #2439 (by clausification #[2438]): ∀ (a a_1 : Iota), Eq (times_times_int a a_1) (times_times_int a_1 a) % 198.70/198.88 Clause #2500 (by clausification #[2325]): Eq (number_number_of_int (bit1 pls)) (bit1 pls) % 198.70/198.88 Clause #2501 (by superposition #[2500, 1336]): Eq one_one_int (bit1 pls) % 198.70/198.88 Clause #4177 (by clausification #[99]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 198.70/198.88 Clause #4178 (by forward demodulation #[4177, 2501]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 198.70/198.88 Clause #4198 (by clausification #[100]): ∀ (a : Iota), Eq (Eq (times_times_int pls a) pls) True % 198.70/198.88 Clause #4199 (by clausification #[4198]): ∀ (a : Iota), Eq (times_times_int pls a) pls % 198.70/198.88 Clause #4205 (by superposition #[4199, 2439]): ∀ (a : Iota), Eq (times_times_int a pls) pls % 198.70/198.88 Clause #4251 (by clausification #[103]): ∀ (a : Iota), Eq (is_int a → Eq (times_times_int a one_one_int) a) True % 198.70/198.88 Clause #4252 (by clausification #[4251]): ∀ (a : Iota), Or (Eq (is_int a) False) (Eq (Eq (times_times_int a one_one_int) a) True) % 198.70/198.88 Clause #4253 (by clausification #[4252]): ∀ (a : Iota), Or (Eq (is_int a) False) (Eq (times_times_int a one_one_int) a) % 198.70/198.88 Clause #4260 (by superposition #[4253, 1]): Or (Eq (times_times_int one_one_int one_one_int) one_one_int) (Eq False True) % 198.70/198.88 Clause #4373 (by clausification #[4260]): Eq (times_times_int one_one_int one_one_int) one_one_int % 198.70/198.88 Clause #5738 (by clausification #[142]): ∀ (a : Iota), Eq (∀ (W : Iota), Eq (plus_plus_int a W) (plus_plus_int W a)) True % 198.70/198.88 Clause #5739 (by clausification #[5738]): ∀ (a a_1 : Iota), Eq (Eq (plus_plus_int a a_1) (plus_plus_int a_1 a)) True % 198.70/198.88 Clause #5740 (by clausification #[5739]): ∀ (a a_1 : Iota), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 198.70/198.88 Clause #6531 (by clausification #[163]): ∀ (a : Iota), % 198.70/198.88 Eq % 198.70/198.88 (∀ (Y_11 : Iota), % 198.70/198.88 Not (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int Y_11 Y_11)) zero_zero_int)) % 198.70/198.88 True % 198.70/198.88 Clause #6532 (by clausification #[6531]): ∀ (a a_1 : Iota), % 198.70/198.88 Eq (Not (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) zero_zero_int)) True % 198.70/198.88 Clause #6533 (by clausification #[6532]): ∀ (a a_1 : Iota), Eq (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) zero_zero_int) False % 198.70/198.88 Clause #6534 (by forward demodulation #[6533, 737]): ∀ (a a_1 : Iota), Eq (ord_less_int (plus_plus_int (times_times_int a a) (times_times_int a_1 a_1)) pls) False % 198.70/198.88 Clause #6544 (by superposition #[6534, 4373]): ∀ (a : Iota), Eq (ord_less_int (plus_plus_int one_one_int (times_times_int a a)) pls) False % 198.70/198.88 Clause #7639 (by clausification #[205]): ∀ (a : Iota), Eq (Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int a a)) True % 198.70/198.88 Clause #7640 (by clausification #[7639]): ∀ (a : Iota), Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) (times_times_int a a) % 198.70/198.88 Clause #7641 (by forward demodulation #[7640, 2501]): ∀ (a : Iota), Eq (power_power_int a (number_number_of_nat (bit0 one_one_int))) (times_times_int a a) % 198.70/198.88 Clause #7642 (by forward demodulation #[7641, 4178]): ∀ (a : Iota), Eq (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) (times_times_int a a) % 198.70/198.88 Clause #49705 (by forward demodulation #[839, 4205]): Eq (ord_less_int (plus_plus_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls)))) one_one_int) pls) True % 198.70/198.88 Clause #49706 (by forward demodulation #[49705, 5740]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (number_number_of_nat (bit0 (bit1 pls))))) pls) True % 198.70/198.88 Clause #49707 (by forward demodulation #[49706, 2501]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (number_number_of_nat (bit0 one_one_int)))) pls) True % 198.70/198.88 Clause #49708 (by forward demodulation #[49707, 4178]): Eq (ord_less_int (plus_plus_int one_one_int (power_power_int s (plus_plus_nat one_one_nat one_one_nat))) pls) True % 198.70/198.88 Clause #49709 (by forward demodulation #[49708, 7642]): Eq (ord_less_int (plus_plus_int one_one_int (times_times_int s s)) pls) True % 198.96/199.12 Clause #49710 (by superposition #[49709, 6544]): Eq True False % 198.96/199.12 Clause #49728 (by clausification #[49710]): False % 198.96/199.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------