%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM926^2 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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 130.17s 130.40s % Output : Proof 130.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : NUM926^2 : TPTP v9.2.0. Released v5.3.0. % 0.14/0.14 % Command : duper %s % 0.15/0.35 % Computer : n005.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Fri Oct 3 07:07:53 EDT 2025 % 0.15/0.36 % CPUTime : % 130.17/130.40 SZS status Theorem for theBenchmark.p % 130.17/130.40 SZS output start Proof for theBenchmark.p % 130.17/130.40 Clause #0 (by assumption #[]): Eq (ord_less_eq_int one_one_int t) True % 130.17/130.40 Clause #1 (by assumption #[]): Eq % 130.17/130.40 (Eq t one_one_int → % 130.17/130.40 Exists fun X => % 130.17/130.40 Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.17/130.40 True % 130.17/130.40 Clause #2 (by assumption #[]): Eq % 130.17/130.40 (ord_less_int one_one_int t → % 130.17/130.40 Exists fun X => % 130.17/130.40 Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.17/130.40 True % 130.17/130.40 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 % 130.17/130.40 Clause #93 (by assumption #[]): Eq % 130.17/130.40 (∀ (Lx_3 Ly_1 Rx_3 : int), % 130.17/130.40 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)) % 130.17/130.40 True % 130.17/130.40 Clause #111 (by assumption #[]): Eq % 130.17/130.40 (∀ (A_62 B_18 C_9 : int), % 130.17/130.40 Eq (plus_plus_int (plus_plus_int A_62 B_18) C_9) (plus_plus_int (plus_plus_int A_62 C_9) B_18)) % 130.17/130.40 True % 130.17/130.40 Clause #131 (by assumption #[]): Eq (∀ (K : int), Eq (number_number_of_int K) K) True % 130.17/130.40 Clause #157 (by assumption #[]): Eq % 130.17/130.40 (∀ (A_56 M_13 B_16 : int), % 130.17/130.40 Eq (plus_plus_int (times_times_int A_56 M_13) (times_times_int B_16 M_13)) % 130.17/130.40 (times_times_int (plus_plus_int A_56 B_16) M_13)) % 130.17/130.40 True % 130.17/130.40 Clause #168 (by assumption #[]): Eq (∀ (A_53 : nat), Eq (times_times_nat A_53 one_one_nat) A_53) True % 130.17/130.40 Clause #172 (by assumption #[]): Eq (∀ (A_52 : int), Eq (times_times_int one_one_int A_52) A_52) True % 130.17/130.40 Clause #186 (by assumption #[]): Eq (∀ (K : int), Eq (plus_plus_int pls K) K) True % 130.17/130.40 Clause #188 (by assumption #[]): Eq (∀ (K : int), Eq (bit0 K) (plus_plus_int K K)) True % 130.17/130.40 Clause #227 (by assumption #[]): Eq (∀ (K L : int), Eq (plus_plus_int (bit1 K) (bit0 L)) (bit1 (plus_plus_int K L))) True % 130.17/130.40 Clause #239 (by assumption #[]): Eq (Eq one_one_int (number_number_of_int (bit1 pls))) True % 130.17/130.40 Clause #513 (by assumption #[]): Eq (∀ (X_2 Y_2 : int), ord_less_eq_int X_2 Y_2 → Ne X_2 Y_2 → ord_less_int X_2 Y_2) True % 130.17/130.40 Clause #636 (by assumption #[]): Eq % 130.17/130.40 (Not % 130.17/130.40 (Exists fun X => % 130.17/130.40 Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int))) % 130.17/130.40 True % 130.17/130.40 Clause #639 (by clausification #[1]): Or (Eq (Eq t one_one_int) False) % 130.17/130.40 (Eq % 130.17/130.40 (Exists fun X => % 130.17/130.40 Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.17/130.40 True) % 130.17/130.40 Clause #640 (by clausification #[639]): Or % 130.17/130.40 (Eq % 130.17/130.40 (Exists fun X => % 130.17/130.40 Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.17/130.40 True) % 130.17/130.40 (Ne t one_one_int) % 130.17/130.40 Clause #641 (by clausification #[640]): ∀ (a : int), % 130.17/130.40 Or (Ne t one_one_int) % 130.17/130.40 (Eq % 130.17/130.40 (Exists fun Y => % 130.17/130.40 Eq % 130.17/130.40 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.17/130.40 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.17/130.40 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.17/130.40 True) % 130.17/130.40 Clause #642 (by clausification #[641]): ∀ (a a_1 : int), % 130.26/130.42 Or (Ne t one_one_int) % 130.26/130.42 (Eq % 130.26/130.42 (Eq % 130.26/130.42 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.42 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.42 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.42 True) % 130.26/130.42 Clause #643 (by clausification #[642]): ∀ (a a_1 : int), % 130.26/130.42 Or (Ne t one_one_int) % 130.26/130.42 (Eq % 130.26/130.42 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.42 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.42 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.42 Clause #649 (by clausification #[2]): Or (Eq (ord_less_int one_one_int t) False) % 130.26/130.42 (Eq % 130.26/130.42 (Exists fun X => % 130.26/130.42 Exists fun Y => % 130.26/130.42 Eq % 130.26/130.42 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.42 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.42 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.42 True) % 130.26/130.42 Clause #650 (by clausification #[649]): ∀ (a : int), % 130.26/130.42 Or (Eq (ord_less_int one_one_int t) False) % 130.26/130.42 (Eq % 130.26/130.42 (Exists fun Y => % 130.26/130.42 Eq % 130.26/130.42 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.42 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.42 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.42 True) % 130.26/130.42 Clause #651 (by clausification #[650]): ∀ (a a_1 : int), % 130.26/130.42 Or (Eq (ord_less_int one_one_int t) False) % 130.26/130.42 (Eq % 130.26/130.42 (Eq % 130.26/130.42 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.42 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.42 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.42 True) % 130.26/130.42 Clause #652 (by clausification #[651]): ∀ (a a_1 : int), % 130.26/130.42 Or (Eq (ord_less_int one_one_int t) False) % 130.26/130.43 (Eq % 130.26/130.43 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.43 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.43 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.43 Clause #681 (by clausification #[239]): Eq one_one_int (number_number_of_int (bit1 pls)) % 130.26/130.43 Clause #701 (by clausification #[131]): ∀ (a : int), Eq (Eq (number_number_of_int a) a) True % 130.26/130.43 Clause #702 (by clausification #[701]): ∀ (a : int), Eq (number_number_of_int a) a % 130.26/130.43 Clause #703 (by backward demodulation #[702, 643]): ∀ (a a_1 : int), % 130.26/130.43 Or (Ne t one_one_int) % 130.26/130.43 (Eq % 130.26/130.43 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.43 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.43 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.26/130.43 Clause #704 (by backward demodulation #[702, 652]): ∀ (a a_1 : int), % 130.26/130.43 Or (Eq (ord_less_int one_one_int t) False) % 130.26/130.43 (Eq % 130.26/130.43 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.43 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.43 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.26/130.43 Clause #711 (by superposition #[702, 681]): Eq one_one_int (bit1 pls) % 130.26/130.43 Clause #914 (by clausification #[186]): ∀ (a : int), Eq (Eq (plus_plus_int pls a) a) True % 130.26/130.43 Clause #915 (by clausification #[914]): ∀ (a : int), Eq (plus_plus_int pls a) a % 130.26/130.43 Clause #1005 (by clausification #[513]): ∀ (a : int), Eq (∀ (Y_2 : int), ord_less_eq_int a Y_2 → Ne a Y_2 → ord_less_int a Y_2) True % 130.26/130.43 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 % 130.26/130.43 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) % 130.26/130.43 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)) % 130.26/130.45 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)) % 130.26/130.45 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)) % 130.26/130.45 Clause #1021 (by clausification #[1011]): Or (Eq (ord_less_int one_one_int t) True) (Eq one_one_int t) % 130.26/130.45 Clause #1045 (by clausification #[172]): ∀ (a : int), Eq (Eq (times_times_int one_one_int a) a) True % 130.26/130.45 Clause #1046 (by clausification #[1045]): ∀ (a : int), Eq (times_times_int one_one_int a) a % 130.26/130.45 Clause #1056 (by clausification #[168]): ∀ (a : nat), Eq (Eq (times_times_nat a one_one_nat) a) True % 130.26/130.45 Clause #1057 (by clausification #[1056]): ∀ (a : nat), Eq (times_times_nat a one_one_nat) a % 130.26/130.45 Clause #1306 (by clausification #[188]): ∀ (a : int), Eq (Eq (bit0 a) (plus_plus_int a a)) True % 130.26/130.45 Clause #1307 (by clausification #[1306]): ∀ (a : int), Eq (bit0 a) (plus_plus_int a a) % 130.26/130.45 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 % 130.26/130.45 Clause #2524 (by clausification #[2523]): ∀ (a : nat), Eq (times_times_nat (number_number_of_nat (bit0 (bit1 pls))) a) (plus_plus_nat a a) % 130.26/130.45 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) % 130.26/130.45 Clause #2527 (by superposition #[2525, 1057]): Eq (plus_plus_nat one_one_nat one_one_nat) (number_number_of_nat (bit0 one_one_int)) % 130.26/130.45 Clause #4417 (by clausification #[93]): ∀ (a : int), % 130.26/130.45 Eq % 130.26/130.45 (∀ (Ly_1 Rx_3 : int), % 130.26/130.45 Eq (times_times_int (times_times_int a Ly_1) Rx_3) (times_times_int (times_times_int a Rx_3) Ly_1)) % 130.26/130.45 True % 130.26/130.45 Clause #4418 (by clausification #[4417]): ∀ (a a_1 : int), % 130.26/130.45 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)) % 130.26/130.45 True % 130.26/130.45 Clause #4419 (by clausification #[4418]): ∀ (a a_1 a_2 : int), % 130.26/130.45 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 % 130.26/130.45 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) % 130.26/130.45 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) % 130.26/130.45 Clause #4446 (by forward demodulation #[4432, 1046]): ∀ (a a_1 : int), Eq (times_times_int a a_1) (times_times_int a_1 a) % 130.26/130.45 Clause #4986 (by clausification #[111]): ∀ (a : int), % 130.26/130.45 Eq (∀ (B_18 C_9 : int), Eq (plus_plus_int (plus_plus_int a B_18) C_9) (plus_plus_int (plus_plus_int a C_9) B_18)) True % 130.26/130.45 Clause #4987 (by clausification #[4986]): ∀ (a a_1 : int), % 130.26/130.45 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 % 130.26/130.45 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 % 130.26/130.45 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) % 130.26/130.45 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) % 130.26/130.45 Clause #5013 (by forward demodulation #[5009, 915]): ∀ (a a_1 : int), Eq (plus_plus_int a a_1) (plus_plus_int a_1 a) % 130.26/130.45 Clause #7523 (by clausification #[157]): ∀ (a : int), % 130.26/130.45 Eq % 130.26/130.45 (∀ (M_13 B_16 : int), % 130.26/130.45 Eq (plus_plus_int (times_times_int a M_13) (times_times_int B_16 M_13)) % 130.26/130.45 (times_times_int (plus_plus_int a B_16) M_13)) % 130.26/130.45 True % 130.26/130.45 Clause #7524 (by clausification #[7523]): ∀ (a a_1 : int), % 130.26/130.45 Eq % 130.26/130.45 (∀ (B_16 : int), % 130.26/130.45 Eq (plus_plus_int (times_times_int a a_1) (times_times_int B_16 a_1)) % 130.26/130.45 (times_times_int (plus_plus_int a B_16) a_1)) % 130.26/130.45 True % 130.26/130.45 Clause #7525 (by clausification #[7524]): ∀ (a a_1 a_2 : int), % 130.26/130.45 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)) % 130.26/130.48 True % 130.26/130.48 Clause #7526 (by clausification #[7525]): ∀ (a a_1 a_2 : int), % 130.26/130.48 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) % 130.26/130.48 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) % 130.26/130.48 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) % 130.26/130.48 Clause #7578 (by superposition #[7563, 1046]): ∀ (a : int), Eq (bit0 a) (times_times_int (bit0 one_one_int) a) % 130.26/130.48 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) % 130.26/130.48 Clause #7640 (by superposition #[7578, 7563]): ∀ (a : int), Eq (bit0 (bit0 a)) (times_times_int (bit0 (bit0 one_one_int)) a) % 130.26/130.48 Clause #7820 (by superposition #[7640, 4446]): ∀ (a : int), Eq (times_times_int a (bit0 (bit0 one_one_int))) (bit0 (bit0 a)) % 130.26/130.48 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) % 130.26/130.48 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) % 130.26/130.48 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)) % 130.26/130.48 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 % 130.26/130.48 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 % 130.26/130.48 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)) % 130.26/130.48 Clause #9859 (by superposition #[9839, 711]): ∀ (a : int), Eq (plus_plus_int one_one_int (bit0 a)) (bit1 (plus_plus_int pls a)) % 130.26/130.48 Clause #9862 (by forward demodulation #[9859, 915]): ∀ (a : int), Eq (plus_plus_int one_one_int (bit0 a)) (bit1 a) % 130.26/130.48 Clause #31479 (by clausification #[636]): Eq % 130.26/130.48 (Exists fun X => % 130.26/130.48 Exists fun Y => % 130.26/130.48 Eq % 130.26/130.48 (plus_plus_int (power_power_int X (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.48 False % 130.26/130.48 Clause #31480 (by clausification #[31479]): ∀ (a : int), % 130.26/130.48 Eq % 130.26/130.48 (Exists fun Y => % 130.26/130.48 Eq % 130.26/130.48 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int Y (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.48 False % 130.26/130.48 Clause #31481 (by clausification #[31480]): ∀ (a a_1 : int), % 130.26/130.48 Eq % 130.26/130.48 (Eq % 130.26/130.48 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int)) % 130.26/130.48 False % 130.26/130.48 Clause #31482 (by clausification #[31481]): ∀ (a a_1 : int), % 130.26/130.48 Ne % 130.26/130.48 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int a_1 (number_number_of_nat (bit0 (bit1 pls))))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 130.26/130.48 Clause #31483 (by forward demodulation #[31482, 711]): ∀ (a a_1 : int), % 130.26/130.48 Ne % 130.26/130.48 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int a_1 (number_number_of_nat (bit0 one_one_int)))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 130.26/130.48 Clause #31484 (by forward demodulation #[31483, 2527]): ∀ (a a_1 : int), % 130.26/130.48 Ne % 130.26/130.48 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 (bit1 pls)))) % 130.26/130.48 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.26/130.48 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 130.35/130.50 Clause #31485 (by forward demodulation #[31484, 711]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (number_number_of_nat (bit0 one_one_int))) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 130.35/130.50 Clause #31486 (by forward demodulation #[31485, 2527]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m) one_one_int) % 130.35/130.50 Clause #31487 (by forward demodulation #[31486, 5013]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int one_one_int (times_times_int (number_number_of_int (bit0 (bit0 (bit1 pls)))) m)) % 130.35/130.50 Clause #31488 (by forward demodulation #[31487, 4446]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int one_one_int (times_times_int m (number_number_of_int (bit0 (bit0 (bit1 pls)))))) % 130.35/130.50 Clause #31489 (by forward demodulation #[31488, 702]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 130.35/130.50 Clause #31490 (by forward demodulation #[31489, 711]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int)))) % 130.35/130.50 Clause #31491 (by forward demodulation #[31490, 7820]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int one_one_int (bit0 (bit0 m))) % 130.35/130.50 Clause #31492 (by forward demodulation #[31491, 9862]): ∀ (a a_1 : int), % 130.35/130.50 Ne % 130.35/130.50 (plus_plus_int (power_power_int a (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int a_1 (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (bit1 (bit0 m)) % 130.35/130.50 Clause #31624 (by forward demodulation #[703, 711]): ∀ (a a_1 : int), % 130.35/130.50 Or (Ne t one_one_int) % 130.35/130.50 (Eq % 130.35/130.50 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.50 (power_power_int (skS.0 1 a a_1) (number_number_of_nat (bit0 one_one_int)))) % 130.35/130.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.35/130.50 Clause #31625 (by forward demodulation #[31624, 2527]): ∀ (a a_1 : int), % 130.35/130.50 Or (Ne t one_one_int) % 130.35/130.50 (Eq % 130.35/130.50 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.50 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.35/130.50 Clause #31626 (by forward demodulation #[31625, 711]): ∀ (a a_1 : int), % 130.35/130.50 Or (Ne t one_one_int) % 130.35/130.50 (Eq % 130.35/130.50 (plus_plus_int (power_power_int (skS.0 0 a) (number_number_of_nat (bit0 one_one_int))) % 130.35/130.50 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.35/130.50 Clause #31627 (by forward demodulation #[31626, 2527]): ∀ (a a_1 : int), % 130.35/130.50 Or (Ne t one_one_int) % 130.35/130.50 (Eq % 130.35/130.50 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.50 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.50 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.35/130.50 Clause #31628 (by forward demodulation #[31627, 5013]): ∀ (a a_1 : int), % 130.35/130.50 Or (Ne t one_one_int) % 130.35/130.50 (Eq % 130.35/130.50 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m))) % 130.35/130.52 Clause #31629 (by forward demodulation #[31628, 8049]): ∀ (a a_1 : int), % 130.35/130.52 Or (Ne t one_one_int) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int one_one_int (times_times_int (bit0 (bit1 pls)) (bit0 m)))) % 130.35/130.52 Clause #31630 (by forward demodulation #[31629, 8123]): ∀ (a a_1 : int), % 130.35/130.52 Or (Ne t one_one_int) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls)))))) % 130.35/130.52 Clause #31631 (by forward demodulation #[31630, 711]): ∀ (a a_1 : int), % 130.35/130.52 Or (Ne t one_one_int) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int))))) % 130.35/130.52 Clause #31632 (by forward demodulation #[31631, 7820]): ∀ (a a_1 : int), % 130.35/130.52 Or (Ne t one_one_int) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int one_one_int (bit0 (bit0 m)))) % 130.35/130.52 Clause #31633 (by forward demodulation #[31632, 9862]): ∀ (a a_1 : int), % 130.35/130.52 Or (Ne t one_one_int) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 0 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 1 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (bit1 (bit0 m))) % 130.35/130.52 Clause #31634 (by forward contextual literal cutting #[31633, 31492]): Ne t one_one_int % 130.35/130.52 Clause #31635 (by backward contextual literal cutting #[31634, 1021]): Eq (ord_less_int one_one_int t) True % 130.35/130.52 Clause #31681 (by forward demodulation #[704, 31635]): ∀ (a a_1 : int), % 130.35/130.52 Or (Eq True False) % 130.35/130.52 (Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int)) % 130.35/130.52 Clause #31682 (by clausification #[31681]): ∀ (a a_1 : int), % 130.35/130.52 Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 (bit1 pls))))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 130.35/130.52 Clause #31683 (by forward demodulation #[31682, 711]): ∀ (a a_1 : int), % 130.35/130.52 Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (number_number_of_nat (bit0 one_one_int)))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 130.35/130.52 Clause #31684 (by forward demodulation #[31683, 2527]): ∀ (a a_1 : int), % 130.35/130.52 Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 (bit1 pls)))) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 130.35/130.52 Clause #31685 (by forward demodulation #[31684, 711]): ∀ (a a_1 : int), % 130.35/130.52 Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (number_number_of_nat (bit0 one_one_int))) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 130.35/130.52 Clause #31686 (by forward demodulation #[31685, 2527]): ∀ (a a_1 : int), % 130.35/130.52 Eq % 130.35/130.52 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.35/130.52 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.35/130.52 (plus_plus_int (times_times_int (bit0 (bit0 (bit1 pls))) m) one_one_int) % 130.46/130.68 Clause #31687 (by forward demodulation #[31686, 5013]): ∀ (a a_1 : int), % 130.46/130.68 Eq % 130.46/130.68 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.68 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.68 (plus_plus_int one_one_int (times_times_int (bit0 (bit0 (bit1 pls))) m)) % 130.46/130.68 Clause #31688 (by forward demodulation #[31687, 8049]): ∀ (a a_1 : int), % 130.46/130.68 Eq % 130.46/130.68 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.68 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.68 (plus_plus_int one_one_int (times_times_int (bit0 (bit1 pls)) (bit0 m))) % 130.46/130.68 Clause #31689 (by forward demodulation #[31688, 8123]): ∀ (a a_1 : int), % 130.46/130.68 Eq % 130.46/130.68 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.68 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.68 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 (bit1 pls))))) % 130.46/130.68 Clause #31690 (by forward demodulation #[31689, 711]): ∀ (a a_1 : int), % 130.46/130.69 Eq % 130.46/130.69 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.69 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.69 (plus_plus_int one_one_int (times_times_int m (bit0 (bit0 one_one_int)))) % 130.46/130.69 Clause #31691 (by forward demodulation #[31690, 7820]): ∀ (a a_1 : int), % 130.46/130.69 Eq % 130.46/130.69 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.69 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.69 (plus_plus_int one_one_int (bit0 (bit0 m))) % 130.46/130.69 Clause #31692 (by forward demodulation #[31691, 9862]): ∀ (a a_1 : int), % 130.46/130.69 Eq % 130.46/130.69 (plus_plus_int (power_power_int (skS.0 2 a) (plus_plus_nat one_one_nat one_one_nat)) % 130.46/130.69 (power_power_int (skS.0 3 a a_1) (plus_plus_nat one_one_nat one_one_nat))) % 130.46/130.69 (bit1 (bit0 m)) % 130.46/130.69 Clause #31693 (by forward contextual literal cutting #[31692, 31492]): False % 130.46/130.69 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------