%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM926+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:18:25 AM UTC 2026
% Result : Theorem 2.49s 0.84s
% Output : CNFRefutation 2.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 23
% Syntax : Number of formulae : 169 ( 82 unt; 0 def)
% Number of atoms : 272 ( 174 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 219 ( 116 ~; 92 |; 0 &)
% ( 2 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-3 aty)
% Number of variables : 138 ( 56 sgn 28 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_20_zle__refl,axiom,
! [W] : ord_less_eq(int,W,W),
file('theBenchmark.p',fact_20_zle__refl) ).
fof(fact_24_zle__trans,axiom,
! [K,I,J] :
( ord_less_eq(int,I,J)
=> ( ord_less_eq(int,J,K)
=> ord_less_eq(int,I,K) ) ),
file('theBenchmark.p',fact_24_zle__trans) ).
fof(fact_85_zmult__commute,axiom,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
file('theBenchmark.p',fact_85_zmult__commute) ).
fof(fact_86_number__of__is__id,axiom,
! [K] : number_number_of(int,K) = ti(int,K),
file('theBenchmark.p',fact_86_number__of__is__id) ).
fof(fact_87_zadd__assoc,axiom,
! [Z1,Z2,Z3] : plus_plus(int,plus_plus(int,Z1,Z2),Z3) = plus_plus(int,Z1,plus_plus(int,Z2,Z3)),
file('theBenchmark.p',fact_87_zadd__assoc) ).
fof(fact_89_zadd__commute,axiom,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
file('theBenchmark.p',fact_89_zadd__commute) ).
fof(fact_124_add__Pls,axiom,
! [K] : plus_plus(int,pls,K) = ti(int,K),
file('theBenchmark.p',fact_124_add__Pls) ).
fof(fact_126_Bit0__def,axiom,
! [K] : bit0(K) = plus_plus(int,K,K),
file('theBenchmark.p',fact_126_Bit0__def) ).
fof(fact_132_plus__numeral__code_I9_J,axiom,
! [V,W] : plus_plus(int,number_number_of(int,V),number_number_of(int,W)) = number_number_of(int,plus_plus(int,V,W)),
file('theBenchmark.p',fact_132_plus__numeral__code_I9_J) ).
fof(fact_151_Bit1__def,axiom,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
file('theBenchmark.p',fact_151_Bit1__def) ).
fof(fact_204_zadd__0,axiom,
! [Z] : plus_plus(int,zero_zero(int),Z) = ti(int,Z),
file('theBenchmark.p',fact_204_zadd__0) ).
fof(fact_205_zadd__0__right,axiom,
! [Z] : plus_plus(int,Z,zero_zero(int)) = ti(int,Z),
file('theBenchmark.p',fact_205_zadd__0__right) ).
fof(tsy_c_Orderings_Oord__class_Oless_arg1,axiom,
! [B_1_1,B_2_1,X_a] :
( order(X_a)
=> ( ord_less(X_a,ti(X_a,B_1_1),B_2_1)
<=> ord_less(X_a,B_1_1,B_2_1) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless_arg1) ).
fof(tsy_c_Orderings_Oord__class_Oless__eq_arg2,axiom,
! [B_1_1,B_2_1,X_a] :
( order(X_a)
=> ( ord_less_eq(X_a,B_1_1,ti(X_a,B_2_1))
<=> ord_less_eq(X_a,B_1_1,B_2_1) ) ),
file('theBenchmark.p',tsy_c_Orderings_Oord__class_Oless__eq_arg2) ).
fof(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( t = one_one(int)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( ord_less(int,one_one(int),t)
=> ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) ),
file('theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_327_order__le__neq__implies__less,axiom,
! [X_a] :
( order(X_a)
=> ! [X_1,Y_1] :
( ord_less_eq(X_a,X_1,Y_1)
=> ( ti(X_a,X_1) != ti(X_a,Y_1)
=> ord_less(X_a,X_1,Y_1) ) ) ),
file('theBenchmark.p',fact_327_order__le__neq__implies__less) ).
fof(conj_0,conjecture,
? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_567,plain,
( ~ ord_less(A,B,C)
| ord_less(A,ti(A,B),C)
| ~ order(A) ),
inference(clausify,[status(thm)],[tsy_c_Orderings_Oord__class_Oless_arg1]) ).
cnf(c_572,plain,
( ord_less_eq(A,B,C)
| ~ ord_less_eq(A,B,ti(A,C))
| ~ order(A) ),
inference(clausify,[status(thm)],[tsy_c_Orderings_Oord__class_Oless__eq_arg2]) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t,
file('theBenchmark.p',tsy_v_t_____res) ).
cnf(c_601,plain,
ti(int,t) = t,
inference(clausify,[status(thm)],[tsy_v_t_____res]) ).
fof(fact_0_tpos,axiom,
ord_less_eq(int,one_one(int),t),
file('theBenchmark.p',fact_0_tpos) ).
cnf(c_602,plain,
ord_less_eq(int,one_one(int),t),
inference(clausify,[status(thm)],[fact_0_tpos]) ).
fof(nnf_412,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| one_one(int) != t ),
inference(fof_nnf,[status(thm)],[fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(sk_fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,plain,
( plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| one_one(int) != t ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X,sK0),skolemize(Y,sK1)],[nnf_412]) ).
cnf(c_603,plain,
( plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| one_one(int) != t ),
inference(split_conjunct,[status(thm)],[sk_fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c_604,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(copy,[status(thm)],[c_603]) ).
fof(nnf_413,plain,
( ? [X,Y] : plus_plus(int,power_power(int,X,number_number_of(nat,bit0(bit1(pls)))),power_power(int,Y,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(fof_nnf,[status(thm)],[fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(sk_fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,plain,
( plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X,sK2),skolemize(Y,sK3)],[nnf_413]) ).
cnf(c_605,plain,
( plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls))))) = plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int))
| ~ ord_less(int,one_one(int),t) ),
inference(split_conjunct,[status(thm)],[sk_fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c_606,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(copy,[status(thm)],[c_605]) ).
cnf(c_739,plain,
( ord_less(A,B,C)
| ti(A,C) = ti(A,B)
| ~ ord_less_eq(A,B,C)
| ~ order(A) ),
inference(clausify,[status(thm)],[fact_327_order__le__neq__implies__less]) ).
fof(arity_Int_Oint___Orderings_Oorder,axiom,
order(int),
file('theBenchmark.p',arity_Int_Oint___Orderings_Oorder) ).
cnf(c_828,plain,
order(int),
inference(clausify,[status(thm)],[arity_Int_Oint___Orderings_Oorder]) ).
cnf(c_919,plain,
ord_less_eq(int,A,A),
inference(clausify,[status(thm)],[fact_20_zle__refl]) ).
cnf(c_925,plain,
( ord_less_eq(int,A,C)
| ~ ord_less_eq(int,B,C)
| ~ ord_less_eq(int,A,B) ),
inference(clausify,[status(thm)],[fact_24_zle__trans]) ).
cnf(c_995,plain,
times_times(int,A,B) = times_times(int,B,A),
inference(clausify,[status(thm)],[fact_85_zmult__commute]) ).
cnf(c_996,plain,
number_number_of(int,A) = ti(int,A),
inference(clausify,[status(thm)],[fact_86_number__of__is__id]) ).
cnf(c_997,plain,
ti(int,A) = number_number_of(int,A),
inference(copy,[status(thm)],[c_996]) ).
cnf(c_998,plain,
plus_plus(int,plus_plus(int,A,B),C) = plus_plus(int,A,plus_plus(int,B,C)),
inference(clausify,[status(thm)],[fact_87_zadd__assoc]) ).
cnf(c_1000,plain,
plus_plus(int,A,B) = plus_plus(int,B,A),
inference(clausify,[status(thm)],[fact_89_zadd__commute]) ).
cnf(c_1050,plain,
plus_plus(int,pls,A) = ti(int,A),
inference(clausify,[status(thm)],[fact_124_add__Pls]) ).
cnf(c_1051,plain,
plus_plus(int,pls,A) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_997,c_1050]) ).
cnf(c_1054,plain,
bit0(A) = plus_plus(int,A,A),
inference(clausify,[status(thm)],[fact_126_Bit0__def]) ).
cnf(c_1063,plain,
number_number_of(int,plus_plus(int,A,B)) = plus_plus(int,number_number_of(int,A),number_number_of(int,B)),
inference(clausify,[status(thm)],[fact_132_plus__numeral__code_I9_J]) ).
cnf(c_1064,plain,
plus_plus(int,number_number_of(int,A),number_number_of(int,B)) = number_number_of(int,plus_plus(int,A,B)),
inference(copy,[status(thm)],[c_1063]) ).
cnf(c_1080,plain,
bit1(A) = plus_plus(int,plus_plus(int,one_one(int),A),A),
inference(clausify,[status(thm)],[fact_151_Bit1__def]) ).
cnf(c_1081,plain,
bit1(A) = plus_plus(int,A,plus_plus(int,one_one(int),A)),
inference(paramod,[status(thm)],[c_1000,c_1080]) ).
fof(fact_158_one__is__num__one,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('theBenchmark.p',fact_158_one__is__num__one) ).
cnf(c_1091,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(clausify,[status(thm)],[fact_158_one__is__num__one]) ).
cnf(c_2432,plain,
one_one(int) = number_number_of(int,plus_plus(int,pls,plus_plus(int,one_one(int),pls))),
inference(paramod,[status(thm)],[c_1081,c_1091]) ).
cnf(c_2433,plain,
one_one(int) = number_number_of(int,plus_plus(int,pls,plus_plus(int,pls,one_one(int)))),
inference(paramod,[status(thm)],[c_1000,c_2432]) ).
cnf(c_2434,plain,
one_one(int) = number_number_of(int,plus_plus(int,pls,number_number_of(int,one_one(int)))),
inference(paramod,[status(thm)],[c_1051,c_2433]) ).
cnf(c_2435,plain,
one_one(int) = number_number_of(int,number_number_of(int,number_number_of(int,one_one(int)))),
inference(paramod,[status(thm)],[c_1051,c_2434]) ).
cnf(c_1092,plain,
number_number_of(int,number_number_of(int,number_number_of(int,one_one(int)))) = one_one(int),
inference(copy,[status(thm)],[c_2435]) ).
fof(fact_202_Pls__def,axiom,
pls = zero_zero(int),
file('theBenchmark.p',fact_202_Pls__def) ).
cnf(c_1127,plain,
pls = zero_zero(int),
inference(clausify,[status(thm)],[fact_202_Pls__def]) ).
cnf(c_1129,plain,
plus_plus(int,zero_zero(int),A) = ti(int,A),
inference(clausify,[status(thm)],[fact_204_zadd__0]) ).
cnf(c_1130,plain,
plus_plus(int,zero_zero(int),A) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_997,c_1129]) ).
cnf(c_1131,plain,
plus_plus(int,A,zero_zero(int)) = ti(int,A),
inference(clausify,[status(thm)],[fact_205_zadd__0__right]) ).
cnf(c_1132,plain,
plus_plus(int,A,zero_zero(int)) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_997,c_1131]) ).
cnf(c_1574,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,bit0(bit1(pls)))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_2436,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,bit0(bit1(zero_zero(int))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1127,c_1574]) ).
cnf(c_2437,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1081,c_2436]) ).
cnf(c_2438,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1132,c_2437]) ).
cnf(c_2439,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1130,c_2438]) ).
cnf(c_2440,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1054,c_2439]) ).
cnf(c_2441,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2440]) ).
cnf(c_2442,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(pls))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2441]) ).
cnf(c_2443,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(bit1(zero_zero(int)))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1127,c_2442]) ).
cnf(c_2444,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1081,c_2443]) ).
cnf(c_2445,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1132,c_2444]) ).
cnf(c_2446,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1130,c_2445]) ).
cnf(c_2447,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1054,c_2446]) ).
cnf(c_2448,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2447]) ).
cnf(c_2449,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2448]) ).
cnf(c_2450,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1127,c_2449]) ).
cnf(c_2451,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1081,c_2450]) ).
cnf(c_2452,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1132,c_2451]) ).
cnf(c_2453,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1130,c_2452]) ).
cnf(c_2454,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1054,c_2453]) ).
cnf(c_2455,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2454]) ).
cnf(c_2456,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2455]) ).
cnf(c_2457,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))),number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1054,c_2456]) ).
cnf(c_2458,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,plus_plus(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2457]) ).
cnf(c_2459,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),one_one(int)),plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_1064,c_2458]) ).
cnf(c_2460,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))),m),one_one(int)),
inference(paramod,[status(thm)],[c_998,c_2459]) ).
cnf(c_2461,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))),one_one(int)),
inference(paramod,[status(thm)],[c_995,c_2460]) ).
cnf(c_1575,negated_conjecture,
plus_plus(int,power_power(int,A,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,B,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) != plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))),
inference(paramod,[status(thm)],[c_1000,c_2461]) ).
cnf(c_2462,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1127,c_606]) ).
cnf(c_2463,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1081,c_2462]) ).
cnf(c_2464,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1132,c_2463]) ).
cnf(c_2465,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1130,c_2464]) ).
cnf(c_2466,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1054,c_2465]) ).
cnf(c_2467,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2466]) ).
cnf(c_2468,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2467]) ).
cnf(c_2469,plain,
( plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))),number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1054,c_2468]) ).
cnf(c_2470,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,plus_plus(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2469]) ).
cnf(c_2471,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),one_one(int)),plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2470]) ).
cnf(c_2472,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))),m),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_998,c_2471]) ).
cnf(c_2473,plain,
( plus_plus(int,times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))),one_one(int)) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_995,c_2472]) ).
cnf(c_2474,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1000,c_2473]) ).
cnf(c_2475,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(bit1(zero_zero(int))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1127,c_2474]) ).
cnf(c_2476,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1081,c_2475]) ).
cnf(c_2477,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1132,c_2476]) ).
cnf(c_2478,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1130,c_2477]) ).
cnf(c_2479,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1054,c_2478]) ).
cnf(c_2480,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2479]) ).
cnf(c_2481,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(pls)))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2480]) ).
cnf(c_2482,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(bit1(zero_zero(int))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1127,c_2481]) ).
cnf(c_2483,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1081,c_2482]) ).
cnf(c_2484,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1132,c_2483]) ).
cnf(c_2485,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1130,c_2484]) ).
cnf(c_2486,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1054,c_2485]) ).
cnf(c_2487,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2486]) ).
cnf(c_2488,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK2,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK3,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))))
| ~ ord_less(int,one_one(int),t) ),
inference(paramod,[status(thm)],[c_1064,c_2487]) ).
cnf(c_1602,negated_conjecture,
~ ord_less(int,one_one(int),t),
inference(resolve,[status(thm)],[c_1575,c_2488]) ).
cnf(c_2489,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1127,c_604]) ).
cnf(c_2490,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1081,c_2489]) ).
cnf(c_2491,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1132,c_2490]) ).
cnf(c_2492,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1130,c_2491]) ).
cnf(c_2493,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1054,c_2492]) ).
cnf(c_2494,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2493]) ).
cnf(c_2495,plain,
( plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2494]) ).
cnf(c_2496,plain,
( plus_plus(int,times_times(int,number_number_of(int,plus_plus(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))),number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1054,c_2495]) ).
cnf(c_2497,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,plus_plus(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))),number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2496]) ).
cnf(c_2498,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,plus_plus(int,one_one(int),one_one(int)),plus_plus(int,one_one(int),one_one(int)))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2497]) ).
cnf(c_2499,plain,
( plus_plus(int,times_times(int,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))),m),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_998,c_2498]) ).
cnf(c_2500,plain,
( plus_plus(int,times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))),one_one(int)) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_995,c_2499]) ).
cnf(c_2501,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(pls)))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1000,c_2500]) ).
cnf(c_2502,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(bit1(zero_zero(int))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1127,c_2501]) ).
cnf(c_2503,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1081,c_2502]) ).
cnf(c_2504,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1132,c_2503]) ).
cnf(c_2505,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1130,c_2504]) ).
cnf(c_2506,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1054,c_2505]) ).
cnf(c_2507,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2506]) ).
cnf(c_2508,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2507]) ).
cnf(c_2509,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(bit1(zero_zero(int))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1127,c_2508]) ).
cnf(c_2510,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1081,c_2509]) ).
cnf(c_2511,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1132,c_2510]) ).
cnf(c_2512,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1130,c_2511]) ).
cnf(c_2513,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,plus_plus(int,number_number_of(int,number_number_of(int,one_one(int))),number_number_of(int,number_number_of(int,one_one(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1054,c_2512]) ).
cnf(c_2514,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,number_number_of(int,plus_plus(int,number_number_of(int,one_one(int)),number_number_of(int,one_one(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2513]) ).
cnf(c_2515,plain,
( plus_plus(int,one_one(int),times_times(int,m,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int))))))))) = plus_plus(int,power_power(int,sK0,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),power_power(int,sK1,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))))
| one_one(int) != t ),
inference(paramod,[status(thm)],[c_1064,c_2514]) ).
cnf(c_1603,negated_conjecture,
one_one(int) != t,
inference(resolve,[status(thm)],[c_1575,c_2515]) ).
cnf(c_1627,plain,
number_number_of(int,t) = t,
inference(paramod,[status(thm)],[c_997,c_601]) ).
cnf(c_2516,plain,
( ord_less_eq(int,ti(int,A),A)
| ~ order(int) ),
inference(resolve,[status(thm)],[c_919,c_572]) ).
cnf(c_2517,plain,
( ord_less_eq(int,number_number_of(int,A),A)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_997,c_2516]) ).
cnf(c_1896,plain,
ord_less_eq(int,number_number_of(int,A),A),
inference(resolve,[status(thm)],[c_828,c_2517]) ).
cnf(c_2518,plain,
( ord_less_eq(int,number_number_of(int,ti(int,A)),A)
| ~ order(int) ),
inference(resolve,[status(thm)],[c_1896,c_572]) ).
cnf(c_2519,plain,
( ord_less_eq(int,number_number_of(int,number_number_of(int,A)),A)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_997,c_2518]) ).
cnf(c_1908,plain,
ord_less_eq(int,number_number_of(int,number_number_of(int,A)),A),
inference(resolve,[status(thm)],[c_828,c_2519]) ).
cnf(c_2010,plain,
( ord_less_eq(int,A,t)
| ~ ord_less_eq(int,A,one_one(int)) ),
inference(resolve,[status(thm)],[c_925,c_602]) ).
cnf(c_2139,plain,
ord_less_eq(int,number_number_of(int,number_number_of(int,one_one(int))),t),
inference(resolve,[status(thm)],[c_2010,c_1908]) ).
cnf(c_2520,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| ti(int,t) = ti(int,number_number_of(int,number_number_of(int,one_one(int))))
| ~ order(int) ),
inference(resolve,[status(thm)],[c_2139,c_739]) ).
cnf(c_2521,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| number_number_of(int,t) = ti(int,number_number_of(int,number_number_of(int,one_one(int))))
| ~ order(int) ),
inference(paramod,[status(thm)],[c_997,c_2520]) ).
cnf(c_2522,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| t = ti(int,number_number_of(int,number_number_of(int,one_one(int))))
| ~ order(int) ),
inference(paramod,[status(thm)],[c_1627,c_2521]) ).
cnf(c_2523,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| t = number_number_of(int,number_number_of(int,number_number_of(int,one_one(int))))
| ~ order(int) ),
inference(paramod,[status(thm)],[c_997,c_2522]) ).
cnf(c_2524,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| t = one_one(int)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_1092,c_2523]) ).
cnf(c_2525,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| one_one(int) = t
| ~ order(int) ),
inference(copy,[status(thm)],[c_2524]) ).
cnf(c_2526,plain,
( ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t)
| one_one(int) = t ),
inference(resolve,[status(thm)],[c_828,c_2525]) ).
cnf(c_2336,plain,
ord_less(int,number_number_of(int,number_number_of(int,one_one(int))),t),
inference(resolve,[status(thm)],[c_1603,c_2526]) ).
cnf(c_2527,plain,
( ord_less(int,ti(int,number_number_of(int,number_number_of(int,one_one(int)))),t)
| ~ order(int) ),
inference(resolve,[status(thm)],[c_2336,c_567]) ).
cnf(c_2528,plain,
( ord_less(int,number_number_of(int,number_number_of(int,number_number_of(int,one_one(int)))),t)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_997,c_2527]) ).
cnf(c_2529,plain,
( ord_less(int,one_one(int),t)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_1092,c_2528]) ).
cnf(c_2530,plain,
ord_less(int,one_one(int),t),
inference(resolve,[status(thm)],[c_828,c_2529]) ).
cnf(c_2431,plain,
$false,
inference(resolve,[status(thm)],[c_1602,c_2530]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 04:20:48 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1184581 was started by sandbox2 on n005,
% 0.10/0.37 % Sat Sep 26 04:20:48 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.23/0.49
% 0.23/0.49 % From the command line: assign(max_seconds, 300).
% 0.23/0.49
% 0.23/0.49 % SInE: 402 to sos, 250 to usable, of 652 axioms (tolerance 2.00, depth 0 fixpoint).
% 2.49/0.84
% 2.49/0.84 % SZS status Theorem for theBenchmark
% 2.49/0.84
% 2.49/0.84 % Proof 1 at 0.27 (+ 0.05) seconds.
% 2.49/0.84 % Length of proof is 60.
% 2.49/0.84 % Level of proof is 7.
% 2.49/0.84 % Maximum clause weight is 112.000.
% 2.49/0.84 % Given clauses 160.
% 2.49/0.84
% 2.49/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------