Vampire---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : RNG067+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 12:35:22 PM UTC 2026

% Result   : Theorem 2.06s 1.31s
% Output   : Refutation 0.16s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   43
%            Number of leaves      :   25
% Syntax   : Number of formulae    :  194 (  72 unt;   9 def)
%            Number of atoms       :  522 (  32 equ)
%            Maximal formula atoms :    7 (   2 avg)
%            Number of connectives :  653 ( 325   ~; 288   |;  26   &)
%                                         (   9 <=>;   5  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   12 (   3 avg)
%            Maximal term depth    :    7 (   2 avg)
%            Number of predicates  :   14 (  12 usr;  10 prp; 0-2 aty)
%            Number of functors    :   18 (  18 usr;  14 con; 0-2 aty)
%            Number of variables   :   48 (   0 sgn  48   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f10,axiom,
    ! [X0,X1] :
      ( ( aScalar0(X0)
        & aScalar0(X1) )
     => aScalar0(sdtpldt0(X0,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSumSc) ).

fof(f11,axiom,
    ! [X0,X1] :
      ( ( aScalar0(X0)
        & aScalar0(X1) )
     => aScalar0(sdtasdt0(X0,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulSc) ).

fof(f14,axiom,
    ! [X0,X1,X2] :
      ( ( aScalar0(X0)
        & aScalar0(X1)
        & aScalar0(X2) )
     => ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
        & sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
        & sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
        & sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',mArith) ).

fof(f23,axiom,
    ! [X0,X1,X2,X3] :
      ( ( aScalar0(X0)
        & aScalar0(X1)
        & aScalar0(X2)
        & aScalar0(X3) )
     => ( ( sdtlseqdt0(X0,X1)
          & sdtlseqdt0(X2,X3) )
       => sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEMon) ).

fof(f42,axiom,
    ( aVector0(xp)
    & xp = sziznziztdt0(xs) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1709) ).

fof(f43,axiom,
    ( aVector0(xq)
    & xq = sziznziztdt0(xt) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1726) ).

fof(f46,axiom,
    ( aScalar0(xC)
    & xC = sdtasasdt0(xp,xp) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1783) ).

fof(f47,axiom,
    ( aScalar0(xD)
    & xD = sdtasasdt0(xq,xq) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1800) ).

fof(f48,axiom,
    ( aScalar0(xE)
    & xE = sdtasasdt0(xp,xq) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1820) ).

fof(f52,axiom,
    ( aScalar0(xR)
    & xR = sdtasdt0(xC,xG) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1892) ).

fof(f53,axiom,
    ( aScalar0(xP)
    & xP = sdtasdt0(xE,xH) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1911) ).

fof(f54,axiom,
    ( aScalar0(xS)
    & xS = sdtasdt0(xF,xD) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1930) ).

fof(f55,axiom,
    ( aScalar0(xN)
    & xN = sdtasdt0(xR,xS) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1949) ).

fof(f57,axiom,
    sdtlseqdt0(sdtasdt0(xP,xP),xN),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2004) ).

fof(f58,axiom,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2104) ).

fof(f59,conjecture,
    sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).

fof(f60,negated_conjecture,
    ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)),
    inference(negated_conjecture,[status(cth)],[f59]) ).

fof(f61,plain,
    ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)),
    inference(flattening,[],[f60]) ).

fof(f76,plain,
    ! [X0,X1] :
      ( aScalar0(sdtasdt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(ennf_transformation,[],[f11]) ).

fof(f77,plain,
    ! [X0,X1] :
      ( aScalar0(sdtasdt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(flattening,[],[f76]) ).

fof(f91,plain,
    ! [X0,X1,X2,X3] :
      ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
      | ~ sdtlseqdt0(X0,X1)
      | ~ sdtlseqdt0(X2,X3)
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2)
      | ~ aScalar0(X3) ),
    inference(ennf_transformation,[],[f23]) ).

fof(f92,plain,
    ! [X0,X1,X2,X3] :
      ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
      | ~ sdtlseqdt0(X0,X1)
      | ~ sdtlseqdt0(X2,X3)
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2)
      | ~ aScalar0(X3) ),
    inference(flattening,[],[f91]) ).

fof(f97,plain,
    ! [X0,X1,X2] :
      ( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
        & sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
        & sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
        & sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2) ),
    inference(ennf_transformation,[],[f14]) ).

fof(f98,plain,
    ! [X0,X1,X2] :
      ( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
        & sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
        & sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
        & sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2) ),
    inference(flattening,[],[f97]) ).

fof(f99,plain,
    ! [X0,X1] :
      ( aScalar0(sdtpldt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(ennf_transformation,[],[f10]) ).

fof(f100,plain,
    ! [X0,X1] :
      ( aScalar0(sdtpldt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(flattening,[],[f99]) ).

fof(f110,plain,
    xp = sziznziztdt0(xs),
    inference(cnf_transformation,[],[f42]) ).

fof(f112,plain,
    xq = sziznziztdt0(xt),
    inference(cnf_transformation,[],[f43]) ).

fof(f118,plain,
    xC = sdtasasdt0(xp,xp),
    inference(cnf_transformation,[],[f46]) ).

fof(f120,plain,
    xD = sdtasasdt0(xq,xq),
    inference(cnf_transformation,[],[f47]) ).

fof(f122,plain,
    xE = sdtasasdt0(xp,xq),
    inference(cnf_transformation,[],[f48]) ).

fof(f130,plain,
    xR = sdtasdt0(xC,xG),
    inference(cnf_transformation,[],[f52]) ).

fof(f131,plain,
    aScalar0(xR),
    inference(cnf_transformation,[],[f52]) ).

fof(f132,plain,
    xP = sdtasdt0(xE,xH),
    inference(cnf_transformation,[],[f53]) ).

fof(f133,plain,
    aScalar0(xP),
    inference(cnf_transformation,[],[f53]) ).

fof(f134,plain,
    xS = sdtasdt0(xF,xD),
    inference(cnf_transformation,[],[f54]) ).

fof(f135,plain,
    aScalar0(xS),
    inference(cnf_transformation,[],[f54]) ).

fof(f136,plain,
    xN = sdtasdt0(xR,xS),
    inference(cnf_transformation,[],[f55]) ).

fof(f137,plain,
    aScalar0(xN),
    inference(cnf_transformation,[],[f55]) ).

fof(f139,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),xN),
    inference(cnf_transformation,[],[f57]) ).

fof(f140,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS))),
    inference(cnf_transformation,[],[f58]) ).

fof(f141,plain,
    ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN),xN)),
    inference(cnf_transformation,[],[f61]) ).

fof(f147,plain,
    ! [X0,X1] :
      ( aScalar0(sdtasdt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(cnf_transformation,[],[f77]) ).

fof(f160,plain,
    ! [X2,X3,X0,X1] :
      ( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
      | ~ sdtlseqdt0(X0,X1)
      | ~ sdtlseqdt0(X2,X3)
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2)
      | ~ aScalar0(X3) ),
    inference(cnf_transformation,[],[f92]) ).

fof(f166,plain,
    ! [X2,X0,X1] :
      ( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ aScalar0(X2) ),
    inference(cnf_transformation,[],[f98]) ).

fof(f168,plain,
    ! [X0,X1] :
      ( aScalar0(sdtpldt0(X0,X1))
      | ~ aScalar0(X0)
      | ~ aScalar0(X1) ),
    inference(cnf_transformation,[],[f100]) ).

fof(f176,plain,
    ! [X2] :
      ( ~ aScalar0(X2)
      | sP3 ),
    inference(cnf_transformation,[],[f176_D]) ).

fof(f176_D,definition,
    ( ! [X2] : ~ aScalar0(X2)
  <=> ~ sP3 ),
    introduced(definition,[new_symbols(definition,[sP3])],[general_splitting_component_introduction]) ).

fof(f177,plain,
    ! [X0,X1] :
      ( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
      | ~ aScalar0(X0)
      | ~ aScalar0(X1)
      | ~ sP3 ),
    inference(general_splitting,[],[f166,f176_D]) ).

fof(f180,plain,
    aScalar0(sdtasdt0(xR,xS)),
    inference(forward_demodulation,[],[f137,f136]) ).

fof(f181,plain,
    aScalar0(sdtasdt0(xF,xD)),
    inference(forward_demodulation,[],[f135,f134]) ).

fof(f182,plain,
    aScalar0(sdtasdt0(xE,xH)),
    inference(forward_demodulation,[],[f133,f132]) ).

fof(f183,plain,
    aScalar0(sdtasdt0(xC,xG)),
    inference(forward_demodulation,[],[f131,f130]) ).

fof(f191,plain,
    aScalar0(sdtasdt0(xR,sdtasdt0(xF,xD))),
    inference(forward_demodulation,[],[f180,f134]) ).

fof(f192,plain,
    aScalar0(sdtasdt0(xF,sdtasasdt0(xq,xq))),
    inference(forward_demodulation,[],[f181,f120]) ).

fof(f193,plain,
    aScalar0(sdtasdt0(sdtasasdt0(xp,xq),xH)),
    inference(forward_demodulation,[],[f182,f122]) ).

fof(f194,plain,
    aScalar0(sdtasdt0(sdtasasdt0(xp,xp),xG)),
    inference(forward_demodulation,[],[f183,f118]) ).

fof(f199,plain,
    aScalar0(sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(xq,xq)))),
    inference(forward_demodulation,[],[f191,f120]) ).

fof(f200,plain,
    aScalar0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))),
    inference(forward_demodulation,[],[f192,f112]) ).

fof(f201,plain,
    aScalar0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)),
    inference(forward_demodulation,[],[f193,f112]) ).

fof(f202,plain,
    aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),
    inference(forward_demodulation,[],[f194,f110]) ).

fof(f204,plain,
    aScalar0(sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f199,f112]) ).

fof(f205,plain,
    aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),
    inference(forward_demodulation,[],[f201,f110]) ).

fof(f206,plain,
    aScalar0(sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f204,f130]) ).

fof(f207,plain,
    aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f206,f118]) ).

fof(f208,plain,
    aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f207,f110]) ).

fof(f216,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ sdtlseqdt0(sdtasdt0(xP,xP),xN)
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(resolution,[],[f141,f160]) ).

fof(f248,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_subsumption_resolution,[],[f216,f139]) ).

fof(f262,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtasdt0(xR,xS)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f248,f136]) ).

fof(f276,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,xD),sdtasdt0(xF,xD))),sdtasdt0(xR,sdtasdt0(xF,xD))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f262,f134]) ).

fof(f290,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(xq,xq)),sdtasdt0(xF,sdtasasdt0(xq,xq)))),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(xq,xq)))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f276,f120]) ).

fof(f304,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f290,f112]) ).

fof(f318,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xC,xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f304,f130]) ).

fof(f332,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(sdtasasdt0(xp,xp),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f318,f118]) ).

fof(f346,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f332,f110]) ).

fof(f360,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH)),sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH))),sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f346,f132]) ).

fof(f374,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f360,f122]) ).

fof(f388,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f374,f112]) ).

fof(f402,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtasdt0(xP,xP)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f388,f110]) ).

fof(f416,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH)),sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH))),sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f402,f132]) ).

fof(f430,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f416,f122]) ).

fof(f444,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f430,f112]) ).

fof(f459,definition,
    ( spl5_2
  <=> aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))) ),
    introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).

fof(f460,plain,
    ( aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ spl5_2 ),
    inference(avatar_component_clause,[],[f459]) ).

fof(f461,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | spl5_2 ),
    inference(avatar_component_clause,[],[f459]) ).

fof(f466,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),xN))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f444,f110]) ).

fof(f477,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),sdtasdt0(xR,xS)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f466,f136]) ).

fof(f488,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,xD),sdtasdt0(xF,xD))),sdtasdt0(xR,sdtasdt0(xF,xD))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f477,f134]) ).

fof(f499,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(xq,xq)),sdtasdt0(xF,sdtasasdt0(xq,xq)))),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(xq,xq)))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f488,f120]) ).

fof(f511,definition,
    ( spl5_4
  <=> aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))) ),
    introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).

fof(f512,plain,
    ( aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ spl5_4 ),
    inference(avatar_component_clause,[],[f511]) ).

fof(f513,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | spl5_4 ),
    inference(avatar_component_clause,[],[f511]) ).

fof(f518,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f499,f112]) ).

fof(f528,definition,
    ( spl5_6
  <=> aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))) ),
    introduced(definition,[new_symbols(definition,[spl5_6])],[avatar_definition]) ).

fof(f530,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | spl5_6 ),
    inference(avatar_component_clause,[],[f528]) ).

fof(f536,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xC,xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f518,f130]) ).

fof(f542,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(sdtasasdt0(xp,xp),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f536,f118]) ).

fof(f560,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(xP,xP))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f542,f110]) ).

fof(f565,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f560,f132]) ).

fof(f570,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f565,f122]) ).

fof(f578,definition,
    ( spl5_11
  <=> aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    introduced(definition,[new_symbols(definition,[spl5_11])],[avatar_definition]) ).

fof(f579,plain,
    ( aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ spl5_11 ),
    inference(avatar_component_clause,[],[f578]) ).

fof(f580,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | spl5_11 ),
    inference(avatar_component_clause,[],[f578]) ).

fof(f587,definition,
    ( spl5_13
  <=> aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG))) ),
    introduced(definition,[new_symbols(definition,[spl5_13])],[avatar_definition]) ).

fof(f589,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)))
    | spl5_13 ),
    inference(avatar_component_clause,[],[f587]) ).

fof(f591,definition,
    ( spl5_14
  <=> aScalar0(sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))) ),
    introduced(definition,[new_symbols(definition,[spl5_14])],[avatar_definition]) ).

fof(f593,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | spl5_14 ),
    inference(avatar_component_clause,[],[f591]) ).

fof(f595,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f570,f112]) ).

fof(f598,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(xN) ),
    inference(forward_demodulation,[],[f595,f110]) ).

fof(f604,definition,
    ( spl5_16
  <=> aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    introduced(definition,[new_symbols(definition,[spl5_16])],[avatar_definition]) ).

fof(f606,plain,
    ( ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | spl5_16 ),
    inference(avatar_component_clause,[],[f604]) ).

fof(f609,plain,
    ( ~ aScalar0(sdtasdt0(xR,xS))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f598,f136]) ).

fof(f610,plain,
    ( ~ aScalar0(sdtasdt0(xR,sdtasdt0(xF,xD)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f609,f134]) ).

fof(f611,plain,
    ( ~ aScalar0(sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(xq,xq))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f610,f120]) ).

fof(f612,plain,
    ( ~ aScalar0(sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f611,f112]) ).

fof(f613,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f612,f130]) ).

fof(f614,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f613,f118]) ).

fof(f615,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_demodulation,[],[f614,f110]) ).

fof(f616,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    inference(forward_subsumption_resolution,[],[f615,f208]) ).

fof(f618,definition,
    ( spl5_17
  <=> sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))) ),
    introduced(definition,[new_symbols(definition,[spl5_17])],[avatar_definition]) ).

fof(f620,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | spl5_17 ),
    inference(avatar_component_clause,[],[f618]) ).

fof(f621,plain,
    ( ~ spl5_17
    | ~ spl5_6
    | ~ spl5_16
    | ~ spl5_2 ),
    inference(avatar_split_clause,[],[f616,f459,f604,f528,f618]) ).

fof(f623,plain,
    ( ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))
    | ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))
    | spl5_2 ),
    inference(resolution,[],[f461,f147]) ).

fof(f625,plain,
    ( ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))
    | spl5_2 ),
    inference(duplicate_literal_removal,[],[f623]) ).

fof(f627,plain,
    ( $false
    | spl5_2 ),
    inference(forward_subsumption_resolution,[],[f625,f205]) ).

fof(f628,plain,
    spl5_2,
    inference(avatar_contradiction_clause,[],[f627]) ).

fof(f707,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | spl5_6 ),
    inference(resolution,[],[f530,f168]) ).

fof(f723,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ spl5_2
    | spl5_6 ),
    inference(forward_subsumption_resolution,[],[f707,f460]) ).

fof(f727,plain,
    ( ~ spl5_4
    | ~ spl5_2
    | spl5_6 ),
    inference(avatar_split_clause,[],[f723,f528,f459,f511]) ).

fof(f778,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | spl5_4 ),
    inference(resolution,[],[f513,f168]) ).

fof(f784,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | spl5_4 ),
    inference(duplicate_literal_removal,[],[f778]) ).

fof(f788,plain,
    ( $false
    | ~ spl5_2
    | spl5_4 ),
    inference(forward_subsumption_resolution,[],[f784,f460]) ).

fof(f789,plain,
    ( ~ spl5_2
    | spl5_4 ),
    inference(avatar_contradiction_clause,[],[f788]) ).

fof(f1044,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(xR,xS)),
    inference(superposition,[],[f139,f136]) ).

fof(f1045,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(xR,sdtasdt0(xF,xD))),
    inference(forward_demodulation,[],[f1044,f134]) ).

fof(f1049,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(xq,xq)))),
    inference(forward_demodulation,[],[f1045,f120]) ).

fof(f1053,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(xR,sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1049,f112]) ).

fof(f1057,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1053,f130]) ).

fof(f1061,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1057,f118]) ).

fof(f1065,plain,
    sdtlseqdt0(sdtasdt0(xP,xP),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1061,f110]) ).

fof(f1069,plain,
    sdtlseqdt0(sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1065,f132]) ).

fof(f1073,plain,
    sdtlseqdt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1069,f122]) ).

fof(f1077,plain,
    sdtlseqdt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1073,f112]) ).

fof(f1081,plain,
    sdtlseqdt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))),
    inference(forward_demodulation,[],[f1077,f110]) ).

fof(f1351,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,xD),sdtasdt0(xF,xD)))),
    inference(superposition,[],[f140,f134]) ).

fof(f1354,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(xq,xq)),sdtasdt0(xF,sdtasasdt0(xq,xq))))),
    inference(forward_demodulation,[],[f1351,f120]) ).

fof(f1361,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1354,f112]) ).

fof(f1368,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(sdtasdt0(xC,xG),sdtasdt0(xC,xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1361,f130]) ).

fof(f1375,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xp),xG),sdtasdt0(sdtasasdt0(xp,xp),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1368,f118]) ).

fof(f1382,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(xP,xP),sdtasdt0(xP,xP)),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1375,f110]) ).

fof(f1389,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH)),sdtasdt0(sdtasdt0(xE,xH),sdtasdt0(xE,xH))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1382,f132]) ).

fof(f1396,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,xq),xH),sdtasdt0(sdtasasdt0(xp,xq),xH))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1389,f122]) ).

fof(f1403,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(xp,sziznziztdt0(xt)),xH))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1396,f112]) ).

fof(f1410,plain,
    sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))),
    inference(forward_demodulation,[],[f1403,f110]) ).

fof(f1555,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | spl5_11 ),
    inference(resolution,[],[f580,f168]) ).

fof(f1564,plain,
    ( ~ spl5_14
    | ~ spl5_13
    | spl5_11 ),
    inference(avatar_split_clause,[],[f1555,f578,f587,f591]) ).

fof(f1573,plain,
    ( ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG))
    | ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG))
    | spl5_13 ),
    inference(resolution,[],[f589,f147]) ).

fof(f1575,plain,
    ( ~ aScalar0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG))
    | spl5_13 ),
    inference(duplicate_literal_removal,[],[f1573]) ).

fof(f1577,plain,
    ( $false
    | spl5_13 ),
    inference(forward_subsumption_resolution,[],[f1575,f202]) ).

fof(f1578,plain,
    spl5_13,
    inference(avatar_contradiction_clause,[],[f1577]) ).

fof(f1587,plain,
    ( ~ aScalar0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))
    | ~ aScalar0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))
    | spl5_14 ),
    inference(resolution,[],[f593,f147]) ).

fof(f1591,plain,
    ( ~ aScalar0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))
    | spl5_14 ),
    inference(duplicate_literal_removal,[],[f1587]) ).

fof(f1595,plain,
    ( $false
    | spl5_14 ),
    inference(forward_subsumption_resolution,[],[f1591,f200]) ).

fof(f1596,plain,
    spl5_14,
    inference(avatar_contradiction_clause,[],[f1595]) ).

fof(f1692,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ sP3
    | spl5_16 ),
    inference(superposition,[],[f606,f177]) ).

fof(f1695,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ sP3
    | spl5_16 ),
    inference(forward_subsumption_resolution,[],[f1692,f168]) ).

fof(f1704,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | spl5_16 ),
    inference(forward_subsumption_resolution,[],[f1695,f176]) ).

fof(f1714,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | spl5_16 ),
    inference(forward_subsumption_resolution,[],[f1704,f208]) ).

fof(f1723,plain,
    ( $false
    | ~ spl5_11
    | spl5_16 ),
    inference(forward_subsumption_resolution,[],[f1714,f579]) ).

fof(f1724,plain,
    ( ~ spl5_11
    | spl5_16 ),
    inference(avatar_contradiction_clause,[],[f1723]) ).

fof(f2064,plain,
    ( ~ sdtlseqdt0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))),sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ sdtlseqdt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | spl5_17 ),
    inference(resolution,[],[f620,f160]) ).

fof(f2098,plain,
    ( ~ sdtlseqdt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2064,f1410]) ).

fof(f2111,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)),sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH))))
    | ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2098,f1081]) ).

fof(f2121,plain,
    ( ~ aScalar0(sdtpldt0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG)),sdtasdt0(sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt))))))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ spl5_4
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2111,f512]) ).

fof(f2122,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH),sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xt)),xH)))
    | ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ spl5_4
    | ~ spl5_11
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2121,f579]) ).

fof(f2123,plain,
    ( ~ aScalar0(sdtasdt0(sdtasdt0(sdtasasdt0(sziznziztdt0(xs),sziznziztdt0(xs)),xG),sdtasdt0(xF,sdtasasdt0(sziznziztdt0(xt),sziznziztdt0(xt)))))
    | ~ spl5_2
    | ~ spl5_4
    | ~ spl5_11
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2122,f460]) ).

fof(f2124,plain,
    ( $false
    | ~ spl5_2
    | ~ spl5_4
    | ~ spl5_11
    | spl5_17 ),
    inference(forward_subsumption_resolution,[],[f2123,f208]) ).

fof(f2125,plain,
    ( ~ spl5_2
    | ~ spl5_4
    | ~ spl5_11
    | spl5_17 ),
    inference(avatar_contradiction_clause,[],[f2124]) ).

cnf(s12,plain,
    ( ~ spl5_2
    | ~ spl5_6
    | ~ spl5_16
    | ~ spl5_17 ),
    inference(sat_conversion,[],[f621]) ).

cnf(s13,plain,
    spl5_2,
    inference(sat_conversion,[],[f628]) ).

cnf(s20,plain,
    ( ~ spl5_2
    | ~ spl5_4
    | spl5_6 ),
    inference(sat_conversion,[],[f727]) ).

cnf(s23,plain,
    ( ~ spl5_2
    | spl5_4 ),
    inference(sat_conversion,[],[f789]) ).

cnf(s39,plain,
    ( spl5_11
    | ~ spl5_13
    | ~ spl5_14 ),
    inference(sat_conversion,[],[f1564]) ).

cnf(s40,plain,
    spl5_13,
    inference(sat_conversion,[],[f1578]) ).

cnf(s41,plain,
    spl5_14,
    inference(sat_conversion,[],[f1596]) ).

cnf(s44,plain,
    ( ~ spl5_11
    | spl5_16 ),
    inference(sat_conversion,[],[f1724]) ).

cnf(s52,plain,
    ( ~ spl5_2
    | ~ spl5_4
    | ~ spl5_11
    | spl5_17 ),
    inference(sat_conversion,[],[f2125]) ).

cnf(s53,plain,
    spl5_11,
    inference(rat,[],[s39,s41,s40]) ).

cnf(s54,plain,
    spl5_16,
    inference(rat,[],[s44,s53]) ).

cnf(s66,plain,
    spl5_4,
    inference(rat,[],[s23,s13]) ).

cnf(s67,plain,
    spl5_17,
    inference(rat,[],[s52,s13,s53,s66]) ).

cnf(s73,plain,
    spl5_6,
    inference(rat,[],[s20,s13,s66]) ).

cnf(s75,plain,
    $false,
    inference(rat,[],[s12,s67,s54,s73,s13]) ).

fof(f2126,plain,
    $false,
    inference(avatar_sat_refutation,[],[s75]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : RNG067+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38  % Computer : n019.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Sun Sep 27 23:07:49 UTC 2026
% 0.12/0.39  % CPUTime  : 
% 0.12/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42  Running first-order theorem proving
% 0.12/0.42  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
% 2.06/1.31  % (3508964)Detected formulas, will run a generic FOF schedule.
% 2.06/1.31  % (3508975)dis-21_1_sil=8000:lcm=predicate:random_seed=2107512188: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)
% 2.06/1.31  % (3508975)Instruction limit reached! 
% 2.06/1.31  % (3508975)------------------------------
% 2.06/1.31  % (3508975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.06/1.31  % (3508975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/1.31  % (3508975)CaDiCaL version: 2.1.3
% 2.06/1.31  % (3508975)Termination reason: Instruction limit
% 2.06/1.31  % (3508975)Termination phase: Saturation
% 2.06/1.31  % (3508975)Time elapsed: 0.031 s
% 2.06/1.31  % (3508975)Peak memory usage: 89 MB
% 2.06/1.31  % (3508975)Instructions burned: 135 (million)
% 2.06/1.31  % (3508971)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=3735394104:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.06/1.31  % (3508972)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=168700366:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.06/1.31  % (3508970)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=3736133153:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.06/1.31  % (3508969)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=1391081608:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.06/1.31  % (3508973)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2219843891:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.06/1.31  % (3508974)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=754327247:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.06/1.31  % (3508972)First to succeed.
% 2.06/1.31  % (3508973)Also succeeded, but the first one will report.
% 2.06/1.31  % (3508972)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3508964"
% 2.06/1.31  % (3508978)lrs+10_1_sil=8000:sp=occurrence:random_seed=1822020836:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.06/1.31  % (3508974)Instruction limit reached! 
% 2.06/1.31  % (3508974)------------------------------
% 2.06/1.31  % (3508974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.06/1.31  % (3508974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.06/1.31  % (3508974)CaDiCaL version: 2.1.3
% 2.06/1.31  % (3508974)Termination reason: Instruction limit
% 2.06/1.31  % (3508974)Termination phase: Saturation
% 2.06/1.31  % (3508974)Time elapsed: 0.090 s
% 2.06/1.31  % (3508974)Peak memory usage: 90 MB
% 2.06/1.31  % (3508974)Instructions burned: 139 (million)
% 2.06/1.31  % (3508978)Also succeeded, but the first one will report.
% 2.06/1.31  % (3508985)lrs+10_1_sil=32000:urr=on:br=off:random_seed=757159422:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.06/1.31  % (3508972)Refutation found. Thanks to Tanya!
% 2.06/1.31  % SZS status Theorem for theBenchmark
% 2.06/1.31  % SZS output start Proof for theBenchmark
% See solution above
% 0.16/1.50  % (3508972)------------------------------
% 0.16/1.50  % (3508972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/1.50  % (3508972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/1.50  % (3508972)CaDiCaL version: 2.1.3
% 0.16/1.50  % (3508972)Termination reason: Refutation
% 0.16/1.50  % (3508972)Time elapsed: 0.046 s
% 0.16/1.50  % (3508972)Peak memory usage: 90 MB
% 0.16/1.50  % (3508972)Instructions burned: 87 (million)
% 0.16/1.50  % (3508972)------------------------------
% 0.16/1.50  % (3508972)------------------------------
% 0.16/1.50  % (3508964)Success in time 0.445 s
% 0.16/1.50  % Vampire exiting
%------------------------------------------------------------------------------