%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM925^1 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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:35 PM UTC 2025 % Result : Theorem 6.93s 7.14s % Output : Proof 6.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM925^1 : TPTP v9.2.0. Released v5.3.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n015.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 08:53:53 EDT 2025 % 0.14/0.35 % CPUTime : % 6.93/7.14 SZS status Theorem for theBenchmark.p % 6.93/7.14 SZS output start Proof for theBenchmark.p % 6.93/7.14 Clause #0 (by assumption #[]): Eq (ord_less_int zero_zero_int (plus_plus_int one_one_int (semiri1621563631at_int n))) True % 6.93/7.14 Clause #7 (by assumption #[]): Eq % 6.93/7.14 (∀ (A_7 : int), % 6.93/7.14 Iff (Eq (power_power_int A_7 (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_int) (Eq A_7 zero_zero_int)) % 6.93/7.14 True % 6.93/7.14 Clause #11 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 6.93/7.14 Clause #32 (by assumption #[]): Eq (Not (ord_less_int pls pls)) True % 6.93/7.14 Clause #71 (by assumption #[]): Eq (Eq pls zero_zero_int) True % 6.93/7.14 Clause #73 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus_int K pls) K) True % 6.93/7.14 Clause #88 (by assumption #[]): Eq (∀ (K : int), Eq (bit1 K) (plus_plus_int (plus_plus_int one_one_int K) K)) True % 6.93/7.14 Clause #95 (by assumption #[]): Eq % 6.93/7.14 (Not % 6.93/7.14 (Ne % 6.93/7.14 (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 6.93/7.14 zero_zero_int)) % 6.93/7.14 True % 6.93/7.14 Clause #97 (by clausification #[71]): Eq pls zero_zero_int % 6.93/7.14 Clause #100 (by forward demodulation #[0, 97]): Eq (ord_less_int pls (plus_plus_int one_one_int (semiri1621563631at_int n))) True % 6.93/7.14 Clause #101 (by clausification #[32]): Eq (ord_less_int pls pls) False % 6.93/7.14 Clause #146 (by clausification #[73]): ∀ (a : int), Eq (Eq (plus_plus_int a pls) a) True % 6.93/7.14 Clause #147 (by clausification #[146]): ∀ (a : int), Eq (plus_plus_int a pls) a % 6.93/7.14 Clause #168 (by clausification #[7]): ∀ (a : int), % 6.93/7.14 Eq (Iff (Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_int) (Eq a zero_zero_int)) True % 6.93/7.14 Clause #170 (by clausification #[168]): ∀ (a : int), % 6.93/7.14 Or (Eq (Eq (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_int) False) % 6.93/7.14 (Eq (Eq a zero_zero_int) True) % 6.93/7.14 Clause #206 (by clausification #[11]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 6.93/7.14 Clause #2035 (by clausification #[88]): ∀ (a : int), Eq (Eq (bit1 a) (plus_plus_int (plus_plus_int one_one_int a) a)) True % 6.93/7.14 Clause #2036 (by clausification #[2035]): ∀ (a : int), Eq (bit1 a) (plus_plus_int (plus_plus_int one_one_int a) a) % 6.93/7.14 Clause #2037 (by superposition #[2036, 147]): Eq (bit1 pls) (plus_plus_int one_one_int pls) % 6.93/7.14 Clause #2058 (by superposition #[2037, 147]): Eq (bit1 pls) one_one_int % 6.93/7.14 Clause #2070 (by backward demodulation #[2058, 206]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 6.93/7.14 Clause #2376 (by clausification #[95]): Eq % 6.93/7.14 (Ne (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 6.93/7.14 zero_zero_int) % 6.93/7.14 False % 6.93/7.14 Clause #2377 (by clausification #[2376]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 (bit1 pls)))) % 6.93/7.14 zero_zero_int % 6.93/7.14 Clause #2378 (by forward demodulation #[2377, 2058]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (number_number_of_nat (bit0 one_one_int))) % 6.93/7.14 zero_zero_int % 6.93/7.14 Clause #2379 (by forward demodulation #[2378, 2070]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (plus_plus_nat one_one_nat one_one_nat)) % 6.93/7.14 zero_zero_int % 6.93/7.14 Clause #2380 (by forward demodulation #[2379, 97]): Eq (power_power_int (plus_plus_int one_one_int (semiri1621563631at_int n)) (plus_plus_nat one_one_nat one_one_nat)) pls % 6.93/7.14 Clause #2486 (by clausification #[170]): ∀ (a : int), % 6.93/7.14 Or (Eq (Eq a zero_zero_int) True) (Ne (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_int) % 6.93/7.14 Clause #2487 (by clausification #[2486]): ∀ (a : int), Or (Ne (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) zero_zero_int) (Eq a zero_zero_int) % 6.93/7.14 Clause #2488 (by forward demodulation #[2487, 2058]): ∀ (a : int), Or (Ne (power_power_int a (number_number_of_nat (bit0 one_one_int))) zero_zero_int) (Eq a zero_zero_int) % 6.93/7.14 Clause #2489 (by forward demodulation #[2488, 2070]): ∀ (a : int), Or (Ne (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) zero_zero_int) (Eq a zero_zero_int) % 6.93/7.14 Clause #2490 (by forward demodulation #[2489, 97]): ∀ (a : int), Or (Ne (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) pls) (Eq a zero_zero_int) % 6.93/7.14 Clause #2491 (by forward demodulation #[2490, 97]): ∀ (a : int), Or (Ne (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) pls) (Eq a pls) % 6.93/7.14 Clause #2493 (by superposition #[2491, 2380]): Or (Ne pls pls) (Eq (plus_plus_int one_one_int (semiri1621563631at_int n)) pls) % 6.93/7.14 Clause #2496 (by eliminate resolved literals #[2493]): Eq (plus_plus_int one_one_int (semiri1621563631at_int n)) pls % 6.93/7.14 Clause #2497 (by backward demodulation #[2496, 100]): Eq (ord_less_int pls pls) True % 6.93/7.14 Clause #2511 (by superposition #[2497, 101]): Eq True False % 6.93/7.14 Clause #2524 (by clausification #[2511]): False % 6.93/7.14 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------