%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM926_1 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:36 PM UTC 2025 % Result : Theorem 11.25s 11.43s % Output : Proof 11.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NUM926_1 : TPTP v9.2.0. Released v5.3.0. % 0.13/0.13 % Command : duper %s % 0.13/0.34 % Computer : n020.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:58:08 EDT 2025 % 0.13/0.34 % CPUTime : % 11.25/11.43 SZS status Theorem for theBenchmark.p % 11.25/11.43 SZS output start Proof for theBenchmark.p % 11.25/11.43 Clause #0 (by assumption #[]): Eq (ord_less_eq_int one_one_int t) True % 11.25/11.43 Clause #1 (by assumption #[]): Eq % 11.25/11.43 (Eq t one_one_int → % 11.25/11.43 Exists fun X => % 11.25/11.43 Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True % 11.25/11.43 Clause #2 (by assumption #[]): Eq % 11.25/11.43 (ord_less_int one_one_int t → % 11.25/11.43 Exists fun X => % 11.25/11.43 Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True % 11.25/11.43 Clause #24 (by assumption #[]): Eq (Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls)))) True % 11.25/11.43 Clause #28 (by assumption #[]): Eq (∀ (Z_1 W_1 : int), Iff (ord_less_int Z_1 W_1) (And (ord_less_eq_int Z_1 W_1) (Ne Z_1 W_1))) True % 11.25/11.43 Clause #46 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 11.25/11.43 Clause #81 (by assumption #[]): Eq (∀ (A_6 B_3 : int), Eq (times_times_int A_6 B_3) (times_times_int B_3 A_6)) True % 11.25/11.43 Clause #93 (by assumption #[]): Eq (∀ (A C : int), Eq (plus_plus_int A C) (plus_plus_int C A)) True % 11.25/11.43 Clause #100 (by assumption #[]): Eq (∀ (K_1 : int), Eq (number_number_of_int K_1) K_1) True % 11.25/11.43 Clause #107 (by assumption #[]): Eq % 11.25/11.43 (Not % 11.25/11.43 (Exists fun X => % 11.25/11.43 Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 11.25/11.43 True % 11.25/11.43 Clause #110 (by clausification #[1]): Or (Eq (Eq t one_one_int) False) % 11.25/11.43 (Eq % 11.25/11.43 (Exists fun X => % 11.25/11.43 Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True) % 11.25/11.43 Clause #111 (by clausification #[110]): Or % 11.25/11.43 (Eq % 11.25/11.43 (Exists fun X => % 11.25/11.43 Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True) % 11.25/11.43 (Ne t one_one_int) % 11.25/11.43 Clause #112 (by clausification #[111]): ∀ (a : int), % 11.25/11.43 Or (Ne t one_one_int) % 11.25/11.43 (Eq % 11.25/11.43 (Exists fun Y => % 11.25/11.43 Eq % 11.25/11.43 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True) % 11.25/11.43 Clause #113 (by clausification #[112]): ∀ (a a_1 : int), % 11.25/11.43 Or (Ne t one_one_int) % 11.25/11.43 (Eq % 11.25/11.43 (Eq % 11.25/11.43 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 True) % 11.25/11.43 Clause #114 (by clausification #[113]): ∀ (a a_1 : int), % 11.25/11.43 Or (Ne t one_one_int) % 11.25/11.43 (Eq % 11.25/11.43 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.43 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.43 Clause #117 (by clausification #[100]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 11.25/11.43 Clause #118 (by clausification #[117]): ∀ (a : int), Eq (number_number_of_int a) a % 11.25/11.45 Clause #120 (by backward demodulation #[118, 114]): ∀ (a a_1 : int), % 11.25/11.45 Or (Ne t one_one_int) % 11.25/11.45 (Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.45 Clause #123 (by clausification #[2]): Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (Exists fun X => % 11.25/11.45 Exists fun Y => % 11.25/11.45 Eq % 11.25/11.45 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.45 True) % 11.25/11.45 Clause #124 (by clausification #[123]): ∀ (a : int), % 11.25/11.45 Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (Exists fun Y => % 11.25/11.45 Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.45 True) % 11.25/11.45 Clause #125 (by clausification #[124]): ∀ (a a_1 : int), % 11.25/11.45 Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.45 True) % 11.25/11.45 Clause #126 (by clausification #[125]): ∀ (a a_1 : int), % 11.25/11.45 Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.45 Clause #127 (by forward demodulation #[126, 118]): ∀ (a a_1 : int), % 11.25/11.45 Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.45 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.45 Clause #159 (by clausification #[24]): Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls))) % 11.25/11.45 Clause #160 (by superposition #[159, 118]): Eq (plus_plus_int one_one_int one_one_int) (bit0 (bit1 pls)) % 11.25/11.45 Clause #162 (by backward demodulation #[160, 127]): ∀ (a a_1 : int), % 11.25/11.45 Or (Eq (ord_less_int one_one_int t) False) % 11.25/11.45 (Eq % 11.25/11.45 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.45 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.25/11.45 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.45 Clause #259 (by clausification #[46]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 11.25/11.45 Clause #260 (by forward demodulation #[259, 160]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (plus_plus_int one_one_int one_one_int)) % 11.25/11.45 Clause #452 (by clausification #[93]): ∀ (a : int), Eq (∀ (C : int), Eq (plus_plus_int a C) (plus_plus_int C a)) True % 11.25/11.45 Clause #453 (by clausification #[452]): ∀ (a a_1 : int), Eq (Eq (plus_plus_int a a_1) (plus_plus_int a_1 a)) True % 11.25/11.45 Clause #454 (by clausification #[453]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 11.25/11.45 Clause #500 (by clausification #[81]): ∀ (a : int), Eq (∀ (B_3 : int), Eq (times_times_int a B_3) (times_times_int B_3 a)) True % 11.25/11.45 Clause #501 (by clausification #[500]): ∀ (a a_1 : int), Eq (Eq (times_times_int a a_1) (times_times_int a_1 a)) True % 11.25/11.45 Clause #502 (by clausification #[501]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int a_1 a) % 11.25/11.45 Clause #519 (by clausification #[28]): ∀ (a : int), Eq (∀ (W_1 : int), Iff (ord_less_int a W_1) (And (ord_less_eq_int a W_1) (Ne a W_1))) True % 11.25/11.46 Clause #520 (by clausification #[519]): ∀ (a a_1 : int), Eq (Iff (ord_less_int a a_1) (And (ord_less_eq_int a a_1) (Ne a a_1))) True % 11.25/11.46 Clause #521 (by clausification #[520]): ∀ (a a_1 : int), Or (Eq (ord_less_int a a_1) True) (Eq (And (ord_less_eq_int a a_1) (Ne a a_1)) False) % 11.25/11.46 Clause #523 (by clausification #[521]): ∀ (a a_1 : int), Or (Eq (ord_less_int a a_1) True) (Or (Eq (ord_less_eq_int a a_1) False) (Eq (Ne a a_1) False)) % 11.25/11.46 Clause #524 (by clausification #[523]): ∀ (a a_1 : int), Or (Eq (ord_less_int a a_1) True) (Or (Eq (ord_less_eq_int a a_1) False) (Eq a a_1)) % 11.25/11.46 Clause #525 (by superposition #[524, 0]): Or (Eq (ord_less_int one_one_int t) True) (Or (Eq one_one_int t) (Eq False True)) % 11.25/11.46 Clause #544 (by clausification #[525]): Or (Eq (ord_less_int one_one_int t) True) (Eq one_one_int t) % 11.25/11.46 Clause #4762 (by clausification #[107]): Eq % 11.25/11.46 (Exists fun X => % 11.25/11.46 Exists fun Y => % 11.25/11.46 Eq % 11.25/11.46 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.46 False % 11.25/11.46 Clause #4763 (by clausification #[4762]): ∀ (a : int), % 11.25/11.46 Eq % 11.25/11.46 (Exists fun Y => % 11.25/11.46 Eq % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.46 False % 11.25/11.46 Clause #4764 (by clausification #[4763]): ∀ (a a_1 : int), % 11.25/11.46 Eq % 11.25/11.46 (Eq % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.25/11.46 False % 11.25/11.46 Clause #4765 (by clausification #[4764]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.25/11.46 Clause #4766 (by forward demodulation #[4765, 160]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int a_1 (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.25/11.46 Clause #4767 (by forward demodulation #[4766, 260]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.46 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.25/11.46 Clause #4768 (by forward demodulation #[4767, 160]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.25/11.46 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.25/11.46 Clause #4769 (by forward demodulation #[4768, 260]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.46 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.46 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.25/11.46 Clause #4770 (by forward demodulation #[4769, 454]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.46 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.46 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)) % 11.25/11.46 Clause #4771 (by forward demodulation #[4770, 502]): ∀ (a a_1 : int), % 11.25/11.46 Ne % 11.25/11.46 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))) % 11.25/11.48 Clause #4772 (by forward demodulation #[4771, 118]): ∀ (a a_1 : int), % 11.25/11.48 Ne % 11.25/11.48 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 11.25/11.48 Clause #4773 (by forward demodulation #[4772, 160]): ∀ (a a_1 : int), % 11.25/11.48 Ne % 11.25/11.48 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 11.25/11.48 Clause #4882 (by forward demodulation #[120, 160]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.25/11.48 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.48 Clause #4883 (by forward demodulation #[4882, 260]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.48 Clause #4884 (by forward demodulation #[4883, 160]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.48 Clause #4885 (by forward demodulation #[4884, 260]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.48 Clause #4886 (by forward demodulation #[4885, 454]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m))) % 11.25/11.48 Clause #4887 (by forward demodulation #[4886, 502]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls)))))) % 11.25/11.48 Clause #4888 (by forward demodulation #[4887, 160]): ∀ (a a_1 : int), % 11.25/11.48 Or (Ne t one_one_int) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.25/11.48 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.25/11.48 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int))))) % 11.25/11.48 Clause #4889 (by forward contextual literal cutting #[4888, 4773]): Ne t one_one_int % 11.25/11.48 Clause #4891 (by backward contextual literal cutting #[4889, 544]): Eq (ord_less_int one_one_int t) True % 11.25/11.48 Clause #5008 (by forward demodulation #[162, 4891]): ∀ (a a_1 : int), % 11.25/11.48 Or (Eq True False) % 11.25/11.48 (Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.25/11.48 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.25/11.48 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.25/11.48 Clause #5009 (by clausification #[5008]): ∀ (a a_1 : int), % 11.25/11.48 Eq % 11.25/11.48 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.32/11.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.32/11.50 Clause #5010 (by forward demodulation #[5009, 260]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.32/11.50 Clause #5011 (by forward demodulation #[5010, 160]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.32/11.50 Clause #5012 (by forward demodulation #[5011, 260]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.32/11.50 Clause #5013 (by forward demodulation #[5012, 454]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m)) % 11.32/11.50 Clause #5014 (by forward demodulation #[5013, 502]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 11.32/11.50 Clause #5015 (by forward demodulation #[5014, 160]): ∀ (a a_1 : int), % 11.32/11.50 Eq % 11.32/11.50 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.32/11.50 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.32/11.50 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 11.32/11.50 Clause #5016 (by forward contextual literal cutting #[5015, 4773]): False % 11.32/11.50 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------