Vampire-SAT---5.0.1.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire-SAT---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 SAT

% Computer : n003.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:26:08 PM UTC 2026

% Result   : Theorem 4.44s 1.19s
% Output   : Refutation 4.44s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   53
%            Number of leaves      :   17
% Syntax   : Number of formulae    :  148 ( 148 unt;   0 def)
%            Number of atoms       :  148 (  70 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :   54 (  54   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   2 avg)
%            Maximal term depth    :   19 (   3 avg)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :   19 (  19 usr;   7 con; 0-4 aty)
%            Number of variables   :   48 (  48   !;   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(f159,axiom,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_nat__1__add__1) ).

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(f195,axiom,
    ! [X0,X1,X2] : hAPP(int,int,plus_plus(int,X0),hAPP(int,int,plus_plus(int,X1),X2)) = hAPP(int,int,plus_plus(int,X1),hAPP(int,int,plus_plus(int,X0),X2)),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_zadd__left__commute) ).

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(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(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(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(f2364,plain,
    ! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
    inference(cnf_transformation,[],[f89]) ).

fof(f2365,plain,
    ! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = ti(X0,hAPP(X1,X0,X2,X3)),
    inference(cnf_transformation,[],[f90]) ).

fof(f2376,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(f2377,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(f2402,plain,
    ! [X0] : ti(int,X0) = number_number_of(int,X0),
    inference(cnf_transformation,[],[f120]) ).

fof(f2403,plain,
    ! [X0,X1] : hAPP(int,int,times_times(int,X0),X1) = hAPP(int,int,times_times(int,X1),X0),
    inference(cnf_transformation,[],[f121]) ).

fof(f2464,plain,
    number_number_of(nat,bit0(bit1(pls))) = hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)),
    inference(cnf_transformation,[],[f159]) ).

fof(f2465,plain,
    ! [X0] : pls = hAPP(int,int,times_times(int,pls),X0),
    inference(cnf_transformation,[],[f160]) ).

fof(f2518,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(f2519,plain,
    ! [X2,X0,X1] : hAPP(int,int,plus_plus(int,X0),hAPP(int,int,plus_plus(int,X1),X2)) = hAPP(int,int,plus_plus(int,X1),hAPP(int,int,plus_plus(int,X0),X2)),
    inference(cnf_transformation,[],[f195]) ).

fof(f2520,plain,
    ! [X0,X1] : hAPP(int,int,plus_plus(int,X0),X1) = hAPP(int,int,plus_plus(int,X1),X0),
    inference(cnf_transformation,[],[f196]) ).

fof(f2553,plain,
    pls = zero_zero(int),
    inference(cnf_transformation,[],[f220]) ).

fof(f2564,plain,
    ! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,X0),pls),
    inference(cnf_transformation,[],[f227]) ).

fof(f2565,plain,
    ! [X0] : ti(int,X0) = hAPP(int,int,plus_plus(int,pls),X0),
    inference(cnf_transformation,[],[f228]) ).

fof(f2567,plain,
    ! [X0] : bit0(X0) = hAPP(int,int,plus_plus(int,X0),X0),
    inference(cnf_transformation,[],[f230]) ).

fof(f2608,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(f3955,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(f3968,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,[],[f2376,f2567,f2567,f2608,f2567,f2567,f2608]) ).

fof(f3969,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,[],[f2377,f2567,f2567,f2608,f2567,f2608]) ).

fof(f4014,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = 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(definition_unfolding,[],[f2464,f2567,f2608]) ).

fof(f4221,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,[],[f3955,f2567,f2608]) ).

fof(f4329,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(consistent_polarity_flipping,[],[f3968]) ).

fof(f5501,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(consistent_polarity_flipping,[],[f4221]) ).

fof(f5573,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = 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)))),
    inference(forward_demodulation,[],[f4014,f2518]) ).

fof(f5609,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,one_one(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))))),
    inference(forward_demodulation,[],[f3969,f2520]) ).

fof(f5610,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,zero_zero(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))))),
    inference(forward_demodulation,[],[f4329,f2403]) ).

fof(f5636,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls))))),
    inference(forward_demodulation,[],[f5573,f2518]) ).

fof(f5665,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,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) = hAPP(int,int,plus_plus(int,one_one(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)))))),
    inference(forward_demodulation,[],[f5609,f2518]) ).

fof(f5666,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,one_one(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))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(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))))),
    inference(forward_demodulation,[],[f5610,f2520]) ).

fof(f5684,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),
    inference(forward_demodulation,[],[f5636,f2519]) ).

fof(f5709,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls))))),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls))))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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))))))),
    inference(forward_demodulation,[],[f5665,f2518]) ).

fof(f5710,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,one_one(int)),hAPP(int,int,times_times(int,m),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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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))))))))),
    inference(forward_demodulation,[],[f5666,f2403]) ).

fof(f5725,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),
    inference(forward_demodulation,[],[f5684,f2565]) ).

fof(f5750,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,pls),hAPP(int,int,plus_plus(int,one_one(int)),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,pls),hAPP(int,int,plus_plus(int,one_one(int)),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) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),
    inference(forward_demodulation,[],[f5709,f2519]) ).

fof(f5751,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,one_one(int)),hAPP(int,int,times_times(int,m),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,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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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,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))))))))),
    inference(forward_demodulation,[],[f5710,f2402]) ).

fof(f5765,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))),
    inference(forward_demodulation,[],[f5725,f2365]) ).

fof(f5790,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,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),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) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),
    inference(forward_demodulation,[],[f5750,f2565]) ).

fof(f5791,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,one_one(int)),hAPP(int,int,times_times(int,m),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)))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)))))))),
    inference(forward_demodulation,[],[f5751,f2364]) ).

fof(f5803,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))),
    inference(forward_demodulation,[],[f5765,f2519]) ).

fof(f5828,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),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) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),
    inference(forward_demodulation,[],[f5790,f2365]) ).

fof(f5829,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,one_one(int)),hAPP(int,int,times_times(int,m),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,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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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,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))))))))),
    inference(forward_demodulation,[],[f5791,f2518]) ).

fof(f5839,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))),
    inference(forward_demodulation,[],[f5803,f2565]) ).

fof(f5859,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,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),
    inference(forward_demodulation,[],[f5828,f2519]) ).

fof(f5860,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,one_one(int)),hAPP(int,int,times_times(int,m),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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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,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)))))))))),
    inference(forward_demodulation,[],[f5829,f2518]) ).

fof(f5870,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),
    inference(forward_demodulation,[],[f5839,f2365]) ).

fof(f5890,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,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),
    inference(forward_demodulation,[],[f5859,f2565]) ).

fof(f5891,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,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))))))))))),
    inference(forward_demodulation,[],[f5860,f2518]) ).

fof(f5901,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),pls)))),
    inference(forward_demodulation,[],[f5870,f2518]) ).

fof(f5920,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))),
    inference(forward_demodulation,[],[f5890,f2365]) ).

fof(f5921,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,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,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,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(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,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,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(forward_demodulation,[],[f5891,f2519]) ).

fof(f5931,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))),
    inference(forward_demodulation,[],[f5901,f2519]) ).

fof(f5950,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),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,pls),pls)))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),pls)))))),
    inference(forward_demodulation,[],[f5920,f2518]) ).

fof(f5951,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),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,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),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,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))))))))))),
    inference(forward_demodulation,[],[f5921,f2565]) ).

fof(f5954,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,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)),pls)))),
    inference(forward_demodulation,[],[f5931,f2519]) ).

fof(f5973,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))),
    inference(forward_demodulation,[],[f5950,f2519]) ).

fof(f5974,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,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)))))))))),
    inference(forward_demodulation,[],[f5951,f2364]) ).

fof(f5977,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))),
    inference(forward_demodulation,[],[f5954,f2565]) ).

fof(f5996,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,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))),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)),pls)))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,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)),pls)))))),
    inference(forward_demodulation,[],[f5973,f2519]) ).

fof(f5997,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,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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(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,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)))))))))),
    inference(forward_demodulation,[],[f5974,f2519]) ).

fof(f6000,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls))),
    inference(forward_demodulation,[],[f5977,f2365]) ).

fof(f6019,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,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))),
    inference(forward_demodulation,[],[f5996,f2565]) ).

fof(f6020,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(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,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(forward_demodulation,[],[f5997,f2565]) ).

fof(f6023,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),ti(int,one_one(int)))),
    inference(forward_demodulation,[],[f6000,f2564]) ).

fof(f6042,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls))),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls))))),
    inference(forward_demodulation,[],[f6019,f2365]) ).

fof(f6043,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(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,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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(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,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(forward_demodulation,[],[f6020,f2364]) ).

fof(f6046,plain,
    hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)) = number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),
    inference(forward_demodulation,[],[f6023,f2364]) ).

fof(f6065,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),ti(int,one_one(int)))),hAPP(int,int,plus_plus(int,one_one(int)),ti(int,one_one(int)))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),ti(int,one_one(int)))))),
    inference(forward_demodulation,[],[f6042,f2564]) ).

fof(f6066,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(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,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(forward_demodulation,[],[f6043,f2518]) ).

fof(f6087,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),
    inference(forward_demodulation,[],[f6065,f2364]) ).

fof(f6088,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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,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(forward_demodulation,[],[f6066,f2518]) ).

fof(f6096,plain,
    hAPP(int,int,times_times(int,hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),t) = hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))),
    inference(forward_demodulation,[],[f6087,f6046]) ).

fof(f6097,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6088,f2519]) ).

fof(f6103,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m)),one_one(int))),
    inference(forward_demodulation,[],[f6096,f2403]) ).

fof(f6104,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,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,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(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,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))))))))))),
    inference(forward_demodulation,[],[f6097,f2519]) ).

fof(f6110,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))),m))),
    inference(forward_demodulation,[],[f6103,f2520]) ).

fof(f6111,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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))))))))))),
    inference(forward_demodulation,[],[f6104,f2565]) ).

fof(f6125,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),number_number_of(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),
    inference(forward_demodulation,[],[f6110,f2403]) ).

fof(f6126,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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,one_one(int)),pls)),pls)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6111,f2364]) ).

fof(f6131,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))))))),
    inference(forward_demodulation,[],[f6125,f2402]) ).

fof(f6132,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(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)))))))))),
    inference(forward_demodulation,[],[f6126,f2519]) ).

fof(f6137,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int))),hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),
    inference(forward_demodulation,[],[f6131,f2364]) ).

fof(f6138,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,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,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(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,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(forward_demodulation,[],[f6132,f2519]) ).

fof(f6143,plain,
    hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat)))) = hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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))))))),
    inference(forward_demodulation,[],[f6137,f2518]) ).

fof(f6144,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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(forward_demodulation,[],[f6138,f2565]) ).

fof(f6149,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(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))))))))),
    inference(forward_demodulation,[],[f6144,f2364]) ).

fof(f6154,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(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)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(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)))))))))),
    inference(forward_demodulation,[],[f6149,f2518]) ).

fof(f6159,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),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,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),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,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6154,f2518]) ).

fof(f6164,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6159,f2519]) ).

fof(f6169,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6164,f2519]) ).

fof(f6174,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,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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6169,f2519]) ).

fof(f6179,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))))),
    inference(forward_demodulation,[],[f6174,f2565]) ).

fof(f6184,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6179,f2364]) ).

fof(f6189,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6184,f2519]) ).

fof(f6194,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6189,f2519]) ).

fof(f6199,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,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)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(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)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6194,f2519]) ).

fof(f6204,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))))),
    inference(forward_demodulation,[],[f6199,f2565]) ).

fof(f6209,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))))),
    inference(forward_demodulation,[],[f6204,f2364]) ).

fof(f6214,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),pls)))))))))),
    inference(forward_demodulation,[],[f6209,f2518]) ).

fof(f6219,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))))),
    inference(forward_demodulation,[],[f6214,f2519]) ).

fof(f6224,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),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)),pls)))))))))),
    inference(forward_demodulation,[],[f6219,f2519]) ).

fof(f6229,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,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),hAPP(int,int,plus_plus(int,one_one(int)),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)),pls)))))))))),
    inference(forward_demodulation,[],[f6224,f2519]) ).

fof(f6234,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,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)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(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)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))))),
    inference(forward_demodulation,[],[f6229,f2519]) ).

fof(f6239,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,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))))))),
    inference(forward_demodulation,[],[f6234,f2565]) ).

fof(f6244,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,one_one(int)),pls))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),hAPP(int,int,plus_plus(int,one_one(int)),pls))))))))),
    inference(forward_demodulation,[],[f6239,f2364]) ).

fof(f6249,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,one_one(int)),hAPP(int,int,times_times(int,m),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)),ti(int,one_one(int)))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)),ti(int,one_one(int)))))))))),
    inference(forward_demodulation,[],[f6244,f2564]) ).

fof(f6252,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,one_one(int)),hAPP(int,int,times_times(int,m),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))))))),t)),hAPP(int,int,times_times(int,zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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))))))))),
    inference(forward_demodulation,[],[f6249,f2364]) ).

fof(f6254,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,one_one(int)),hAPP(int,int,times_times(int,m),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))))))),t)),hAPP(int,int,times_times(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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))))))))),
    inference(forward_demodulation,[],[f6252,f2553]) ).

fof(f6256,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,one_one(int)),hAPP(int,int,times_times(int,m),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))))))),t)),pls)),
    inference(forward_demodulation,[],[f6254,f2465]) ).

fof(f6258,plain,
    ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,times_times(int,t),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,times_times(int,m),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)))))))),pls)),
    inference(forward_demodulation,[],[f6256,f2403]) ).

fof(f6260,plain,
    ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat))))),pls)),
    inference(forward_demodulation,[],[f6258,f6143]) ).

fof(f6365,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))),pls)),
    inference(superposition,[],[f5501,f2553]) ).

fof(f6366,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(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)))))),pls)),
    inference(forward_demodulation,[],[f6365,f2520]) ).

fof(f6367,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(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))))))),pls)),
    inference(forward_demodulation,[],[f6366,f2518]) ).

fof(f6368,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,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)))))))),pls)),
    inference(forward_demodulation,[],[f6367,f2518]) ).

fof(f6369,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),pls)),
    inference(forward_demodulation,[],[f6368,f2519]) ).

fof(f6370,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))))),pls)),
    inference(forward_demodulation,[],[f6369,f2565]) ).

fof(f6371,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6370,f2365]) ).

fof(f6372,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6371,f2519]) ).

fof(f6373,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6372,f2565]) ).

fof(f6374,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,hAPP(int,int,plus_plus(int,one_one(int)),pls)),pls)))))),pls)),
    inference(forward_demodulation,[],[f6373,f2365]) ).

fof(f6375,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),pls))))))),pls)),
    inference(forward_demodulation,[],[f6374,f2518]) ).

fof(f6376,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,pls),hAPP(int,int,plus_plus(int,one_one(int)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6375,f2519]) ).

fof(f6377,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,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)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6376,f2519]) ).

fof(f6378,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,ti(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls))))))),pls)),
    inference(forward_demodulation,[],[f6377,f2565]) ).

fof(f6379,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(int,int,plus_plus(int,one_one(int)),pls)))))),pls)),
    inference(forward_demodulation,[],[f6378,f2365]) ).

fof(f6380,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),ti(int,one_one(int))))))),pls)),
    inference(forward_demodulation,[],[f6379,f2564]) ).

fof(f6381,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),number_number_of(nat,hAPP(int,int,plus_plus(int,one_one(int)),one_one(int)))))),pls)),
    inference(forward_demodulation,[],[f6380,f2364]) ).

fof(f6382,plain,
    hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,power_power(int,s),hAPP(nat,nat,plus_plus(nat,one_one(nat)),one_one(nat))))),pls)),
    inference(forward_demodulation,[],[f6381,f6046]) ).

fof(f6383,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f6382,f6260]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : NUM924+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39  % Computer : n003.cluster.edu
% 0.11/0.39  % Model    : x86_64 x86_64
% 0.11/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39  % Memory   : 8046.5625MB
% 0.11/0.39  % OS       : Linux 6.8.0-71-generic
% 0.11/0.39  % CPULimit : 300
% 0.11/0.39  % WCLimit  : 300
% 0.11/0.39  % DateTime : Sun Sep 27 21:43:11 UTC 2026
% 0.11/0.39  % CPUTime  : 
% 0.11/0.39  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43  Running first-order model finding
% 0.11/0.43  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.44/1.19  % (942813)Will run a generic schedule for satisfiability detection.
% 4.44/1.19  % (942823)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3789762848:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.44/1.19  % (942818)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3657278041_2999 on theBenchmark for (2999ds/0Mi)
% 4.44/1.19  % (942820)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3517078290:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.44/1.19  % (942821)dis+10_1_sil=32000:sp=arity:random_seed=1793728529:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.44/1.19  % (942822)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1889924006:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.44/1.19  % (942824)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=929599382:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.44/1.19  % (942819)% WARNING: option uhcvi not known.
% 4.44/1.19  % (942819)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=300940988:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.44/1.19  % (942823)Instruction limit reached! 
% 4.44/1.19  % (942823)------------------------------
% 4.44/1.19  % (942823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942823)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942823)Termination reason: Instruction limit
% 4.44/1.19  % (942823)Termination phase: Property scanning
% 4.44/1.19  % (942823)Time elapsed: 0.030 s
% 4.44/1.19  % (942823)Peak memory usage: 13 MB
% 4.44/1.19  % (942823)Instructions burned: 133 (million)
% 4.44/1.19  % (942832)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3283713872:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 4.44/1.19  % (942821)Instruction limit reached! 
% 4.44/1.19  % (942821)------------------------------
% 4.44/1.19  % (942821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942821)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942821)Termination reason: Instruction limit
% 4.44/1.19  % (942821)Termination phase: Property scanning
% 4.44/1.19  % (942821)Time elapsed: 0.046 s
% 4.44/1.19  % (942821)Peak memory usage: 13 MB
% 4.44/1.19  % (942821)Instructions burned: 106 (million)
% 4.44/1.19  % (942822)Instruction limit reached! 
% 4.44/1.19  % (942822)------------------------------
% 4.44/1.19  % (942822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942822)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942822)Termination reason: Instruction limit
% 4.44/1.19  % (942822)Termination phase: Property scanning
% 4.44/1.19  % (942822)Time elapsed: 0.051 s
% 4.44/1.19  % (942822)Peak memory usage: 13 MB
% 4.44/1.19  % (942822)Instructions burned: 118 (million)
% 4.44/1.19  % (942834)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2504306112:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.44/1.19  % (942824)Instruction limit reached! 
% 4.44/1.19  % (942824)------------------------------
% 4.44/1.19  % (942824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942824)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942824)Termination reason: Instruction limit
% 4.44/1.19  % (942824)Termination phase: Saturation
% 4.44/1.19  % (942824)Time elapsed: 0.069 s
% 4.44/1.19  % (942824)Peak memory usage: 14 MB
% 4.44/1.19  % (942824)Instructions burned: 161 (million)
% 4.44/1.19  % (942835)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2432815689:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.44/1.19  % (942837)ott-21_1_sil=16000:fs=off:random_seed=2798497579:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.44/1.19  % (942834)Instruction limit reached! 
% 4.44/1.19  % (942834)------------------------------
% 4.44/1.19  % (942834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942834)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942834)Termination reason: Instruction limit
% 4.44/1.19  % (942834)Termination phase: Property scanning
% 4.44/1.19  % (942834)Time elapsed: 0.055 s
% 4.44/1.19  % (942834)Peak memory usage: 13 MB
% 4.44/1.19  % (942834)Instructions burned: 132 (million)
% 4.44/1.19  % (942840)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2601840292:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 4.44/1.19  % (942837)Instruction limit reached! 
% 4.44/1.19  % (942837)------------------------------
% 4.44/1.19  % (942837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942837)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942837)Termination reason: Instruction limit
% 4.44/1.19  % (942837)Termination phase: Saturation
% 4.44/1.19  % (942837)Time elapsed: 0.076 s
% 4.44/1.19  % (942837)Peak memory usage: 14 MB
% 4.44/1.19  % (942837)Instructions burned: 181 (million)
% 4.44/1.19  % (942842)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=613704797:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.44/1.19  % (942832)Instruction limit reached! 
% 4.44/1.19  % (942832)------------------------------
% 4.44/1.19  % (942832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942832)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942832)Termination reason: Instruction limit
% 4.44/1.19  % (942832)Termination phase: Finite model building preprocessing
% 4.44/1.19  % (942832)Time elapsed: 0.178 s
% 4.44/1.19  % (942832)Peak memory usage: 19 MB
% 4.44/1.19  % (942832)Instructions burned: 717 (million)
% 4.44/1.19  % (942844)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3036311088:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 4.44/1.19  % (942840)Instruction limit reached! 
% 4.44/1.19  % (942840)------------------------------
% 4.44/1.19  % (942840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942840)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942840)Termination reason: Instruction limit
% 4.44/1.19  % (942840)Termination phase: Saturation
% 4.44/1.19  % (942840)Time elapsed: 0.265 s
% 4.44/1.19  % (942840)Peak memory usage: 16 MB
% 4.44/1.19  % (942840)Instructions burned: 477 (million)
% 4.44/1.19  % (942846)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4198779498:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 4.44/1.19  % (942835)Instruction limit reached! 
% 4.44/1.19  % (942835)------------------------------
% 4.44/1.19  % (942835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942835)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942835)Termination reason: Instruction limit
% 4.44/1.19  % (942835)Termination phase: Saturation
% 4.44/1.19  % (942835)Time elapsed: 0.370 s
% 4.44/1.19  % (942835)Peak memory usage: 19 MB
% 4.44/1.19  % (942835)Instructions burned: 684 (million)
% 4.44/1.19  % (942848)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3623590080:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 4.44/1.19  % (942844)Instruction limit reached! 
% 4.44/1.19  % (942844)------------------------------
% 4.44/1.19  % (942844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942844)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942844)Termination reason: Instruction limit
% 4.44/1.19  % (942844)Termination phase: Saturation
% 4.44/1.19  % (942844)Time elapsed: 0.332 s
% 4.44/1.19  % (942844)Peak memory usage: 22 MB
% 4.44/1.19  % (942844)Instructions burned: 1183 (million)
% 4.44/1.19  % (942850)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=647002337:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.44/1.19  % (942842)Instruction limit reached! 
% 4.44/1.19  % (942842)------------------------------
% 4.44/1.19  % (942842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942842)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942842)Termination reason: Instruction limit
% 4.44/1.19  % (942842)Termination phase: Finite model building preprocessing
% 4.44/1.19  % (942842)Time elapsed: 0.407 s
% 4.44/1.19  % (942842)Peak memory usage: 19 MB
% 4.44/1.19  % (942842)Instructions burned: 865 (million)
% 4.44/1.19  % (942852)fmb+10_1_sil=64000:random_seed=1899656081:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 4.44/1.19  % (942848) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-942813-942848"...
% 4.44/1.19  % (942848)...printing done.
% 4.44/1.19  % (942848)Refutation found. Thanks to Tanya!
% 4.44/1.19  % SZS status Theorem for theBenchmark
% 4.44/1.19  % SZS output start Proof for theBenchmark
% See solution above
% 4.44/1.19  % (942848)------------------------------
% 4.44/1.19  % (942848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.44/1.19  % (942848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.44/1.19  % (942848)CaDiCaL version: 2.1.3
% 4.44/1.19  % (942848)Termination reason: Refutation
% 4.44/1.19  % (942848)Time elapsed: 0.172 s
% 4.44/1.19  % (942848)Peak memory usage: 18 MB
% 4.44/1.19  % (942848)Instructions burned: 346 (million)
% 4.44/1.19  % (942813)Success in time 0.752 s
% 4.44/1.19  % Vampire exiting
%------------------------------------------------------------------------------