%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM926_2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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:37 PM UTC 2025 % Result : Theorem 159.63s 159.97s % Output : Proof 160.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : NUM926_2 : TPTP v9.2.0. Released v5.3.0. % 0.10/0.12 % Command : duper %s % 0.12/0.32 % Computer : n025.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Fri Oct 3 07:07:53 EDT 2025 % 0.12/0.33 % CPUTime : % 159.63/159.97 SZS status Theorem for theBenchmark.p % 159.63/159.97 SZS output start Proof for theBenchmark.p % 159.63/159.97 Clause #0 (by assumption #[]): Eq (ord_less_eq_int one_one_int t) True % 159.63/159.97 Clause #1 (by assumption #[]): Eq % 159.63/159.97 (Eq t one_one_int → % 159.63/159.97 Exists fun X => % 159.63/159.97 Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.63/159.97 True % 159.63/159.97 Clause #2 (by assumption #[]): Eq % 159.63/159.97 (ord_less_int one_one_int t → % 159.63/159.97 Exists fun X => % 159.63/159.97 Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.63/159.97 True % 159.63/159.97 Clause #59 (by assumption #[]): Eq (∀ (Z : nat), Eq (times_times_nat (number_number_of_nat (bit0 (bit1 pls))) Z) (plus_plus_nat Z Z)) True % 159.63/159.97 Clause #93 (by assumption #[]): Eq % 159.63/159.97 (∀ (Lx_3 Ly_1 Rx_3 : int), % 159.63/159.97 Eq (times_times_int (times_times_int Lx_3 Ly_1) Rx_3) (times_times_int (times_times_int Lx_3 Rx_3) Ly_1)) % 159.63/159.97 True % 159.63/159.97 Clause #111 (by assumption #[]): Eq % 159.63/159.97 (∀ (A_54 B_15 C_9 : int), % 159.63/159.97 Eq (plus_plus_int (plus_plus_int A_54 B_15) C_9) (plus_plus_int (plus_plus_int A_54 C_9) B_15)) % 159.63/159.97 True % 159.63/159.97 Clause #131 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of_int K) K) True % 159.63/159.97 Clause #157 (by assumption #[]): Eq % 159.63/159.97 (∀ (A_48 M_12 B_13 : int), % 159.63/159.97 Eq (plus_plus_int (times_times_int A_48 M_12) (times_times_int B_13 M_12)) % 159.63/159.97 (times_times_int (plus_plus_int A_48 B_13) M_12)) % 159.63/159.97 True % 159.63/159.97 Clause #168 (by assumption #[]): Eq (∀ (A_46 : nat), Eq (times_times_nat A_46 one_one_nat) A_46) True % 159.63/159.97 Clause #172 (by assumption #[]): Eq (∀ (A_45 : int), Eq (times_times_int one_one_int A_45) A_45) True % 159.63/159.97 Clause #186 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus_int pls K) K) True % 159.63/159.97 Clause #188 (by assumption #[]): Eq (∀ (K : int), Eq (bit0 K) (plus_plus_int K K)) True % 159.63/159.97 Clause #227 (by assumption #[]): Eq (∀ (K L : int), Eq (plus_plus_int (bit1 K) (bit0 L)) (bit1 (plus_plus_int K L))) True % 159.63/159.97 Clause #239 (by assumption #[]): Eq (Eq one_one_int (number_number_of_int (bit1 pls))) True % 159.63/159.97 Clause #513 (by assumption #[]): Eq (∀ (X_3 Y_3 : int), ord_less_eq_int X_3 Y_3 → Ne X_3 Y_3 → ord_less_int X_3 Y_3) True % 159.63/159.97 Clause #636 (by assumption #[]): Eq % 159.63/159.97 (Not % 159.63/159.97 (Exists fun X => % 159.63/159.97 Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 159.63/159.97 True % 159.63/159.97 Clause #639 (by clausification #[1]): Or (Eq (Eq t one_one_int) False) % 159.63/159.97 (Eq % 159.63/159.97 (Exists fun X => % 159.63/159.97 Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.63/159.97 True) % 159.63/159.97 Clause #640 (by clausification #[639]): Or % 159.63/159.97 (Eq % 159.63/159.97 (Exists fun X => % 159.63/159.97 Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.63/159.97 True) % 159.63/159.97 (Ne t one_one_int) % 159.63/159.97 Clause #641 (by clausification #[640]): ∀ (a : int), % 159.63/159.97 Or (Ne t one_one_int) % 159.63/159.97 (Eq % 159.63/159.97 (Exists fun Y => % 159.63/159.97 Eq % 159.63/159.97 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.63/159.97 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.63/159.97 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.63/159.97 True) % 159.63/159.97 Clause #642 (by clausification #[641]): ∀ (a a_1 : int), % 159.74/160.02 Or (Ne t one_one_int) % 159.74/160.02 (Eq % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 True) % 159.74/160.02 Clause #643 (by clausification #[642]): ∀ (a a_1 : int), % 159.74/160.02 Or (Ne t one_one_int) % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 Clause #649 (by clausification #[2]): Or (Eq (ord_less_int one_one_int t) False) % 159.74/160.02 (Eq % 159.74/160.02 (Exists fun X => % 159.74/160.02 Exists fun Y => % 159.74/160.02 Eq % 159.74/160.02 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 True) % 159.74/160.02 Clause #650 (by clausification #[649]): ∀ (a : int), % 159.74/160.02 Or (Eq (ord_less_int one_one_int t) False) % 159.74/160.02 (Eq % 159.74/160.02 (Exists fun Y => % 159.74/160.02 Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 True) % 159.74/160.02 Clause #651 (by clausification #[650]): ∀ (a a_1 : int), % 159.74/160.02 Or (Eq (ord_less_int one_one_int t) False) % 159.74/160.02 (Eq % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 True) % 159.74/160.02 Clause #652 (by clausification #[651]): ∀ (a a_1 : int), % 159.74/160.02 Or (Eq (ord_less_int one_one_int t) False) % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.74/160.02 Clause #681 (by clausification #[239]): Eq one_one_int (number_number_of_int (bit1 pls)) % 159.74/160.02 Clause #701 (by clausification #[131]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 159.74/160.02 Clause #702 (by clausification #[701]): ∀ (a : int), Eq (number_number_of_int a) a % 159.74/160.02 Clause #703 (by backward demodulation #[702, 643]): ∀ (a a_1 : int), % 159.74/160.02 Or (Ne t one_one_int) % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.74/160.02 Clause #704 (by backward demodulation #[702, 652]): ∀ (a a_1 : int), % 159.74/160.02 Or (Eq (ord_less_int one_one_int t) False) % 159.74/160.02 (Eq % 159.74/160.02 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.74/160.02 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.74/160.02 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.74/160.02 Clause #711 (by superposition #[702, 681]): Eq one_one_int (bit1 pls) % 159.74/160.02 Clause #914 (by clausification #[186]): ∀ (a : int), Eq (Eq (plus_plus_int pls a) a) True % 159.74/160.02 Clause #915 (by clausification #[914]): ∀ (a : int), Eq (plus_plus_int pls a) a % 159.74/160.02 Clause #1005 (by clausification #[513]): ∀ (a : int), Eq (∀ (Y_3 : int), ord_less_eq_int a Y_3 → Ne a Y_3 → ord_less_int a Y_3) True % 159.74/160.02 Clause #1006 (by clausification #[1005]): ∀ (a a_1 : int), Eq (ord_less_eq_int a a_1 → Ne a a_1 → ord_less_int a a_1) True % 159.74/160.02 Clause #1007 (by clausification #[1006]): ∀ (a a_1 : int), Or (Eq (ord_less_eq_int a a_1) False) (Eq (Ne a a_1 → ord_less_int a a_1) True) % 159.74/160.02 Clause #1008 (by clausification #[1007]): ∀ (a a_1 : int), Or (Eq (ord_less_eq_int a a_1) False) (Or (Eq (Ne a a_1) False) (Eq (ord_less_int a a_1) True)) % 159.74/160.08 Clause #1009 (by clausification #[1008]): ∀ (a a_1 : int), Or (Eq (ord_less_eq_int a a_1) False) (Or (Eq (ord_less_int a a_1) True) (Eq a a_1)) % 159.74/160.08 Clause #1011 (by superposition #[1009, 0]): Or (Eq (ord_less_int one_one_int t) True) (Or (Eq one_one_int t) (Eq False True)) % 159.74/160.08 Clause #1021 (by clausification #[1011]): Or (Eq (ord_less_int one_one_int t) True) (Eq one_one_int t) % 159.74/160.08 Clause #1045 (by clausification #[172]): ∀ (a : int), Eq (Eq (times_times_int one_one_int a) a) True % 159.74/160.08 Clause #1046 (by clausification #[1045]): ∀ (a : int), Eq (times_times_int one_one_int a) a % 159.74/160.08 Clause #1056 (by clausification #[168]): ∀ (a : nat), Eq (Eq (times_times_nat a one_one_nat) a) True % 159.74/160.08 Clause #1057 (by clausification #[1056]): ∀ (a : nat), Eq (times_times_nat a one_one_nat) a % 159.74/160.08 Clause #1306 (by clausification #[188]): ∀ (a : int), Eq (Eq (bit0 a) (plus_plus_int a a)) True % 159.74/160.08 Clause #1307 (by clausification #[1306]): ∀ (a : int), Eq (bit0 a) (plus_plus_int a a) % 159.74/160.08 Clause #2523 (by clausification #[59]): ∀ (a : nat), Eq (Eq (times_times_nat (number_number_of_nat (bit0 (bit1 pls))) a) (plus_plus_nat a a)) True % 159.74/160.08 Clause #2524 (by clausification #[2523]): ∀ (a : nat), Eq (times_times_nat (number_number_of_nat (bit0 (bit1 pls))) a) (plus_plus_nat a a) % 159.74/160.08 Clause #2525 (by forward demodulation #[2524, 711]): ∀ (a : nat), Eq (times_times_nat (number_number_of_nat (bit0 one_one_int)) a) (plus_plus_nat a a) % 159.74/160.08 Clause #2527 (by superposition #[2525, 1057]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 159.74/160.08 Clause #4417 (by clausification #[93]): ∀ (a : int), % 159.74/160.08 Eq % 159.74/160.08 (∀ (Ly_1 Rx_3 : int), % 159.74/160.08 Eq (times_times_int (times_times_int a Ly_1) Rx_3) (times_times_int (times_times_int a Rx_3) Ly_1)) % 159.74/160.08 True % 159.74/160.08 Clause #4418 (by clausification #[4417]): ∀ (a a_1 : int), % 159.74/160.08 Eq (∀ (Rx_3 : int), Eq (times_times_int (times_times_int a a_1) Rx_3) (times_times_int (times_times_int a Rx_3) a_1)) % 159.74/160.08 True % 159.74/160.08 Clause #4419 (by clausification #[4418]): ∀ (a a_1 a_2 : int), % 159.74/160.08 Eq (Eq (times_times_int (times_times_int a a_1) a_2) (times_times_int (times_times_int a a_2) a_1)) True % 159.74/160.08 Clause #4420 (by clausification #[4419]): ∀ (a a_1 a_2 : int), Eq (times_times_int (times_times_int a a_1) a_2) (times_times_int (times_times_int a a_2) a_1) % 159.74/160.08 Clause #4432 (by superposition #[4420, 1046]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int (times_times_int one_one_int a_1) a) % 159.74/160.08 Clause #4446 (by forward demodulation #[4432, 1046]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int a_1 a) % 159.74/160.08 Clause #4986 (by clausification #[111]): ∀ (a : int), % 159.74/160.08 Eq (∀ (B_15 C_9 : int), Eq (plus_plus_int (plus_plus_int a B_15) C_9) (plus_plus_int (plus_plus_int a C_9) B_15)) True % 159.74/160.08 Clause #4987 (by clausification #[4986]): ∀ (a a_1 : int), % 159.74/160.08 Eq (∀ (C_9 : int), Eq (plus_plus_int (plus_plus_int a a_1) C_9) (plus_plus_int (plus_plus_int a C_9) a_1)) True % 159.74/160.08 Clause #4988 (by clausification #[4987]): ∀ (a a_1 a_2 : int), Eq (Eq (plus_plus_int (plus_plus_int a a_1) a_2) (plus_plus_int (plus_plus_int a a_2) a_1)) True % 159.74/160.08 Clause #4989 (by clausification #[4988]): ∀ (a a_1 a_2 : int), Eq (plus_plus_int (plus_plus_int a a_1) a_2) (plus_plus_int (plus_plus_int a a_2) a_1) % 159.74/160.08 Clause #5009 (by superposition #[4989, 915]): ∀ (a a_1 : int), Eq (plus_plus_int (plus_plus_int pls a) a_1) (plus_plus_int a_1 a) % 159.74/160.08 Clause #5013 (by forward demodulation #[5009, 915]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 159.74/160.08 Clause #7523 (by clausification #[157]): ∀ (a : int), % 159.74/160.08 Eq % 159.74/160.08 (∀ (M_12 B_13 : int), % 159.74/160.08 Eq (plus_plus_int (times_times_int a M_12) (times_times_int B_13 M_12)) % 159.74/160.08 (times_times_int (plus_plus_int a B_13) M_12)) % 159.74/160.08 True % 159.74/160.08 Clause #7524 (by clausification #[7523]): ∀ (a a_1 : int), % 159.74/160.08 Eq % 159.74/160.08 (∀ (B_13 : int), % 159.74/160.08 Eq (plus_plus_int (times_times_int a a_1) (times_times_int B_13 a_1)) % 159.74/160.08 (times_times_int (plus_plus_int a B_13) a_1)) % 159.74/160.08 True % 159.74/160.08 Clause #7525 (by clausification #[7524]): ∀ (a a_1 a_2 : int), % 159.74/160.08 Eq (Eq (plus_plus_int (times_times_int a a_1) (times_times_int a_2 a_1)) (times_times_int (plus_plus_int a a_2) a_1)) % 159.83/160.12 True % 159.83/160.12 Clause #7526 (by clausification #[7525]): ∀ (a a_1 a_2 : int), % 159.83/160.12 Eq (plus_plus_int (times_times_int a a_1) (times_times_int a_2 a_1)) (times_times_int (plus_plus_int a a_2) a_1) % 159.83/160.12 Clause #7527 (by superposition #[7526, 1307]): ∀ (a a_1 : int), Eq (bit0 (times_times_int a a_1)) (times_times_int (plus_plus_int a a) a_1) % 159.83/160.12 Clause #7563 (by forward demodulation #[7527, 1307]): ∀ (a a_1 : int), Eq (bit0 (times_times_int a a_1)) (times_times_int (bit0 a) a_1) % 159.83/160.12 Clause #7578 (by superposition #[7563, 1046]): ∀ (a : int), Eq (bit0 a) (times_times_int (bit0 one_one_int) a) % 159.83/160.12 Clause #7581 (by superposition #[7563, 4446]): ∀ (a a_1 : int), Eq (bit0 (times_times_int a a_1)) (times_times_int (bit0 a_1) a) % 159.83/160.12 Clause #7640 (by superposition #[7578, 7563]): ∀ (a : int), Eq (bit0 (bit0 a)) (times_times_int (bit0 (bit0 one_one_int)) a) % 159.83/160.12 Clause #7820 (by superposition #[7640, 4446]): ∀ (a : int), Eq (times_times_int a (bit0 (bit0 one_one_int))) (bit0 (bit0 a)) % 159.83/160.12 Clause #8026 (by superposition #[7581, 7563]): ∀ (a a_1 : int), Eq (times_times_int (bit0 a) a_1) (times_times_int (bit0 a_1) a) % 159.83/160.12 Clause #8049 (by superposition #[8026, 4446]): ∀ (a a_1 : int), Eq (times_times_int a (bit0 a_1)) (times_times_int (bit0 a) a_1) % 159.83/160.12 Clause #8123 (by superposition #[8049, 4446]): ∀ (a a_1 : int), Eq (times_times_int a (bit0 a_1)) (times_times_int a_1 (bit0 a)) % 159.83/160.12 Clause #9837 (by clausification #[227]): ∀ (a : int), Eq (∀ (L : int), Eq (plus_plus_int (bit1 a) (bit0 L)) (bit1 (plus_plus_int a L))) True % 159.83/160.12 Clause #9838 (by clausification #[9837]): ∀ (a a_1 : int), Eq (Eq (plus_plus_int (bit1 a) (bit0 a_1)) (bit1 (plus_plus_int a a_1))) True % 159.83/160.12 Clause #9839 (by clausification #[9838]): ∀ (a a_1 : int), Eq (plus_plus_int (bit1 a) (bit0 a_1)) (bit1 (plus_plus_int a a_1)) % 159.83/160.12 Clause #9859 (by superposition #[9839, 711]): ∀ (a : int), Eq (plus_plus_int one_one_int (bit0 a)) (bit1 (plus_plus_int pls a)) % 159.83/160.12 Clause #9862 (by forward demodulation #[9859, 915]): ∀ (a : int), Eq (plus_plus_int one_one_int (bit0 a)) (bit1 a) % 159.83/160.12 Clause #31479 (by clausification #[636]): Eq % 159.83/160.12 (Exists fun X => % 159.83/160.12 Exists fun Y => % 159.83/160.12 Eq % 159.83/160.12 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.83/160.12 False % 159.83/160.12 Clause #31480 (by clausification #[31479]): ∀ (a : int), % 159.83/160.12 Eq % 159.83/160.12 (Exists fun Y => % 159.83/160.12 Eq % 159.83/160.12 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.83/160.12 False % 159.83/160.12 Clause #31481 (by clausification #[31480]): ∀ (a a_1 : int), % 159.83/160.12 Eq % 159.83/160.12 (Eq % 159.83/160.12 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 159.83/160.12 False % 159.83/160.12 Clause #31482 (by clausification #[31481]): ∀ (a a_1 : int), % 159.83/160.12 Ne % 159.83/160.12 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 159.83/160.12 Clause #31483 (by forward demodulation #[31482, 711]): ∀ (a a_1 : int), % 159.83/160.12 Ne % 159.83/160.12 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int a_1 (number_number_of_nat (bit0 one_one_int)))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 159.83/160.12 Clause #31484 (by forward demodulation #[31483, 2527]): ∀ (a a_1 : int), % 159.83/160.12 Ne % 159.83/160.12 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.12 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.12 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 159.83/160.17 Clause #31485 (by forward demodulation #[31484, 711]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 one_one_int))) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 159.83/160.17 Clause #31486 (by forward demodulation #[31485, 2527]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 159.83/160.17 Clause #31487 (by forward demodulation #[31486, 5013]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)) % 159.83/160.17 Clause #31488 (by forward demodulation #[31487, 4446]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))) % 159.83/160.17 Clause #31489 (by forward demodulation #[31488, 702]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 159.83/160.17 Clause #31490 (by forward demodulation #[31489, 711]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int)))) % 159.83/160.17 Clause #31491 (by forward demodulation #[31490, 7820]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int one_one_int (bit0 (bit0 m))) % 159.83/160.17 Clause #31492 (by forward demodulation #[31491, 9862]): ∀ (a a_1 : int), % 159.83/160.17 Ne % 159.83/160.17 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (bit1 (bit0 m)) % 159.83/160.17 Clause #31624 (by forward demodulation #[703, 711]): ∀ (a a_1 : int), % 159.83/160.17 Or (Ne t one_one_int) % 159.83/160.17 (Eq % 159.83/160.17 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.17 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 one_one_int)))) % 159.83/160.17 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.83/160.17 Clause #31625 (by forward demodulation #[31624, 2527]): ∀ (a a_1 : int), % 159.83/160.17 Or (Ne t one_one_int) % 159.83/160.17 (Eq % 159.83/160.17 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.83/160.17 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.83/160.17 Clause #31626 (by forward demodulation #[31625, 711]): ∀ (a a_1 : int), % 159.83/160.17 Or (Ne t one_one_int) % 159.83/160.17 (Eq % 159.83/160.17 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 one_one_int))) % 159.83/160.17 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.83/160.17 Clause #31627 (by forward demodulation #[31626, 2527]): ∀ (a a_1 : int), % 159.83/160.17 Or (Ne t one_one_int) % 159.83/160.17 (Eq % 159.83/160.17 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.83/160.17 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.83/160.17 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.83/160.17 Clause #31628 (by forward demodulation #[31627, 5013]): ∀ (a a_1 : int), % 159.83/160.17 Or (Ne t one_one_int) % 159.83/160.17 (Eq % 159.83/160.17 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m))) % 159.93/160.21 Clause #31629 (by forward demodulation #[31628, 8049]): ∀ (a a_1 : int), % 159.93/160.21 Or (Ne t one_one_int) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int one_one_int (times_times_int (bit0 (bit1 pls)) (bit0 m)))) % 159.93/160.21 Clause #31630 (by forward demodulation #[31629, 8123]): ∀ (a a_1 : int), % 159.93/160.21 Or (Ne t one_one_int) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls)))))) % 159.93/160.21 Clause #31631 (by forward demodulation #[31630, 711]): ∀ (a a_1 : int), % 159.93/160.21 Or (Ne t one_one_int) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int))))) % 159.93/160.21 Clause #31632 (by forward demodulation #[31631, 7820]): ∀ (a a_1 : int), % 159.93/160.21 Or (Ne t one_one_int) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int one_one_int (bit0 (bit0 m)))) % 159.93/160.21 Clause #31633 (by forward demodulation #[31632, 9862]): ∀ (a a_1 : int), % 159.93/160.21 Or (Ne t one_one_int) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (bit1 (bit0 m))) % 159.93/160.21 Clause #31634 (by forward contextual literal cutting #[31633, 31492]): Ne t one_one_int % 159.93/160.21 Clause #31635 (by backward contextual literal cutting #[31634, 1021]): Eq (ord_less_int one_one_int t) True % 159.93/160.21 Clause #31681 (by forward demodulation #[704, 31635]): ∀ (a a_1 : int), % 159.93/160.21 Or (Eq True False) % 159.93/160.21 (Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 159.93/160.21 Clause #31682 (by clausification #[31681]): ∀ (a a_1 : int), % 159.93/160.21 Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 159.93/160.21 Clause #31683 (by forward demodulation #[31682, 711]): ∀ (a a_1 : int), % 159.93/160.21 Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 one_one_int)))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 159.93/160.21 Clause #31684 (by forward demodulation #[31683, 2527]): ∀ (a a_1 : int), % 159.93/160.21 Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 159.93/160.21 Clause #31685 (by forward demodulation #[31684, 711]): ∀ (a a_1 : int), % 159.93/160.21 Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 one_one_int))) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 159.93/160.21 Clause #31686 (by forward demodulation #[31685, 2527]): ∀ (a a_1 : int), % 159.93/160.21 Eq % 159.93/160.21 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 159.93/160.21 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 159.93/160.21 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 160.12/160.40 Clause #31687 (by forward demodulation #[31686, 5013]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m)) % 160.12/160.40 Clause #31688 (by forward demodulation #[31687, 8049]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (plus_plus_int one_one_int (times_times_int (bit0 (bit1 pls)) (bit0 m))) % 160.12/160.40 Clause #31689 (by forward demodulation #[31688, 8123]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 160.12/160.40 Clause #31690 (by forward demodulation #[31689, 711]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int)))) % 160.12/160.40 Clause #31691 (by forward demodulation #[31690, 7820]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (plus_plus_int one_one_int (bit0 (bit0 m))) % 160.12/160.40 Clause #31692 (by forward demodulation #[31691, 9862]): ∀ (a a_1 : int), % 160.12/160.40 Eq % 160.12/160.40 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 160.12/160.40 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 160.12/160.40 (bit1 (bit0 m)) % 160.12/160.40 Clause #31693 (by forward contextual literal cutting #[31692, 31492]): False % 160.12/160.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------