%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM926+1 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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.47s 11.66s % Output : Proof 11.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM926+1 : TPTP v9.2.0. Released v5.3.0. % 0.11/0.13 % Command : duper %s % 0.13/0.35 % Computer : n031.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 07:23:08 EDT 2025 % 0.13/0.35 % CPUTime : % 11.47/11.66 SZS status Theorem for theBenchmark.p % 11.47/11.66 SZS output start Proof for theBenchmark.p % 11.47/11.66 Clause #0 (by assumption #[]): Eq (ord_less_eq_int one_one_int t) True % 11.47/11.66 Clause #1 (by assumption #[]): Eq % 11.47/11.66 (Eq t one_one_int → % 11.47/11.66 Exists fun X => % 11.47/11.66 Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True % 11.47/11.66 Clause #2 (by assumption #[]): Eq % 11.47/11.66 (ord_less_int one_one_int t → % 11.47/11.66 Exists fun X => % 11.47/11.66 Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True % 11.47/11.66 Clause #24 (by assumption #[]): Eq (Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls)))) True % 11.47/11.66 Clause #28 (by assumption #[]): Eq (∀ (Z_1 W_1 : Iota), Iff (ord_less_int Z_1 W_1) (And (ord_less_eq_int Z_1 W_1) (Ne Z_1 W_1))) True % 11.47/11.66 Clause #46 (by assumption #[]): Eq (Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls)))) True % 11.47/11.66 Clause #81 (by assumption #[]): Eq (∀ (A_6 B_3 : Iota), Eq (times_times_int A_6 B_3) (times_times_int B_3 A_6)) True % 11.47/11.66 Clause #93 (by assumption #[]): Eq (∀ (A C : Iota), Eq (plus_plus_int A C) (plus_plus_int C A)) True % 11.47/11.66 Clause #100 (by assumption #[]): Eq (∀ (K_1 : Iota), Eq (number_number_of_int K_1) K_1) True % 11.47/11.66 Clause #107 (by assumption #[]): Eq % 11.47/11.66 (Not % 11.47/11.66 (Exists fun X => % 11.47/11.66 Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 11.47/11.66 True % 11.47/11.66 Clause #110 (by clausification #[1]): Or (Eq (Eq t one_one_int) False) % 11.47/11.66 (Eq % 11.47/11.66 (Exists fun X => % 11.47/11.66 Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True) % 11.47/11.66 Clause #111 (by clausification #[110]): Or % 11.47/11.66 (Eq % 11.47/11.66 (Exists fun X => % 11.47/11.66 Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True) % 11.47/11.66 (Ne t one_one_int) % 11.47/11.66 Clause #112 (by clausification #[111]): ∀ (a : Iota), % 11.47/11.66 Or (Ne t one_one_int) % 11.47/11.66 (Eq % 11.47/11.66 (Exists fun Y => % 11.47/11.66 Eq % 11.47/11.66 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True) % 11.47/11.66 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), % 11.47/11.66 Or (Ne t one_one_int) % 11.47/11.66 (Eq % 11.47/11.66 (Eq % 11.47/11.66 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 True) % 11.47/11.66 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), % 11.47/11.66 Or (Ne t one_one_int) % 11.47/11.66 (Eq % 11.47/11.66 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.66 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.66 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.66 Clause #117 (by clausification #[100]): ∀ (a : Iota), Eq (Eq (number_number_of_int a) a) True % 11.47/11.66 Clause #118 (by clausification #[117]): ∀ (a : Iota), Eq (number_number_of_int a) a % 11.47/11.68 Clause #120 (by backward demodulation #[118, 114]): ∀ (a a_1 : Iota), % 11.47/11.68 Or (Ne t one_one_int) % 11.47/11.68 (Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.47/11.68 Clause #123 (by clausification #[2]): Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (Exists fun X => % 11.47/11.68 Exists fun Y => % 11.47/11.68 Eq % 11.47/11.68 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.68 True) % 11.47/11.68 Clause #124 (by clausification #[123]): ∀ (a : Iota), % 11.47/11.68 Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (Exists fun Y => % 11.47/11.68 Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.68 True) % 11.47/11.68 Clause #125 (by clausification #[124]): ∀ (a a_1 : Iota), % 11.47/11.68 Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.68 True) % 11.47/11.68 Clause #126 (by clausification #[125]): ∀ (a a_1 : Iota), % 11.47/11.68 Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.68 Clause #127 (by forward demodulation #[126, 118]): ∀ (a a_1 : Iota), % 11.47/11.68 Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.68 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.47/11.68 Clause #159 (by clausification #[24]): Eq (plus_plus_int one_one_int one_one_int) (number_number_of_int (bit0 (bit1 pls))) % 11.47/11.68 Clause #160 (by superposition #[159, 118]): Eq (plus_plus_int one_one_int one_one_int) (bit0 (bit1 pls)) % 11.47/11.68 Clause #162 (by backward demodulation #[160, 127]): ∀ (a a_1 : Iota), % 11.47/11.68 Or (Eq (ord_less_int one_one_int t) False) % 11.47/11.68 (Eq % 11.47/11.68 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.68 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.47/11.68 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.47/11.68 Clause #259 (by clausification #[46]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 (bit1 pls))) % 11.47/11.68 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.47/11.68 Clause #452 (by clausification #[93]): ∀ (a : Iota), Eq (∀ (C : Iota), Eq (plus_plus_int a C) (plus_plus_int C a)) True % 11.47/11.68 Clause #453 (by clausification #[452]): ∀ (a a_1 : Iota), Eq (Eq (plus_plus_int a a_1) (plus_plus_int a_1 a)) True % 11.47/11.68 Clause #454 (by clausification #[453]): ∀ (a a_1 : Iota), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 11.47/11.68 Clause #500 (by clausification #[81]): ∀ (a : Iota), Eq (∀ (B_3 : Iota), Eq (times_times_int a B_3) (times_times_int B_3 a)) True % 11.47/11.68 Clause #501 (by clausification #[500]): ∀ (a a_1 : Iota), Eq (Eq (times_times_int a a_1) (times_times_int a_1 a)) True % 11.47/11.68 Clause #502 (by clausification #[501]): ∀ (a a_1 : Iota), Eq (times_times_int a a_1) (times_times_int a_1 a) % 11.47/11.69 Clause #519 (by clausification #[28]): ∀ (a : Iota), Eq (∀ (W_1 : Iota), Iff (ord_less_int a W_1) (And (ord_less_eq_int a W_1) (Ne a W_1))) True % 11.47/11.69 Clause #520 (by clausification #[519]): ∀ (a a_1 : Iota), Eq (Iff (ord_less_int a a_1) (And (ord_less_eq_int a a_1) (Ne a a_1))) True % 11.47/11.69 Clause #521 (by clausification #[520]): ∀ (a a_1 : Iota), Or (Eq (ord_less_int a a_1) True) (Eq (And (ord_less_eq_int a a_1) (Ne a a_1)) False) % 11.47/11.69 Clause #523 (by clausification #[521]): ∀ (a a_1 : Iota), 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.47/11.69 Clause #524 (by clausification #[523]): ∀ (a a_1 : Iota), Or (Eq (ord_less_int a a_1) True) (Or (Eq (ord_less_eq_int a a_1) False) (Eq a a_1)) % 11.47/11.69 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.47/11.69 Clause #544 (by clausification #[525]): Or (Eq (ord_less_int one_one_int t) True) (Eq one_one_int t) % 11.47/11.69 Clause #4958 (by clausification #[107]): Eq % 11.47/11.69 (Exists fun X => % 11.47/11.69 Exists fun Y => % 11.47/11.69 Eq % 11.47/11.69 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.69 False % 11.47/11.69 Clause #4959 (by clausification #[4958]): ∀ (a : Iota), % 11.47/11.69 Eq % 11.47/11.69 (Exists fun Y => % 11.47/11.69 Eq % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.69 False % 11.47/11.69 Clause #4960 (by clausification #[4959]): ∀ (a a_1 : Iota), % 11.47/11.69 Eq % 11.47/11.69 (Eq % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 11.47/11.69 False % 11.47/11.69 Clause #4961 (by clausification #[4960]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.47/11.69 Clause #4962 (by forward demodulation #[4961, 160]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int a_1 (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.47/11.69 Clause #4963 (by forward demodulation #[4962, 260]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 11.47/11.69 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.47/11.69 Clause #4964 (by forward demodulation #[4963, 160]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.47/11.69 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.47/11.69 Clause #4965 (by forward demodulation #[4964, 260]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.47/11.69 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.47/11.69 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 11.47/11.69 Clause #4966 (by forward demodulation #[4965, 454]): ∀ (a a_1 : Iota), % 11.47/11.69 Ne % 11.47/11.69 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.47/11.69 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.47/11.69 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)) % 11.47/11.69 Clause #4967 (by forward demodulation #[4966, 502]): ∀ (a a_1 : Iota), % 11.54/11.71 Ne % 11.54/11.71 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))) % 11.54/11.71 Clause #4968 (by forward demodulation #[4967, 118]): ∀ (a a_1 : Iota), % 11.54/11.71 Ne % 11.54/11.71 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 11.54/11.71 Clause #4969 (by forward demodulation #[4968, 160]): ∀ (a a_1 : Iota), % 11.54/11.71 Ne % 11.54/11.71 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 11.54/11.71 Clause #5084 (by forward demodulation #[120, 160]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.54/11.71 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.54/11.71 Clause #5085 (by forward demodulation #[5084, 260]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.54/11.71 Clause #5086 (by forward demodulation #[5085, 160]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.54/11.71 Clause #5087 (by forward demodulation #[5086, 260]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.54/11.71 Clause #5088 (by forward demodulation #[5087, 454]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m))) % 11.54/11.71 Clause #5089 (by forward demodulation #[5088, 502]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls)))))) % 11.54/11.71 Clause #5090 (by forward demodulation #[5089, 160]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Ne t one_one_int) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.71 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.71 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int))))) % 11.54/11.71 Clause #5091 (by forward contextual literal cutting #[5090, 4969]): Ne t one_one_int % 11.54/11.71 Clause #5093 (by backward contextual literal cutting #[5091, 544]): Eq (ord_less_int one_one_int t) True % 11.54/11.71 Clause #5204 (by forward demodulation #[162, 5093]): ∀ (a a_1 : Iota), % 11.54/11.71 Or (Eq True False) % 11.54/11.71 (Eq % 11.54/11.71 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.54/11.71 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.54/11.71 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 11.54/11.71 Clause #5205 (by clausification #[5204]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (plus_plus_int one_one_int one_one_int)))) % 11.54/11.73 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.54/11.73 Clause #5206 (by forward demodulation #[5205, 260]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.54/11.73 Clause #5207 (by forward demodulation #[5206, 160]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (plus_plus_int one_one_int one_one_int))) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.54/11.73 Clause #5208 (by forward demodulation #[5207, 260]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 11.54/11.73 Clause #5209 (by forward demodulation #[5208, 454]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m)) % 11.54/11.73 Clause #5210 (by forward demodulation #[5209, 502]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 11.54/11.73 Clause #5211 (by forward demodulation #[5210, 160]): ∀ (a a_1 : Iota), % 11.54/11.73 Eq % 11.54/11.73 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 11.54/11.73 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 11.54/11.73 (plus_plus_int one_one_int (times_times_int m (bit0 (plus_plus_int one_one_int one_one_int)))) % 11.54/11.73 Clause #5212 (by forward contextual literal cutting #[5211, 4969]): False % 11.54/11.73 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------