%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+7 : 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 : n017.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 5.69s 2.45s
% Output : CNFRefutation 5.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 21
% Syntax : Number of formulae : 207 ( 207 unt; 0 def)
% Number of atoms : 207 ( 132 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 23 ( 23 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-4 aty)
% Number of variables : 64 ( 4 sgn 21 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(tsy_c_Int_OBit0_arg1,axiom,
! [B_1_1] : bit0(ti(int,B_1_1)) = bit0(B_1_1),
file('theBenchmark.p',tsy_c_Int_OBit0_arg1) ).
fof(tsy_c_hAPP_arg2,axiom,
! [X_a,X_c,B_1_1,B_2_1] : hAPP(X_a,X_c,B_1_1,ti(X_a,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
file('theBenchmark.p',tsy_c_hAPP_arg2) ).
fof(fact_18__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,axiom,
~ ! [T_4] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) != hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),T_4),
file('theBenchmark.p',fact_18__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_) ).
fof(fact_22_number__of__is__id,axiom,
! [K_1] : number_number_of(int,K_1) = ti(int,K_1),
file('theBenchmark.p',fact_22_number__of__is__id) ).
fof(fact_23_zmult__commute,axiom,
! [Z_1,W] : hAPP(int,int,times_times(int,Z_1),W) = hAPP(int,int,times_times(int,W),Z_1),
file('theBenchmark.p',fact_23_zmult__commute) ).
fof(fact_25_times__numeral__code_I5_J,axiom,
! [V,W] : hAPP(int,int,times_times(int,number_number_of(int,V)),number_number_of(int,W)) = number_number_of(int,hAPP(int,int,times_times(int,V),W)),
file('theBenchmark.p',fact_25_times__numeral__code_I5_J) ).
fof(fact_62_mult__Pls,axiom,
! [W] : hAPP(int,int,times_times(int,pls),W) = pls,
file('theBenchmark.p',fact_62_mult__Pls) ).
fof(fact_67_plus__numeral__code_I9_J,axiom,
! [V,W] : hAPP(int,int,plus_plus(int,number_number_of(int,V)),number_number_of(int,W)) = number_number_of(int,hAPP(int,int,plus_plus(int,V),W)),
file('theBenchmark.p',fact_67_plus__numeral__code_I9_J) ).
fof(fact_96_zadd__assoc,axiom,
! [Z1,Z2,Z3] : hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,Z1),Z2)),Z3) = hAPP(int,int,plus_plus(int,Z1),hAPP(int,int,plus_plus(int,Z2),Z3)),
file('theBenchmark.p',fact_96_zadd__assoc) ).
fof(fact_129_add__Pls__right,axiom,
! [K_1] : hAPP(int,int,plus_plus(int,K_1),pls) = ti(int,K_1),
file('theBenchmark.p',fact_129_add__Pls__right) ).
fof(fact_130_add__Pls,axiom,
! [K_1] : hAPP(int,int,plus_plus(int,pls),K_1) = ti(int,K_1),
file('theBenchmark.p',fact_130_add__Pls) ).
fof(fact_132_Bit0__def,axiom,
! [K_1] : bit0(K_1) = hAPP(int,int,plus_plus(int,K_1),K_1),
file('theBenchmark.p',fact_132_Bit0__def) ).
fof(fact_164_Bit1__def,axiom,
! [K_1] : bit1(K_1) = hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),K_1)),K_1),
file('theBenchmark.p',fact_164_Bit1__def) ).
fof(conj_0,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,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,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,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_1770,plain,
bit0(ti(int,A)) = bit0(A),
inference(clausify,[status(thm)],[tsy_c_Int_OBit0_arg1]) ).
fof(tsy_c_Int_OMin_res,axiom,
ti(int,min) = min,
file('theBenchmark.p',tsy_c_Int_OMin_res) ).
cnf(c_1776,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_1777,plain,
ti(int,pls) = pls,
inference(clausify,[status(thm)],[tsy_c_Int_OPls_res]) ).
cnf(c_1784,plain,
hAPP(A,B,C,ti(A,D)) = hAPP(A,B,C,D),
inference(clausify,[status(thm)],[tsy_c_hAPP_arg2]) ).
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,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,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_1795,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,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,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,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_1796,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(clausify,[status(thm)],[fact_3_t]) ).
fof(nnf_25,plain,
? [T_4] : hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),T_4) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(fof_nnf,[status(thm)],[fact_18__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_]) ).
fof(sk_fact_18__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(T_4,sK0)],[nnf_25]) ).
cnf(c_1822,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(split_conjunct,[status(thm)],[sk_fact_18__096_B_Bthesis_O_A_I_B_Bt_O_As_A_094_A2_A_L_A1_A_061_A_I4_A_K_Am_A_L_A1_]) ).
cnf(c_3629,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1796,c_1822]) ).
cnf(c_1823,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(copy,[status(thm)],[c_3629]) ).
cnf(c_1828,plain,
number_number_of(int,A) = ti(int,A),
inference(clausify,[status(thm)],[fact_22_number__of__is__id]) ).
cnf(c_1829,plain,
ti(int,A) = number_number_of(int,A),
inference(copy,[status(thm)],[c_1828]) ).
cnf(c_1830,plain,
hAPP(int,int,times_times(int,A),B) = hAPP(int,int,times_times(int,B),A),
inference(clausify,[status(thm)],[fact_23_zmult__commute]) ).
cnf(c_1832,plain,
hAPP(int,int,times_times(int,number_number_of(int,A)),number_number_of(int,B)) = number_number_of(int,hAPP(int,int,times_times(int,A),B)),
inference(clausify,[status(thm)],[fact_25_times__numeral__code_I5_J]) ).
cnf(c_1879,plain,
hAPP(int,int,times_times(int,pls),A) = pls,
inference(clausify,[status(thm)],[fact_62_mult__Pls]) ).
cnf(c_1887,plain,
hAPP(int,int,plus_plus(int,number_number_of(int,A)),number_number_of(int,B)) = number_number_of(int,hAPP(int,int,plus_plus(int,A),B)),
inference(clausify,[status(thm)],[fact_67_plus__numeral__code_I9_J]) ).
cnf(c_1924,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,A),B)),C) = hAPP(int,int,plus_plus(int,A),hAPP(int,int,plus_plus(int,B),C)),
inference(clausify,[status(thm)],[fact_96_zadd__assoc]) ).
fof(fact_111_one__is__num__one,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('theBenchmark.p',fact_111_one__is__num__one) ).
cnf(c_1940,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(clausify,[status(thm)],[fact_111_one__is__num__one]) ).
cnf(c_1941,plain,
number_number_of(int,bit1(pls)) = one_one(int),
inference(copy,[status(thm)],[c_1940]) ).
fof(fact_122_Pls__def,axiom,
pls = zero_zero(int),
file('theBenchmark.p',fact_122_Pls__def) ).
cnf(c_1959,plain,
pls = zero_zero(int),
inference(clausify,[status(thm)],[fact_122_Pls__def]) ).
cnf(c_1967,plain,
hAPP(int,int,plus_plus(int,A),pls) = ti(int,A),
inference(clausify,[status(thm)],[fact_129_add__Pls__right]) ).
cnf(c_3630,plain,
hAPP(int,int,plus_plus(int,A),zero_zero(int)) = ti(int,A),
inference(paramod,[status(thm)],[c_1959,c_1967]) ).
cnf(c_1968,plain,
hAPP(int,int,plus_plus(int,A),zero_zero(int)) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_1829,c_3630]) ).
cnf(c_1969,plain,
hAPP(int,int,plus_plus(int,pls),A) = ti(int,A),
inference(clausify,[status(thm)],[fact_130_add__Pls]) ).
cnf(c_3631,plain,
hAPP(int,int,plus_plus(int,zero_zero(int)),A) = ti(int,A),
inference(paramod,[status(thm)],[c_1959,c_1969]) ).
cnf(c_1970,plain,
hAPP(int,int,plus_plus(int,zero_zero(int)),A) = number_number_of(int,A),
inference(paramod,[status(thm)],[c_1829,c_3631]) ).
cnf(c_1972,plain,
hAPP(int,int,plus_plus(int,A),A) = bit0(A),
inference(clausify,[status(thm)],[fact_132_Bit0__def]) ).
cnf(c_1973,plain,
bit0(A) = hAPP(int,int,plus_plus(int,A),A),
inference(copy,[status(thm)],[c_1972]) ).
cnf(c_2022,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),A)),A) = bit1(A),
inference(clausify,[status(thm)],[fact_164_Bit1__def]) ).
cnf(c_3632,plain,
hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,A),A)) = bit1(A),
inference(paramod,[status(thm)],[c_1924,c_2022]) ).
cnf(c_2023,plain,
bit1(A) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,A),A)),
inference(copy,[status(thm)],[c_3632]) ).
fof(fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096,axiom,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
file('theBenchmark.p',fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
cnf(c_2361,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(clausify,[status(thm)],[fact_466__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096]) ).
cnf(c_3633,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(zero_zero(int)))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_1959,c_2361]) ).
cnf(c_3634,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_2023,c_3633]) ).
cnf(c_3635,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_1968,c_3634]) ).
cnf(c_3636,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_1973,c_3635]) ).
cnf(c_3637,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_1924,c_3636]) ).
cnf(c_3638,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(zero_zero(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_1959,c_3637]) ).
cnf(c_3639,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),one_one(int)),
inference(paramod,[status(thm)],[c_2023,c_3638]) ).
cnf(c_3640,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int)),
inference(paramod,[status(thm)],[c_1968,c_3639]) ).
cnf(c_3641,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int)),
inference(paramod,[status(thm)],[c_1973,c_3640]) ).
cnf(c_3642,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),one_one(int)),
inference(paramod,[status(thm)],[c_1924,c_3641]) ).
cnf(c_2362,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),one_one(int)) = hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)),
inference(copy,[status(thm)],[c_3642]) ).
cnf(c_2929,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,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_3643,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,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_1959,c_2929]) ).
cnf(c_3644,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_2023,c_3643]) ).
cnf(c_3645,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1968,c_3644]) ).
cnf(c_3646,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1973,c_3645]) ).
cnf(c_3647,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1924,c_3646]) ).
cnf(c_2930,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_2362,c_3647]) ).
cnf(c_3648,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(zero_zero(int)))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1959,c_1796]) ).
cnf(c_3649,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2023,c_3648]) ).
cnf(c_3650,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1968,c_3649]) ).
cnf(c_3651,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1973,c_3650]) ).
cnf(c_3652,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1924,c_3651]) ).
cnf(c_3653,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2362,c_3652]) ).
cnf(c_3654,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int)))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1959,c_3653]) ).
cnf(c_3655,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2023,c_3654]) ).
cnf(c_3656,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1968,c_3655]) ).
cnf(c_3657,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1973,c_3656]) ).
cnf(c_3658,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1924,c_3657]) ).
cnf(c_3659,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1973,c_3658]) ).
cnf(c_3660,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1924,c_3659]) ).
cnf(c_3661,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1924,c_3660]) ).
cnf(c_2934,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1924,c_3661]) ).
cnf(c_3662,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int)))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1959,c_1795]) ).
cnf(c_3663,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2023,c_3662]) ).
cnf(c_3664,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1968,c_3663]) ).
cnf(c_3665,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1973,c_3664]) ).
cnf(c_3666,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3665]) ).
cnf(c_3667,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1973,c_3666]) ).
cnf(c_3668,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3667]) ).
cnf(c_3669,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3668]) ).
cnf(c_3670,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3669]) ).
cnf(c_3671,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,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_1959,c_3670]) ).
cnf(c_3672,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2023,c_3671]) ).
cnf(c_3673,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1968,c_3672]) ).
cnf(c_3674,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1973,c_3673]) ).
cnf(c_3675,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3674]) ).
cnf(c_3676,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1973,c_3675]) ).
cnf(c_3677,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3676]) ).
cnf(c_3678,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3677]) ).
cnf(c_2935,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1924,c_3678]) ).
cnf(c_3679,plain,
ti(int,zero_zero(int)) = pls,
inference(paramod,[status(thm)],[c_1959,c_1777]) ).
cnf(c_3680,plain,
number_number_of(int,zero_zero(int)) = pls,
inference(paramod,[status(thm)],[c_1829,c_3679]) ).
cnf(c_2943,plain,
number_number_of(int,zero_zero(int)) = zero_zero(int),
inference(paramod,[status(thm)],[c_1959,c_3680]) ).
cnf(c_2944,plain,
number_number_of(int,min) = min,
inference(paramod,[status(thm)],[c_1829,c_1776]) ).
cnf(c_3681,plain,
bit0(number_number_of(int,A)) = bit0(A),
inference(paramod,[status(thm)],[c_1829,c_1770]) ).
cnf(c_3682,plain,
hAPP(int,int,plus_plus(int,number_number_of(int,A)),number_number_of(int,A)) = bit0(A),
inference(paramod,[status(thm)],[c_1973,c_3681]) ).
cnf(c_3683,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,A),A)) = bit0(A),
inference(paramod,[status(thm)],[c_1887,c_3682]) ).
cnf(c_2946,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,A),A)) = hAPP(int,int,plus_plus(int,A),A),
inference(paramod,[status(thm)],[c_1973,c_3683]) ).
cnf(c_3684,plain,
number_number_of(int,bit1(zero_zero(int))) = one_one(int),
inference(paramod,[status(thm)],[c_1959,c_1941]) ).
cnf(c_3685,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int)))) = one_one(int),
inference(paramod,[status(thm)],[c_2023,c_3684]) ).
cnf(c_3686,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))) = one_one(int),
inference(paramod,[status(thm)],[c_1968,c_3685]) ).
cnf(c_3687,plain,
number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int))) = one_one(int),
inference(paramod,[status(thm)],[c_2943,c_3686]) ).
cnf(c_2987,plain,
number_number_of(int,number_number_of(int,one_one(int))) = one_one(int),
inference(paramod,[status(thm)],[c_1968,c_3687]) ).
cnf(c_3688,plain,
hAPP(int,int,times_times(int,zero_zero(int)),A) = pls,
inference(paramod,[status(thm)],[c_1959,c_1879]) ).
cnf(c_3005,plain,
hAPP(int,int,times_times(int,zero_zero(int)),A) = zero_zero(int),
inference(paramod,[status(thm)],[c_1959,c_3688]) ).
cnf(c_3689,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1959,c_1823]) ).
cnf(c_3690,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2023,c_3689]) ).
cnf(c_3691,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1968,c_3690]) ).
cnf(c_3692,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2943,c_3691]) ).
cnf(c_3693,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(number_number_of(int,one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1968,c_3692]) ).
cnf(c_3694,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,number_number_of(int,one_one(int))),number_number_of(int,one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1973,c_3693]) ).
cnf(c_3695,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1887,c_3694]) ).
cnf(c_3696,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2946,c_3695]) ).
cnf(c_3697,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1973,c_3696]) ).
cnf(c_3698,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1924,c_3697]) ).
cnf(c_3699,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(zero_zero(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1959,c_3698]) ).
cnf(c_3700,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),zero_zero(int))))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2023,c_3699]) ).
cnf(c_3701,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1968,c_3700]) ).
cnf(c_3702,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2943,c_3701]) ).
cnf(c_3703,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(number_number_of(int,one_one(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1968,c_3702]) ).
cnf(c_3704,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,number_number_of(int,one_one(int))),number_number_of(int,one_one(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1973,c_3703]) ).
cnf(c_3705,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1887,c_3704]) ).
cnf(c_3706,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_2946,c_3705]) ).
cnf(c_3707,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1973,c_3706]) ).
cnf(c_3028,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),sK0),
inference(paramod,[status(thm)],[c_1924,c_3707]) ).
cnf(c_3708,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_2943,c_2930]) ).
cnf(c_3709,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int))))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_2943,c_3708]) ).
cnf(c_3710,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),number_number_of(int,one_one(int))))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1968,c_3709]) ).
cnf(c_3711,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,number_number_of(int,one_one(int))))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_1970,c_3710]) ).
cnf(c_3712,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),number_number_of(int,min))),zero_zero(int))),
inference(paramod,[status(thm)],[c_2987,c_3711]) ).
cnf(c_3182,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min)),zero_zero(int))),
inference(paramod,[status(thm)],[c_2944,c_3712]) ).
cnf(c_3713,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_2935]) ).
cnf(c_3714,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3713]) ).
cnf(c_3715,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3714]) ).
cnf(c_3716,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int)))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3715]) ).
cnf(c_3717,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),number_number_of(int,one_one(int)))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1968,c_3716]) ).
cnf(c_3718,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,number_number_of(int,one_one(int)))))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1970,c_3717]) ).
cnf(c_3719,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2987,c_3718]) ).
cnf(c_3720,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1970,c_3719]) ).
cnf(c_3721,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2946,c_3720]) ).
cnf(c_3722,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1970,c_3721]) ).
cnf(c_3723,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3722]) ).
cnf(c_3724,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3723]) ).
cnf(c_3725,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3724]) ).
cnf(c_3726,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int)))))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2943,c_3725]) ).
cnf(c_3727,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,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_1968,c_3726]) ).
cnf(c_3728,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(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_1970,c_3727]) ).
cnf(c_3729,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2987,c_3728]) ).
cnf(c_3730,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1970,c_3729]) ).
cnf(c_3731,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_2946,c_3730]) ).
cnf(c_3185,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_1970,c_3731]) ).
cnf(c_3732,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int)))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_2934]) ).
cnf(c_3733,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_3732]) ).
cnf(c_3734,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),number_number_of(int,one_one(int))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1968,c_3733]) ).
cnf(c_3735,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,number_number_of(int,one_one(int))))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1970,c_3734]) ).
cnf(c_3736,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),number_number_of(int,min)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2987,c_3735]) ).
cnf(c_3737,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2944,c_3736]) ).
cnf(c_3738,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_3737]) ).
cnf(c_3739,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,number_number_of(int,zero_zero(int))),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_3738]) ).
cnf(c_3740,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,zero_zero(int))))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_3739]) ).
cnf(c_3741,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),zero_zero(int)))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2943,c_3740]) ).
cnf(c_3742,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),number_number_of(int,one_one(int)))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1968,c_3741]) ).
cnf(c_3743,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,number_number_of(int,one_one(int)))))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1970,c_3742]) ).
cnf(c_3744,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2987,c_3743]) ).
cnf(c_3745,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1970,c_3744]) ).
cnf(c_3746,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_2946,c_3745]) ).
cnf(c_3186,plain,
hAPP(int,int,minus_minus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),min) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t),
inference(paramod,[status(thm)],[c_1970,c_3746]) ).
cnf(c_3267,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),t)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3186,c_3182]) ).
cnf(c_3370,plain,
hAPP(int,A,B,number_number_of(int,C)) = hAPP(int,A,B,C),
inference(paramod,[status(thm)],[c_1829,c_1784]) ).
cnf(c_3747,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3370,c_3267]) ).
cnf(c_3391,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),sK0)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3028,c_3747]) ).
cnf(c_3748,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3370,c_3185]) ).
cnf(c_3749,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3028,c_3748]) ).
cnf(c_3416,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3370,c_3749]) ).
cnf(c_3428,plain,
hAPP(int,int,plus_plus(int,number_number_of(int,A)),B) = number_number_of(int,hAPP(int,int,plus_plus(int,A),B)),
inference(paramod,[status(thm)],[c_3370,c_1887]) ).
cnf(c_3429,plain,
hAPP(int,int,times_times(int,number_number_of(int,A)),B) = number_number_of(int,hAPP(int,int,times_times(int,A),B)),
inference(paramod,[status(thm)],[c_3370,c_1832]) ).
cnf(c_3750,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m))),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3429,c_3416]) ).
cnf(c_3751,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int)))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3428,c_3750]) ).
cnf(c_3752,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0))),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3429,c_3751]) ).
cnf(c_3753,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3370,c_3752]) ).
cnf(c_3754,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3429,c_3753]) ).
cnf(c_3755,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int)))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3428,c_3754]) ).
cnf(c_3756,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),zero_zero(int))))),
inference(paramod,[status(thm)],[c_3429,c_3755]) ).
cnf(c_3432,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_3370,c_3756]) ).
cnf(c_3757,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m))),one_one(int))),sK0)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3429,c_3391]) ).
cnf(c_3758,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int)))),sK0)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3428,c_3757]) ).
cnf(c_3759,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),number_number_of(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0))),zero_zero(int))),
inference(paramod,[status(thm)],[c_3429,c_3758]) ).
cnf(c_3448,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3370,c_3759]) ).
cnf(c_3624,plain,
hAPP(int,int,times_times(int,A),zero_zero(int)) = zero_zero(int),
inference(paramod,[status(thm)],[c_1830,c_3005]) ).
cnf(c_3760,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),sK0)),zero_zero(int))),
inference(paramod,[status(thm)],[c_3624,c_3432]) ).
cnf(c_3628,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3448,c_3760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.54 % Computer : n017.cluster.edu
% 0.09/0.54 % Model : x86_64 x86_64
% 0.09/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.54 % Memory : 8046.5625MB
% 0.09/0.54 % OS : Linux 6.8.0-71-generic
% 0.09/0.54 % CPULimit : 300
% 0.09/0.54 % WCLimit : 300
% 0.09/0.54 % DateTime : Sat Sep 26 04:13:49 UTC 2026
% 0.09/0.54 % CPUTime :
% 0.09/0.55 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.55 % Process 3980800 was started by sandbox on n017,
% 0.09/0.55 % Sat Sep 26 04:13:49 2026
% 0.09/0.55 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.82
% 0.12/0.82 % From the command line: assign(max_seconds, 300).
% 0.12/0.82
% 0.12/0.82 % SInE: 707 to sos, 547 to usable, of 1254 axioms (tolerance 2.00, depth 0 fixpoint).
% 5.69/2.45
% 5.69/2.45 % SZS status Theorem for theBenchmark
% 5.69/2.45
% 5.69/2.45 % Proof 1 at 0.67 (+ 0.10) seconds.
% 5.69/2.45 % Length of proof is 65.
% 5.69/2.45 % Level of proof is 10.
% 5.69/2.45 % Maximum clause weight is 172.000.
% 5.69/2.45 % Given clauses 144.
% 5.69/2.45
% 5.69/2.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------