%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:31 PM UTC 2026
% Result : Theorem 12.68s 2.84s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 35
% Syntax : Number of formulae : 180 ( 180 unt; 17 def)
% Number of atoms : 180 ( 132 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 22 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 24 con; 0-4 aty)
% Number of variables : 54 ( 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f89,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_arg2) ).
fof(f90,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).
fof(f100,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
file('/export/starexec/sandbox2/benchmark/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) ).
fof(f101,axiom,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
fof(f120,axiom,
! [X0] : number_number_of(int,X0) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(f121,axiom,
! [X0,X1] : hAPP(int,int,times_times(int,X0),X1) = hAPP(int,int,times_times(int,X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_zmult__commute) ).
fof(f160,axiom,
! [X0] : hAPP(int,int,times_times(int,pls),X0) = pls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_mult__Pls) ).
fof(f194,axiom,
! [X0,X1,X2] : hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X0),X1)),X2) = hAPP(int,int,plus_plus(int,X0),hAPP(int,int,plus_plus(int,X1),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_zadd__assoc) ).
fof(f196,axiom,
! [X0,X1] : hAPP(int,int,plus_plus(int,X0),X1) = hAPP(int,int,plus_plus(int,X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_zadd__commute) ).
fof(f209,axiom,
one_one(int) = number_number_of(int,bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_one__is__num__one) ).
fof(f220,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_Pls__def) ).
fof(f227,axiom,
! [X0] : hAPP(int,int,plus_plus(int,X0),pls) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_add__Pls__right) ).
fof(f228,axiom,
! [X0] : hAPP(int,int,plus_plus(int,pls),X0) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_add__Pls) ).
fof(f230,axiom,
! [X0] : bit0(X0) = hAPP(int,int,plus_plus(int,X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_Bit0__def) ).
fof(f231,axiom,
! [X0] : hAPP(int,int,plus_plus(int,X0),zero_zero(int)) = ti(int,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_zadd__0__right) ).
fof(f262,axiom,
! [X0] : bit1(X0) = hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X0)),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_Bit1__def) ).
fof(f1248,axiom,
! [X0,X1] : ti(X0,ti(X0,X1)) = ti(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_ti_idem) ).
fof(f1255,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1256,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(negated_conjecture,[status(cth)],[f1255]) ).
fof(f1261,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(flattening,[],[f1256]) ).
fof(f2747,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
inference(cnf_transformation,[],[f89]) ).
fof(f2748,plain,
! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = ti(X0,hAPP(X1,X0,X2,X3)),
inference(cnf_transformation,[],[f90]) ).
fof(f2759,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),zero_zero(int)))),
inference(cnf_transformation,[],[f100]) ).
fof(f2760,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int)),
inference(cnf_transformation,[],[f101]) ).
fof(f2785,plain,
! [X0] : ti(int,X0) = number_number_of(int,X0),
inference(cnf_transformation,[],[f120]) ).
fof(f2786,plain,
! [X0,X1] : hAPP(int,int,times_times(int,X0),X1) = hAPP(int,int,times_times(int,X1),X0),
inference(cnf_transformation,[],[f121]) ).
fof(f2848,plain,
! [X0] : pls = hAPP(int,int,times_times(int,pls),X0),
inference(cnf_transformation,[],[f160]) ).
fof(f2904,plain,
! [X2,X0,X1] : hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,X0),X1)),X2) = hAPP(int,int,plus_plus(int,X0),hAPP(int,int,plus_plus(int,X1),X2)),
inference(cnf_transformation,[],[f194]) ).
fof(f2906,plain,
! [X0,X1] : hAPP(int,int,plus_plus(int,X0),X1) = hAPP(int,int,plus_plus(int,X1),X0),
inference(cnf_transformation,[],[f196]) ).
fof(f2923,plain,
one_one(int) = number_number_of(int,bit1(pls)),
inference(cnf_transformation,[],[f209]) ).
fof(f2939,plain,
pls = zero_zero(int),
inference(cnf_transformation,[],[f220]) ).
fof(f2950,plain,
! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,X0),pls),
inference(cnf_transformation,[],[f227]) ).
fof(f2951,plain,
! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,pls),X0),
inference(cnf_transformation,[],[f228]) ).
fof(f2953,plain,
! [X0] : bit0(X0) = hAPP(int,int,plus_plus(int,X0),X0),
inference(cnf_transformation,[],[f230]) ).
fof(f2954,plain,
! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,X0),zero_zero(int)),
inference(cnf_transformation,[],[f231]) ).
fof(f2994,plain,
! [X0] : bit1(X0) = hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),X0)),X0),
inference(cnf_transformation,[],[f262]) ).
fof(f4348,plain,
! [X0,X1] : ti(X0,X1) = ti(X0,ti(X0,X1)),
inference(cnf_transformation,[],[f1248]) ).
fof(f4355,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,bit0(bit1(pls))))),one_one(int))),zero_zero(int))),
inference(cnf_transformation,[],[f1261]) ).
fof(f4368,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))),zero_zero(int)))),
inference(definition_unfolding,[],[f2759,f2953,f2953,f2994,f2953,f2953,f2994]) ).
fof(f4369,plain,
hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))),t) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))))),one_one(int)),
inference(definition_unfolding,[],[f2760,f2953,f2953,f2994,f2953,f2994]) ).
fof(f4444,plain,
one_one(int) = number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)),
inference(definition_unfolding,[],[f2923,f2994]) ).
fof(f4621,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))))),one_one(int))),zero_zero(int))),
inference(definition_unfolding,[],[f4355,f2953,f2994]) ).
fof(f4715,definition,
sF48 = fun(int,bool),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f4716,plain,
fun(int,bool) = sF48,
inference(reorient_equations,[],[f4715]) ).
fof(f4717,definition,
sF49 = ord_less(int),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f4718,plain,
ord_less(int) = sF49,
inference(reorient_equations,[],[f4717]) ).
fof(f4719,definition,
sF50 = power_power(int,s),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f4720,plain,
power_power(int,s) = sF50,
inference(reorient_equations,[],[f4719]) ).
fof(f4721,definition,
sF51 = one_one(int),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f4722,plain,
one_one(int) = sF51,
inference(reorient_equations,[],[f4721]) ).
fof(f4723,definition,
sF52 = plus_plus(int,sF51),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f4724,plain,
plus_plus(int,sF51) = sF52,
inference(reorient_equations,[],[f4723]) ).
fof(f4725,definition,
sF53 = hAPP(int,int,sF52,pls),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f4726,plain,
hAPP(int,int,sF52,pls) = sF53,
inference(reorient_equations,[],[f4725]) ).
fof(f4727,definition,
sF54 = plus_plus(int,sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f4728,plain,
plus_plus(int,sF53) = sF54,
inference(reorient_equations,[],[f4727]) ).
fof(f4729,definition,
sF55 = hAPP(int,int,sF54,pls),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f4730,plain,
hAPP(int,int,sF54,pls) = sF55,
inference(reorient_equations,[],[f4729]) ).
fof(f4731,definition,
sF56 = plus_plus(int,sF55),
introduced(definition,[new_symbols(definition,[sF56])],[function_definition]) ).
fof(f4732,plain,
plus_plus(int,sF55) = sF56,
inference(reorient_equations,[],[f4731]) ).
fof(f4733,definition,
sF57 = hAPP(int,int,sF56,sF55),
introduced(definition,[new_symbols(definition,[sF57])],[function_definition]) ).
fof(f4734,plain,
hAPP(int,int,sF56,sF55) = sF57,
inference(reorient_equations,[],[f4733]) ).
fof(f4735,definition,
sF58 = number_number_of(nat,sF57),
introduced(definition,[new_symbols(definition,[sF58])],[function_definition]) ).
fof(f4736,plain,
number_number_of(nat,sF57) = sF58,
inference(reorient_equations,[],[f4735]) ).
fof(f4737,definition,
sF59 = hAPP(nat,int,sF50,sF58),
introduced(definition,[new_symbols(definition,[sF59])],[function_definition]) ).
fof(f4738,plain,
hAPP(nat,int,sF50,sF58) = sF59,
inference(reorient_equations,[],[f4737]) ).
fof(f4739,definition,
sF60 = plus_plus(int,sF59),
introduced(definition,[new_symbols(definition,[sF60])],[function_definition]) ).
fof(f4740,plain,
plus_plus(int,sF59) = sF60,
inference(reorient_equations,[],[f4739]) ).
fof(f4741,definition,
sF61 = hAPP(int,int,sF60,sF51),
introduced(definition,[new_symbols(definition,[sF61])],[function_definition]) ).
fof(f4742,plain,
hAPP(int,int,sF60,sF51) = sF61,
inference(reorient_equations,[],[f4741]) ).
fof(f4743,definition,
sF62 = hAPP(int,sF48,sF49,sF61),
introduced(definition,[new_symbols(definition,[sF62])],[function_definition]) ).
fof(f4744,plain,
hAPP(int,sF48,sF49,sF61) = sF62,
inference(reorient_equations,[],[f4743]) ).
fof(f4745,definition,
sF63 = zero_zero(int),
introduced(definition,[new_symbols(definition,[sF63])],[function_definition]) ).
fof(f4746,plain,
zero_zero(int) = sF63,
inference(reorient_equations,[],[f4745]) ).
fof(f4747,definition,
sF64 = hAPP(int,bool,sF62,sF63),
introduced(definition,[new_symbols(definition,[sF64])],[function_definition]) ).
fof(f4748,plain,
hAPP(int,bool,sF62,sF63) = sF64,
inference(reorient_equations,[],[f4747]) ).
fof(f4749,plain,
~ hBOOL(sF64),
inference(definition_folding,[],[f4621,f4748,f4746,f4744,f4742,f4722,f4740,f4738,f4736,f4734,f4730,f4728,f4726,f4724,f4722,f4732,f4730,f4728,f4726,f4724,f4722,f4720,f4718,f4716]) ).
fof(f4788,plain,
one_one(int) = number_number_of(int,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),pls))),
inference(forward_demodulation,[],[f4444,f2950]) ).
fof(f4856,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),one_one(int)) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),hAPP(int,int,plus_plus(int,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,one_one(int)),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),m)),one_one(int))),t),
inference(forward_demodulation,[],[f4369,f2904]) ).
fof(f4857,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,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))),pls))),
inference(forward_demodulation,[],[f4368,f2939]) ).
fof(f4862,plain,
pls = sF63,
inference(forward_demodulation,[],[f4746,f2939]) ).
fof(f4870,plain,
one_one(int) = ti(int,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),pls))),
inference(forward_demodulation,[],[f4788,f2785]) ).
fof(f4938,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f4856,f4722]) ).
fof(f4939,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))),m)),sF51)),pls))),
inference(forward_demodulation,[],[f4857,f4722]) ).
fof(f4949,plain,
one_one(int) = ti(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),
inference(forward_demodulation,[],[f4870,f4348]) ).
fof(f5015,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f4938,f2785]) ).
fof(f5016,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f4939,f4862]) ).
fof(f5026,plain,
one_one(int) = hAPP(int,int,plus_plus(int,one_one(int)),pls),
inference(forward_demodulation,[],[f4949,f2748]) ).
fof(f5090,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5015,f2748]) ).
fof(f5091,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(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,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,ti(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,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5016,f2785]) ).
fof(f5099,plain,
one_one(int) = ti(int,one_one(int)),
inference(forward_demodulation,[],[f5026,f2950]) ).
fof(f5160,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5090,f2904]) ).
fof(f5161,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(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,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5091,f2748]) ).
fof(f5167,plain,
sF51 = ti(int,sF51),
inference(forward_demodulation,[],[f5099,f4722]) ).
fof(f5218,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5160,f2904]) ).
fof(f5219,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5161,f2904]) ).
fof(f5260,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5218,f2951]) ).
fof(f5261,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5219,f2904]) ).
fof(f5296,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5260,f2747]) ).
fof(f5297,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5261,f2904]) ).
fof(f5326,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5296,f2904]) ).
fof(f5327,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5297,f2904]) ).
fof(f5355,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5326,f2951]) ).
fof(f5356,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5327,f2904]) ).
fof(f5377,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5355,f2747]) ).
fof(f5378,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63)))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5356,f2904]) ).
fof(f5399,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5377,f2904]) ).
fof(f5400,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),sF63)),sF63))))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5378,f2904]) ).
fof(f5421,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5399,f2904]) ).
fof(f5422,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5400,f2904]) ).
fof(f5429,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5421,f2951]) ).
fof(f5430,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5422,f4724]) ).
fof(f5436,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5429,f2747]) ).
fof(f5437,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),sF49,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5430,f4718]) ).
fof(f5443,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5436,f2951]) ).
fof(f5444,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),t)),hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),sF63))),
inference(forward_demodulation,[],[f5437,f4716]) ).
fof(f5450,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5443,f2747]) ).
fof(f5456,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5450,f2904]) ).
fof(f5470,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5456,f2951]) ).
fof(f5475,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5470,f2747]) ).
fof(f5480,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5475,f2951]) ).
fof(f5485,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,sF51),pls)),pls))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5480,f2747]) ).
fof(f5490,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,pls),pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5485,f2904]) ).
fof(f5495,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,pls)))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,pls)))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5490,f2950]) ).
fof(f5500,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),pls))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),pls))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5495,f2747]) ).
fof(f5505,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),ti(int,sF51))))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),ti(int,sF51))))),m)),sF51)),t),
inference(forward_demodulation,[],[f5500,f2950]) ).
fof(f5510,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,sF51),sF51)))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),hAPP(int,int,plus_plus(int,sF51),sF51)))),m)),sF51)),t),
inference(forward_demodulation,[],[f5505,f2747]) ).
fof(f5515,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,sF52,sF51)))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,sF51)))),m)),sF51)),t),
inference(forward_demodulation,[],[f5510,f4724]) ).
fof(f5519,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,sF50,number_number_of(nat,hAPP(int,int,sF52,sF51)))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,sF51)))),m)),sF51)),t),
inference(forward_demodulation,[],[f5515,f4720]) ).
fof(f5584,plain,
sF53 = hAPP(int,int,sF52,sF63),
inference(superposition,[],[f4726,f4862]) ).
fof(f5590,plain,
! [X0] : hAPP(int,int,sF52,X0) = hAPP(int,int,plus_plus(int,X0),sF51),
inference(superposition,[],[f2906,f4724]) ).
fof(f5593,plain,
! [X0] : hAPP(int,int,plus_plus(int,X0),sF59) = hAPP(int,int,sF60,X0),
inference(superposition,[],[f2906,f4740]) ).
fof(f5599,plain,
ti(int,sF51) = hAPP(int,int,sF52,zero_zero(int)),
inference(superposition,[],[f2954,f4724]) ).
fof(f5611,plain,
hAPP(int,int,sF52,pls) = ti(int,sF51),
inference(forward_demodulation,[],[f5599,f2939]) ).
fof(f5615,plain,
sF51 = hAPP(int,int,sF52,pls),
inference(forward_demodulation,[],[f5611,f5167]) ).
fof(f5616,plain,
sF51 = sF53,
inference(forward_demodulation,[],[f5615,f4726]) ).
fof(f5617,plain,
plus_plus(int,sF51) = sF54,
inference(superposition,[],[f4728,f5616]) ).
fof(f5618,plain,
sF52 = sF54,
inference(forward_demodulation,[],[f5617,f4724]) ).
fof(f5620,plain,
hAPP(int,int,sF52,pls) = sF55,
inference(superposition,[],[f4730,f5618]) ).
fof(f5621,plain,
sF53 = sF55,
inference(forward_demodulation,[],[f5620,f4726]) ).
fof(f5623,plain,
sF51 = sF55,
inference(forward_demodulation,[],[f5621,f5616]) ).
fof(f5626,plain,
plus_plus(int,sF51) = sF56,
inference(superposition,[],[f4732,f5623]) ).
fof(f5627,plain,
sF52 = sF56,
inference(forward_demodulation,[],[f5626,f4724]) ).
fof(f5628,plain,
sF57 = hAPP(int,int,sF52,sF55),
inference(superposition,[],[f4734,f5627]) ).
fof(f5629,plain,
sF57 = hAPP(int,int,sF52,sF51),
inference(forward_demodulation,[],[f5628,f5623]) ).
fof(f5641,plain,
! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,X0),sF63),
inference(superposition,[],[f2950,f4862]) ).
fof(f5658,plain,
! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,sF63),X0),
inference(superposition,[],[f2906,f5641]) ).
fof(f5677,plain,
hAPP(int,int,sF60,sF51) = hAPP(int,int,sF52,sF59),
inference(superposition,[],[f5593,f4724]) ).
fof(f5690,plain,
sF61 = hAPP(int,int,sF52,sF59),
inference(forward_demodulation,[],[f5677,f4742]) ).
fof(f5754,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,sF50,number_number_of(nat,sF57))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m)),sF51)),t),
inference(superposition,[],[f5519,f5629]) ).
fof(f5771,plain,
hAPP(int,int,plus_plus(int,hAPP(nat,int,sF50,number_number_of(nat,sF57))),sF51) = hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t),
inference(forward_demodulation,[],[f5754,f5590]) ).
fof(f5780,plain,
hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t) = hAPP(int,int,sF52,hAPP(nat,int,sF50,number_number_of(nat,sF57))),
inference(forward_demodulation,[],[f5771,f5590]) ).
fof(f5789,plain,
hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t) = hAPP(int,int,sF52,hAPP(nat,int,sF50,sF58)),
inference(forward_demodulation,[],[f5780,f4736]) ).
fof(f5798,plain,
hAPP(int,int,sF52,sF59) = hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t),
inference(forward_demodulation,[],[f5789,f4738]) ).
fof(f5807,plain,
sF61 = hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t),
inference(forward_demodulation,[],[f5798,f5690]) ).
fof(f13893,plain,
! [X0] : pls = hAPP(int,int,times_times(int,X0),pls),
inference(superposition,[],[f2786,f2848]) ).
fof(f13898,plain,
! [X0] : sF63 = hAPP(int,int,times_times(int,X0),sF63),
inference(forward_demodulation,[],[f13893,f4862]) ).
fof(f13907,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m)),sF51)),t)),sF63)),
inference(superposition,[],[f5444,f13898]) ).
fof(f13914,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13907,f5590]) ).
fof(f13915,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,ti(int,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13914,f5658]) ).
fof(f13916,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13915,f2747]) ).
fof(f13917,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,ti(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13916,f5658]) ).
fof(f13918,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13917,f2747]) ).
fof(f13919,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,ti(int,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13918,f5658]) ).
fof(f13920,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13919,f2747]) ).
fof(f13921,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,ti(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13920,f5658]) ).
fof(f13922,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13921,f2747]) ).
fof(f13923,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,ti(int,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13922,f5658]) ).
fof(f13924,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13923,f2747]) ).
fof(f13925,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,ti(int,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63))))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13924,f5658]) ).
fof(f13926,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,plus_plus(int,sF63),sF63)))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13925,f2747]) ).
fof(f13927,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,ti(int,sF63)))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13926,f5641]) ).
fof(f13928,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,sF63))))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13927,f2747]) ).
fof(f13929,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,sF53)))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13928,f5584]) ).
fof(f13930,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,hAPP(int,int,sF52,sF51)))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13929,f5616]) ).
fof(f13931,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,times_times(int,hAPP(int,int,sF52,hAPP(int,int,sF52,sF57))),m))),t)),sF63)),
inference(forward_demodulation,[],[f13930,f5629]) ).
fof(f13932,plain,
hBOOL(hAPP(int,bool,hAPP(int,sF48,sF49,sF61),sF63)),
inference(forward_demodulation,[],[f13931,f5807]) ).
fof(f13933,plain,
hBOOL(hAPP(int,bool,sF62,sF63)),
inference(forward_demodulation,[],[f13932,f4744]) ).
fof(f13934,plain,
hBOOL(sF64),
inference(forward_demodulation,[],[f13933,f4748]) ).
fof(f13935,plain,
$false,
inference(forward_subsumption_resolution,[],[f13934,f4749]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 21:41:17 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.68/2.84 % (197724)Detected formulas, will run a generic FOF schedule.
% 12.68/2.84 % (197730)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=246712150:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.68/2.84 % (197729)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4189999083:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.68/2.84 % (197731)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=613545226:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.68/2.84 % (197732)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3294985694:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.68/2.84 % (197735)dis-21_1_sil=8000:lcm=predicate:random_seed=2867312848:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 12.68/2.84 % (197733)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1850686306:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.68/2.84 % (197734)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4068193455:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.68/2.84 % (197732)Instruction limit reached!
% 12.68/2.84 % (197732)------------------------------
% 12.68/2.84 % (197732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197732)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197732)Termination reason: Instruction limit
% 12.68/2.84 % (197732)Termination phase: Saturation
% 12.68/2.84 % (197732)Time elapsed: 0.053 s
% 12.68/2.84 % (197732)Peak memory usage: 90 MB
% 12.68/2.84 % (197732)Instructions burned: 110 (million)
% 12.68/2.84 % (197735)Instruction limit reached!
% 12.68/2.84 % (197735)------------------------------
% 12.68/2.84 % (197735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197735)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197735)Termination reason: Instruction limit
% 12.68/2.84 % (197735)Termination phase: Property scanning
% 12.68/2.84 % (197735)Time elapsed: 0.055 s
% 12.68/2.84 % (197735)Peak memory usage: 88 MB
% 12.68/2.84 % (197735)Instructions burned: 132 (million)
% 12.68/2.84 % (197733)Instruction limit reached!
% 12.68/2.84 % (197733)------------------------------
% 12.68/2.84 % (197733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197733)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197733)Termination reason: Instruction limit
% 12.68/2.84 % (197733)Termination phase: Saturation
% 12.68/2.84 % (197733)Time elapsed: 0.055 s
% 12.68/2.84 % (197733)Peak memory usage: 89 MB
% 12.68/2.84 % (197733)Instructions burned: 120 (million)
% 12.68/2.84 % (197734)Instruction limit reached!
% 12.68/2.84 % (197734)------------------------------
% 12.68/2.84 % (197734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197734)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197734)Termination reason: Instruction limit
% 12.68/2.84 % (197734)Termination phase: Property scanning
% 12.68/2.84 % (197734)Time elapsed: 0.058 s
% 12.68/2.84 % (197734)Peak memory usage: 88 MB
% 12.68/2.84 % (197734)Instructions burned: 139 (million)
% 12.68/2.84 % (197744)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1183987677:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.68/2.84 % (197743)lrs+10_1_sil=8000:sp=occurrence:random_seed=4163465292:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 12.68/2.84 % (197745)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2609005361:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 12.68/2.84 % (197746)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3432464446:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 12.68/2.84 % (197744)Instruction limit reached!
% 12.68/2.84 % (197744)------------------------------
% 12.68/2.84 % (197744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197744)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197744)Termination reason: Instruction limit
% 12.68/2.84 % (197744)Termination phase: Saturation
% 12.68/2.84 % (197744)Time elapsed: 0.079 s
% 12.68/2.84 % (197744)Peak memory usage: 90 MB
% 12.68/2.84 % (197744)Instructions burned: 158 (million)
% 12.68/2.84 % (197743)Instruction limit reached!
% 12.68/2.84 % (197743)------------------------------
% 12.68/2.84 % (197743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197743)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197743)Termination reason: Instruction limit
% 12.68/2.84 % (197743)Termination phase: Saturation
% 12.68/2.84 % (197743)Time elapsed: 0.148 s
% 12.68/2.84 % (197743)Peak memory usage: 92 MB
% 12.68/2.84 % (197743)Instructions burned: 285 (million)
% 12.68/2.84 % (197746)Instruction limit reached!
% 12.68/2.84 % (197746)------------------------------
% 12.68/2.84 % (197746)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197746)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197746)Termination reason: Instruction limit
% 12.68/2.84 % (197746)Termination phase: Saturation
% 12.68/2.84 % (197746)Time elapsed: 0.127 s
% 12.68/2.84 % (197746)Peak memory usage: 91 MB
% 12.68/2.84 % (197746)Instructions burned: 249 (million)
% 12.68/2.84 % (197745)Instruction limit reached!
% 12.68/2.84 % (197745)------------------------------
% 12.68/2.84 % (197745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197745)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197745)Termination reason: Instruction limit
% 12.68/2.84 % (197745)Termination phase: Saturation
% 12.68/2.84 % (197745)Time elapsed: 0.182 s
% 12.68/2.84 % (197745)Peak memory usage: 92 MB
% 12.68/2.84 % (197745)Instructions burned: 325 (million)
% 12.68/2.84 % (197751)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1962548140:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.68/2.84 % (197753)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2107370124:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 12.68/2.84 % (197752)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2804014475:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 12.68/2.84 % (197753)Instruction limit reached!
% 12.68/2.84 % (197753)------------------------------
% 12.68/2.84 % (197753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197753)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197753)Termination reason: Instruction limit
% 12.68/2.84 % (197753)Termination phase: Property scanning
% 12.68/2.84 % (197753)Time elapsed: 0.049 s
% 12.68/2.84 % (197753)Peak memory usage: 88 MB
% 12.68/2.84 % (197753)Instructions burned: 115 (million)
% 12.68/2.84 % (197754)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3593412954:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 12.68/2.84 % (197751)Instruction limit reached!
% 12.68/2.84 % (197751)------------------------------
% 12.68/2.84 % (197751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197751)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197751)Termination reason: Instruction limit
% 12.68/2.84 % (197751)Termination phase: Saturation
% 12.68/2.84 % (197751)Time elapsed: 0.145 s
% 12.68/2.84 % (197751)Peak memory usage: 92 MB
% 12.68/2.84 % (197751)Instructions burned: 295 (million)
% 12.68/2.84 % (197754)Instruction limit reached!
% 12.68/2.84 % (197754)------------------------------
% 12.68/2.84 % (197754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197754)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197754)Termination reason: Instruction limit
% 12.68/2.84 % (197754)Termination phase: Property scanning
% 12.68/2.84 % (197754)Time elapsed: 0.052 s
% 12.68/2.84 % (197754)Peak memory usage: 88 MB
% 12.68/2.84 % (197754)Instructions burned: 130 (million)
% 12.68/2.84 % (197759)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1549085754:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 12.68/2.84 % (197760)lrs+10_1_sil=8000:sp=occurrence:random_seed=640873512:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 12.68/2.84 % (197759)Instruction limit reached!
% 12.68/2.84 % (197759)------------------------------
% 12.68/2.84 % (197759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197759)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197759)Termination reason: Instruction limit
% 12.68/2.84 % (197759)Termination phase: Saturation
% 12.68/2.84 % (197759)Time elapsed: 0.048 s
% 12.68/2.84 % (197759)Peak memory usage: 89 MB
% 12.68/2.84 % (197759)Instructions burned: 116 (million)
% 12.68/2.84 % (197761)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3215559761:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 12.68/2.84 % (197764)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1257314509:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 12.68/2.84 % (197761)Instruction limit reached!
% 12.68/2.84 % (197761)------------------------------
% 12.68/2.84 % (197761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197761)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197761)Termination reason: Instruction limit
% 12.68/2.84 % (197761)Termination phase: Saturation
% 12.68/2.84 % (197761)Time elapsed: 0.220 s
% 12.68/2.84 % (197761)Peak memory usage: 93 MB
% 12.68/2.84 % (197761)Instructions burned: 438 (million)
% 12.68/2.84 % (197767)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1686724833:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 12.68/2.84 % (197767)Instruction limit reached!
% 12.68/2.84 % (197767)------------------------------
% 12.68/2.84 % (197767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197767)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197767)Termination reason: Instruction limit
% 12.68/2.84 % (197767)Termination phase: Saturation
% 12.68/2.84 % (197767)Time elapsed: 0.057 s
% 12.68/2.84 % (197767)Peak memory usage: 89 MB
% 12.68/2.84 % (197767)Instructions burned: 136 (million)
% 12.68/2.84 % (197760)Instruction limit reached!
% 12.68/2.84 % (197760)------------------------------
% 12.68/2.84 % (197760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197760)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197760)Termination reason: Instruction limit
% 12.68/2.84 % (197760)Termination phase: Saturation
% 12.68/2.84 % (197760)Time elapsed: 0.510 s
% 12.68/2.84 % (197760)Peak memory usage: 97 MB
% 12.68/2.84 % (197760)Instructions burned: 908 (million)
% 12.68/2.84 % (197769)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1202138218:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 12.68/2.84 % (197770)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3903086014:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 12.68/2.84 % (197729)First to succeed.
% 12.68/2.84 % (197729)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-197724"
% 12.68/2.84 % (197731)Also succeeded, but the first one will report.
% 12.68/2.84 % (197769)Instruction limit reached!
% 12.68/2.84 % (197769)------------------------------
% 12.68/2.84 % (197769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.68/2.84 % (197769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.68/2.84 % (197769)CaDiCaL version: 2.1.3
% 12.68/2.84 % (197769)Termination reason: Instruction limit
% 12.68/2.84 % (197769)Termination phase: Saturation
% 12.68/2.84 % (197769)Time elapsed: 0.317 s
% 12.68/2.84 % (197769)Peak memory usage: 95 MB
% 12.68/2.84 % (197769)Instructions burned: 593 (million)
% 12.68/2.84 % (197729)Refutation found. Thanks to Tanya!
% 12.68/2.84 % SZS status Theorem for theBenchmark
% 12.68/2.84 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/3.04 % (197729)------------------------------
% 0.16/3.04 % (197729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.04 % (197729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.04 % (197729)CaDiCaL version: 2.1.3
% 0.16/3.04 % (197729)Termination reason: Refutation
% 0.16/3.04 % (197729)Time elapsed: 1.448 s
% 0.16/3.04 % (197729)Peak memory usage: 152 MB
% 0.16/3.04 % (197729)Instructions burned: 2529 (million)
% 0.16/3.04 % (197729)------------------------------
% 0.16/3.04 % (197729)------------------------------
% 0.16/3.04 % (197724)Success in time 1.977 s
% 0.16/3.04 % Vampire exiting
%------------------------------------------------------------------------------