%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM926+7 : TPTP v7.0.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n083.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Mon Jan 8 15:22:44 EST 2018
% Result : Theorem 4.88s
% Output : CNFRefutation 4.88s
% Verified :
% SZS Type : None (Could not find formula named theqry(equality))
% Syntax : Number of formulae : 100
% Comments :
%------------------------------------------------------------------------------
fof(120,axiom,
equal(ti(int,t),t),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',tsy_v_t_____res) ).
fof(203,axiom,
! [X25] : equal(bit0(ti(int,X25)),bit0(X25)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',tsy_c_Int_OBit0_arg1) ).
fof(247,axiom,
! [X22,X24] : equal(hAPP(int,int,plus_plus(int,X22),X24),hAPP(int,int,plus_plus(int,X24),X22)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_91_zadd__commute) ).
fof(406,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_0_tpos) ).
fof(416,axiom,
monoid_mult(int),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',arity_Int_Oint___Groups_Omonoid__mult) ).
fof(484,axiom,
! [X5] :
( monoid_mult(X5)
=> ! [X6] : equal(hAPP(nat,X5,power_power(X5,one_one(X5)),X6),one_one(X5)) ),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_262_power__one) ).
fof(654,axiom,
! [X17] : equal(bit1(X17),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X17)),X17)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_153_Bit1__def) ).
fof(713,axiom,
! [X47,X42] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X47),X42))
<=> ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X47),X42))
& ~ equal(ti(int,X47),ti(int,X42)) ) ),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_22_zless__le) ).
fof(755,axiom,
! [X17] : equal(bit0(X17),hAPP(int,int,plus_plus(int,X17),X17)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_128_Bit0__def) ).
fof(800,axiom,
! [X17] : equal(hAPP(int,int,plus_plus(int,X17),pls),ti(int,X17)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_125_add__Pls__right) ).
fof(921,axiom,
! [X8,X45,X22] : equal(hAPP(nat,int,power_power(int,X8),hAPP(nat,nat,plus_plus(nat,X45),X22)),hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,X8),X45)),hAPP(nat,int,power_power(int,X8),X22))),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_34_zpower__zadd__distrib) ).
fof(1024,axiom,
! [X17] : equal(hAPP(int,int,plus_plus(int,pls),X17),ti(int,X17)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_126_add__Pls) ).
fof(1036,axiom,
! [X22,X24] : equal(hAPP(int,int,times_times(int,X22),X24),hAPP(int,int,times_times(int,X24),X22)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_87_zmult__commute) ).
fof(1064,axiom,
! [X31,X24] : equal(hAPP(int,int,plus_plus(int,number_number_of(int,X31)),number_number_of(int,X24)),number_number_of(int,hAPP(int,int,plus_plus(int,X31),X24))),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_134_plus__numeral__code_I9_J) ).
fof(1126,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(1132,axiom,
( equal(t,one_one(int))
=> ? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(1162,axiom,
! [X22] : equal(hAPP(int,int,times_times(int,one_one(int)),X22),ti(int,X22)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_130_zmult__1) ).
fof(1172,conjecture,
? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',conj_0) ).
fof(1188,axiom,
! [X17] : equal(number_number_of(int,X17),ti(int,X17)),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_88_number__of__is__id) ).
fof(1193,axiom,
! [X77,X78,X84] : equal(hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X77),X78)),X84),hAPP(int,int,plus_plus(int,X77),hAPP(int,int,plus_plus(int,X78),X84))),
file('/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1',fact_89_zadd__assoc) ).
fof(1256,negated_conjecture,
~ ? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
inference(assume_negation,[status(cth)],[1172]) ).
cnf(1760,plain,
ti(int,t) = t,
inference(split_conjunct,[status(thm)],[120]) ).
fof(2061,plain,
! [X26] : equal(bit0(ti(int,X26)),bit0(X26)),
inference(variable_rename,[status(thm)],[203]) ).
cnf(2062,plain,
bit0(ti(int,X1)) = bit0(X1),
inference(split_conjunct,[status(thm)],[2061]) ).
fof(2213,plain,
! [X25,X26] : equal(hAPP(int,int,plus_plus(int,X25),X26),hAPP(int,int,plus_plus(int,X26),X25)),
inference(variable_rename,[status(thm)],[247]) ).
cnf(2214,plain,
hAPP(int,int,plus_plus(int,X1),X2) = hAPP(int,int,plus_plus(int,X2),X1),
inference(split_conjunct,[status(thm)],[2213]) ).
cnf(2700,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(split_conjunct,[status(thm)],[406]) ).
cnf(2728,plain,
monoid_mult(int),
inference(split_conjunct,[status(thm)],[416]) ).
fof(2961,plain,
! [X5] :
( ~ monoid_mult(X5)
| ! [X6] : equal(hAPP(nat,X5,power_power(X5,one_one(X5)),X6),one_one(X5)) ),
inference(fof_nnf,[status(thm)],[484]) ).
fof(2962,plain,
! [X7] :
( ~ monoid_mult(X7)
| ! [X8] : equal(hAPP(nat,X7,power_power(X7,one_one(X7)),X8),one_one(X7)) ),
inference(variable_rename,[status(thm)],[2961]) ).
fof(2963,plain,
! [X7,X8] :
( equal(hAPP(nat,X7,power_power(X7,one_one(X7)),X8),one_one(X7))
| ~ monoid_mult(X7) ),
inference(shift_quantors,[status(thm)],[2962]) ).
cnf(2964,plain,
( hAPP(nat,X1,power_power(X1,one_one(X1)),X2) = one_one(X1)
| ~ monoid_mult(X1) ),
inference(split_conjunct,[status(thm)],[2963]) ).
fof(3487,plain,
! [X18] : equal(bit1(X18),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X18)),X18)),
inference(variable_rename,[status(thm)],[654]) ).
cnf(3488,plain,
bit1(X1) = hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X1)),X1),
inference(split_conjunct,[status(thm)],[3487]) ).
fof(3708,plain,
! [X47,X42] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X47),X42))
| ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X47),X42))
& ~ equal(ti(int,X47),ti(int,X42)) ) )
& ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X47),X42))
| equal(ti(int,X47),ti(int,X42))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X47),X42)) ) ),
inference(fof_nnf,[status(thm)],[713]) ).
fof(3709,plain,
! [X48,X49] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X48),X49))
| ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X48),X49))
& ~ equal(ti(int,X48),ti(int,X49)) ) )
& ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X48),X49))
| equal(ti(int,X48),ti(int,X49))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X48),X49)) ) ),
inference(variable_rename,[status(thm)],[3708]) ).
fof(3710,plain,
! [X48,X49] :
( ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X48),X49))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X48),X49)) )
& ( ~ equal(ti(int,X48),ti(int,X49))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X48),X49)) )
& ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X48),X49))
| equal(ti(int,X48),ti(int,X49))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X48),X49)) ) ),
inference(distribute,[status(thm)],[3709]) ).
cnf(3711,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X1),X2))
| ti(int,X1) = ti(int,X2)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),X2)) ),
inference(split_conjunct,[status(thm)],[3710]) ).
fof(3843,plain,
! [X18] : equal(bit0(X18),hAPP(int,int,plus_plus(int,X18),X18)),
inference(variable_rename,[status(thm)],[755]) ).
cnf(3844,plain,
bit0(X1) = hAPP(int,int,plus_plus(int,X1),X1),
inference(split_conjunct,[status(thm)],[3843]) ).
fof(4016,plain,
! [X18] : equal(hAPP(int,int,plus_plus(int,X18),pls),ti(int,X18)),
inference(variable_rename,[status(thm)],[800]) ).
cnf(4017,plain,
hAPP(int,int,plus_plus(int,X1),pls) = ti(int,X1),
inference(split_conjunct,[status(thm)],[4016]) ).
fof(4420,plain,
! [X46,X47,X48] : equal(hAPP(nat,int,power_power(int,X46),hAPP(nat,nat,plus_plus(nat,X47),X48)),hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,X46),X47)),hAPP(nat,int,power_power(int,X46),X48))),
inference(variable_rename,[status(thm)],[921]) ).
cnf(4421,plain,
hAPP(nat,int,power_power(int,X1),hAPP(nat,nat,plus_plus(nat,X2),X3)) = hAPP(int,int,times_times(int,hAPP(nat,int,power_power(int,X1),X2)),hAPP(nat,int,power_power(int,X1),X3)),
inference(split_conjunct,[status(thm)],[4420]) ).
fof(4765,plain,
! [X18] : equal(hAPP(int,int,plus_plus(int,pls),X18),ti(int,X18)),
inference(variable_rename,[status(thm)],[1024]) ).
cnf(4766,plain,
hAPP(int,int,plus_plus(int,pls),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[4765]) ).
fof(4809,plain,
! [X25,X26] : equal(hAPP(int,int,times_times(int,X25),X26),hAPP(int,int,times_times(int,X26),X25)),
inference(variable_rename,[status(thm)],[1036]) ).
cnf(4810,plain,
hAPP(int,int,times_times(int,X1),X2) = hAPP(int,int,times_times(int,X2),X1),
inference(split_conjunct,[status(thm)],[4809]) ).
fof(4894,plain,
! [X32,X33] : equal(hAPP(int,int,plus_plus(int,number_number_of(int,X32)),number_number_of(int,X33)),number_number_of(int,hAPP(int,int,plus_plus(int,X32),X33))),
inference(variable_rename,[status(thm)],[1064]) ).
cnf(4895,plain,
hAPP(int,int,plus_plus(int,number_number_of(int,X1)),number_number_of(int,X2)) = number_number_of(int,hAPP(int,int,plus_plus(int,X1),X2)),
inference(split_conjunct,[status(thm)],[4894]) ).
fof(5115,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| ? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(fof_nnf,[status(thm)],[1126]) ).
fof(5116,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| ? [X65,X66] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X65),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X66),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(variable_rename,[status(thm)],[5115]) ).
fof(5117,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(skolemize,[status(esa)],[5116]) ).
cnf(5118,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(split_conjunct,[status(thm)],[5117]) ).
fof(5135,plain,
( ~ equal(t,one_one(int))
| ? [X35,X64] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(fof_nnf,[status(thm)],[1132]) ).
fof(5136,plain,
( ~ equal(t,one_one(int))
| ? [X65,X66] : equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X65),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X66),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(variable_rename,[status(thm)],[5135]) ).
fof(5137,plain,
( ~ equal(t,one_one(int))
| equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))) ),
inference(skolemize,[status(esa)],[5136]) ).
cnf(5138,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,bit0(bit1(pls))))) = 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 != one_one(int) ),
inference(split_conjunct,[status(thm)],[5137]) ).
fof(5232,plain,
! [X23] : equal(hAPP(int,int,times_times(int,one_one(int)),X23),ti(int,X23)),
inference(variable_rename,[status(thm)],[1162]) ).
cnf(5233,plain,
hAPP(int,int,times_times(int,one_one(int)),X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[5232]) ).
fof(5258,negated_conjecture,
! [X35,X64] : ~ equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X35),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X64),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
inference(fof_nnf,[status(thm)],[1256]) ).
fof(5259,negated_conjecture,
! [X65,X66] : ~ equal(hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X65),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X66),number_number_of(nat,bit0(bit1(pls))))),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),
inference(variable_rename,[status(thm)],[5258]) ).
cnf(5260,negated_conjecture,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X1),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,X2),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(split_conjunct,[status(thm)],[5259]) ).
fof(5308,plain,
! [X18] : equal(number_number_of(int,X18),ti(int,X18)),
inference(variable_rename,[status(thm)],[1188]) ).
cnf(5309,plain,
number_number_of(int,X1) = ti(int,X1),
inference(split_conjunct,[status(thm)],[5308]) ).
fof(5322,plain,
! [X85,X86,X87] : equal(hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X85),X86)),X87),hAPP(int,int,plus_plus(int,X85),hAPP(int,int,plus_plus(int,X86),X87))),
inference(variable_rename,[status(thm)],[1193]) ).
cnf(5323,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X1),X2)),X3) = hAPP(int,int,plus_plus(int,X1),hAPP(int,int,plus_plus(int,X2),X3)),
inference(split_conjunct,[status(thm)],[5322]) ).
cnf(5584,plain,
hAPP(int,int,plus_plus(int,ti(int,X1)),ti(int,X1)) = hAPP(int,int,plus_plus(int,X1),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[2062,3844,theory(equality)]),3844,theory(equality)]),
[unfolding] ).
cnf(5714,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))) = 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,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int))
| one_one(int) != t ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5138,3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),
[unfolding] ).
cnf(5719,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))) = 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,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5118,3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),
[unfolding] ).
cnf(5766,negated_conjecture,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X1),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),hAPP(nat,int,power_power(int,X2),number_number_of(nat,hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))) != 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,bit1(pls)),bit1(pls))),hAPP(int,int,plus_plus(int,bit1(pls)),bit1(pls))))),m)),one_one(int)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5260,3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),3844,theory(equality)]),
[unfolding] ).
cnf(5927,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))) = 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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),m)),one_one(int))
| one_one(int) != t ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5714,3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),
[unfolding] ).
cnf(5932,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))) = 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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5719,3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),
[unfolding] ).
cnf(5987,negated_conjecture,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X1),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),hAPP(nat,int,power_power(int,X2),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))) != 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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),m)),one_one(int)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5766,3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),3488,theory(equality)]),
[unfolding] ).
cnf(6009,plain,
number_number_of(int,t) = t,
inference(rw,[status(thm)],[1760,5309,theory(equality)]) ).
cnf(6018,plain,
hAPP(int,int,plus_plus(int,pls),X1) = number_number_of(int,X1),
inference(rw,[status(thm)],[4766,5309,theory(equality)]) ).
cnf(6028,plain,
hAPP(int,int,plus_plus(int,X1),pls) = hAPP(int,int,plus_plus(int,pls),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[4017,5309,theory(equality)]),6018,theory(equality)]) ).
cnf(6050,plain,
hAPP(int,int,times_times(int,one_one(int)),X1) = hAPP(int,int,plus_plus(int,pls),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[5233,5309,theory(equality)]),6018,theory(equality)]) ).
cnf(6192,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),X1)),hAPP(int,int,plus_plus(int,pls),X2)) = number_number_of(int,hAPP(int,int,plus_plus(int,X1),X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[4895,6018,theory(equality)]),6018,theory(equality)]) ).
cnf(6193,plain,
hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),X1)),hAPP(int,int,plus_plus(int,pls),X2)) = hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,X1),X2)),
inference(rw,[status(thm)],[6192,6018,theory(equality)]) ).
cnf(6613,plain,
hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,X1),X1)) = hAPP(int,int,plus_plus(int,X1),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5584,5309,theory(equality)]),6018,theory(equality)]),5309,theory(equality)]),6018,theory(equality)]),6193,theory(equality)]) ).
cnf(6993,negated_conjecture,
hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,pls),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))))))) != hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X1),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),hAPP(nat,int,power_power(int,X2),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5987,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),5323,theory(equality)]),6018,theory(equality)]),4810,theory(equality)]),2214,theory(equality)]) ).
cnf(6994,negated_conjecture,
hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,pls),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))))))) != hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X1),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),hAPP(nat,int,power_power(int,X2),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[6993,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]) ).
cnf(7279,plain,
hAPP(nat,int,power_power(int,one_one(int)),X1) = one_one(int),
inference(spm,[status(thm)],[2964,2728,theory(equality)]) ).
cnf(13337,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),m)),one_one(int))
| one_one(int) != t ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5927,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]) ).
cnf(13338,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk39_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),hAPP(nat,int,power_power(int,esk40_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,pls),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)))))))
| one_one(int) != t ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[13337,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),5323,theory(equality)]),6018,theory(equality)]),4810,theory(equality)]),2214,theory(equality)]) ).
cnf(13339,plain,
one_one(int) != t,
inference(sr,[status(thm)],[13338,6994,theory(equality)]) ).
cnf(25733,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(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,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[5932,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]) ).
cnf(25734,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,esk36_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),hAPP(nat,int,power_power(int,esk37_0),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,pls),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)))))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[25733,6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6028,theory(equality)]),6193,theory(equality)]),6193,theory(equality)]),6613,theory(equality)]),6613,theory(equality)]),5323,theory(equality)]),6018,theory(equality)]),4810,theory(equality)]),2214,theory(equality)]) ).
cnf(25735,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)),
inference(sr,[status(thm)],[25734,6994,theory(equality)]) ).
cnf(42965,plain,
( hAPP(int,int,plus_plus(int,pls),X1) = ti(int,X2)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),X1),X2))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[3711,5309,theory(equality)]),6018,theory(equality)]) ).
cnf(42967,plain,
( hAPP(int,int,plus_plus(int,pls),one_one(int)) = ti(int,t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(spm,[status(thm)],[42965,2700,theory(equality)]) ).
cnf(43008,plain,
( hAPP(int,int,plus_plus(int,pls),one_one(int)) = hAPP(int,int,plus_plus(int,pls),t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[42967,5309,theory(equality)]),6018,theory(equality)]) ).
cnf(43009,plain,
hAPP(int,int,plus_plus(int,pls),one_one(int)) = hAPP(int,int,plus_plus(int,pls),t),
inference(sr,[status(thm)],[43008,25735,theory(equality)]) ).
cnf(190071,plain,
hAPP(int,int,plus_plus(int,pls),t) = t,
inference(rw,[status(thm)],[6009,6018,theory(equality)]) ).
cnf(190312,plain,
hAPP(int,int,times_times(int,one_one(int)),hAPP(nat,int,power_power(int,one_one(int)),X2)) = hAPP(nat,int,power_power(int,one_one(int)),hAPP(nat,nat,plus_plus(nat,X1),X2)),
inference(spm,[status(thm)],[4421,7279,theory(equality)]) ).
cnf(190384,plain,
t = hAPP(nat,int,power_power(int,one_one(int)),hAPP(nat,nat,plus_plus(nat,X1),X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[190312,7279,theory(equality)]),6050,theory(equality)]),43009,theory(equality)]),190071,theory(equality)]) ).
cnf(190385,plain,
t = one_one(int),
inference(rw,[status(thm)],[190384,7279,theory(equality)]) ).
cnf(190386,plain,
$false,
inference(sr,[status(thm)],[190385,13339,theory(equality)]) ).
cnf(190387,plain,
$false,
190386,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+7 : TPTP v7.0.0. Released v5.3.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n083.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 16:22:49 CST 2018
% 0.02/0.23 % CPUTime :
% 0.07/0.27 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.28 --creating new selector for []
% 4.88/5.09 -running prover on /export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1 with time limit 29
% 4.88/5.09 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox/tmp/tmpQy6fxW/sel_theBenchmark.p_1']
% 4.88/5.09 -prover status Theorem
% 4.88/5.09 Problem theBenchmark.p solved in phase 0.
% 4.88/5.09 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.88/5.09 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.88/5.09 Solved 1 out of 1.
% 4.88/5.09 # Problem is unsatisfiable (or provable), constructing proof object
% 4.88/5.09 # SZS status Theorem
% 4.88/5.09 # SZS output start CNFRefutation.
% See solution above
% 4.88/5.09 # SZS output end CNFRefutation
%------------------------------------------------------------------------------