%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:22 AM UTC 2026
% Result : Theorem 1.57s 0.75s
% Output : CNFRefutation 1.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 28
% Syntax : Number of formulae : 240 ( 228 unt; 0 def)
% Number of atoms : 259 ( 144 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 29 ~; 15 |; 0 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 93 ( 3 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Int_OBit0_res,axiom,
! [B_1_1] : ti(int,bit0(B_1_1)) = bit0(B_1_1),
file('theBenchmark.p',tsy_c_Int_OBit0_res) ).
fof(fact_21_zle__refl,axiom,
! [W] : ord_less_eq(int,W,W),
file('theBenchmark.p',fact_21_zle__refl) ).
fof(fact_22_number__of__is__id,axiom,
! [K] : number_number_of(int,K) = ti(int,K),
file('theBenchmark.p',fact_22_number__of__is__id) ).
fof(fact_23_zmult__commute,axiom,
! [Z,W] : times_times(int,Z,W) = times_times(int,W,Z),
file('theBenchmark.p',fact_23_zmult__commute) ).
fof(fact_25_times__numeral__code_I5_J,axiom,
! [V,W] : times_times(int,number_number_of(int,V),number_number_of(int,W)) = number_number_of(int,times_times(int,V,W)),
file('theBenchmark.p',fact_25_times__numeral__code_I5_J) ).
fof(fact_30_zle__antisym,axiom,
! [Z,W] :
( ord_less_eq(int,Z,W)
=> ( ord_less_eq(int,W,Z)
=> ti(int,Z) = ti(int,W) ) ),
file('theBenchmark.p',fact_30_zle__antisym) ).
fof(fact_62_mult__Pls,axiom,
! [W] : times_times(int,pls,W) = pls,
file('theBenchmark.p',fact_62_mult__Pls) ).
fof(fact_65_zmult__1__right,axiom,
! [Z] : times_times(int,Z,one_one(int)) = ti(int,Z),
file('theBenchmark.p',fact_65_zmult__1__right) ).
fof(fact_66_zmult__1,axiom,
! [Z] : times_times(int,one_one(int),Z) = ti(int,Z),
file('theBenchmark.p',fact_66_zmult__1) ).
fof(fact_67_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_67_plus__numeral__code_I9_J) ).
fof(fact_69_zadd__zmult__distrib2,axiom,
! [W,Z1,Z2] : times_times(int,W,plus_plus(int,Z1,Z2)) = plus_plus(int,times_times(int,W,Z1),times_times(int,W,Z2)),
file('theBenchmark.p',fact_69_zadd__zmult__distrib2) ).
fof(fact_94_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_94_zadd__assoc) ).
fof(fact_96_zadd__commute,axiom,
! [Z,W] : plus_plus(int,Z,W) = plus_plus(int,W,Z),
file('theBenchmark.p',fact_96_zadd__commute) ).
fof(fact_127_add__Pls__right,axiom,
! [K] : plus_plus(int,K,pls) = ti(int,K),
file('theBenchmark.p',fact_127_add__Pls__right) ).
fof(fact_128_add__Pls,axiom,
! [K] : plus_plus(int,pls,K) = ti(int,K),
file('theBenchmark.p',fact_128_add__Pls) ).
fof(fact_130_Bit0__def,axiom,
! [K] : bit0(K) = plus_plus(int,K,K),
file('theBenchmark.p',fact_130_Bit0__def) ).
fof(fact_162_Bit1__def,axiom,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
file('theBenchmark.p',fact_162_Bit1__def) ).
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(conj_0,conjecture,
ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_565,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]) ).
cnf(c_566,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(arity_Int_Oint___Orderings_Oorder,axiom,
order(int),
file('theBenchmark.p',arity_Int_Oint___Orderings_Oorder) ).
cnf(c_784,plain,
order(int),
inference(clausify,[status(thm)],[arity_Int_Oint___Orderings_Oorder]) ).
cnf(c_854,plain,
bit0(A) = ti(int,bit0(A)),
inference(clausify,[status(thm)],[tsy_c_Int_OBit0_res]) ).
cnf(c_855,plain,
ti(int,bit0(A)) = bit0(A),
inference(copy,[status(thm)],[c_854]) ).
fof(tsy_c_Int_OMin_res,axiom,
ti(int,min) = min,
file('theBenchmark.p',tsy_c_Int_OMin_res) ).
cnf(c_859,plain,
ti(int,min) = min,
inference(clausify,[status(thm)],[tsy_c_Int_OMin_res]) ).
fof(tsy_c_Int_OPls_res,axiom,
ti(int,pls) = pls,
file('theBenchmark.p',tsy_c_Int_OPls_res) ).
cnf(c_860,plain,
ti(int,pls) = pls,
inference(clausify,[status(thm)],[tsy_c_Int_OPls_res]) ).
fof(tsy_v_m_res,axiom,
ti(int,m) = m,
file('theBenchmark.p',tsy_v_m_res) ).
cnf(c_861,plain,
ti(int,m) = m,
inference(clausify,[status(thm)],[tsy_v_m_res]) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t,
file('theBenchmark.p',tsy_v_t_____res) ).
cnf(c_864,plain,
ti(int,t) = t,
inference(clausify,[status(thm)],[tsy_v_t_____res]) ).
fof(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
file('theBenchmark.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
cnf(c_867,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(clausify,[status(thm)],[fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096]) ).
fof(fact_3_t,axiom,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
file('theBenchmark.p',fact_3_t) ).
cnf(c_868,plain,
plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)) = times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t),
inference(clausify,[status(thm)],[fact_3_t]) ).
cnf(c_869,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(copy,[status(thm)],[c_868]) ).
cnf(c_897,plain,
ord_less_eq(int,A,A),
inference(clausify,[status(thm)],[fact_21_zle__refl]) ).
cnf(c_898,plain,
number_number_of(int,A) = ti(int,A),
inference(clausify,[status(thm)],[fact_22_number__of__is__id]) ).
cnf(c_899,plain,
ti(int,A) = number_number_of(int,A),
inference(copy,[status(thm)],[c_898]) ).
cnf(c_900,plain,
times_times(int,A,B) = times_times(int,B,A),
inference(clausify,[status(thm)],[fact_23_zmult__commute]) ).
cnf(c_902,plain,
number_number_of(int,times_times(int,A,B)) = times_times(int,number_number_of(int,A),number_number_of(int,B)),
inference(clausify,[status(thm)],[fact_25_times__numeral__code_I5_J]) ).
cnf(c_903,plain,
times_times(int,number_number_of(int,A),number_number_of(int,B)) = number_number_of(int,times_times(int,A,B)),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_910,plain,
( ti(int,A) = ti(int,B)
| ~ ord_less_eq(int,B,A)
| ~ ord_less_eq(int,A,B) ),
inference(clausify,[status(thm)],[fact_30_zle__antisym]) ).
cnf(c_2119,plain,
( number_number_of(int,A) = ti(int,B)
| ~ ord_less_eq(int,B,A)
| ~ ord_less_eq(int,A,B) ),
inference(paramod,[status(thm)],[c_899,c_910]) ).
cnf(c_911,plain,
( number_number_of(int,A) = number_number_of(int,B)
| ~ ord_less_eq(int,B,A)
| ~ ord_less_eq(int,A,B) ),
inference(paramod,[status(thm)],[c_899,c_2119]) ).
cnf(c_950,plain,
times_times(int,pls,A) = pls,
inference(clausify,[status(thm)],[fact_62_mult__Pls]) ).
cnf(c_955,plain,
times_times(int,A,one_one(int)) = ti(int,A),
inference(clausify,[status(thm)],[fact_65_zmult__1__right]) ).
cnf(c_956,plain,
times_times(int,A,one_one(int)) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_899,c_955]) ).
cnf(c_957,plain,
times_times(int,one_one(int),A) = ti(int,A),
inference(clausify,[status(thm)],[fact_66_zmult__1]) ).
cnf(c_958,plain,
times_times(int,one_one(int),A) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_899,c_957]) ).
cnf(c_959,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_67_plus__numeral__code_I9_J]) ).
cnf(c_960,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_959]) ).
cnf(c_962,plain,
times_times(int,A,plus_plus(int,B,C)) = plus_plus(int,times_times(int,A,B),times_times(int,A,C)),
inference(clausify,[status(thm)],[fact_69_zadd__zmult__distrib2]) ).
cnf(c_999,plain,
plus_plus(int,plus_plus(int,A,B),C) = plus_plus(int,A,plus_plus(int,B,C)),
inference(clausify,[status(thm)],[fact_94_zadd__assoc]) ).
cnf(c_1001,plain,
plus_plus(int,A,B) = plus_plus(int,B,A),
inference(clausify,[status(thm)],[fact_96_zadd__commute]) ).
fof(fact_120_Pls__def,axiom,
pls = zero_zero(int),
file('theBenchmark.p',fact_120_Pls__def) ).
cnf(c_1034,plain,
pls = zero_zero(int),
inference(clausify,[status(thm)],[fact_120_Pls__def]) ).
cnf(c_1042,plain,
plus_plus(int,A,pls) = ti(int,A),
inference(clausify,[status(thm)],[fact_127_add__Pls__right]) ).
cnf(c_2120,plain,
plus_plus(int,A,zero_zero(int)) = ti(int,A),
inference(paramod,[status(thm)],[c_1034,c_1042]) ).
cnf(c_1043,plain,
plus_plus(int,A,zero_zero(int)) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_899,c_2120]) ).
cnf(c_1044,plain,
plus_plus(int,pls,A) = ti(int,A),
inference(clausify,[status(thm)],[fact_128_add__Pls]) ).
cnf(c_2121,plain,
plus_plus(int,zero_zero(int),A) = ti(int,A),
inference(paramod,[status(thm)],[c_1034,c_1044]) ).
cnf(c_1045,plain,
plus_plus(int,zero_zero(int),A) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_899,c_2121]) ).
cnf(c_1048,plain,
bit0(A) = plus_plus(int,A,A),
inference(clausify,[status(thm)],[fact_130_Bit0__def]) ).
cnf(c_1097,plain,
bit1(A) = plus_plus(int,plus_plus(int,one_one(int),A),A),
inference(clausify,[status(thm)],[fact_162_Bit1__def]) ).
cnf(c_1098,plain,
bit1(A) = plus_plus(int,A,plus_plus(int,one_one(int),A)),
inference(paramod,[status(thm)],[c_1001,c_1097]) ).
fof(fact_324__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096,axiom,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
file('theBenchmark.p',fact_324__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
cnf(c_1392,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(clausify,[status(thm)],[fact_324__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096]) ).
cnf(c_2122,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(bit1(zero_zero(int))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1034,c_1392]) ).
cnf(c_2123,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1098,c_2122]) ).
cnf(c_2124,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1043,c_2123]) ).
cnf(c_2125,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1045,c_2124]) ).
cnf(c_2126,plain,
minus_minus(int,power_power(int,s,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)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1048,c_2125]) ).
cnf(c_2127,plain,
minus_minus(int,power_power(int,s,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)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2126]) ).
cnf(c_2128,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2127]) ).
cnf(c_2129,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(zero_zero(int))))),one_one(int)),
inference(paramod,[status(thm)],[c_1034,c_2128]) ).
cnf(c_2130,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1098,c_2129]) ).
cnf(c_2131,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1043,c_2130]) ).
cnf(c_2132,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1045,c_2131]) ).
cnf(c_2133,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,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)),
inference(paramod,[status(thm)],[c_1048,c_2132]) ).
cnf(c_2134,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,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)),
inference(paramod,[status(thm)],[c_960,c_2133]) ).
cnf(c_2135,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2134]) ).
cnf(c_2136,plain,
minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)) = plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))),
inference(paramod,[status(thm)],[c_1001,c_2135]) ).
cnf(c_1393,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)),
inference(copy,[status(thm)],[c_2136]) ).
cnf(c_1575,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),zero_zero(int)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_2137,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(zero_zero(int))))),one_one(int)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1034,c_1575]) ).
cnf(c_2138,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),one_one(int)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1098,c_2137]) ).
cnf(c_2139,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),one_one(int)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1043,c_2138]) ).
cnf(c_2140,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),one_one(int)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1045,c_2139]) ).
cnf(c_2141,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,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)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1048,c_2140]) ).
cnf(c_2142,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,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)),zero_zero(int)),
inference(paramod,[status(thm)],[c_960,c_2141]) ).
cnf(c_2143,negated_conjecture,
~ ord_less(int,plus_plus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),one_one(int)),zero_zero(int)),
inference(paramod,[status(thm)],[c_960,c_2142]) ).
cnf(c_2144,negated_conjecture,
~ ord_less(int,plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1001,c_2143]) ).
cnf(c_1576,negated_conjecture,
~ ord_less(int,minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1393,c_2144]) ).
cnf(c_2145,plain,
ord_less(int,times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1034,c_867]) ).
cnf(c_2146,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1098,c_2145]) ).
cnf(c_2147,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1043,c_2146]) ).
cnf(c_2148,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1045,c_2147]) ).
cnf(c_2149,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1048,c_2148]) ).
cnf(c_2150,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2149]) ).
cnf(c_2151,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2150]) ).
cnf(c_2152,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1048,c_2151]) ).
cnf(c_2153,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2152]) ).
cnf(c_2154,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2153]) ).
cnf(c_2155,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_999,c_2154]) ).
cnf(c_2156,plain,
ord_less(int,times_times(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)),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_900,c_2155]) ).
cnf(c_2157,plain,
ord_less(int,times_times(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))))))))),t),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1001,c_2156]) ).
cnf(c_2158,plain,
ord_less(int,times_times(int,t,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)))))))))),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_900,c_2157]) ).
cnf(c_2159,plain,
ord_less(int,plus_plus(int,times_times(int,t,one_one(int)),times_times(int,t,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)))))))))),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_962,c_2158]) ).
cnf(c_2160,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls)))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_956,c_2159]) ).
cnf(c_2161,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1034,c_2160]) ).
cnf(c_2162,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1098,c_2161]) ).
cnf(c_2163,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1043,c_2162]) ).
cnf(c_2164,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1045,c_2163]) ).
cnf(c_2165,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1048,c_2164]) ).
cnf(c_2166,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2165]) ).
cnf(c_2167,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2166]) ).
cnf(c_2168,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_1048,c_2167]) ).
cnf(c_2169,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2168]) ).
cnf(c_2170,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_960,c_2169]) ).
cnf(c_2171,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_999,c_2170]) ).
cnf(c_2172,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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)),zero_zero(int))),
inference(paramod,[status(thm)],[c_900,c_2171]) ).
cnf(c_2173,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(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))))))))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1001,c_2172]) ).
cnf(c_2174,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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)))))))))),times_times(int,zero_zero(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_900,c_2173]) ).
cnf(c_2175,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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,times_times(int,zero_zero(int),one_one(int)),times_times(int,zero_zero(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_962,c_2174]) ).
cnf(c_2176,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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,times_times(int,one_one(int),zero_zero(int)),times_times(int,zero_zero(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_900,c_2175]) ).
cnf(c_1577,plain,
ord_less(int,plus_plus(int,number_number_of(int,t),times_times(int,t,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,number_number_of(int,zero_zero(int)),times_times(int,zero_zero(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_958,c_2176]) ).
cnf(c_1581,plain,
number_number_of(int,t) = t,
inference(paramod,[status(thm)],[c_899,c_864]) ).
cnf(c_1584,plain,
number_number_of(int,m) = m,
inference(paramod,[status(thm)],[c_899,c_861]) ).
cnf(c_2177,plain,
ti(int,zero_zero(int)) = pls,
inference(paramod,[status(thm)],[c_1034,c_860]) ).
cnf(c_2178,plain,
number_number_of(int,zero_zero(int)) = pls,
inference(paramod,[status(thm)],[c_899,c_2177]) ).
cnf(c_1585,plain,
number_number_of(int,zero_zero(int)) = zero_zero(int),
inference(paramod,[status(thm)],[c_1034,c_2178]) ).
cnf(c_1586,plain,
number_number_of(int,min) = min,
inference(paramod,[status(thm)],[c_899,c_859]) ).
cnf(c_2179,plain,
ti(int,plus_plus(int,A,A)) = bit0(A),
inference(paramod,[status(thm)],[c_1048,c_855]) ).
cnf(c_2180,plain,
number_number_of(int,plus_plus(int,A,A)) = bit0(A),
inference(paramod,[status(thm)],[c_899,c_2179]) ).
cnf(c_1589,plain,
number_number_of(int,plus_plus(int,A,A)) = plus_plus(int,A,A),
inference(paramod,[status(thm)],[c_1048,c_2180]) ).
cnf(c_2181,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int))))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1034,c_869]) ).
cnf(c_2182,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1098,c_2181]) ).
cnf(c_2183,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1043,c_2182]) ).
cnf(c_2184,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1045,c_2183]) ).
cnf(c_2185,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1048,c_2184]) ).
cnf(c_2186,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2185]) ).
cnf(c_2187,plain,
times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2186]) ).
cnf(c_2188,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(number_number_of(int,plus_plus(int,one_one(int),one_one(int))))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1589,c_2187]) ).
cnf(c_2189,plain,
times_times(int,plus_plus(int,times_times(int,number_number_of(int,bit0(plus_plus(int,one_one(int),one_one(int)))),m),one_one(int)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1589,c_2188]) ).
cnf(c_2190,plain,
times_times(int,plus_plus(int,times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1048,c_2189]) ).
cnf(c_2191,plain,
times_times(int,plus_plus(int,times_times(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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_999,c_2190]) ).
cnf(c_2192,plain,
times_times(int,plus_plus(int,times_times(int,m,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)),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_900,c_2191]) ).
cnf(c_2193,plain,
times_times(int,plus_plus(int,one_one(int),times_times(int,m,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))))))),t) = plus_plus(int,power_power(int,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1001,c_2192]) ).
cnf(c_2194,plain,
times_times(int,t,plus_plus(int,one_one(int),times_times(int,m,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,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_900,c_2193]) ).
cnf(c_2195,plain,
plus_plus(int,times_times(int,t,one_one(int)),times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_962,c_2194]) ).
cnf(c_2196,plain,
plus_plus(int,number_number_of(int,t),times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_956,c_2195]) ).
cnf(c_2197,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(bit1(pls)))),one_one(int)),
inference(paramod,[status(thm)],[c_1581,c_2196]) ).
cnf(c_2198,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(bit1(zero_zero(int))))),one_one(int)),
inference(paramod,[status(thm)],[c_1034,c_2197]) ).
cnf(c_2199,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),plus_plus(int,one_one(int),zero_zero(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1098,c_2198]) ).
cnf(c_2200,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(plus_plus(int,zero_zero(int),number_number_of(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1043,c_2199]) ).
cnf(c_2201,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,bit0(number_number_of(int,number_number_of(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1045,c_2200]) ).
cnf(c_2202,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,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)),
inference(paramod,[status(thm)],[c_1048,c_2201]) ).
cnf(c_2203,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,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)),
inference(paramod,[status(thm)],[c_960,c_2202]) ).
cnf(c_2204,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_960,c_2203]) ).
cnf(c_2205,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))),one_one(int)),
inference(paramod,[status(thm)],[c_1589,c_2204]) ).
cnf(c_2206,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),one_one(int)),
inference(paramod,[status(thm)],[c_1589,c_2205]) ).
cnf(c_1614,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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,one_one(int),power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))),
inference(paramod,[status(thm)],[c_1001,c_2206]) ).
cnf(c_2207,plain,
times_times(int,zero_zero(int),A) = pls,
inference(paramod,[status(thm)],[c_1034,c_950]) ).
cnf(c_1645,plain,
times_times(int,zero_zero(int),A) = zero_zero(int),
inference(paramod,[status(thm)],[c_1034,c_2207]) ).
cnf(c_2208,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,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,number_number_of(int,zero_zero(int)),times_times(int,zero_zero(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_1581,c_1577]) ).
cnf(c_2209,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,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,zero_zero(int),times_times(int,zero_zero(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_1585,c_2208]) ).
cnf(c_2210,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,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,zero_zero(int),zero_zero(int))),
inference(paramod,[status(thm)],[c_1645,c_2209]) ).
cnf(c_2211,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,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)))))))))),number_number_of(int,zero_zero(int))),
inference(paramod,[status(thm)],[c_1043,c_2210]) ).
cnf(c_1763,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,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)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1585,c_2211]) ).
cnf(c_2212,negated_conjecture,
~ ord_less(int,minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))),number_number_of(int,min)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1589,c_1576]) ).
cnf(c_2213,negated_conjecture,
~ ord_less(int,minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),number_number_of(int,min)),zero_zero(int)),
inference(paramod,[status(thm)],[c_1589,c_2212]) ).
cnf(c_1764,negated_conjecture,
~ ord_less(int,minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),zero_zero(int)),
inference(paramod,[status(thm)],[c_1586,c_2213]) ).
cnf(c_2214,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)),
inference(paramod,[status(thm)],[c_1589,c_1393]) ).
cnf(c_2215,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) = minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,number_number_of(int,plus_plus(int,one_one(int),one_one(int)))))),number_number_of(int,min)),
inference(paramod,[status(thm)],[c_1589,c_2214]) ).
cnf(c_2216,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) = minus_minus(int,power_power(int,s,number_number_of(nat,number_number_of(int,plus_plus(int,one_one(int),one_one(int))))),number_number_of(int,min)),
inference(paramod,[status(thm)],[c_1589,c_2215]) ).
cnf(c_2217,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),number_number_of(int,min)),
inference(paramod,[status(thm)],[c_1589,c_2216]) ).
cnf(c_1767,plain,
plus_plus(int,one_one(int),power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1586,c_2217]) ).
cnf(c_1813,plain,
plus_plus(int,t,times_times(int,t,times_times(int,m,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)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1767,c_1614]) ).
cnf(c_2218,plain,
( ord_less_eq(int,A,ti(int,A))
| ~ order(int) ),
inference(resolve,[status(thm)],[c_897,c_566]) ).
cnf(c_2219,plain,
( ord_less_eq(int,A,number_number_of(int,A))
| ~ order(int) ),
inference(paramod,[status(thm)],[c_899,c_2218]) ).
cnf(c_1900,plain,
ord_less_eq(int,A,number_number_of(int,A)),
inference(resolve,[status(thm)],[c_784,c_2219]) ).
cnf(c_2220,plain,
( ord_less_eq(int,ti(int,A),A)
| ~ order(int) ),
inference(resolve,[status(thm)],[c_897,c_565]) ).
cnf(c_2221,plain,
( ord_less_eq(int,number_number_of(int,A),A)
| ~ order(int) ),
inference(paramod,[status(thm)],[c_899,c_2220]) ).
cnf(c_1901,plain,
ord_less_eq(int,number_number_of(int,A),A),
inference(resolve,[status(thm)],[c_784,c_2221]) ).
cnf(c_2004,plain,
times_times(int,t,number_number_of(int,A)) = number_number_of(int,times_times(int,t,A)),
inference(paramod,[status(thm)],[c_1581,c_903]) ).
cnf(c_2010,plain,
times_times(int,m,number_number_of(int,A)) = number_number_of(int,times_times(int,m,A)),
inference(paramod,[status(thm)],[c_1584,c_903]) ).
cnf(c_2222,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_2010,c_1813]) ).
cnf(c_2223,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2222]) ).
cnf(c_2224,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,number_number_of(int,m),times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_956,c_2223]) ).
cnf(c_2225,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1584,c_2224]) ).
cnf(c_2226,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2225]) ).
cnf(c_2227,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,number_number_of(int,m),times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_956,c_2226]) ).
cnf(c_2228,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1584,c_2227]) ).
cnf(c_2229,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2228]) ).
cnf(c_2230,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,number_number_of(int,m),times_times(int,m,one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_956,c_2229]) ).
cnf(c_2231,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,times_times(int,m,one_one(int)))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1584,c_2230]) ).
cnf(c_2232,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,number_number_of(int,m))))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_956,c_2231]) ).
cnf(c_2233,plain,
plus_plus(int,t,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_1584,c_2232]) ).
cnf(c_2234,plain,
plus_plus(int,t,number_number_of(int,times_times(int,t,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_2004,c_2233]) ).
cnf(c_2235,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,t,m),times_times(int,t,plus_plus(int,m,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2234]) ).
cnf(c_2236,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),times_times(int,t,plus_plus(int,m,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_900,c_2235]) ).
cnf(c_2237,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,t,m),times_times(int,t,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2236]) ).
cnf(c_2238,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,t,plus_plus(int,m,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_900,c_2237]) ).
cnf(c_2239,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,t,m),times_times(int,t,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_962,c_2238]) ).
cnf(c_2240,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,t,m)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_900,c_2239]) ).
cnf(c_2020,plain,
plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,m,t)))))) = minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),
inference(paramod,[status(thm)],[c_900,c_2240]) ).
cnf(c_2241,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,times_times(int,m,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)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2010,c_1763]) ).
cnf(c_2242,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,times_times(int,m,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)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2010,c_2241]) ).
cnf(c_2243,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2010,c_2242]) ).
cnf(c_2244,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2243]) ).
cnf(c_2245,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,number_number_of(int,m),times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_956,c_2244]) ).
cnf(c_2246,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,times_times(int,m,plus_plus(int,one_one(int),plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1584,c_2245]) ).
cnf(c_2247,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2246]) ).
cnf(c_2248,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,number_number_of(int,m),times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_956,c_2247]) ).
cnf(c_2249,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,times_times(int,m,plus_plus(int,one_one(int),one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1584,c_2248]) ).
cnf(c_2250,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,times_times(int,m,one_one(int)),times_times(int,m,one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2249]) ).
cnf(c_2251,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,number_number_of(int,m),times_times(int,m,one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_956,c_2250]) ).
cnf(c_2252,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,times_times(int,m,one_one(int)))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1584,c_2251]) ).
cnf(c_2253,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,number_number_of(int,m))))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_956,c_2252]) ).
cnf(c_2254,plain,
ord_less(int,plus_plus(int,t,times_times(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_1584,c_2253]) ).
cnf(c_2255,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,times_times(int,t,number_number_of(int,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2004,c_2254]) ).
cnf(c_2256,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,times_times(int,t,number_number_of(int,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2004,c_2255]) ).
cnf(c_2257,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,times_times(int,t,plus_plus(int,m,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2004,c_2256]) ).
cnf(c_2258,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,t,m),times_times(int,t,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2257]) ).
cnf(c_2259,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),times_times(int,t,plus_plus(int,m,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_900,c_2258]) ).
cnf(c_2260,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,t,m),times_times(int,t,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2259]) ).
cnf(c_2261,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,t,plus_plus(int,m,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_900,c_2260]) ).
cnf(c_2262,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,t,m),times_times(int,t,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_962,c_2261]) ).
cnf(c_2263,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,t,m)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_900,c_2262]) ).
cnf(c_2026,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,m,t)))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_900,c_2263]) ).
cnf(c_2264,plain,
( number_number_of(int,number_number_of(int,A)) = number_number_of(int,A)
| ~ ord_less_eq(int,A,number_number_of(int,A)) ),
inference(resolve,[status(thm)],[c_911,c_1901]) ).
cnf(c_2107,plain,
number_number_of(int,number_number_of(int,A)) = number_number_of(int,A),
inference(resolve,[status(thm)],[c_1900,c_2264]) ).
cnf(c_2265,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,m,t))))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2107,c_2026]) ).
cnf(c_2266,plain,
ord_less(int,plus_plus(int,t,number_number_of(int,plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),plus_plus(int,times_times(int,m,t),times_times(int,m,t)))))),zero_zero(int)),
inference(paramod,[status(thm)],[c_2107,c_2265]) ).
cnf(c_2267,plain,
ord_less(int,minus_minus(int,power_power(int,s,number_number_of(nat,plus_plus(int,one_one(int),one_one(int)))),min),zero_zero(int)),
inference(paramod,[status(thm)],[c_2020,c_2266]) ).
cnf(c_2118,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1764,c_2267]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 04:18:18 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 2124704 was started by sandbox on n014,
% 0.13/0.36 % Sat Sep 26 04:18:18 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.22/0.47
% 0.22/0.47 % From the command line: assign(max_seconds, 300).
% 0.22/0.47
% 0.22/0.47 % SInE: 421 to sos, 228 to usable, of 649 axioms (tolerance 2.00, depth 0 fixpoint).
% 1.57/0.75
% 1.57/0.75 % SZS status Theorem for theBenchmark
% 1.57/0.75
% 1.57/0.75 % Proof 1 at 0.19 (+ 0.04) seconds.
% 1.57/0.75 % Length of proof is 81.
% 1.57/0.75 % Level of proof is 8.
% 1.57/0.75 % Maximum clause weight is 185.000.
% 1.57/0.75 % Given clauses 68.
% 1.57/0.75
% 1.57/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------