Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n007.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 01:08:06 PM UTC 2026

% Result   : Theorem 1.63s 0.90s
% Output   : Refutation 3.63s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   86
%            Number of leaves      :   54
% Syntax   : Number of formulae    :  356 (  79 unt;  46 def)
%            Number of atoms       : 1516 ( 282 equ)
%            Maximal formula atoms :   36 (   4 avg)
%            Number of connectives : 1478 ( 318   ~;1033   |;  99   &)
%                                         (  25 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   37 (   5 avg)
%            Maximal term depth    :    8 (   2 avg)
%            Number of predicates  :   48 (  46 usr;  26 prp; 0-2 aty)
%            Number of functors    :   16 (  16 usr;  12 con; 0-3 aty)
%            Number of variables   :   30 (   0 sgn  30   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f48,axiom,
    ! [X0,X1,X2] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_1) ).

fof(f49,axiom,
    ! [X0,X1,X2,X3,X4] :
      ( ( X0 != X1
        & a_select2(X2,X1) = X3 )
     => a_select2(tptp_update2(X2,X0,X4),X1) = X3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',sel2_update_2) ).

fof(f53,conjecture,
    ( ( a_select2(rho_defuse,n0) = use
      & a_select2(rho_defuse,n1) = use
      & a_select2(rho_defuse,n2) = use
      & a_select2(sigma_defuse,n0) = use
      & a_select2(sigma_defuse,n1) = use
      & a_select2(sigma_defuse,n2) = use
      & a_select2(sigma_defuse,n3) = use
      & a_select2(sigma_defuse,n4) = use
      & a_select2(sigma_defuse,n5) = use
      & a_select3(u_defuse,n0,n0) = use
      & a_select3(u_defuse,n1,n0) = use
      & a_select3(u_defuse,n2,n0) = use
      & a_select2(xinit_defuse,n3) = use
      & a_select2(xinit_defuse,n4) = use
      & a_select2(xinit_defuse,n5) = use )
   => ( a_select2(rho_defuse,n0) = use
      & a_select2(rho_defuse,n1) = use
      & a_select2(rho_defuse,n2) = use
      & a_select2(sigma_defuse,n0) = use
      & a_select2(sigma_defuse,n1) = use
      & a_select2(sigma_defuse,n2) = use
      & a_select2(sigma_defuse,n3) = use
      & a_select2(sigma_defuse,n4) = use
      & a_select2(sigma_defuse,n5) = use
      & a_select3(u_defuse,n0,n0) = use
      & a_select3(u_defuse,n1,n0) = use
      & a_select3(u_defuse,n2,n0) = use
      & a_select2(xinit_defuse,n3) = use
      & a_select2(xinit_defuse,n4) = use
      & a_select2(xinit_defuse,n5) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use
      & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',quaternion_ds1_inuse_0002) ).

fof(f54,negated_conjecture,
    ~ ( ( a_select2(rho_defuse,n0) = use
        & a_select2(rho_defuse,n1) = use
        & a_select2(rho_defuse,n2) = use
        & a_select2(sigma_defuse,n0) = use
        & a_select2(sigma_defuse,n1) = use
        & a_select2(sigma_defuse,n2) = use
        & a_select2(sigma_defuse,n3) = use
        & a_select2(sigma_defuse,n4) = use
        & a_select2(sigma_defuse,n5) = use
        & a_select3(u_defuse,n0,n0) = use
        & a_select3(u_defuse,n1,n0) = use
        & a_select3(u_defuse,n2,n0) = use
        & a_select2(xinit_defuse,n3) = use
        & a_select2(xinit_defuse,n4) = use
        & a_select2(xinit_defuse,n5) = use )
     => ( a_select2(rho_defuse,n0) = use
        & a_select2(rho_defuse,n1) = use
        & a_select2(rho_defuse,n2) = use
        & a_select2(sigma_defuse,n0) = use
        & a_select2(sigma_defuse,n1) = use
        & a_select2(sigma_defuse,n2) = use
        & a_select2(sigma_defuse,n3) = use
        & a_select2(sigma_defuse,n4) = use
        & a_select2(sigma_defuse,n5) = use
        & a_select3(u_defuse,n0,n0) = use
        & a_select3(u_defuse,n1,n0) = use
        & a_select3(u_defuse,n2,n0) = use
        & a_select2(xinit_defuse,n3) = use
        & a_select2(xinit_defuse,n4) = use
        & a_select2(xinit_defuse,n5) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4) = use
        & a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) = use ) ),
    inference(negated_conjecture,[status(cth)],[f53]) ).

fof(f82,axiom,
    succ(succ(succ(succ(n0)))) = n4,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4) ).

fof(f83,axiom,
    succ(succ(succ(succ(succ(n0))))) = n5,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5) ).

fof(f84,axiom,
    succ(n0) = n1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1) ).

fof(f85,axiom,
    succ(succ(n0)) = n2,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2) ).

fof(f86,axiom,
    succ(succ(succ(n0))) = n3,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3) ).

fof(f102,plain,
    ( ( use != a_select2(rho_defuse,n0)
      | use != a_select2(rho_defuse,n1)
      | use != a_select2(rho_defuse,n2)
      | use != a_select2(sigma_defuse,n0)
      | use != a_select2(sigma_defuse,n1)
      | use != a_select2(sigma_defuse,n2)
      | use != a_select2(sigma_defuse,n3)
      | use != a_select2(sigma_defuse,n4)
      | use != a_select2(sigma_defuse,n5)
      | use != a_select3(u_defuse,n0,n0)
      | use != a_select3(u_defuse,n1,n0)
      | use != a_select3(u_defuse,n2,n0)
      | use != a_select2(xinit_defuse,n3)
      | use != a_select2(xinit_defuse,n4)
      | use != a_select2(xinit_defuse,n5)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) )
    & a_select2(rho_defuse,n0) = use
    & a_select2(rho_defuse,n1) = use
    & a_select2(rho_defuse,n2) = use
    & a_select2(sigma_defuse,n0) = use
    & a_select2(sigma_defuse,n1) = use
    & a_select2(sigma_defuse,n2) = use
    & a_select2(sigma_defuse,n3) = use
    & a_select2(sigma_defuse,n4) = use
    & a_select2(sigma_defuse,n5) = use
    & a_select3(u_defuse,n0,n0) = use
    & a_select3(u_defuse,n1,n0) = use
    & a_select3(u_defuse,n2,n0) = use
    & a_select2(xinit_defuse,n3) = use
    & a_select2(xinit_defuse,n4) = use
    & a_select2(xinit_defuse,n5) = use ),
    inference(ennf_transformation,[],[f54]) ).

fof(f103,plain,
    ( ( use != a_select2(rho_defuse,n0)
      | use != a_select2(rho_defuse,n1)
      | use != a_select2(rho_defuse,n2)
      | use != a_select2(sigma_defuse,n0)
      | use != a_select2(sigma_defuse,n1)
      | use != a_select2(sigma_defuse,n2)
      | use != a_select2(sigma_defuse,n3)
      | use != a_select2(sigma_defuse,n4)
      | use != a_select2(sigma_defuse,n5)
      | use != a_select3(u_defuse,n0,n0)
      | use != a_select3(u_defuse,n1,n0)
      | use != a_select3(u_defuse,n2,n0)
      | use != a_select2(xinit_defuse,n3)
      | use != a_select2(xinit_defuse,n4)
      | use != a_select2(xinit_defuse,n5)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
      | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) )
    & a_select2(rho_defuse,n0) = use
    & a_select2(rho_defuse,n1) = use
    & a_select2(rho_defuse,n2) = use
    & a_select2(sigma_defuse,n0) = use
    & a_select2(sigma_defuse,n1) = use
    & a_select2(sigma_defuse,n2) = use
    & a_select2(sigma_defuse,n3) = use
    & a_select2(sigma_defuse,n4) = use
    & a_select2(sigma_defuse,n5) = use
    & a_select3(u_defuse,n0,n0) = use
    & a_select3(u_defuse,n1,n0) = use
    & a_select3(u_defuse,n2,n0) = use
    & a_select2(xinit_defuse,n3) = use
    & a_select2(xinit_defuse,n4) = use
    & a_select2(xinit_defuse,n5) = use ),
    inference(flattening,[],[f102]) ).

fof(f116,plain,
    ! [X0,X1,X2,X3,X4] :
      ( a_select2(tptp_update2(X2,X0,X4),X1) = X3
      | X0 = X1
      | a_select2(X2,X1) != X3 ),
    inference(ennf_transformation,[],[f49]) ).

fof(f117,plain,
    ! [X0,X1,X2,X3,X4] :
      ( a_select2(tptp_update2(X2,X0,X4),X1) = X3
      | X0 = X1
      | a_select2(X2,X1) != X3 ),
    inference(flattening,[],[f116]) ).

fof(f119,plain,
    use = a_select2(xinit_defuse,n5),
    inference(cnf_transformation,[],[f103]) ).

fof(f120,plain,
    use = a_select2(xinit_defuse,n4),
    inference(cnf_transformation,[],[f103]) ).

fof(f121,plain,
    use = a_select2(xinit_defuse,n3),
    inference(cnf_transformation,[],[f103]) ).

fof(f122,plain,
    use = a_select3(u_defuse,n2,n0),
    inference(cnf_transformation,[],[f103]) ).

fof(f123,plain,
    use = a_select3(u_defuse,n1,n0),
    inference(cnf_transformation,[],[f103]) ).

fof(f124,plain,
    use = a_select3(u_defuse,n0,n0),
    inference(cnf_transformation,[],[f103]) ).

fof(f125,plain,
    use = a_select2(sigma_defuse,n5),
    inference(cnf_transformation,[],[f103]) ).

fof(f126,plain,
    use = a_select2(sigma_defuse,n4),
    inference(cnf_transformation,[],[f103]) ).

fof(f127,plain,
    use = a_select2(sigma_defuse,n3),
    inference(cnf_transformation,[],[f103]) ).

fof(f128,plain,
    use = a_select2(sigma_defuse,n2),
    inference(cnf_transformation,[],[f103]) ).

fof(f129,plain,
    use = a_select2(sigma_defuse,n1),
    inference(cnf_transformation,[],[f103]) ).

fof(f130,plain,
    use = a_select2(sigma_defuse,n0),
    inference(cnf_transformation,[],[f103]) ).

fof(f131,plain,
    use = a_select2(rho_defuse,n2),
    inference(cnf_transformation,[],[f103]) ).

fof(f132,plain,
    use = a_select2(rho_defuse,n1),
    inference(cnf_transformation,[],[f103]) ).

fof(f133,plain,
    use = a_select2(rho_defuse,n0),
    inference(cnf_transformation,[],[f103]) ).

fof(f134,plain,
    ( use != a_select2(rho_defuse,n0)
    | use != a_select2(rho_defuse,n1)
    | use != a_select2(rho_defuse,n2)
    | use != a_select2(sigma_defuse,n0)
    | use != a_select2(sigma_defuse,n1)
    | use != a_select2(sigma_defuse,n2)
    | use != a_select2(sigma_defuse,n3)
    | use != a_select2(sigma_defuse,n4)
    | use != a_select2(sigma_defuse,n5)
    | use != a_select3(u_defuse,n0,n0)
    | use != a_select3(u_defuse,n1,n0)
    | use != a_select3(u_defuse,n2,n0)
    | use != a_select2(xinit_defuse,n3)
    | use != a_select2(xinit_defuse,n4)
    | use != a_select2(xinit_defuse,n5)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4)
    | use != a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5) ),
    inference(cnf_transformation,[],[f103]) ).

fof(f135,plain,
    n1 = succ(n0),
    inference(cnf_transformation,[],[f84]) ).

fof(f137,plain,
    n2 = succ(succ(n0)),
    inference(cnf_transformation,[],[f85]) ).

fof(f139,plain,
    n3 = succ(succ(succ(n0))),
    inference(cnf_transformation,[],[f86]) ).

fof(f141,plain,
    n4 = succ(succ(succ(succ(n0)))),
    inference(cnf_transformation,[],[f82]) ).

fof(f143,plain,
    n5 = succ(succ(succ(succ(succ(n0))))),
    inference(cnf_transformation,[],[f83]) ).

fof(f148,plain,
    ! [X2,X3,X0,X1,X4] :
      ( a_select2(tptp_update2(X2,X0,X4),X1) = X3
      | X0 = X1
      | a_select2(X2,X1) != X3 ),
    inference(cnf_transformation,[],[f117]) ).

fof(f149,plain,
    ! [X2,X0,X1] : a_select2(tptp_update2(X0,X1,X2),X1) = X2,
    inference(cnf_transformation,[],[f48]) ).

fof(f150,definition,
    ~ sP1(use),
    introduced(definition,[new_symbols(definition,[sP1])],[inequality_splitting_name_introduction]) ).

fof(f151,definition,
    ~ sP2(use),
    introduced(definition,[new_symbols(definition,[sP2])],[inequality_splitting_name_introduction]) ).

fof(f152,definition,
    ~ sP3(use),
    introduced(definition,[new_symbols(definition,[sP3])],[inequality_splitting_name_introduction]) ).

fof(f153,definition,
    ~ sP4(use),
    introduced(definition,[new_symbols(definition,[sP4])],[inequality_splitting_name_introduction]) ).

fof(f154,definition,
    ~ sP5(use),
    introduced(definition,[new_symbols(definition,[sP5])],[inequality_splitting_name_introduction]) ).

fof(f155,definition,
    ~ sP6(use),
    introduced(definition,[new_symbols(definition,[sP6])],[inequality_splitting_name_introduction]) ).

fof(f156,definition,
    ~ sP7(use),
    introduced(definition,[new_symbols(definition,[sP7])],[inequality_splitting_name_introduction]) ).

fof(f157,definition,
    ~ sP8(use),
    introduced(definition,[new_symbols(definition,[sP8])],[inequality_splitting_name_introduction]) ).

fof(f158,definition,
    ~ sP9(use),
    introduced(definition,[new_symbols(definition,[sP9])],[inequality_splitting_name_introduction]) ).

fof(f159,definition,
    ~ sP10(use),
    introduced(definition,[new_symbols(definition,[sP10])],[inequality_splitting_name_introduction]) ).

fof(f160,definition,
    ~ sP11(use),
    introduced(definition,[new_symbols(definition,[sP11])],[inequality_splitting_name_introduction]) ).

fof(f161,definition,
    ~ sP12(use),
    introduced(definition,[new_symbols(definition,[sP12])],[inequality_splitting_name_introduction]) ).

fof(f162,definition,
    ~ sP13(use),
    introduced(definition,[new_symbols(definition,[sP13])],[inequality_splitting_name_introduction]) ).

fof(f163,definition,
    ~ sP14(use),
    introduced(definition,[new_symbols(definition,[sP14])],[inequality_splitting_name_introduction]) ).

fof(f164,definition,
    ~ sP15(use),
    introduced(definition,[new_symbols(definition,[sP15])],[inequality_splitting_name_introduction]) ).

fof(f165,definition,
    ~ sP16(use),
    introduced(definition,[new_symbols(definition,[sP16])],[inequality_splitting_name_introduction]) ).

fof(f166,definition,
    ~ sP17(use),
    introduced(definition,[new_symbols(definition,[sP17])],[inequality_splitting_name_introduction]) ).

fof(f167,definition,
    ~ sP18(use),
    introduced(definition,[new_symbols(definition,[sP18])],[inequality_splitting_name_introduction]) ).

fof(f168,definition,
    ~ sP19(use),
    introduced(definition,[new_symbols(definition,[sP19])],[inequality_splitting_name_introduction]) ).

fof(f169,definition,
    ~ sP20(use),
    introduced(definition,[new_symbols(definition,[sP20])],[inequality_splitting_name_introduction]) ).

fof(f170,definition,
    ~ sP21(use),
    introduced(definition,[new_symbols(definition,[sP21])],[inequality_splitting_name_introduction]) ).

fof(f171,plain,
    ( sP1(a_select2(rho_defuse,n0))
    | sP2(a_select2(rho_defuse,n1))
    | sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(inequality_splitting,[],[f134,f170,f169,f168,f167,f166,f165,f164,f163,f162,f161,f160,f159,f158,f157,f156,f155,f154,f153,f152,f151,f150]) ).

fof(f172,plain,
    ! [X2,X0,X1,X4] :
      ( a_select2(X2,X1) = a_select2(tptp_update2(X2,X0,X4),X1)
      | X0 = X1 ),
    inference(equality_resolution,[],[f148]) ).

fof(f173,plain,
    use = a_select2(xinit_defuse,succ(succ(succ(succ(succ(n0)))))),
    inference(forward_demodulation,[],[f119,f143]) ).

fof(f174,plain,
    use = a_select2(xinit_defuse,succ(succ(succ(succ(n0))))),
    inference(forward_demodulation,[],[f120,f141]) ).

fof(f175,plain,
    use = a_select2(xinit_defuse,succ(succ(succ(n0)))),
    inference(forward_demodulation,[],[f121,f139]) ).

fof(f176,plain,
    use = a_select3(u_defuse,succ(succ(n0)),n0),
    inference(forward_demodulation,[],[f122,f137]) ).

fof(f177,plain,
    use = a_select3(u_defuse,succ(n0),n0),
    inference(forward_demodulation,[],[f123,f135]) ).

fof(f178,plain,
    use = a_select2(sigma_defuse,succ(succ(succ(succ(succ(n0)))))),
    inference(forward_demodulation,[],[f125,f143]) ).

fof(f179,plain,
    use = a_select2(sigma_defuse,succ(succ(succ(succ(n0))))),
    inference(forward_demodulation,[],[f126,f141]) ).

fof(f180,plain,
    use = a_select2(sigma_defuse,succ(succ(succ(n0)))),
    inference(forward_demodulation,[],[f127,f139]) ).

fof(f181,plain,
    use = a_select2(sigma_defuse,succ(succ(n0))),
    inference(forward_demodulation,[],[f128,f137]) ).

fof(f182,plain,
    use = a_select2(sigma_defuse,succ(n0)),
    inference(forward_demodulation,[],[f129,f135]) ).

fof(f183,plain,
    use = a_select2(rho_defuse,succ(succ(n0))),
    inference(forward_demodulation,[],[f131,f137]) ).

fof(f184,plain,
    use = a_select2(rho_defuse,succ(n0)),
    inference(forward_demodulation,[],[f132,f135]) ).

fof(f185,plain,
    ( sP1(use)
    | sP2(a_select2(rho_defuse,n1))
    | sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f171,f133]) ).

fof(f186,plain,
    ( sP2(a_select2(rho_defuse,n1))
    | sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f185,f150]) ).

fof(f187,plain,
    ( sP2(a_select2(rho_defuse,succ(n0)))
    | sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f186,f135]) ).

fof(f188,plain,
    ( sP2(use)
    | sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f187,f184]) ).

fof(f189,plain,
    ( sP3(a_select2(rho_defuse,n2))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f188,f151]) ).

fof(f190,plain,
    ( sP3(a_select2(rho_defuse,succ(succ(n0))))
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f189,f137]) ).

fof(f191,plain,
    ( sP3(use)
    | sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f190,f183]) ).

fof(f192,plain,
    ( sP4(a_select2(sigma_defuse,n0))
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f191,f152]) ).

fof(f193,plain,
    ( sP4(use)
    | sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f192,f130]) ).

fof(f194,plain,
    ( sP5(a_select2(sigma_defuse,n1))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f193,f153]) ).

fof(f195,plain,
    ( sP5(a_select2(sigma_defuse,succ(n0)))
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f194,f135]) ).

fof(f196,plain,
    ( sP5(use)
    | sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f195,f182]) ).

fof(f197,plain,
    ( sP6(a_select2(sigma_defuse,n2))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f196,f154]) ).

fof(f198,plain,
    ( sP6(a_select2(sigma_defuse,succ(succ(n0))))
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f197,f137]) ).

fof(f199,plain,
    ( sP6(use)
    | sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f198,f181]) ).

fof(f200,plain,
    ( sP7(a_select2(sigma_defuse,n3))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f199,f155]) ).

fof(f201,plain,
    ( sP7(a_select2(sigma_defuse,succ(succ(succ(n0)))))
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f200,f139]) ).

fof(f202,plain,
    ( sP7(use)
    | sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f201,f180]) ).

fof(f203,plain,
    ( sP8(a_select2(sigma_defuse,n4))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f202,f156]) ).

fof(f204,plain,
    ( sP8(a_select2(sigma_defuse,succ(succ(succ(succ(n0))))))
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f203,f141]) ).

fof(f205,plain,
    ( sP8(use)
    | sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f204,f179]) ).

fof(f206,plain,
    ( sP9(a_select2(sigma_defuse,n5))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f205,f157]) ).

fof(f207,plain,
    ( sP9(a_select2(sigma_defuse,succ(succ(succ(succ(succ(n0)))))))
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f206,f143]) ).

fof(f208,plain,
    ( sP9(use)
    | sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f207,f178]) ).

fof(f209,plain,
    ( sP10(a_select3(u_defuse,n0,n0))
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f208,f158]) ).

fof(f210,plain,
    ( sP10(use)
    | sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f209,f124]) ).

fof(f211,plain,
    ( sP11(a_select3(u_defuse,n1,n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f210,f159]) ).

fof(f212,plain,
    ( sP11(a_select3(u_defuse,succ(n0),n0))
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f211,f135]) ).

fof(f213,plain,
    ( sP11(use)
    | sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f212,f177]) ).

fof(f214,plain,
    ( sP12(a_select3(u_defuse,n2,n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f213,f160]) ).

fof(f215,plain,
    ( sP12(a_select3(u_defuse,succ(succ(n0)),n0))
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f214,f137]) ).

fof(f216,plain,
    ( sP12(use)
    | sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f215,f176]) ).

fof(f217,plain,
    ( sP13(a_select2(xinit_defuse,n3))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f216,f161]) ).

fof(f218,plain,
    ( sP13(a_select2(xinit_defuse,succ(succ(succ(n0)))))
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f217,f139]) ).

fof(f219,plain,
    ( sP13(use)
    | sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f218,f175]) ).

fof(f220,plain,
    ( sP14(a_select2(xinit_defuse,n4))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f219,f162]) ).

fof(f221,plain,
    ( sP14(a_select2(xinit_defuse,succ(succ(succ(succ(n0))))))
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f220,f141]) ).

fof(f222,plain,
    ( sP14(use)
    | sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f221,f174]) ).

fof(f223,plain,
    ( sP15(a_select2(xinit_defuse,n5))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f222,f163]) ).

fof(f224,plain,
    ( sP15(a_select2(xinit_defuse,succ(succ(succ(succ(succ(n0)))))))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f223,f143]) ).

fof(f225,plain,
    ( sP15(use)
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f224,f173]) ).

fof(f226,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_subsumption_resolution,[],[f225,f164]) ).

fof(f227,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f226,f143]) ).

fof(f228,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f227,f141]) ).

fof(f229,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f228,f139]) ).

fof(f230,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f229,f137]) ).

fof(f231,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n1))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f230,f135]) ).

fof(f232,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n2,use),n3,use),n4,use),n5,use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f231,f135]) ).

fof(f233,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n2,use),n3,use),n4,use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f232,f143]) ).

fof(f234,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n2,use),n3,use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f233,f141]) ).

fof(f235,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n2,use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f234,f139]) ).

fof(f236,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n2))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f235,f137]) ).

fof(f237,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),n3,use),n4,use),n5,use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f236,f137]) ).

fof(f238,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),n3,use),n4,use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f237,f143]) ).

fof(f239,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),n3,use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f238,f141]) ).

fof(f240,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f239,f139]) ).

fof(f241,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n3))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f240,f135]) ).

fof(f242,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),succ(succ(succ(n0))),use),n4,use),n5,use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f241,f139]) ).

fof(f243,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),succ(succ(succ(n0))),use),n4,use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f242,f143]) ).

fof(f244,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f243,f141]) ).

fof(f245,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f244,f137]) ).

fof(f246,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n4))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f245,f135]) ).

fof(f247,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),succ(succ(succ(succ(n0)))),use),n5,use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f246,f141]) ).

fof(f248,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f247,f143]) ).

fof(f249,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f248,f139]) ).

fof(f250,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f249,f137]) ).

fof(f251,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | sP21(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n1,use),n2,use),n3,use),n4,use),n5,use),n5)) ),
    inference(forward_demodulation,[],[f250,f135]) ).

fof(f252,plain,
    ( sP21(use)
    | sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0)) ),
    inference(forward_demodulation,[],[f251,f149]) ).

fof(f253,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0)) ),
    inference(forward_subsumption_resolution,[],[f252,f170]) ).

fof(f255,definition,
    ( spl22_1
  <=> sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0)) ),
    introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition]) ).

fof(f257,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),n0))
    | ~ spl22_1 ),
    inference(avatar_component_clause,[],[f255]) ).

fof(f259,definition,
    ( spl22_2
  <=> sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition]) ).

fof(f261,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(n0)))
    | ~ spl22_2 ),
    inference(avatar_component_clause,[],[f259]) ).

fof(f263,definition,
    ( spl22_3
  <=> sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition]) ).

fof(f265,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(n0))))
    | ~ spl22_3 ),
    inference(avatar_component_clause,[],[f263]) ).

fof(f267,definition,
    ( spl22_4
  <=> sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition]) ).

fof(f269,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(n0)))))
    | ~ spl22_4 ),
    inference(avatar_component_clause,[],[f267]) ).

fof(f271,definition,
    ( spl22_5
  <=> sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0)))))) ),
    introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition]) ).

fof(f273,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(succ(n0))))),use),succ(succ(succ(succ(n0))))))
    | ~ spl22_5 ),
    inference(avatar_component_clause,[],[f271]) ).

fof(f274,plain,
    ( spl22_1
    | spl22_2
    | spl22_3
    | spl22_4
    | spl22_5 ),
    inference(avatar_split_clause,[],[f253,f271,f267,f263,f259,f255]) ).

fof(f275,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(n0)))
    | succ(n0) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_2 ),
    inference(superposition,[],[f261,f172]) ).

fof(f281,definition,
    ( spl22_6
  <=> succ(n0) = succ(succ(succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition]) ).

fof(f282,plain,
    ( succ(n0) != succ(succ(succ(succ(succ(n0)))))
    | spl22_6 ),
    inference(avatar_component_clause,[],[f281]) ).

fof(f283,plain,
    ( succ(n0) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_6 ),
    inference(avatar_component_clause,[],[f281]) ).

fof(f285,definition,
    ( spl22_7
  <=> sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition]) ).

fof(f287,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(n0)))
    | ~ spl22_7 ),
    inference(avatar_component_clause,[],[f285]) ).

fof(f288,plain,
    ( spl22_6
    | spl22_7
    | ~ spl22_2 ),
    inference(avatar_split_clause,[],[f275,f259,f285,f281]) ).

fof(f308,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(n0),use),succ(n0)))
    | ~ spl22_2
    | ~ spl22_6 ),
    inference(superposition,[],[f261,f283]) ).

fof(f311,plain,
    ( sP17(use)
    | ~ spl22_2
    | ~ spl22_6 ),
    inference(forward_demodulation,[],[f308,f149]) ).

fof(f312,plain,
    ( $false
    | ~ spl22_2
    | ~ spl22_6 ),
    inference(forward_subsumption_resolution,[],[f311,f166]) ).

fof(f313,plain,
    ( ~ spl22_2
    | ~ spl22_6 ),
    inference(avatar_contradiction_clause,[],[f312]) ).

fof(f314,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(n0)))
    | succ(n0) = succ(succ(succ(succ(n0))))
    | ~ spl22_7 ),
    inference(superposition,[],[f287,f172]) ).

fof(f320,definition,
    ( spl22_12
  <=> succ(n0) = succ(succ(succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_12])],[avatar_definition]) ).

fof(f322,plain,
    ( succ(n0) = succ(succ(succ(succ(n0))))
    | ~ spl22_12 ),
    inference(avatar_component_clause,[],[f320]) ).

fof(f324,definition,
    ( spl22_13
  <=> sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_13])],[avatar_definition]) ).

fof(f326,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(n0)))
    | ~ spl22_13 ),
    inference(avatar_component_clause,[],[f324]) ).

fof(f327,plain,
    ( spl22_12
    | spl22_13
    | ~ spl22_7 ),
    inference(avatar_split_clause,[],[f314,f285,f324,f320]) ).

fof(f353,definition,
    ( spl22_17
  <=> succ(n0) = succ(succ(succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_17])],[avatar_definition]) ).

fof(f354,plain,
    ( succ(n0) != succ(succ(succ(n0)))
    | spl22_17 ),
    inference(avatar_component_clause,[],[f353]) ).

fof(f355,plain,
    ( succ(n0) = succ(succ(succ(n0)))
    | ~ spl22_17 ),
    inference(avatar_component_clause,[],[f353]) ).

fof(f357,definition,
    ( spl22_18
  <=> sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_18])],[avatar_definition]) ).

fof(f358,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(n0)))
    | ~ spl22_18 ),
    inference(avatar_component_clause,[],[f357]) ).

fof(f359,plain,
    ( ~ sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(n0)))
    | spl22_18 ),
    inference(avatar_component_clause,[],[f357]) ).

fof(f361,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(n0))))))
    | succ(succ(succ(succ(n0)))) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_5 ),
    inference(superposition,[],[f273,f172]) ).

fof(f366,plain,
    ( sP20(use)
    | succ(succ(succ(succ(n0)))) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_5 ),
    inference(forward_demodulation,[],[f361,f149]) ).

fof(f377,plain,
    ( succ(succ(succ(succ(n0)))) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_5 ),
    inference(forward_subsumption_resolution,[],[f366,f169]) ).

fof(f382,plain,
    ( sP20(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(succ(n0))))))
    | ~ spl22_5 ),
    inference(superposition,[],[f273,f377]) ).

fof(f387,plain,
    ( sP20(use)
    | ~ spl22_5 ),
    inference(forward_demodulation,[],[f382,f149]) ).

fof(f388,plain,
    ( $false
    | ~ spl22_5 ),
    inference(forward_subsumption_resolution,[],[f387,f169]) ).

fof(f389,plain,
    ~ spl22_5,
    inference(avatar_contradiction_clause,[],[f388]) ).

fof(f390,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(n0)))))
    | succ(succ(succ(n0))) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_4 ),
    inference(superposition,[],[f269,f172]) ).

fof(f396,definition,
    ( spl22_21
  <=> succ(succ(succ(n0))) = succ(succ(succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition]) ).

fof(f398,plain,
    ( succ(succ(succ(n0))) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_21 ),
    inference(avatar_component_clause,[],[f396]) ).

fof(f400,definition,
    ( spl22_22
  <=> sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_22])],[avatar_definition]) ).

fof(f402,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(n0)))))
    | ~ spl22_22 ),
    inference(avatar_component_clause,[],[f400]) ).

fof(f403,plain,
    ( spl22_21
    | spl22_22
    | ~ spl22_4 ),
    inference(avatar_split_clause,[],[f390,f267,f400,f396]) ).

fof(f418,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(n0))))
    | succ(succ(n0)) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_3 ),
    inference(superposition,[],[f265,f172]) ).

fof(f424,definition,
    ( spl22_25
  <=> succ(succ(n0)) = succ(succ(succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_25])],[avatar_definition]) ).

fof(f425,plain,
    ( succ(succ(n0)) != succ(succ(succ(succ(succ(n0)))))
    | spl22_25 ),
    inference(avatar_component_clause,[],[f424]) ).

fof(f426,plain,
    ( succ(succ(n0)) = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_25 ),
    inference(avatar_component_clause,[],[f424]) ).

fof(f428,definition,
    ( spl22_26
  <=> sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_26])],[avatar_definition]) ).

fof(f430,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(n0))))
    | ~ spl22_26 ),
    inference(avatar_component_clause,[],[f428]) ).

fof(f431,plain,
    ( spl22_25
    | spl22_26
    | ~ spl22_3 ),
    inference(avatar_split_clause,[],[f418,f263,f428,f424]) ).

fof(f442,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),n0))
    | n0 = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_1 ),
    inference(superposition,[],[f257,f172]) ).

fof(f448,definition,
    ( spl22_29
  <=> n0 = succ(succ(succ(succ(succ(n0))))) ),
    introduced(definition,[new_symbols(definition,[spl22_29])],[avatar_definition]) ).

fof(f450,plain,
    ( n0 = succ(succ(succ(succ(succ(n0)))))
    | ~ spl22_29 ),
    inference(avatar_component_clause,[],[f448]) ).

fof(f452,definition,
    ( spl22_30
  <=> sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),n0)) ),
    introduced(definition,[new_symbols(definition,[spl22_30])],[avatar_definition]) ).

fof(f454,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),n0))
    | ~ spl22_30 ),
    inference(avatar_component_clause,[],[f452]) ).

fof(f455,plain,
    ( spl22_29
    | spl22_30
    | ~ spl22_1 ),
    inference(avatar_split_clause,[],[f442,f255,f452,f448]) ).

fof(f472,definition,
    ( spl22_33
  <=> n0 = succ(succ(succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_33])],[avatar_definition]) ).

fof(f473,plain,
    ( n0 != succ(succ(succ(n0)))
    | spl22_33 ),
    inference(avatar_component_clause,[],[f472]) ).

fof(f474,plain,
    ( n0 = succ(succ(succ(n0)))
    | ~ spl22_33 ),
    inference(avatar_component_clause,[],[f472]) ).

fof(f481,definition,
    ( spl22_34
  <=> succ(succ(n0)) = succ(succ(succ(n0))) ),
    introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition]) ).

fof(f482,plain,
    ( succ(succ(n0)) != succ(succ(succ(n0)))
    | spl22_34 ),
    inference(avatar_component_clause,[],[f481]) ).

fof(f483,plain,
    ( succ(succ(n0)) = succ(succ(succ(n0)))
    | ~ spl22_34 ),
    inference(avatar_component_clause,[],[f481]) ).

fof(f494,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(succ(n0))),use),succ(succ(succ(n0)))))
    | ~ spl22_4
    | ~ spl22_21 ),
    inference(superposition,[],[f269,f398]) ).

fof(f500,plain,
    ( sP19(use)
    | ~ spl22_4
    | ~ spl22_21 ),
    inference(forward_demodulation,[],[f494,f149]) ).

fof(f503,plain,
    ( $false
    | ~ spl22_4
    | ~ spl22_21 ),
    inference(forward_subsumption_resolution,[],[f500,f168]) ).

fof(f504,plain,
    ( ~ spl22_4
    | ~ spl22_21 ),
    inference(avatar_contradiction_clause,[],[f503]) ).

fof(f591,definition,
    ( spl22_35
  <=> n0 = succ(succ(n0)) ),
    introduced(definition,[new_symbols(definition,[spl22_35])],[avatar_definition]) ).

fof(f592,plain,
    ( n0 != succ(succ(n0))
    | spl22_35 ),
    inference(avatar_component_clause,[],[f591]) ).

fof(f593,plain,
    ( n0 = succ(succ(n0))
    | ~ spl22_35 ),
    inference(avatar_component_clause,[],[f591]) ).

fof(f595,definition,
    ( spl22_36
  <=> sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),succ(succ(n0)),use),n0)) ),
    introduced(definition,[new_symbols(definition,[spl22_36])],[avatar_definition]) ).

fof(f596,plain,
    ( ~ sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | spl22_36 ),
    inference(avatar_component_clause,[],[f595]) ).

fof(f597,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | ~ spl22_36 ),
    inference(avatar_component_clause,[],[f595]) ).

fof(f614,plain,
    ( succ(n0) != succ(n0)
    | spl22_17
    | ~ spl22_35 ),
    inference(superposition,[],[f354,f593]) ).

fof(f626,plain,
    ( $false
    | spl22_17
    | ~ spl22_35 ),
    inference(trivial_inequality_removal,[],[f614]) ).

fof(f627,plain,
    ( spl22_17
    | ~ spl22_35 ),
    inference(avatar_contradiction_clause,[],[f626]) ).

fof(f672,plain,
    ( succ(succ(n0)) != succ(succ(succ(succ(n0))))
    | spl22_25
    | ~ spl22_34 ),
    inference(forward_demodulation,[],[f425,f483]) ).

fof(f696,plain,
    ( succ(succ(n0)) != succ(succ(succ(n0)))
    | spl22_25
    | ~ spl22_34 ),
    inference(forward_demodulation,[],[f672,f483]) ).

fof(f720,plain,
    ( $false
    | spl22_25
    | ~ spl22_34 ),
    inference(forward_subsumption_resolution,[],[f696,f483]) ).

fof(f721,plain,
    ( spl22_25
    | ~ spl22_34 ),
    inference(avatar_contradiction_clause,[],[f720]) ).

fof(f791,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | n0 = succ(succ(n0))
    | ~ spl22_36 ),
    inference(superposition,[],[f597,f172]) ).

fof(f794,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_subsumption_resolution,[],[f791,f592]) ).

fof(f810,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0))
    | n0 = succ(succ(n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(superposition,[],[f794,f172]) ).

fof(f813,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_subsumption_resolution,[],[f810,f592]) ).

fof(f817,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n0))
    | n0 = succ(succ(n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(superposition,[],[f813,f172]) ).

fof(f820,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_subsumption_resolution,[],[f817,f592]) ).

fof(f824,plain,
    ( sP16(a_select2(tptp_update2(xinit_mean_defuse,n0,use),n0))
    | n0 = succ(n0)
    | spl22_35
    | ~ spl22_36 ),
    inference(superposition,[],[f820,f172]) ).

fof(f827,plain,
    ( sP16(use)
    | n0 = succ(n0)
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_demodulation,[],[f824,f149]) ).

fof(f828,plain,
    ( n0 = succ(n0)
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_subsumption_resolution,[],[f827,f165]) ).

fof(f863,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n0,use),succ(n0),use),succ(n0),use),succ(n0),use),n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(superposition,[],[f597,f828]) ).

fof(f870,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),n0,use),n0,use),n0,use),n0,use),n0))
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_demodulation,[],[f863,f828]) ).

fof(f897,plain,
    ( sP16(use)
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_demodulation,[],[f870,f149]) ).

fof(f914,plain,
    ( $false
    | spl22_35
    | ~ spl22_36 ),
    inference(forward_subsumption_resolution,[],[f897,f165]) ).

fof(f915,plain,
    ( spl22_35
    | ~ spl22_36 ),
    inference(avatar_contradiction_clause,[],[f914]) ).

fof(f957,plain,
    ( ~ sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | n0 = succ(succ(n0))
    | spl22_36 ),
    inference(superposition,[],[f596,f172]) ).

fof(f960,plain,
    ( ~ sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0)),use),n0))
    | spl22_35
    | spl22_36 ),
    inference(forward_subsumption_resolution,[],[f957,f592]) ).

fof(f961,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),n0))
    | n0 = succ(succ(succ(succ(n0))))
    | ~ spl22_30 ),
    inference(superposition,[],[f454,f172]) ).

fof(f965,definition,
    ( spl22_37
  <=> n0 = succ(succ(succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_37])],[avatar_definition]) ).

fof(f966,plain,
    ( n0 != succ(succ(succ(succ(n0))))
    | spl22_37 ),
    inference(avatar_component_clause,[],[f965]) ).

fof(f967,plain,
    ( n0 = succ(succ(succ(succ(n0))))
    | ~ spl22_37 ),
    inference(avatar_component_clause,[],[f965]) ).

fof(f969,definition,
    ( spl22_38
  <=> sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),n0)) ),
    introduced(definition,[new_symbols(definition,[spl22_38])],[avatar_definition]) ).

fof(f971,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),n0))
    | ~ spl22_38 ),
    inference(avatar_component_clause,[],[f969]) ).

fof(f972,plain,
    ( spl22_37
    | spl22_38
    | ~ spl22_30 ),
    inference(avatar_split_clause,[],[f961,f452,f969,f965]) ).

fof(f989,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),n0,use),n0))
    | ~ spl22_30
    | ~ spl22_37 ),
    inference(superposition,[],[f454,f967]) ).

fof(f997,plain,
    ( sP16(use)
    | ~ spl22_30
    | ~ spl22_37 ),
    inference(forward_demodulation,[],[f989,f149]) ).

fof(f1002,plain,
    ( $false
    | ~ spl22_30
    | ~ spl22_37 ),
    inference(forward_subsumption_resolution,[],[f997,f165]) ).

fof(f1003,plain,
    ( ~ spl22_30
    | ~ spl22_37 ),
    inference(avatar_contradiction_clause,[],[f1002]) ).

fof(f1008,definition,
    ( spl22_39
  <=> succ(succ(n0)) = succ(succ(succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_39])],[avatar_definition]) ).

fof(f1010,plain,
    ( succ(succ(n0)) = succ(succ(succ(succ(n0))))
    | ~ spl22_39 ),
    inference(avatar_component_clause,[],[f1008]) ).

fof(f1012,definition,
    ( spl22_40
  <=> sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(n0)))) ),
    introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition]) ).

fof(f1013,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(n0))))
    | ~ spl22_40 ),
    inference(avatar_component_clause,[],[f1012]) ).

fof(f1014,plain,
    ( ~ sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(n0))))
    | spl22_40 ),
    inference(avatar_component_clause,[],[f1012]) ).

fof(f1016,plain,
    ( ~ sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0))
    | n0 = succ(succ(n0))
    | spl22_35
    | spl22_36 ),
    inference(superposition,[],[f960,f172]) ).

fof(f1019,plain,
    ( ~ sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0))
    | spl22_35
    | spl22_36 ),
    inference(forward_subsumption_resolution,[],[f1016,f592]) ).

fof(f1024,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0))
    | n0 = succ(succ(succ(n0)))
    | ~ spl22_38 ),
    inference(superposition,[],[f971,f172]) ).

fof(f1027,plain,
    ( n0 = succ(succ(succ(n0)))
    | spl22_35
    | spl22_36
    | ~ spl22_38 ),
    inference(forward_subsumption_resolution,[],[f1024,f1019]) ).

fof(f1028,plain,
    ( $false
    | spl22_33
    | spl22_35
    | spl22_36
    | ~ spl22_38 ),
    inference(forward_subsumption_resolution,[],[f1027,f473]) ).

fof(f1029,plain,
    ( spl22_33
    | spl22_35
    | spl22_36
    | ~ spl22_38 ),
    inference(avatar_contradiction_clause,[],[f1028]) ).

fof(f1040,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),n0,use),n0))
    | ~ spl22_1
    | ~ spl22_29 ),
    inference(superposition,[],[f257,f450]) ).

fof(f1051,plain,
    ( sP16(use)
    | ~ spl22_1
    | ~ spl22_29 ),
    inference(forward_demodulation,[],[f1040,f149]) ).

fof(f1052,plain,
    ( $false
    | ~ spl22_1
    | ~ spl22_29 ),
    inference(forward_subsumption_resolution,[],[f1051,f165]) ).

fof(f1053,plain,
    ( ~ spl22_1
    | ~ spl22_29 ),
    inference(avatar_contradiction_clause,[],[f1052]) ).

fof(f1054,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),n0))
    | ~ spl22_30
    | spl22_37 ),
    inference(forward_subsumption_resolution,[],[f961,f966]) ).

fof(f1058,plain,
    ( sP16(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),n0,use),n0))
    | ~ spl22_30
    | ~ spl22_33
    | spl22_37 ),
    inference(forward_demodulation,[],[f1054,f474]) ).

fof(f1061,plain,
    ( sP16(use)
    | ~ spl22_30
    | ~ spl22_33
    | spl22_37 ),
    inference(forward_demodulation,[],[f1058,f149]) ).

fof(f1064,plain,
    ( $false
    | ~ spl22_30
    | ~ spl22_33
    | spl22_37 ),
    inference(forward_subsumption_resolution,[],[f1061,f165]) ).

fof(f1065,plain,
    ( ~ spl22_30
    | ~ spl22_33
    | spl22_37 ),
    inference(avatar_contradiction_clause,[],[f1064]) ).

fof(f1080,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(n0))))
    | succ(succ(n0)) = succ(succ(succ(succ(n0))))
    | ~ spl22_26 ),
    inference(superposition,[],[f430,f172]) ).

fof(f1083,plain,
    ( succ(succ(n0)) = succ(succ(succ(succ(n0))))
    | ~ spl22_26
    | spl22_40 ),
    inference(forward_subsumption_resolution,[],[f1080,f1014]) ).

fof(f1084,plain,
    ( spl22_39
    | ~ spl22_26
    | spl22_40 ),
    inference(avatar_split_clause,[],[f1083,f1012,f428,f1008]) ).

fof(f1092,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0))))
    | succ(succ(n0)) = succ(succ(succ(n0)))
    | ~ spl22_40 ),
    inference(superposition,[],[f1013,f172]) ).

fof(f1095,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(n0))))
    | spl22_34
    | ~ spl22_40 ),
    inference(forward_subsumption_resolution,[],[f1092,f482]) ).

fof(f1096,plain,
    ( sP18(use)
    | spl22_34
    | ~ spl22_40 ),
    inference(forward_demodulation,[],[f1095,f149]) ).

fof(f1097,plain,
    ( $false
    | spl22_34
    | ~ spl22_40 ),
    inference(forward_subsumption_resolution,[],[f1096,f167]) ).

fof(f1098,plain,
    ( spl22_34
    | ~ spl22_40 ),
    inference(avatar_contradiction_clause,[],[f1097]) ).

fof(f1116,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(n0)),use),succ(succ(n0))))
    | ~ spl22_26
    | ~ spl22_39 ),
    inference(superposition,[],[f430,f1010]) ).

fof(f1125,plain,
    ( sP18(use)
    | ~ spl22_26
    | ~ spl22_39 ),
    inference(forward_demodulation,[],[f1116,f149]) ).

fof(f1127,plain,
    ( $false
    | ~ spl22_26
    | ~ spl22_39 ),
    inference(forward_subsumption_resolution,[],[f1125,f167]) ).

fof(f1128,plain,
    ( ~ spl22_26
    | ~ spl22_39 ),
    inference(avatar_contradiction_clause,[],[f1127]) ).

fof(f1133,plain,
    ( sP18(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(succ(n0)))),use),succ(succ(n0)),use),succ(succ(n0))))
    | ~ spl22_3
    | ~ spl22_25 ),
    inference(superposition,[],[f265,f426]) ).

fof(f1144,plain,
    ( sP18(use)
    | ~ spl22_3
    | ~ spl22_25 ),
    inference(forward_demodulation,[],[f1133,f149]) ).

fof(f1145,plain,
    ( $false
    | ~ spl22_3
    | ~ spl22_25 ),
    inference(forward_subsumption_resolution,[],[f1144,f167]) ).

fof(f1146,plain,
    ( ~ spl22_3
    | ~ spl22_25 ),
    inference(avatar_contradiction_clause,[],[f1145]) ).

fof(f1156,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(n0)))))
    | succ(succ(succ(n0))) = succ(succ(succ(succ(n0))))
    | ~ spl22_22 ),
    inference(superposition,[],[f402,f172]) ).

fof(f1159,plain,
    ( sP19(use)
    | succ(succ(succ(n0))) = succ(succ(succ(succ(n0))))
    | ~ spl22_22 ),
    inference(forward_demodulation,[],[f1156,f149]) ).

fof(f1160,plain,
    ( succ(succ(succ(n0))) = succ(succ(succ(succ(n0))))
    | ~ spl22_22 ),
    inference(forward_subsumption_resolution,[],[f1159,f168]) ).

fof(f1173,plain,
    ( sP19(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(succ(succ(n0))),use),succ(succ(succ(n0)))))
    | ~ spl22_22 ),
    inference(superposition,[],[f402,f1160]) ).

fof(f1191,plain,
    ( sP19(use)
    | ~ spl22_22 ),
    inference(forward_demodulation,[],[f1173,f149]) ).

fof(f1200,plain,
    ( $false
    | ~ spl22_22 ),
    inference(forward_subsumption_resolution,[],[f1191,f168]) ).

fof(f1201,plain,
    ~ spl22_22,
    inference(avatar_contradiction_clause,[],[f1200]) ).

fof(f1217,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(n0)))
    | succ(n0) = succ(succ(succ(n0)))
    | ~ spl22_13 ),
    inference(superposition,[],[f326,f172]) ).

fof(f1220,plain,
    ( succ(n0) = succ(succ(succ(n0)))
    | ~ spl22_13
    | spl22_18 ),
    inference(forward_subsumption_resolution,[],[f1217,f359]) ).

fof(f1221,plain,
    ( $false
    | ~ spl22_13
    | spl22_17
    | spl22_18 ),
    inference(forward_subsumption_resolution,[],[f1220,f354]) ).

fof(f1222,plain,
    ( ~ spl22_13
    | spl22_17
    | spl22_18 ),
    inference(avatar_contradiction_clause,[],[f1221]) ).

fof(f1245,plain,
    ( succ(n0) != succ(succ(succ(n0)))
    | spl22_6
    | ~ spl22_17 ),
    inference(superposition,[],[f282,f355]) ).

fof(f1263,plain,
    ( n0 != succ(succ(n0))
    | ~ spl22_17
    | spl22_37 ),
    inference(superposition,[],[f966,f355]) ).

fof(f1281,plain,
    ( $false
    | spl22_6
    | ~ spl22_17 ),
    inference(forward_subsumption_resolution,[],[f1245,f355]) ).

fof(f1282,plain,
    ( spl22_6
    | ~ spl22_17 ),
    inference(avatar_contradiction_clause,[],[f1281]) ).

fof(f1296,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(n0)))
    | succ(n0) = succ(succ(n0))
    | ~ spl22_18 ),
    inference(superposition,[],[f358,f172]) ).

fof(f1299,plain,
    ( sP17(use)
    | succ(n0) = succ(succ(n0))
    | ~ spl22_18 ),
    inference(forward_demodulation,[],[f1296,f149]) ).

fof(f1300,plain,
    ( succ(n0) = succ(succ(n0))
    | ~ spl22_18 ),
    inference(forward_subsumption_resolution,[],[f1299,f166]) ).

fof(f1326,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(n0),use),succ(n0)))
    | ~ spl22_18 ),
    inference(superposition,[],[f358,f1300]) ).

fof(f1360,plain,
    ( sP17(use)
    | ~ spl22_18 ),
    inference(forward_demodulation,[],[f1326,f149]) ).

fof(f1379,plain,
    ( $false
    | ~ spl22_18 ),
    inference(forward_subsumption_resolution,[],[f1360,f166]) ).

fof(f1380,plain,
    ~ spl22_18,
    inference(avatar_contradiction_clause,[],[f1379]) ).

fof(f1426,plain,
    ( sP17(a_select2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(tptp_update2(xinit_mean_defuse,n0,use),succ(n0),use),succ(succ(n0)),use),succ(succ(succ(n0))),use),succ(n0),use),succ(n0)))
    | ~ spl22_7
    | ~ spl22_12 ),
    inference(superposition,[],[f287,f322]) ).

fof(f1442,plain,
    ( sP17(use)
    | ~ spl22_7
    | ~ spl22_12 ),
    inference(forward_demodulation,[],[f1426,f149]) ).

fof(f1444,plain,
    ( $false
    | ~ spl22_7
    | ~ spl22_12 ),
    inference(forward_subsumption_resolution,[],[f1442,f166]) ).

fof(f1445,plain,
    ( ~ spl22_7
    | ~ spl22_12 ),
    inference(avatar_contradiction_clause,[],[f1444]) ).

fof(f1449,plain,
    ( ~ spl22_35
    | ~ spl22_17
    | spl22_37 ),
    inference(avatar_split_clause,[],[f1263,f965,f353,f591]) ).

cnf(s1,plain,
    ( spl22_1
    | spl22_2
    | spl22_3
    | spl22_4
    | spl22_5 ),
    inference(sat_conversion,[],[f274]) ).

cnf(s2,plain,
    ( ~ spl22_2
    | spl22_6
    | spl22_7 ),
    inference(sat_conversion,[],[f288]) ).

cnf(s5,plain,
    ( ~ spl22_2
    | ~ spl22_6 ),
    inference(sat_conversion,[],[f313]) ).

cnf(s6,plain,
    ( ~ spl22_7
    | spl22_12
    | spl22_13 ),
    inference(sat_conversion,[],[f327]) ).

cnf(s15,plain,
    ~ spl22_5,
    inference(sat_conversion,[],[f389]) ).

cnf(s16,plain,
    ( ~ spl22_4
    | spl22_21
    | spl22_22 ),
    inference(sat_conversion,[],[f403]) ).

cnf(s19,plain,
    ( ~ spl22_3
    | spl22_25
    | spl22_26 ),
    inference(sat_conversion,[],[f431]) ).

cnf(s22,plain,
    ( ~ spl22_1
    | spl22_29
    | spl22_30 ),
    inference(sat_conversion,[],[f455]) ).

cnf(s28,plain,
    ( ~ spl22_4
    | ~ spl22_21 ),
    inference(sat_conversion,[],[f504]) ).

cnf(s37,plain,
    ( spl22_17
    | ~ spl22_35 ),
    inference(sat_conversion,[],[f627]) ).

cnf(s49,plain,
    ( spl22_25
    | ~ spl22_34 ),
    inference(sat_conversion,[],[f721]) ).

cnf(s60,plain,
    ( spl22_35
    | ~ spl22_36 ),
    inference(sat_conversion,[],[f915]) ).

cnf(s63,plain,
    ( ~ spl22_30
    | spl22_37
    | spl22_38 ),
    inference(sat_conversion,[],[f972]) ).

cnf(s68,plain,
    ( ~ spl22_30
    | ~ spl22_37 ),
    inference(sat_conversion,[],[f1003]) ).

cnf(s70,plain,
    ( spl22_33
    | spl22_35
    | spl22_36
    | ~ spl22_38 ),
    inference(sat_conversion,[],[f1029]) ).

cnf(s73,plain,
    ( ~ spl22_1
    | ~ spl22_29 ),
    inference(sat_conversion,[],[f1053]) ).

cnf(s75,plain,
    ( ~ spl22_30
    | ~ spl22_33
    | spl22_37 ),
    inference(sat_conversion,[],[f1065]) ).

cnf(s76,plain,
    ( ~ spl22_26
    | spl22_39
    | spl22_40 ),
    inference(sat_conversion,[],[f1084]) ).

cnf(s77,plain,
    ( spl22_34
    | ~ spl22_40 ),
    inference(sat_conversion,[],[f1098]) ).

cnf(s80,plain,
    ( ~ spl22_26
    | ~ spl22_39 ),
    inference(sat_conversion,[],[f1128]) ).

cnf(s81,plain,
    ( ~ spl22_3
    | ~ spl22_25 ),
    inference(sat_conversion,[],[f1146]) ).

cnf(s85,plain,
    ~ spl22_22,
    inference(sat_conversion,[],[f1201]) ).

cnf(s87,plain,
    ( ~ spl22_13
    | spl22_17
    | spl22_18 ),
    inference(sat_conversion,[],[f1222]) ).

cnf(s92,plain,
    ( spl22_6
    | ~ spl22_17 ),
    inference(sat_conversion,[],[f1282]) ).

cnf(s96,plain,
    ~ spl22_18,
    inference(sat_conversion,[],[f1380]) ).

cnf(s101,plain,
    ( ~ spl22_7
    | ~ spl22_12 ),
    inference(sat_conversion,[],[f1445]) ).

cnf(s103,plain,
    ( ~ spl22_17
    | ~ spl22_35
    | spl22_37 ),
    inference(sat_conversion,[],[f1449]) ).

cnf(s109,plain,
    ( ~ spl22_13
    | spl22_17 ),
    inference(rat,[],[s87,s96]) ).

cnf(s110,plain,
    ( ~ spl22_4
    | spl22_21 ),
    inference(rat,[],[s16,s85]) ).

cnf(s111,plain,
    ( spl22_1
    | spl22_2
    | spl22_3
    | spl22_4 ),
    inference(rat,[],[s1,s15]) ).

cnf(s112,plain,
    ~ spl22_4,
    inference(rat,[],[s110,s28]) ).

cnf(s113,plain,
    ~ spl22_3,
    inference(rat,[],[s76,s80,s77,s19,s49,s81]) ).

cnf(s114,plain,
    ~ spl22_2,
    inference(rat,[],[s6,s101,s109,s2,s92,s5]) ).

cnf(s115,plain,
    spl22_1,
    inference(rat,[],[s111,s112,s113,s114]) ).

cnf(s116,plain,
    ~ spl22_29,
    inference(rat,[],[s73,s115]) ).

cnf(s117,plain,
    spl22_30,
    inference(rat,[],[s22,s116,s115]) ).

cnf(s118,plain,
    ~ spl22_37,
    inference(rat,[],[s68,s117]) ).

cnf(s119,plain,
    spl22_38,
    inference(rat,[],[s63,s118,s117]) ).

cnf(s120,plain,
    ~ spl22_33,
    inference(rat,[],[s75,s118,s117]) ).

cnf(s121,plain,
    spl22_35,
    inference(rat,[],[s70,s60,s120,s119]) ).

cnf(s123,plain,
    ~ spl22_17,
    inference(rat,[],[s103,s118,s121]) ).

cnf(s124,plain,
    $false,
    inference(rat,[],[s37,s121,s123]) ).

fof(f1501,plain,
    $false,
    inference(avatar_sat_refutation,[],[s124]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWV090+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19  % Computer : n007.cluster.edu
% 0.09/0.19  % Model    : x86_64 x86_64
% 0.09/0.19  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19  % Memory   : 8046.5625MB
% 0.09/0.19  % OS       : Linux 6.8.0-71-generic
% 0.09/0.19  % CPULimit : 300
% 0.09/0.19  % WCLimit  : 300
% 0.09/0.19  % DateTime : Mon Sep 28 09:49:40 UTC 2026
% 0.09/0.19  % CPUTime  : 
% 0.09/0.19  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23  Running first-order theorem proving
% 0.09/0.23  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.63/0.90  % (2287317)Detected formulas, will run a generic FOF schedule.
% 1.63/0.90  % (2287328)dis-21_1_sil=8000:lcm=predicate:random_seed=1431771840:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.63/0.90  % (2287325)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4209949593:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.63/0.90  % (2287322)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3367795723:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.63/0.90  % (2287326)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=892060818:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.63/0.90  % (2287324)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3926930775:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.63/0.90  % (2287328)Instruction limit reached! 
% 1.63/0.90  % (2287328)------------------------------
% 1.63/0.90  % (2287328)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.63/0.90  % (2287328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.63/0.90  % (2287328)CaDiCaL version: 2.1.3
% 1.63/0.90  % (2287328)Termination reason: Instruction limit
% 1.63/0.90  % (2287328)Termination phase: Saturation
% 1.63/0.90  % (2287328)Time elapsed: 0.040 s
% 1.63/0.90  % (2287328)Peak memory usage: 89 MB
% 1.63/0.90  % (2287328)Instructions burned: 130 (million)
% 1.63/0.90  % (2287323)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=833114750:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.63/0.90  % (2287327)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4151459198:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.63/0.90  % (2287325)First to succeed.
% 1.63/0.90  % (2287325)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2287317"
% 1.63/0.90  % (2287327)Also succeeded, but the first one will report.
% 1.63/0.90  % (2287326)Instruction limit reached! 
% 1.63/0.90  % (2287326)------------------------------
% 1.63/0.90  % (2287326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.63/0.90  % (2287326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.63/0.90  % (2287326)CaDiCaL version: 2.1.3
% 1.63/0.90  % (2287326)Termination reason: Instruction limit
% 1.63/0.90  % (2287326)Termination phase: Saturation
% 1.63/0.90  % (2287326)Time elapsed: 0.068 s
% 1.63/0.90  % (2287326)Peak memory usage: 88 MB
% 1.63/0.90  % (2287326)Instructions burned: 119 (million)
% 1.63/0.90  % (2287361)lrs+10_1_sil=8000:sp=occurrence:random_seed=2369545388:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 1.63/0.90  % (2287361)Also succeeded, but the first one will report.
% 1.63/0.90  % (2287383)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1537666772:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 1.63/0.90  % (2287383)Also succeeded, but the first one will report.
% 1.63/0.90  % (2287325)Refutation found. Thanks to Tanya!
% 1.63/0.90  % SZS status Theorem for theBenchmark
% 1.63/0.90  % SZS output start Proof for theBenchmark
% See solution above
% 3.63/1.10  % (2287325)------------------------------
% 3.63/1.10  % (2287325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.10  % (2287325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.10  % (2287325)CaDiCaL version: 2.1.3
% 3.63/1.10  % (2287325)Termination reason: Refutation
% 3.63/1.10  % (2287325)Time elapsed: 0.039 s
% 3.63/1.10  % (2287325)Peak memory usage: 90 MB
% 3.63/1.10  % (2287325)Instructions burned: 72 (million)
% 3.63/1.10  % (2287325)------------------------------
% 3.63/1.10  % (2287325)------------------------------
% 3.63/1.10  % (2287317)Success in time 0.461 s
% 3.63/1.10  % Vampire exiting
%------------------------------------------------------------------------------