%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+8 : 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 : n008.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 28.35s 4.78s
% Output : CNFRefutation 28.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 27
% Syntax : Number of formulae : 191 ( 174 unt; 0 def)
% Number of atoms : 214 ( 159 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 53 ( 30 ~; 18 |; 3 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 14 con; 0-4 aty)
% Number of variables : 86 ( 6 sgn 30 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(tsy_c_hAPP_res,axiom,
! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
file('theBenchmark.p',tsy_c_hAPP_res) ).
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,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) != hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,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_4] : hAPP(int,int,number_number_of(int),K_4) = ti(int,K_4),
file('theBenchmark.p',fact_22_number__of__is__id) ).
fof(fact_62_mult__Pls,axiom,
! [W] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),W) = pls,
file('theBenchmark.p',fact_62_mult__Pls) ).
fof(fact_63_mult__Bit0,axiom,
! [K_4,L_4] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,K_4)),L_4) = hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),K_4),L_4)),
file('theBenchmark.p',fact_63_mult__Bit0) ).
fof(fact_66_zmult__1,axiom,
! [Z_1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),Z_1) = ti(int,Z_1),
file('theBenchmark.p',fact_66_zmult__1) ).
fof(fact_120_rel__simps_I44_J,axiom,
! [K] :
( hAPP(int,int,bit0,K) = pls
<=> ti(int,K) = pls ),
file('theBenchmark.p',fact_120_rel__simps_I44_J) ).
fof(fact_134_zadd__0__right,axiom,
! [Z_1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),Z_1),zero_zero(int)) = ti(int,Z_1),
file('theBenchmark.p',fact_134_zadd__0__right) ).
fof(fact_2143_zminus__zminus,axiom,
! [Z_1] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),Z_1)) = ti(int,Z_1),
file('theBenchmark.p',fact_2143_zminus__zminus) ).
fof(fact_23_zmult__commute,axiom,
! [Z_1,W] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),Z_1),W) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),W),Z_1),
file('theBenchmark.p',fact_23_zmult__commute) ).
fof(fact_163_add__Bit0__Bit1,axiom,
! [K_4,L_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,K_4)),hAPP(int,int,bit1,L_4)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),K_4),L_4)),
file('theBenchmark.p',fact_163_add__Bit0__Bit1) ).
fof(fact_1113_nat__number__of,axiom,
! [W] : hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),W)) = hAPP(int,nat,number_number_of(nat),W),
file('theBenchmark.p',fact_1113_nat__number__of) ).
fof(fact_1447_even__equiv__def,axiom,
! [X_1] :
( hBOOL(hAPP(int,bool,even_odd_even(int),X_1))
<=> ? [Y_2] : ti(int,X_1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),Y_2) ),
file('theBenchmark.p',fact_1447_even__equiv__def) ).
fof(conj_0,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,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,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_2018,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),B),A),
inference(clausify,[status(thm)],[fact_23_zmult__commute]) ).
fof(fact_112_one__is__num__one,axiom,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
file('theBenchmark.p',fact_112_one__is__num__one) ).
cnf(c_2066,plain,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
inference(clausify,[status(thm)],[fact_112_one__is__num__one]) ).
cnf(c_2067,plain,
hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)) = one_one(int),
inference(copy,[status(thm)],[c_2066]) ).
cnf(c_2099,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,A)),hAPP(int,int,bit1,B)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),B)),
inference(clausify,[status(thm)],[fact_163_add__Bit0__Bit1]) ).
fof(fact_736__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096,axiom,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
file('theBenchmark.p',fact_736__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096) ).
cnf(c_2315,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
inference(clausify,[status(thm)],[fact_736__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096]) ).
cnf(c_2316,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(copy,[status(thm)],[c_2315]) ).
cnf(c_2707,plain,
hAPP(int,nat,number_number_of(nat),A) = hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),A)),
inference(clausify,[status(thm)],[fact_1113_nat__number__of]) ).
cnf(c_2708,plain,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),A)) = hAPP(int,nat,number_number_of(nat),A),
inference(copy,[status(thm)],[c_2707]) ).
fof(fact_1255_even__zero__int,axiom,
hBOOL(hAPP(int,bool,even_odd_even(int),zero_zero(int))),
file('theBenchmark.p',fact_1255_even__zero__int) ).
cnf(c_2816,plain,
hBOOL(hAPP(int,bool,even_odd_even(int),zero_zero(int))),
inference(clausify,[status(thm)],[fact_1255_even__zero__int]) ).
fof(nnf_1040,plain,
! [X_1] :
( ( ! [Y_2] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),Y_2) != ti(int,X_1)
| hBOOL(hAPP(int,bool,even_odd_even(int),X_1)) )
& ( ? [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0) = ti(int,X_1)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),X_1)) ) ),
inference(fof_nnf,[status(thm)],[fact_1447_even__equiv__def]) ).
fof(sk_fact_1447_even__equiv__def_sk,plain,
! [X_1] :
( ( ! [Y_2] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),Y_2) != ti(int,X_1)
| hBOOL(hAPP(int,bool,even_odd_even(int),X_1)) )
& ( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),sK0(X_1)) = ti(int,X_1)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),X_1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(X_1))],[nnf_1040]) ).
fof(sk_fact_1447_even__equiv__def,plain,
( ! [VAR_0,VAR_1] :
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),VAR_1) != ti(int,VAR_0)
| hBOOL(hAPP(int,bool,even_odd_even(int),VAR_0)) )
& ! [VAR_0] :
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),sK0(VAR_0)) = ti(int,VAR_0)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),VAR_0)) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_1447_even__equiv__def_sk]) ).
cnf(c_3002,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(split_conjunct,[status(thm)],[sk_fact_1447_even__equiv__def]) ).
fof(fact_1452_nat__2,axiom,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
file('theBenchmark.p',fact_1452_nat__2) ).
cnf(c_3011,plain,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(clausify,[status(thm)],[fact_1452_nat__2]) ).
fof(tsy_c_Int_OPls_res,axiom,
ti(int,pls) = pls,
file('theBenchmark.p',tsy_c_Int_OPls_res) ).
cnf(c_4903,plain,
ti(int,pls) = pls,
inference(clausify,[status(thm)],[tsy_c_Int_OPls_res]) ).
cnf(c_4909,plain,
hAPP(A,B,C,ti(A,D)) = hAPP(A,B,C,D),
inference(clausify,[status(thm)],[tsy_c_hAPP_arg2]) ).
cnf(c_4910,plain,
hAPP(A,B,C,D) = ti(B,hAPP(A,B,C,D)),
inference(clausify,[status(thm)],[tsy_c_hAPP_res]) ).
cnf(c_4911,plain,
ti(A,hAPP(B,A,C,D)) = hAPP(B,A,C,D),
inference(copy,[status(thm)],[c_4910]) ).
fof(tsy_v_m_res,axiom,
ti(int,m) = m,
file('theBenchmark.p',tsy_v_m_res) ).
cnf(c_4914,plain,
ti(int,m) = m,
inference(clausify,[status(thm)],[tsy_v_m_res]) ).
fof(fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,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_4920,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,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,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
file('theBenchmark.p',fact_3_t) ).
cnf(c_4921,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
inference(clausify,[status(thm)],[fact_3_t]) ).
cnf(c_4922,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(copy,[status(thm)],[c_4921]) ).
fof(nnf_6,plain,
? [T_4] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),T_4),
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,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(T_4,sK1)],[nnf_6]) ).
cnf(c_4928,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),sK1),
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_4929,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(copy,[status(thm)],[c_4928]) ).
cnf(c_4931,plain,
hAPP(int,int,number_number_of(int),A) = ti(int,A),
inference(clausify,[status(thm)],[fact_22_number__of__is__id]) ).
cnf(c_4961,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),A) = pls,
inference(clausify,[status(thm)],[fact_62_mult__Pls]) ).
cnf(c_4962,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,A)),B) = hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),B)),
inference(clausify,[status(thm)],[fact_63_mult__Bit0]) ).
cnf(c_4964,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),A) = ti(int,A),
inference(clausify,[status(thm)],[fact_66_zmult__1]) ).
fof(fact_100_zero__is__num__zero,axiom,
zero_zero(int) = hAPP(int,int,number_number_of(int),pls),
file('theBenchmark.p',fact_100_zero__is__num__zero) ).
cnf(c_4993,plain,
zero_zero(int) = hAPP(int,int,number_number_of(int),pls),
inference(clausify,[status(thm)],[fact_100_zero__is__num__zero]) ).
cnf(c_7835,plain,
zero_zero(int) = ti(int,pls),
inference(paramod,[status(thm)],[c_4931,c_4993]) ).
cnf(c_7836,plain,
zero_zero(int) = pls,
inference(paramod,[status(thm)],[c_4903,c_7835]) ).
cnf(c_4994,plain,
pls = zero_zero(int),
inference(copy,[status(thm)],[c_7836]) ).
cnf(c_5000,plain,
( ti(int,A) = pls
| hAPP(int,int,bit0,A) != pls ),
inference(clausify,[status(thm)],[fact_120_rel__simps_I44_J]) ).
cnf(c_7837,plain,
( ti(int,A) = pls
| hAPP(int,int,bit0,A) != zero_zero(int) ),
inference(paramod,[status(thm)],[c_4994,c_5000]) ).
cnf(c_5001,plain,
( ti(int,A) = zero_zero(int)
| hAPP(int,int,bit0,A) != zero_zero(int) ),
inference(paramod,[status(thm)],[c_4994,c_7837]) ).
cnf(c_5018,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),zero_zero(int)) = ti(int,A),
inference(clausify,[status(thm)],[fact_134_zadd__0__right]) ).
fof(fact_1330_One__nat__def,axiom,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
file('theBenchmark.p',fact_1330_One__nat__def) ).
cnf(c_5537,plain,
one_one(nat) = hAPP(nat,nat,suc,zero_zero(nat)),
inference(clausify,[status(thm)],[fact_1330_One__nat__def]) ).
cnf(c_5538,plain,
hAPP(nat,nat,suc,zero_zero(nat)) = one_one(nat),
inference(copy,[status(thm)],[c_5537]) ).
cnf(c_5713,plain,
hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),A)) = ti(int,A),
inference(clausify,[status(thm)],[fact_2143_zminus__zminus]) ).
fof(fact_2157_Int_OMin__def,axiom,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
file('theBenchmark.p',fact_2157_Int_OMin__def) ).
cnf(c_5724,plain,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
inference(clausify,[status(thm)],[fact_2157_Int_OMin__def]) ).
fof(fact_2164_minus__Min,axiom,
hAPP(int,int,uminus_uminus(int),min_1) = hAPP(int,int,bit1,pls),
file('theBenchmark.p',fact_2164_minus__Min) ).
cnf(c_5727,plain,
hAPP(int,int,uminus_uminus(int),min_1) = hAPP(int,int,bit1,pls),
inference(clausify,[status(thm)],[fact_2164_minus__Min]) ).
cnf(c_7838,plain,
hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),one_one(int))) = hAPP(int,int,bit1,pls),
inference(paramod,[status(thm)],[c_5724,c_5727]) ).
cnf(c_7839,plain,
ti(int,one_one(int)) = hAPP(int,int,bit1,pls),
inference(paramod,[status(thm)],[c_5713,c_7838]) ).
cnf(c_7840,plain,
ti(int,one_one(int)) = hAPP(int,int,bit1,zero_zero(int)),
inference(paramod,[status(thm)],[c_4994,c_7839]) ).
cnf(c_5728,plain,
hAPP(int,int,bit1,zero_zero(int)) = ti(int,one_one(int)),
inference(copy,[status(thm)],[c_7840]) ).
cnf(c_5932,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_7841,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_4994,c_5932]) ).
cnf(c_7842,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_5728,c_7841]) ).
cnf(c_5933,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_4909,c_7842]) ).
cnf(c_7843,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4994,c_4920]) ).
cnf(c_7844,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,one_one(int)))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_5728,c_7843]) ).
cnf(c_7845,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4909,c_7844]) ).
cnf(c_7846,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4931,c_7845]) ).
cnf(c_7847,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4911,c_7846]) ).
cnf(c_7848,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4962,c_7847]) ).
cnf(c_7849,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4962,c_7848]) ).
cnf(c_7850,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4964,c_7849]) ).
cnf(c_7851,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4914,c_7850]) ).
cnf(c_7852,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4994,c_7851]) ).
cnf(c_7853,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,one_one(int)))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_5728,c_7852]) ).
cnf(c_7854,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4909,c_7853]) ).
cnf(c_7855,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4931,c_7854]) ).
cnf(c_7856,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4911,c_7855]) ).
cnf(c_7857,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4962,c_7856]) ).
cnf(c_7858,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4962,c_7857]) ).
cnf(c_7859,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4964,c_7858]) ).
cnf(c_5934,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_4914,c_7859]) ).
cnf(c_7860,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4994,c_2316]) ).
cnf(c_7861,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,one_one(int)))))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_5728,c_7860]) ).
cnf(c_7862,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4909,c_7861]) ).
cnf(c_7863,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4931,c_7862]) ).
cnf(c_7864,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4911,c_7863]) ).
cnf(c_7865,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4962,c_7864]) ).
cnf(c_7866,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4962,c_7865]) ).
cnf(c_7867,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4964,c_7866]) ).
cnf(c_5935,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_4914,c_7867]) ).
cnf(c_7868,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4994,c_4929]) ).
cnf(c_7869,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,one_one(int)))))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_5728,c_7868]) ).
cnf(c_7870,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4909,c_7869]) ).
cnf(c_7871,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4931,c_7870]) ).
cnf(c_7872,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4911,c_7871]) ).
cnf(c_7873,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4962,c_7872]) ).
cnf(c_7874,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4962,c_7873]) ).
cnf(c_7875,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4964,c_7874]) ).
cnf(c_7876,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4914,c_7875]) ).
cnf(c_7877,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_4994,c_7876]) ).
cnf(c_7878,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_5728,c_7877]) ).
cnf(c_7879,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),one_one(int)),
inference(paramod,[status(thm)],[c_4909,c_7878]) ).
cnf(c_5938,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1),
inference(copy,[status(thm)],[c_7879]) ).
cnf(c_7880,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4994,c_4922]) ).
cnf(c_7881,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_5728,c_7880]) ).
cnf(c_7882,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4909,c_7881]) ).
cnf(c_7883,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4931,c_7882]) ).
cnf(c_7884,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit0,one_one(int)))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4911,c_7883]) ).
cnf(c_7885,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),m))),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4962,c_7884]) ).
cnf(c_7886,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),m)))),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4962,c_7885]) ).
cnf(c_7887,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,ti(int,m)))),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4964,c_7886]) ).
cnf(c_7888,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_4914,c_7887]) ).
cnf(c_7889,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(paramod,[status(thm)],[c_5935,c_7888]) ).
cnf(c_7890,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_4994,c_7889]) ).
cnf(c_7891,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,ti(int,one_one(int)))))),one_one(int)),
inference(paramod,[status(thm)],[c_5728,c_7890]) ).
cnf(c_7892,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,one_one(int))))),one_one(int)),
inference(paramod,[status(thm)],[c_4909,c_7891]) ).
cnf(c_7893,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1),
inference(paramod,[status(thm)],[c_5938,c_7892]) ).
cnf(c_5941,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(copy,[status(thm)],[c_7893]) ).
cnf(c_7894,plain,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int))))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(paramod,[status(thm)],[c_4994,c_3011]) ).
cnf(c_7895,plain,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,ti(int,one_one(int))))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(paramod,[status(thm)],[c_5728,c_7894]) ).
cnf(c_7896,plain,
hAPP(int,nat,nat_1,hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,one_one(int)))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(paramod,[status(thm)],[c_4909,c_7895]) ).
cnf(c_7897,plain,
hAPP(int,nat,nat_1,ti(int,hAPP(int,int,bit0,one_one(int)))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(paramod,[status(thm)],[c_4931,c_7896]) ).
cnf(c_7898,plain,
hAPP(int,nat,nat_1,hAPP(int,int,bit0,one_one(int))) = hAPP(nat,nat,suc,hAPP(nat,nat,suc,zero_zero(nat))),
inference(paramod,[status(thm)],[c_4911,c_7897]) ).
cnf(c_5960,plain,
hAPP(int,nat,nat_1,hAPP(int,int,bit0,one_one(int))) = hAPP(nat,nat,suc,one_one(nat)),
inference(paramod,[status(thm)],[c_5538,c_7898]) ).
cnf(c_7899,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,zero_zero(int))))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4994,c_3002]) ).
cnf(c_7900,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,ti(int,one_one(int))))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_5728,c_7899]) ).
cnf(c_7901,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,one_one(int)))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4909,c_7900]) ).
cnf(c_7902,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,one_one(int)))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4931,c_7901]) ).
cnf(c_7903,plain,
( hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,one_one(int))),sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4911,c_7902]) ).
cnf(c_7904,plain,
( hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),sK0(A))) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4962,c_7903]) ).
cnf(c_7905,plain,
( hAPP(int,int,bit0,ti(int,sK0(A))) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4964,c_7904]) ).
cnf(c_5964,plain,
( hAPP(int,int,bit0,sK0(A)) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,even_odd_even(int),A)) ),
inference(paramod,[status(thm)],[c_4909,c_7905]) ).
cnf(c_7906,plain,
hAPP(int,nat,nat_1,ti(int,A)) = hAPP(int,nat,number_number_of(nat),A),
inference(paramod,[status(thm)],[c_4931,c_2708]) ).
cnf(c_7907,plain,
hAPP(int,nat,nat_1,A) = hAPP(int,nat,number_number_of(nat),A),
inference(paramod,[status(thm)],[c_4909,c_7906]) ).
cnf(c_5977,plain,
hAPP(int,nat,number_number_of(nat),A) = hAPP(int,nat,nat_1,A),
inference(copy,[status(thm)],[c_7907]) ).
cnf(c_7908,plain,
hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,zero_zero(int))) = one_one(int),
inference(paramod,[status(thm)],[c_4994,c_2067]) ).
cnf(c_7909,plain,
hAPP(int,int,number_number_of(int),ti(int,one_one(int))) = one_one(int),
inference(paramod,[status(thm)],[c_5728,c_7908]) ).
cnf(c_7910,plain,
hAPP(int,int,number_number_of(int),one_one(int)) = one_one(int),
inference(paramod,[status(thm)],[c_4909,c_7909]) ).
cnf(c_5997,plain,
ti(int,one_one(int)) = one_one(int),
inference(paramod,[status(thm)],[c_4931,c_7910]) ).
cnf(c_7911,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),zero_zero(int)),A) = pls,
inference(paramod,[status(thm)],[c_4994,c_4961]) ).
cnf(c_6012,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),zero_zero(int)),A) = zero_zero(int),
inference(paramod,[status(thm)],[c_4994,c_7911]) ).
cnf(c_7912,plain,
ti(int,zero_zero(int)) = pls,
inference(paramod,[status(thm)],[c_4994,c_4903]) ).
cnf(c_6018,plain,
ti(int,zero_zero(int)) = zero_zero(int),
inference(paramod,[status(thm)],[c_4994,c_7912]) ).
cnf(c_6467,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int)))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_5935,c_5934]) ).
cnf(c_7913,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,nat_1,hAPP(int,int,bit0,one_one(int))))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_5977,c_5933]) ).
cnf(c_6468,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),one_one(int))),zero_zero(int))),
inference(paramod,[status(thm)],[c_5960,c_7913]) ).
cnf(c_7914,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,nat_1,hAPP(int,int,bit0,one_one(int))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1),
inference(paramod,[status(thm)],[c_5977,c_5938]) ).
cnf(c_7915,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,hAPP(int,int,bit0,m))),one_one(int))),sK1),
inference(paramod,[status(thm)],[c_5960,c_7914]) ).
cnf(c_6469,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),one_one(int)) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_5941,c_7915]) ).
cnf(c_6506,plain,
hAPP(int,int,bit1,zero_zero(int)) = one_one(int),
inference(paramod,[status(thm)],[c_5997,c_5728]) ).
cnf(c_6529,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int)))),zero_zero(int))),
inference(paramod,[status(thm)],[c_6469,c_6468]) ).
cnf(c_7916,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,A)),one_one(int)) = hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),A),zero_zero(int))),
inference(paramod,[status(thm)],[c_6506,c_2099]) ).
cnf(c_7917,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,A)),one_one(int)) = hAPP(int,int,bit1,ti(int,A)),
inference(paramod,[status(thm)],[c_5018,c_7916]) ).
cnf(c_6549,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,bit0,A)),one_one(int)) = hAPP(int,int,bit1,A),
inference(paramod,[status(thm)],[c_4909,c_7917]) ).
cnf(c_6553,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int)))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_6549,c_6467]) ).
cnf(c_7918,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_6549,c_5941]) ).
cnf(c_6568,plain,
hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1),
inference(copy,[status(thm)],[c_7918]) ).
cnf(c_7919,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t) = hAPP(product_prod(int,int),int,twoSqu1094008024sum2sq,hAPP(int,product_prod(int,int),hAPP(int,fun(int,product_prod(int,int)),product_Pair(int,int),s),one_one(int))),
inference(paramod,[status(thm)],[c_6549,c_5935]) ).
cnf(c_7920,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1),
inference(paramod,[status(thm)],[c_6568,c_7919]) ).
cnf(c_6572,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t),
inference(copy,[status(thm)],[c_7920]) ).
cnf(c_7921,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_6568,c_6553]) ).
cnf(c_6573,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),zero_zero(int)))),
inference(paramod,[status(thm)],[c_6572,c_7921]) ).
cnf(c_7922,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),sK1)),zero_zero(int))),
inference(paramod,[status(thm)],[c_6568,c_6529]) ).
cnf(c_6577,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t)),zero_zero(int))),
inference(paramod,[status(thm)],[c_6572,c_7922]) ).
cnf(c_7923,plain,
hAPP(int,int,bit0,sK0(zero_zero(int))) = ti(int,zero_zero(int)),
inference(resolve,[status(thm)],[c_5964,c_2816]) ).
cnf(c_7282,plain,
hAPP(int,int,bit0,sK0(zero_zero(int))) = zero_zero(int),
inference(paramod,[status(thm)],[c_6018,c_7923]) ).
cnf(c_7284,plain,
ti(int,sK0(zero_zero(int))) = zero_zero(int),
inference(resolve,[status(thm)],[c_7282,c_5001]) ).
cnf(c_7924,plain,
hAPP(int,A,B,zero_zero(int)) = hAPP(int,A,B,sK0(zero_zero(int))),
inference(paramod,[status(thm)],[c_7284,c_4909]) ).
cnf(c_7294,plain,
hAPP(int,A,B,sK0(zero_zero(int))) = hAPP(int,A,B,zero_zero(int)),
inference(copy,[status(thm)],[c_7924]) ).
cnf(c_7925,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),zero_zero(int)),A) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),sK0(zero_zero(int))),
inference(paramod,[status(thm)],[c_7294,c_2018]) ).
cnf(c_7926,plain,
zero_zero(int) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),sK0(zero_zero(int))),
inference(paramod,[status(thm)],[c_6012,c_7925]) ).
cnf(c_7927,plain,
zero_zero(int) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),zero_zero(int)),
inference(paramod,[status(thm)],[c_7294,c_7926]) ).
cnf(c_7813,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),A),zero_zero(int)) = zero_zero(int),
inference(copy,[status(thm)],[c_7927]) ).
cnf(c_7928,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,hAPP(int,int,bit0,m))),t)),zero_zero(int))),
inference(paramod,[status(thm)],[c_7813,c_6573]) ).
cnf(c_7834,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_6577,c_7928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n008.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 04:19:11 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 2757860 was started by sandbox on n008,
% 0.07/0.35 % Sat Sep 26 04:19:11 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 28.35/4.78
% 28.35/4.78 % SInE (scan): 1631 to sos (tol 1.5x), 497 to usable (tol 2.0x), 3609 zapped, of 5737 axioms (depth 3).
% 28.35/4.78
% 28.35/4.78 % From the command line: assign(max_seconds, 300).
% 28.35/4.78
% 28.35/4.78 % SZS status Theorem for theBenchmark
% 28.35/4.78
% 28.35/4.78 % Proof 1 at 2.97 (+ 0.53) seconds.
% 28.35/4.78 % Length of proof is 79.
% 28.35/4.78 % Level of proof is 10.
% 28.35/4.78 % Maximum clause weight is 281.000.
% 28.35/4.78 % Given clauses 127.
% 28.35/4.78
% 28.35/4.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------