%------------------------------------------------------------------------------ % 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 13.09s 13.26s % Output : Proof 13.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM926^1 : TPTP v9.2.0. Released v5.3.0. % 0.03/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 07:03:53 EDT 2025 % 0.13/0.34 % CPUTime : % 13.09/13.26 SZS status Theorem for theBenchmark.p % 13.09/13.26 SZS output start Proof for theBenchmark.p % 13.09/13.26 Clause #0 (by assumption #[]): Eq (ord_less_eq_int one_one_int t) True % 13.09/13.26 Clause #1 (by assumption #[]): Eq % 13.09/13.26 (Eq t one_one_int → % 13.09/13.26 Exists fun X => % 13.09/13.26 Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True % 13.09/13.26 Clause #2 (by assumption #[]): Eq % 13.09/13.26 (ord_less_int one_one_int t → % 13.09/13.26 Exists fun X => % 13.09/13.26 Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True % 13.09/13.26 Clause #24 (by assumption #[]): Eq (Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls)))) True % 13.09/13.26 Clause #28 (by assumption #[]): Eq (∀ (Z W : int), Iff (ord_less_int Z W) (And (ord_less_eq_int Z W) (Ne Z W))) True % 13.09/13.26 Clause #46 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 13.09/13.26 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 % 13.09/13.26 Clause #93 (by assumption #[]): Eq (∀ (A C : int), Eq (plus_plus_int A C) (plus_plus_int C A)) True % 13.09/13.26 Clause #100 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of_int K) K) True % 13.09/13.26 Clause #107 (by assumption #[]): Eq % 13.09/13.26 (Not % 13.09/13.26 (Exists fun X => % 13.09/13.26 Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 13.09/13.26 True % 13.09/13.26 Clause #110 (by clausification #[1]): Or (Eq (Eq t one_one_int) False) % 13.09/13.26 (Eq % 13.09/13.26 (Exists fun X => % 13.09/13.26 Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True) % 13.09/13.26 Clause #111 (by clausification #[110]): Or % 13.09/13.26 (Eq % 13.09/13.26 (Exists fun X => % 13.09/13.26 Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True) % 13.09/13.26 (Ne t one_one_int) % 13.09/13.26 Clause #112 (by clausification #[111]): ∀ (a : int), % 13.09/13.26 Or (Ne t one_one_int) % 13.09/13.26 (Eq % 13.09/13.26 (Exists fun Y => % 13.09/13.26 Eq % 13.09/13.26 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True) % 13.09/13.26 Clause #113 (by clausification #[112]): ∀ (a a_1 : int), % 13.09/13.26 Or (Ne t one_one_int) % 13.09/13.26 (Eq % 13.09/13.26 (Eq % 13.09/13.26 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 True) % 13.09/13.26 Clause #114 (by clausification #[113]): ∀ (a a_1 : int), % 13.09/13.26 Or (Ne t one_one_int) % 13.09/13.26 (Eq % 13.09/13.26 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.26 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.26 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.26 Clause #117 (by clausification #[100]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 13.09/13.26 Clause #118 (by clausification #[117]): ∀ (a : int), Eq (number_number_of_int a) a % 13.09/13.28 Clause #120 (by backward demodulation #[118, 114]): ∀ (a a_1 : int), % 13.09/13.28 Or (Ne t one_one_int) % 13.09/13.28 (Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.09/13.28 Clause #123 (by clausification #[2]): Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (Exists fun X => % 13.09/13.28 Exists fun Y => % 13.09/13.28 Eq % 13.09/13.28 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.28 True) % 13.09/13.28 Clause #124 (by clausification #[123]): ∀ (a : int), % 13.09/13.28 Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (Exists fun Y => % 13.09/13.28 Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.28 True) % 13.09/13.28 Clause #125 (by clausification #[124]): ∀ (a a_1 : int), % 13.09/13.28 Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.28 True) % 13.09/13.28 Clause #126 (by clausification #[125]): ∀ (a a_1 : int), % 13.09/13.28 Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.09/13.28 Clause #127 (by forward demodulation #[126, 118]): ∀ (a a_1 : int), % 13.09/13.28 Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 13.09/13.28 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.09/13.28 Clause #159 (by clausification #[24]): Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls))) % 13.09/13.28 Clause #160 (by superposition #[159, 118]): Eq (plus_plus_int one_one_int one_one_int) (bit0 (bit1 pls)) % 13.09/13.28 Clause #162 (by backward demodulation #[160, 127]): ∀ (a a_1 : int), % 13.09/13.28 Or (Eq (ord_less_int one_one_int t) False) % 13.09/13.28 (Eq % 13.09/13.28 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.09/13.28 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 13.09/13.28 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.09/13.28 Clause #259 (by clausification #[46]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 13.09/13.28 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)) % 13.09/13.28 Clause #452 (by clausification #[93]): ∀ (a : int), Eq (∀ (C : int), Eq (plus_plus_int a C) (plus_plus_int C a)) True % 13.09/13.28 Clause #453 (by clausification #[452]): ∀ (a a_1 : int), Eq (Eq (plus_plus_int a a_1) (plus_plus_int a_1 a)) True % 13.09/13.28 Clause #454 (by clausification #[453]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 13.09/13.28 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 % 13.09/13.28 Clause #501 (by clausification #[500]): ∀ (a a_1 : int), Eq (Eq (times_times_int a a_1) (times_times_int a_1 a)) True % 13.09/13.28 Clause #502 (by clausification #[501]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int a_1 a) % 13.09/13.28 Clause #519 (by clausification #[28]): ∀ (a : int), Eq (∀ (W : int), Iff (ord_less_int a W) (And (ord_less_eq_int a W) (Ne a W))) True % 13.12/13.29 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 % 13.12/13.29 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) % 13.12/13.29 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)) % 13.12/13.29 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)) % 13.12/13.29 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)) % 13.12/13.29 Clause #544 (by clausification #[525]): Or (Eq (ord_less_int one_one_int t) True) (Eq one_one_int t) % 13.12/13.29 Clause #4762 (by clausification #[107]): Eq % 13.12/13.29 (Exists fun X => % 13.12/13.29 Exists fun Y => % 13.12/13.29 Eq % 13.12/13.29 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.12/13.29 False % 13.12/13.29 Clause #4763 (by clausification #[4762]): ∀ (a : int), % 13.12/13.29 Eq % 13.12/13.29 (Exists fun Y => % 13.12/13.29 Eq % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.12/13.29 False % 13.12/13.29 Clause #4764 (by clausification #[4763]): ∀ (a a_1 : int), % 13.12/13.29 Eq % 13.12/13.29 (Eq % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 13.12/13.29 False % 13.12/13.29 Clause #4765 (by clausification #[4764]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 13.12/13.29 Clause #4766 (by forward demodulation #[4765, 160]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int a_1 (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 13.12/13.29 Clause #4767 (by forward demodulation #[4766, 260]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.29 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 13.12/13.29 Clause #4768 (by forward demodulation #[4767, 160]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 13.12/13.29 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 13.12/13.29 Clause #4769 (by forward demodulation #[4768, 260]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.29 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.29 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 13.12/13.29 Clause #4770 (by forward demodulation #[4769, 454]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.29 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.29 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)) % 13.12/13.29 Clause #4771 (by forward demodulation #[4770, 502]): ∀ (a a_1 : int), % 13.12/13.29 Ne % 13.12/13.29 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))) % 13.12/13.31 Clause #4772 (by forward demodulation #[4771, 118]): ∀ (a a_1 : int), % 13.12/13.31 Ne % 13.12/13.31 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 13.12/13.31 Clause #4773 (by forward demodulation #[4772, 160]): ∀ (a a_1 : int), % 13.12/13.31 Ne % 13.12/13.31 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 13.12/13.31 Clause #4882 (by forward demodulation #[120, 160]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 13.12/13.31 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.12/13.31 Clause #4883 (by forward demodulation #[4882, 260]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.12/13.31 Clause #4884 (by forward demodulation #[4883, 160]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.12/13.31 Clause #4885 (by forward demodulation #[4884, 260]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.12/13.31 Clause #4886 (by forward demodulation #[4885, 454]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m))) % 13.12/13.31 Clause #4887 (by forward demodulation #[4886, 502]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls)))))) % 13.12/13.31 Clause #4888 (by forward demodulation #[4887, 160]): ∀ (a a_1 : int), % 13.12/13.31 Or (Ne t one_one_int) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.12/13.31 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.12/13.31 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int))))) % 13.12/13.31 Clause #4889 (by forward contextual literal cutting #[4888, 4773]): Ne t one_one_int % 13.12/13.31 Clause #4891 (by backward contextual literal cutting #[4889, 544]): Eq (ord_less_int one_one_int t) True % 13.12/13.31 Clause #5008 (by forward demodulation #[162, 4891]): ∀ (a a_1 : int), % 13.12/13.31 Or (Eq True False) % 13.12/13.31 (Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.12/13.31 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 13.12/13.31 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 13.12/13.31 Clause #5009 (by clausification #[5008]): ∀ (a a_1 : int), % 13.12/13.31 Eq % 13.12/13.31 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 13.16/13.34 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 13.16/13.34 Clause #5010 (by forward demodulation #[5009, 260]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 13.16/13.34 Clause #5011 (by forward demodulation #[5010, 160]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 13.16/13.34 Clause #5012 (by forward demodulation #[5011, 260]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 13.16/13.34 Clause #5013 (by forward demodulation #[5012, 454]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m)) % 13.16/13.34 Clause #5014 (by forward demodulation #[5013, 502]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 13.16/13.34 Clause #5015 (by forward demodulation #[5014, 160]): ∀ (a a_1 : int), % 13.16/13.34 Eq % 13.16/13.34 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 13.16/13.34 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 13.16/13.34 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 13.16/13.34 Clause #5016 (by forward contextual literal cutting #[5015, 4773]): False % 13.16/13.34 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------