%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG063+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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:54 PM UTC 2026
% Result : Theorem 216.37s 36.07s
% Output : Refutation 216.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 112
% Syntax : Number of formulae : 846 ( 139 unt; 76 def)
% Number of atoms : 2606 ( 335 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 2661 ( 901 ~;1578 |; 81 &)
% ( 76 <=>; 25 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 82 ( 80 usr; 77 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 17 con; 0-2 aty)
% Number of variables : 327 ( 0 sgn 327 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
aScalar0(sz0z00),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSZeroSc) ).
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(f12,axiom,
! [X0] :
( aScalar0(X0)
=> aScalar0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mNegSc) ).
fof(f13,axiom,
! [X0] :
( aScalar0(X0)
=> ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScZero) ).
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(f17,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMNeg) ).
fof(f18,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMDNeg) ).
fof(f20,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLERef) ).
fof(f21,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEASm) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETrn) ).
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(f24,axiom,
! [X0,X1,X2,X3] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2)
& aScalar0(X3) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(sz0z00,X2)
& sdtlseqdt0(X2,X3) )
=> sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEMonM) ).
fof(f25,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETot) ).
fof(f26,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(sz0z00,X0)
& sdtlseqdt0(sz0z00,X1) )
=> ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mPosMon) ).
fof(f27,axiom,
! [X0] :
( aScalar0(X0)
=> sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSqPos) ).
fof(f28,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> ( ( sdtlseqdt0(sz0z00,X0)
& sdtlseqdt0(sz0z00,X1)
& sdtasdt0(X0,X0) = sdtasdt0(X1,X1) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSqrt) ).
fof(f37,axiom,
! [X0] :
( aVector0(X0)
=> sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mScSqPos) ).
fof(f42,axiom,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0) )
& xp = sziznziztdt0(xs) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1709) ).
fof(f43,axiom,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( aNaturalNumber0(X0)
=> sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0) )
& xq = sziznziztdt0(xt) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1726) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1746) ).
fof(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1766) ).
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(f49,axiom,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1837) ).
fof(f50,axiom,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1854) ).
fof(f51,axiom,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1873) ).
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,
( sdtasdt0(xR,smndt0(xS)) = smndt0(xN)
& sdtasdt0(smndt0(xS),xR) = smndt0(xN)
& sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2144) ).
fof(f61,axiom,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2262) ).
fof(f62,conjecture,
sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN) = sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f63,negated_conjecture,
sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN) != sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),
inference(negated_conjecture,[status(cth)],[f62]) ).
fof(f64,plain,
sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN),
inference(flattening,[],[f63]) ).
fof(f75,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f76,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f75]) ).
fof(f77,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f78,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f77]) ).
fof(f79,plain,
! [X0] :
( aScalar0(smndt0(X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f80,plain,
! [X0] :
( ( sdtpldt0(X0,sz0z00) = X0
& sdtpldt0(sz0z00,X0) = X0
& sdtasdt0(X0,sz0z00) = sz0z00
& sdtasdt0(sz0z00,X0) = sz0z00
& sdtpldt0(X0,smndt0(X0)) = sz0z00
& sdtpldt0(smndt0(X0),X0) = sz0z00
& smndt0(smndt0(X0)) = X0
& smndt0(sz0z00) = sz0z00 )
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f81,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(f82,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,[],[f81]) ).
fof(f87,plain,
! [X0,X1] :
( ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) )
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f88,plain,
! [X0,X1] :
( ( sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1))
& sdtasdt0(smndt0(X0),X1) = smndt0(sdtasdt0(X0,X1)) )
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f87]) ).
fof(f89,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f90,plain,
! [X0,X1] :
( sdtasdt0(smndt0(X0),smndt0(X1)) = sdtasdt0(X0,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f89]) ).
fof(f93,plain,
! [X0] :
( sdtlseqdt0(X0,X0)
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f94,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f95,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f94]) ).
fof(f96,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f97,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f96]) ).
fof(f98,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(f99,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,[],[f98]) ).
fof(f100,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(ennf_transformation,[],[f24]) ).
fof(f101,plain,
! [X0,X1,X2,X3] :
( sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X2,X3)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ aScalar0(X3) ),
inference(flattening,[],[f100]) ).
fof(f102,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f25]) ).
fof(f103,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) )
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f105,plain,
! [X0,X1] :
( ( sdtlseqdt0(sz0z00,sdtpldt0(X0,X1))
& sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) )
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| ~ aScalar0(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f107,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f28]) ).
fof(f108,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f107]) ).
fof(f123,plain,
! [X0] :
( sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| ~ aVector0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f126,plain,
( aVector0(xp)
& szszuzczcdt0(aDimensionOf0(xp)) = aDimensionOf0(xs)
& ! [X0] :
( sdtlbdtrb0(xp,X0) = sdtlbdtrb0(xs,X0)
| ~ aNaturalNumber0(X0) )
& xp = sziznziztdt0(xs) ),
inference(ennf_transformation,[],[f42]) ).
fof(f127,plain,
( aVector0(xq)
& szszuzczcdt0(aDimensionOf0(xq)) = aDimensionOf0(xt)
& ! [X0] :
( sdtlbdtrb0(xq,X0) = sdtlbdtrb0(xt,X0)
| ~ aNaturalNumber0(X0) )
& xq = sziznziztdt0(xt) ),
inference(ennf_transformation,[],[f43]) ).
fof(f135,plain,
aScalar0(sz0z00),
inference(cnf_transformation,[],[f9]) ).
fof(f136,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| aScalar0(sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f76]) ).
fof(f137,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| aScalar0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f78]) ).
fof(f138,plain,
! [X0] :
( ~ aScalar0(X0)
| aScalar0(smndt0(X0)) ),
inference(cnf_transformation,[],[f79]) ).
fof(f139,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = smndt0(sz0z00) ),
inference(cnf_transformation,[],[f80]) ).
fof(f140,plain,
! [X0] :
( ~ aScalar0(X0)
| smndt0(smndt0(X0)) = X0 ),
inference(cnf_transformation,[],[f80]) ).
fof(f142,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtpldt0(X0,smndt0(X0)) ),
inference(cnf_transformation,[],[f80]) ).
fof(f143,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(sz0z00,X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f144,plain,
! [X0] :
( ~ aScalar0(X0)
| sz0z00 = sdtasdt0(X0,sz0z00) ),
inference(cnf_transformation,[],[f80]) ).
fof(f145,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(sz0z00,X0) = X0 ),
inference(cnf_transformation,[],[f80]) ).
fof(f146,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(X0,sz0z00) = X0 ),
inference(cnf_transformation,[],[f80]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f82]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(cnf_transformation,[],[f82]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
inference(cnf_transformation,[],[f82]) ).
fof(f154,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| smndt0(sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f155,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f88]) ).
fof(f156,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(smndt0(X0),smndt0(X1)) ),
inference(cnf_transformation,[],[f90]) ).
fof(f157,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtlseqdt0(X0,X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f158,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f95]) ).
fof(f159,plain,
! [X2,X0,X1] :
( ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(cnf_transformation,[],[f97]) ).
fof(f160,plain,
! [X2,X3,X0,X1] :
( ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3)) ),
inference(cnf_transformation,[],[f99]) ).
fof(f161,plain,
! [X2,X3,X0,X1] :
( ~ aScalar0(X3)
| ~ aScalar0(X2)
| ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(X2,X3)
| ~ sdtlseqdt0(sz0z00,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3)) ),
inference(cnf_transformation,[],[f101]) ).
fof(f162,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f163,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f105]) ).
fof(f165,plain,
! [X0] :
( ~ aScalar0(X0)
| sdtlseqdt0(sz0z00,sdtasdt0(X0,X0)) ),
inference(cnf_transformation,[],[f106]) ).
fof(f166,plain,
! [X0,X1] :
( ~ aScalar0(X1)
| ~ aScalar0(X0)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ sdtlseqdt0(sz0z00,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f108]) ).
fof(f178,plain,
! [X0] :
( ~ aVector0(X0)
| sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f187,plain,
aVector0(xp),
inference(cnf_transformation,[],[f126]) ).
fof(f191,plain,
aVector0(xq),
inference(cnf_transformation,[],[f127]) ).
fof(f193,plain,
aScalar0(xA),
inference(cnf_transformation,[],[f44]) ).
fof(f195,plain,
aScalar0(xB),
inference(cnf_transformation,[],[f45]) ).
fof(f196,plain,
xC = sdtasasdt0(xp,xp),
inference(cnf_transformation,[],[f46]) ).
fof(f197,plain,
aScalar0(xC),
inference(cnf_transformation,[],[f46]) ).
fof(f198,plain,
xD = sdtasasdt0(xq,xq),
inference(cnf_transformation,[],[f47]) ).
fof(f199,plain,
aScalar0(xD),
inference(cnf_transformation,[],[f47]) ).
fof(f201,plain,
aScalar0(xE),
inference(cnf_transformation,[],[f48]) ).
fof(f202,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[],[f49]) ).
fof(f203,plain,
aScalar0(xF),
inference(cnf_transformation,[],[f49]) ).
fof(f204,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[],[f50]) ).
fof(f205,plain,
aScalar0(xG),
inference(cnf_transformation,[],[f50]) ).
fof(f207,plain,
aScalar0(xH),
inference(cnf_transformation,[],[f51]) ).
fof(f208,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[],[f52]) ).
fof(f209,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f210,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[],[f53]) ).
fof(f211,plain,
aScalar0(xP),
inference(cnf_transformation,[],[f53]) ).
fof(f212,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[],[f54]) ).
fof(f213,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f214,plain,
xN = sdtasdt0(xR,xS),
inference(cnf_transformation,[],[f55]) ).
fof(f215,plain,
aScalar0(xN),
inference(cnf_transformation,[],[f55]) ).
fof(f217,plain,
sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(cnf_transformation,[],[f57]) ).
fof(f218,plain,
sdtasdt0(smndt0(xS),smndt0(xS)) = sdtasdt0(xS,xS),
inference(cnf_transformation,[],[f58]) ).
fof(f219,plain,
smndt0(xN) = sdtasdt0(smndt0(xS),xR),
inference(cnf_transformation,[],[f58]) ).
fof(f223,plain,
sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))) = sdtpldt0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)),smndt0(xN)),
inference(cnf_transformation,[],[f61]) ).
fof(f224,plain,
sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xN),xN),
inference(cnf_transformation,[],[f64]) ).
fof(f228,plain,
~ aScalar0(sz0z00),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f229,plain,
! [X0,X1] :
( ~ aScalar0(sdtpldt0(X0,X1))
| aScalar0(X0)
| aScalar0(X1) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f230,plain,
! [X0,X1] :
( ~ aScalar0(sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(X1) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f231,plain,
! [X0] :
( ~ aScalar0(smndt0(X0))
| aScalar0(X0) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f232,plain,
! [X0] :
( aScalar0(X0)
| sdtpldt0(X0,sz0z00) = X0 ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f233,plain,
! [X0] :
( aScalar0(X0)
| sdtpldt0(sz0z00,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f234,plain,
! [X0] :
( aScalar0(X0)
| sz0z00 = sdtasdt0(X0,sz0z00) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f235,plain,
! [X0] :
( aScalar0(X0)
| sz0z00 = sdtasdt0(sz0z00,X0) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f236,plain,
! [X0] :
( aScalar0(X0)
| sz0z00 = sdtpldt0(X0,smndt0(X0)) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f238,plain,
! [X0] :
( aScalar0(X0)
| smndt0(smndt0(X0)) = X0 ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f239,plain,
! [X0] :
( aScalar0(X0)
| sz0z00 = smndt0(sz0z00) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f240,plain,
! [X2,X0,X1] :
( aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f242,plain,
! [X2,X0,X1] :
( aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f243,plain,
! [X2,X0,X1] :
( aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f247,plain,
! [X0,X1] :
( aScalar0(X1)
| aScalar0(X0)
| sdtasdt0(X0,smndt0(X1)) = smndt0(sdtasdt0(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f248,plain,
! [X0,X1] :
( aScalar0(X1)
| aScalar0(X0)
| smndt0(sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f249,plain,
! [X0,X1] :
( aScalar0(X1)
| aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(smndt0(X0),smndt0(X1)) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f250,plain,
! [X0] :
( ~ sdtlseqdt0(X0,X0)
| aScalar0(X0) ),
inference(consistent_polarity_flipping,[],[f157]) ).
fof(f251,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| aScalar0(X1)
| aScalar0(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f252,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(X0,X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,X2)
| sdtlseqdt0(X0,X1)
| aScalar0(X2) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f253,plain,
! [X2,X3,X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X3))
| aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X2,X3)
| sdtlseqdt0(X0,X1)
| aScalar0(X3) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f254,plain,
! [X2,X3,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X2),sdtasdt0(X1,X3))
| aScalar0(X2)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X2,X3)
| sdtlseqdt0(sz0z00,X2)
| sdtlseqdt0(X0,X1)
| aScalar0(X3) ),
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f255,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| aScalar0(X0)
| ~ sdtlseqdt0(X1,X0)
| aScalar0(X1) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f257,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,X0)
| aScalar0(X1) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f258,plain,
! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasdt0(X0,X0))
| aScalar0(X0) ),
inference(consistent_polarity_flipping,[],[f165]) ).
fof(f259,plain,
! [X0,X1] :
( sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| aScalar0(X0)
| aScalar0(X1)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(sz0z00,X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f271,plain,
! [X0] :
( ~ sdtlseqdt0(sz0z00,sdtasasdt0(X0,X0))
| aVector0(X0) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f275,plain,
~ aVector0(xp),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f276,plain,
~ aVector0(xq),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f277,plain,
~ aScalar0(xA),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f278,plain,
~ aScalar0(xB),
inference(consistent_polarity_flipping,[],[f195]) ).
fof(f279,plain,
~ aScalar0(xC),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f280,plain,
~ aScalar0(xD),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f281,plain,
~ aScalar0(xE),
inference(consistent_polarity_flipping,[],[f201]) ).
fof(f282,plain,
~ aScalar0(xF),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f283,plain,
~ aScalar0(xG),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f284,plain,
~ aScalar0(xH),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f285,plain,
~ aScalar0(xR),
inference(consistent_polarity_flipping,[],[f209]) ).
fof(f286,plain,
~ aScalar0(xP),
inference(consistent_polarity_flipping,[],[f211]) ).
fof(f287,plain,
~ aScalar0(xS),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f288,plain,
~ aScalar0(xN),
inference(consistent_polarity_flipping,[],[f215]) ).
fof(f290,plain,
~ sdtlseqdt0(sdtasdt0(xP,xP),xN),
inference(consistent_polarity_flipping,[],[f217]) ).
fof(f292,definition,
( spl2_1
<=> ! [X0,X1] :
( aScalar0(X1)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition]) ).
fof(f293,plain,
( ! [X0,X1] :
( aScalar0(X1)
| aScalar0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ spl2_1 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f295,definition,
( spl2_2
<=> ! [X2] : aScalar0(X2) ),
introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition]) ).
fof(f296,plain,
( ! [X2] : aScalar0(X2)
| ~ spl2_2 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f297,plain,
( spl2_1
| spl2_2 ),
inference(avatar_split_clause,[],[f243,f295,f292]) ).
fof(f303,definition,
( spl2_4
<=> sz0z00 = smndt0(sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_4])],[avatar_definition]) ).
fof(f305,plain,
( sz0z00 = smndt0(sz0z00)
| ~ spl2_4 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f306,plain,
( spl2_4
| spl2_2 ),
inference(avatar_split_clause,[],[f239,f295,f303]) ).
fof(f319,plain,
( $false
| ~ spl2_2 ),
inference(backward_subsumption_resolution,[],[f288,f296]) ).
fof(f332,plain,
~ spl2_2,
inference(avatar_contradiction_clause,[],[f319]) ).
fof(f362,plain,
sz0z00 = sdtpldt0(sz0z00,sz0z00),
inference(resolution,[],[f232,f228]) ).
fof(f368,plain,
xE = sdtpldt0(xE,sz0z00),
inference(resolution,[],[f232,f281]) ).
fof(f371,plain,
xH = sdtpldt0(xH,sz0z00),
inference(resolution,[],[f232,f284]) ).
fof(f372,plain,
xR = sdtpldt0(xR,sz0z00),
inference(resolution,[],[f232,f285]) ).
fof(f374,plain,
xS = sdtpldt0(xS,sz0z00),
inference(resolution,[],[f232,f287]) ).
fof(f390,plain,
sz0z00 = sdtasdt0(sz0z00,sz0z00),
inference(resolution,[],[f234,f228]) ).
fof(f396,plain,
sz0z00 = sdtasdt0(xE,sz0z00),
inference(resolution,[],[f234,f281]) ).
fof(f400,plain,
sz0z00 = sdtasdt0(xR,sz0z00),
inference(resolution,[],[f234,f285]) ).
fof(f401,plain,
sz0z00 = sdtasdt0(xP,sz0z00),
inference(resolution,[],[f234,f286]) ).
fof(f403,plain,
sz0z00 = sdtasdt0(xN,sz0z00),
inference(resolution,[],[f234,f288]) ).
fof(f414,plain,
sz0z00 = sdtasdt0(sz0z00,xR),
inference(resolution,[],[f235,f285]) ).
fof(f428,plain,
xR = smndt0(smndt0(xR)),
inference(resolution,[],[f238,f285]) ).
fof(f429,plain,
xP = smndt0(smndt0(xP)),
inference(resolution,[],[f238,f286]) ).
fof(f431,plain,
xN = smndt0(smndt0(xN)),
inference(resolution,[],[f238,f288]) ).
fof(f433,plain,
( ~ sdtlseqdt0(sz0z00,xF)
| aScalar0(xA) ),
inference(superposition,[],[f258,f202]) ).
fof(f434,plain,
( ~ sdtlseqdt0(sz0z00,xG)
| aScalar0(xB) ),
inference(superposition,[],[f258,f204]) ).
fof(f435,plain,
~ sdtlseqdt0(sz0z00,xG),
inference(forward_subsumption_resolution,[],[f434,f278]) ).
fof(f436,plain,
~ sdtlseqdt0(sz0z00,xF),
inference(forward_subsumption_resolution,[],[f433,f277]) ).
fof(f437,plain,
( ~ sdtlseqdt0(sz0z00,xC)
| aVector0(xp) ),
inference(superposition,[],[f271,f196]) ).
fof(f438,plain,
( ~ sdtlseqdt0(sz0z00,xD)
| aVector0(xq) ),
inference(superposition,[],[f271,f198]) ).
fof(f439,plain,
~ sdtlseqdt0(sz0z00,xD),
inference(forward_subsumption_resolution,[],[f438,f276]) ).
fof(f440,plain,
~ sdtlseqdt0(sz0z00,xC),
inference(forward_subsumption_resolution,[],[f437,f275]) ).
fof(f454,plain,
( ~ aScalar0(smndt0(xN))
| aScalar0(smndt0(xS))
| aScalar0(xR) ),
inference(superposition,[],[f230,f219]) ).
fof(f466,plain,
( ~ aScalar0(smndt0(xN))
| aScalar0(smndt0(xS)) ),
inference(forward_subsumption_resolution,[],[f454,f285]) ).
fof(f468,definition,
( spl2_9
<=> aScalar0(smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_9])],[avatar_definition]) ).
fof(f469,plain,
( ~ aScalar0(smndt0(xS))
| spl2_9 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( aScalar0(smndt0(xS))
| ~ spl2_9 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl2_10
<=> aScalar0(smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl2_10])],[avatar_definition]) ).
fof(f474,plain,
( ~ aScalar0(smndt0(xN))
| spl2_10 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,plain,
( spl2_9
| ~ spl2_10 ),
inference(avatar_split_clause,[],[f466,f472,f468]) ).
fof(f488,plain,
sz0z00 = sdtpldt0(xE,smndt0(xE)),
inference(resolution,[],[f236,f281]) ).
fof(f491,plain,
sz0z00 = sdtpldt0(xH,smndt0(xH)),
inference(resolution,[],[f236,f284]) ).
fof(f494,plain,
sz0z00 = sdtpldt0(xS,smndt0(xS)),
inference(resolution,[],[f236,f287]) ).
fof(f537,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xS,xS))
| aScalar0(smndt0(xS)) ),
inference(superposition,[],[f258,f218]) ).
fof(f538,plain,
( ~ aScalar0(sdtasdt0(xS,xS))
| aScalar0(smndt0(xS))
| aScalar0(smndt0(xS)) ),
inference(superposition,[],[f230,f218]) ).
fof(f539,plain,
( ~ aScalar0(sdtasdt0(xS,xS))
| aScalar0(smndt0(xS)) ),
inference(duplicate_literal_removal,[],[f538]) ).
fof(f541,definition,
( spl2_11
<=> aScalar0(sdtasdt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_11])],[avatar_definition]) ).
fof(f543,plain,
( ~ aScalar0(sdtasdt0(xS,xS))
| spl2_11 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( spl2_9
| ~ spl2_11 ),
inference(avatar_split_clause,[],[f539,f541,f468]) ).
fof(f546,definition,
( spl2_12
<=> sdtlseqdt0(sz0z00,sdtasdt0(xS,xS)) ),
introduced(definition,[new_symbols(definition,[spl2_12])],[avatar_definition]) ).
fof(f548,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xS,xS))
| spl2_12 ),
inference(avatar_component_clause,[],[f546]) ).
fof(f549,plain,
( spl2_9
| ~ spl2_12 ),
inference(avatar_split_clause,[],[f537,f546,f468]) ).
fof(f587,plain,
( ! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xE) = sdtasdt0(xE,X0) )
| ~ spl2_1 ),
inference(resolution,[],[f293,f281]) ).
fof(f591,plain,
( ! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xR) = sdtasdt0(xR,X0) )
| ~ spl2_1 ),
inference(resolution,[],[f293,f285]) ).
fof(f592,plain,
( ! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xP) = sdtasdt0(xP,X0) )
| ~ spl2_1 ),
inference(resolution,[],[f293,f286]) ).
fof(f668,plain,
! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,smndt0(xP)) = smndt0(sdtasdt0(X0,xP)) ),
inference(resolution,[],[f247,f286]) ).
fof(f697,plain,
! [X0] :
( aScalar0(X0)
| smndt0(sdtasdt0(X0,xE)) = sdtasdt0(smndt0(X0),xE) ),
inference(resolution,[],[f248,f281]) ).
fof(f734,plain,
! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xH) = sdtasdt0(smndt0(X0),smndt0(xH)) ),
inference(resolution,[],[f249,f284]) ).
fof(f735,plain,
! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xR) = sdtasdt0(smndt0(X0),smndt0(xR)) ),
inference(resolution,[],[f249,f285]) ).
fof(f736,plain,
! [X0] :
( aScalar0(X0)
| sdtasdt0(X0,xP) = sdtasdt0(smndt0(X0),smndt0(xP)) ),
inference(resolution,[],[f249,f286]) ).
fof(f758,plain,
( sdtlseqdt0(xN,sdtasdt0(xP,xP))
| aScalar0(sdtasdt0(xP,xP))
| aScalar0(xN)
| xN = sdtasdt0(xP,xP) ),
inference(resolution,[],[f251,f290]) ).
fof(f767,plain,
( sdtlseqdt0(xN,sdtasdt0(xP,xP))
| aScalar0(sdtasdt0(xP,xP))
| xN = sdtasdt0(xP,xP) ),
inference(forward_subsumption_resolution,[],[f758,f288]) ).
fof(f769,definition,
( spl2_17
<=> xN = sdtasdt0(xP,xP) ),
introduced(definition,[new_symbols(definition,[spl2_17])],[avatar_definition]) ).
fof(f771,plain,
( xN = sdtasdt0(xP,xP)
| ~ spl2_17 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f773,definition,
( spl2_18
<=> aScalar0(sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_18])],[avatar_definition]) ).
fof(f774,plain,
( ~ aScalar0(sdtasdt0(xP,xP))
| spl2_18 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f775,plain,
( aScalar0(sdtasdt0(xP,xP))
| ~ spl2_18 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f777,definition,
( spl2_19
<=> sdtlseqdt0(xN,sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_19])],[avatar_definition]) ).
fof(f779,plain,
( sdtlseqdt0(xN,sdtasdt0(xP,xP))
| ~ spl2_19 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f781,plain,
( spl2_17
| spl2_18
| spl2_19 ),
inference(avatar_split_clause,[],[f767,f777,f773,f769]) ).
fof(f827,plain,
! [X2,X0,X1] :
( aScalar0(X0)
| aScalar0(X1)
| sdtlseqdt0(X0,X2)
| sdtlseqdt0(X1,X0)
| aScalar0(X2)
| sdtlseqdt0(X2,X1)
| aScalar0(X1)
| aScalar0(X2)
| X1 = X2 ),
inference(resolution,[],[f252,f251]) ).
fof(f828,plain,
! [X2,X0,X1] :
( sdtlseqdt0(X0,X2)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X2,X1)
| aScalar0(X1)
| aScalar0(X2)
| aScalar0(X0)
| X1 = X2 ),
inference(duplicate_literal_removal,[],[f827]) ).
fof(f830,plain,
( sdtasdt0(xS,xS) = sdtpldt0(sdtasdt0(xS,xS),sz0z00)
| spl2_11 ),
inference(resolution,[],[f543,f232]) ).
fof(f831,plain,
( sdtasdt0(xS,xS) = sdtpldt0(sz0z00,sdtasdt0(xS,xS))
| spl2_11 ),
inference(resolution,[],[f543,f233]) ).
fof(f852,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| aScalar0(xC)
| sdtlseqdt0(sz0z00,xG)
| sdtlseqdt0(sz0z00,xC)
| aScalar0(xG) ),
inference(superposition,[],[f257,f208]) ).
fof(f854,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| aScalar0(xF)
| sdtlseqdt0(sz0z00,xD)
| sdtlseqdt0(sz0z00,xF)
| aScalar0(xD) ),
inference(superposition,[],[f257,f212]) ).
fof(f855,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| aScalar0(xR)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(sz0z00,xR)
| aScalar0(xS) ),
inference(superposition,[],[f257,f214]) ).
fof(f861,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(sz0z00,xR)
| aScalar0(xS) ),
inference(forward_subsumption_resolution,[],[f855,f285]) ).
fof(f862,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(sz0z00,xD)
| sdtlseqdt0(sz0z00,xF)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f854,f282]) ).
fof(f864,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(sz0z00,xG)
| sdtlseqdt0(sz0z00,xC)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f852,f279]) ).
fof(f867,definition,
( spl2_22
<=> sdtlseqdt0(sz0z00,smndt0(xS)) ),
introduced(definition,[new_symbols(definition,[spl2_22])],[avatar_definition]) ).
fof(f869,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| ~ spl2_22 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f873,definition,
( spl2_23
<=> sdtlseqdt0(sz0z00,xR) ),
introduced(definition,[new_symbols(definition,[spl2_23])],[avatar_definition]) ).
fof(f874,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| spl2_23 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f877,definition,
( spl2_24
<=> sdtlseqdt0(sz0z00,smndt0(xN)) ),
introduced(definition,[new_symbols(definition,[spl2_24])],[avatar_definition]) ).
fof(f881,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(sz0z00,xR) ),
inference(forward_subsumption_resolution,[],[f861,f287]) ).
fof(f882,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(sz0z00,xF)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f862,f439]) ).
fof(f884,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(sz0z00,xC)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f864,f435]) ).
fof(f888,definition,
( spl2_25
<=> sdtlseqdt0(sz0z00,xS) ),
introduced(definition,[new_symbols(definition,[spl2_25])],[avatar_definition]) ).
fof(f889,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| spl2_25 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f892,definition,
( spl2_26
<=> sdtlseqdt0(sz0z00,xN) ),
introduced(definition,[new_symbols(definition,[spl2_26])],[avatar_definition]) ).
fof(f894,plain,
( ~ sdtlseqdt0(sz0z00,xN)
| spl2_26 ),
inference(avatar_component_clause,[],[f892]) ).
fof(f895,plain,
( spl2_23
| spl2_25
| ~ spl2_26 ),
inference(avatar_split_clause,[],[f881,f892,f888,f873]) ).
fof(f896,plain,
( ~ sdtlseqdt0(sz0z00,xS)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f882,f436]) ).
fof(f898,definition,
( spl2_27
<=> sdtlseqdt0(sz0z00,xE) ),
introduced(definition,[new_symbols(definition,[spl2_27])],[avatar_definition]) ).
fof(f902,definition,
( spl2_28
<=> sdtlseqdt0(sz0z00,xH) ),
introduced(definition,[new_symbols(definition,[spl2_28])],[avatar_definition]) ).
fof(f906,definition,
( spl2_29
<=> sdtlseqdt0(sz0z00,xP) ),
introduced(definition,[new_symbols(definition,[spl2_29])],[avatar_definition]) ).
fof(f907,plain,
( sdtlseqdt0(sz0z00,xP)
| ~ spl2_29 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f908,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| spl2_29 ),
inference(avatar_component_clause,[],[f906]) ).
fof(f910,plain,
( ~ sdtlseqdt0(sz0z00,xR)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f884,f440]) ).
fof(f920,plain,
~ sdtlseqdt0(sz0z00,xS),
inference(forward_subsumption_resolution,[],[f896,f280]) ).
fof(f921,plain,
~ sdtlseqdt0(sz0z00,xR),
inference(forward_subsumption_resolution,[],[f910,f283]) ).
fof(f922,plain,
~ spl2_25,
inference(avatar_split_clause,[],[f920,f888]) ).
fof(f923,plain,
~ spl2_23,
inference(avatar_split_clause,[],[f921,f873]) ).
fof(f985,plain,
! [X0,X1] :
( aScalar0(X0)
| aScalar0(X1)
| sdtpldt0(sdtpldt0(X1,X0),X0) = sdtpldt0(X1,sdtpldt0(X0,X0)) ),
inference(factoring,[],[f240]) ).
fof(f1002,plain,
! [X0,X1] :
( aScalar0(X0)
| aScalar0(X1)
| sdtasdt0(sdtasdt0(X1,X0),xR) = sdtasdt0(X1,sdtasdt0(X0,xR)) ),
inference(resolution,[],[f242,f285]) ).
fof(f1110,definition,
( spl2_32
<=> sz0z00 = xS ),
introduced(definition,[new_symbols(definition,[spl2_32])],[avatar_definition]) ).
fof(f1111,plain,
( sz0z00 != xS
| spl2_32 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1112,plain,
( sz0z00 = xS
| ~ spl2_32 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1114,definition,
( spl2_33
<=> sdtlseqdt0(xS,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_33])],[avatar_definition]) ).
fof(f1116,plain,
( sdtlseqdt0(xS,sz0z00)
| ~ spl2_33 ),
inference(avatar_component_clause,[],[f1114]) ).
fof(f1176,plain,
! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| aScalar0(smndt0(xS))
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,smndt0(xS))
| smndt0(xS) = X0 ),
inference(superposition,[],[f259,f218]) ).
fof(f1187,definition,
( spl2_34
<=> ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| smndt0(xS) = X0
| sdtlseqdt0(sz0z00,X0)
| aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_34])],[avatar_definition]) ).
fof(f1188,plain,
( ! [X0] :
( sdtasdt0(X0,X0) != sdtasdt0(xS,xS)
| smndt0(xS) = X0
| sdtlseqdt0(sz0z00,X0)
| aScalar0(X0) )
| ~ spl2_34 ),
inference(avatar_component_clause,[],[f1187]) ).
fof(f1192,plain,
( spl2_22
| spl2_9
| spl2_34 ),
inference(avatar_split_clause,[],[f1176,f1187,f468,f867]) ).
fof(f1237,definition,
( spl2_39
<=> aScalar0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS)))) ),
introduced(definition,[new_symbols(definition,[spl2_39])],[avatar_definition]) ).
fof(f1239,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| spl2_39 ),
inference(avatar_component_clause,[],[f1237]) ).
fof(f1293,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| aScalar0(smndt0(xN)) ),
inference(superposition,[],[f229,f223]) ).
fof(f1294,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))))
| aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| spl2_10 ),
inference(forward_subsumption_resolution,[],[f1293,f474]) ).
fof(f1299,definition,
( spl2_49
<=> aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN))) ),
introduced(definition,[new_symbols(definition,[spl2_49])],[avatar_definition]) ).
fof(f1301,plain,
( aScalar0(sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)),smndt0(xN)))
| ~ spl2_49 ),
inference(avatar_component_clause,[],[f1299]) ).
fof(f1322,plain,
! [X0,X1] :
( ~ sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| aScalar0(xR)
| aScalar0(X0)
| aScalar0(smndt0(xS))
| sdtlseqdt0(xR,X1)
| sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(smndt0(xS),X0)
| aScalar0(X1) ),
inference(superposition,[],[f254,f219]) ).
fof(f1327,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xR,sdtasdt0(X0,X1))
| aScalar0(xG)
| aScalar0(X0)
| aScalar0(xC)
| sdtlseqdt0(xG,X1)
| sdtlseqdt0(sz0z00,xG)
| sdtlseqdt0(xC,X0)
| aScalar0(X1) ),
inference(superposition,[],[f254,f208]) ).
fof(f1329,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtasdt0(X0,X1))
| aScalar0(xD)
| aScalar0(X0)
| aScalar0(xF)
| sdtlseqdt0(xD,X1)
| sdtlseqdt0(sz0z00,xD)
| sdtlseqdt0(xF,X0)
| aScalar0(X1) ),
inference(superposition,[],[f254,f212]) ).
fof(f1330,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xN,sdtasdt0(X0,X1))
| aScalar0(xS)
| aScalar0(X0)
| aScalar0(xR)
| sdtlseqdt0(xS,X1)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xR,X0)
| aScalar0(X1) ),
inference(superposition,[],[f254,f214]) ).
fof(f1332,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| aScalar0(X1)
| aScalar0(smndt0(xS))
| aScalar0(X0)
| sdtlseqdt0(X1,xR)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,smndt0(xS))
| aScalar0(xR) ),
inference(superposition,[],[f254,f219]) ).
fof(f1338,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xP)
| aScalar0(X1)
| aScalar0(xE)
| aScalar0(X0)
| sdtlseqdt0(X1,xH)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xE)
| aScalar0(xH) ),
inference(superposition,[],[f254,f210]) ).
fof(f1340,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| aScalar0(X1)
| aScalar0(xR)
| aScalar0(X0)
| sdtlseqdt0(X1,xS)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xR)
| aScalar0(xS) ),
inference(superposition,[],[f254,f214]) ).
fof(f1349,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,xS)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xR)
| aScalar0(xS) ),
inference(forward_subsumption_resolution,[],[f1340,f285]) ).
fof(f1351,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xP)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,xH)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xE)
| aScalar0(xH) ),
inference(forward_subsumption_resolution,[],[f1338,f281]) ).
fof(f1360,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| aScalar0(X1)
| aScalar0(smndt0(xS))
| aScalar0(X0)
| sdtlseqdt0(X1,xR)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,smndt0(xS)) ),
inference(forward_subsumption_resolution,[],[f1332,f285]) ).
fof(f1362,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xN,sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(xR)
| sdtlseqdt0(xS,X1)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xR,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1330,f287]) ).
fof(f1363,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(xF)
| sdtlseqdt0(xD,X1)
| sdtlseqdt0(sz0z00,xD)
| sdtlseqdt0(xF,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1329,f280]) ).
fof(f1365,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xR,sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(xC)
| sdtlseqdt0(xG,X1)
| sdtlseqdt0(sz0z00,xG)
| sdtlseqdt0(xC,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1327,f283]) ).
fof(f1372,plain,
! [X0,X1] :
( ~ sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(smndt0(xS))
| sdtlseqdt0(xR,X1)
| sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(smndt0(xS),X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1322,f285]) ).
fof(f1379,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xN)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,xS)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xR) ),
inference(forward_subsumption_resolution,[],[f1349,f287]) ).
fof(f1381,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),xP)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,xH)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X0,xE) ),
inference(forward_subsumption_resolution,[],[f1351,f284]) ).
fof(f1385,definition,
( spl2_56
<=> ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| sdtlseqdt0(X0,smndt0(xS))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X1,xR)
| aScalar0(X0)
| aScalar0(X1) ) ),
introduced(definition,[new_symbols(definition,[spl2_56])],[avatar_definition]) ).
fof(f1386,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),smndt0(xN))
| sdtlseqdt0(X0,smndt0(xS))
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(X1,xR)
| aScalar0(X0)
| aScalar0(X1) )
| ~ spl2_56 ),
inference(avatar_component_clause,[],[f1385]) ).
fof(f1387,plain,
( spl2_9
| spl2_56 ),
inference(avatar_split_clause,[],[f1360,f1385,f468]) ).
fof(f1392,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xN,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xS,X1)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xR,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1362,f285]) ).
fof(f1393,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xD,X1)
| sdtlseqdt0(sz0z00,xD)
| sdtlseqdt0(xF,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1363,f282]) ).
fof(f1395,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xR,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xG,X1)
| sdtlseqdt0(sz0z00,xG)
| sdtlseqdt0(xC,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1365,f279]) ).
fof(f1401,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| aScalar0(X0)
| aScalar0(smndt0(xS))
| sdtlseqdt0(xR,X1)
| sdtlseqdt0(smndt0(xS),X0)
| aScalar0(X1) )
| spl2_23 ),
inference(forward_subsumption_resolution,[],[f1372,f874]) ).
fof(f1404,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(xN,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xS,X1)
| sdtlseqdt0(xR,X0)
| aScalar0(X1) )
| spl2_25 ),
inference(forward_subsumption_resolution,[],[f1392,f889]) ).
fof(f1405,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xD,X1)
| sdtlseqdt0(xF,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1393,f439]) ).
fof(f1407,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xR,sdtasdt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(xG,X1)
| sdtlseqdt0(xC,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1395,f435]) ).
fof(f1413,definition,
( spl2_60
<=> ! [X0,X1] :
( ~ sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| aScalar0(X1)
| sdtlseqdt0(smndt0(xS),X0)
| sdtlseqdt0(xR,X1)
| aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_60])],[avatar_definition]) ).
fof(f1414,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(smndt0(xN),sdtasdt0(X0,X1))
| aScalar0(X1)
| sdtlseqdt0(smndt0(xS),X0)
| sdtlseqdt0(xR,X1)
| aScalar0(X0) )
| ~ spl2_60 ),
inference(avatar_component_clause,[],[f1413]) ).
fof(f1415,plain,
( spl2_9
| spl2_60
| spl2_23 ),
inference(avatar_split_clause,[],[f1401,f873,f1413,f468]) ).
fof(f1416,plain,
( aScalar0(xS)
| ~ spl2_9 ),
inference(resolution,[],[f470,f231]) ).
fof(f1417,plain,
( $false
| ~ spl2_9 ),
inference(forward_subsumption_resolution,[],[f1416,f287]) ).
fof(f1418,plain,
~ spl2_9,
inference(avatar_contradiction_clause,[],[f1417]) ).
fof(f1419,plain,
( spl2_49
| ~ spl2_39
| spl2_10 ),
inference(avatar_split_clause,[],[f1294,f472,f1237,f1299]) ).
fof(f1424,plain,
( smndt0(xS) = sdtpldt0(sz0z00,smndt0(xS))
| spl2_9 ),
inference(resolution,[],[f469,f233]) ).
fof(f1425,plain,
( sz0z00 = sdtasdt0(smndt0(xS),sz0z00)
| spl2_9 ),
inference(resolution,[],[f469,f234]) ).
fof(f1597,plain,
( xS = smndt0(xS)
| ~ spl2_4
| ~ spl2_32 ),
inference(superposition,[],[f305,f1112]) ).
fof(f1604,plain,
( ~ sdtlseqdt0(xS,xN)
| spl2_26
| ~ spl2_32 ),
inference(superposition,[],[f894,f1112]) ).
fof(f1647,plain,
( aScalar0(sz0z00)
| ~ sdtlseqdt0(smndt0(xS),sz0z00)
| aScalar0(smndt0(xS))
| ~ spl2_22 ),
inference(resolution,[],[f869,f255]) ).
fof(f1648,plain,
( ~ sdtlseqdt0(smndt0(xS),sz0z00)
| aScalar0(smndt0(xS))
| ~ spl2_22 ),
inference(forward_subsumption_resolution,[],[f1647,f228]) ).
fof(f1650,plain,
( ~ sdtlseqdt0(smndt0(xS),sz0z00)
| spl2_9
| ~ spl2_22 ),
inference(forward_subsumption_resolution,[],[f1648,f469]) ).
fof(f1714,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xE)
| aScalar0(X1)
| aScalar0(xE)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xE)
| aScalar0(sz0z00) ),
inference(superposition,[],[f253,f368]) ).
fof(f1719,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xE)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xE)
| aScalar0(sz0z00) ),
inference(forward_subsumption_resolution,[],[f1714,f281]) ).
fof(f1721,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xE)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xE) ),
inference(forward_subsumption_resolution,[],[f1719,f228]) ).
fof(f1738,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xH)
| aScalar0(X1)
| aScalar0(xH)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xH)
| aScalar0(sz0z00) ),
inference(superposition,[],[f253,f371]) ).
fof(f1743,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xH)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xH)
| aScalar0(sz0z00) ),
inference(forward_subsumption_resolution,[],[f1738,f284]) ).
fof(f1745,plain,
! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),xH)
| aScalar0(X1)
| aScalar0(X0)
| sdtlseqdt0(X1,sz0z00)
| sdtlseqdt0(X0,xH) ),
inference(forward_subsumption_resolution,[],[f1743,f228]) ).
fof(f1766,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtpldt0(X0,X1))
| aScalar0(sz0z00)
| aScalar0(X0)
| aScalar0(xS)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(xS,X0)
| aScalar0(X1) ),
inference(superposition,[],[f253,f374]) ).
fof(f1769,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtpldt0(X0,X1))
| aScalar0(X0)
| aScalar0(xS)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(xS,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1766,f228]) ).
fof(f1771,plain,
! [X0,X1] :
( ~ sdtlseqdt0(xS,sdtpldt0(X0,X1))
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X1)
| sdtlseqdt0(xS,X0)
| aScalar0(X1) ),
inference(forward_subsumption_resolution,[],[f1769,f287]) ).
fof(f1886,definition,
( spl2_67
<=> sdtlseqdt0(sz0z00,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_67])],[avatar_definition]) ).
fof(f1887,plain,
( ~ sdtlseqdt0(sz0z00,sz0z00)
| spl2_67 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1888,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl2_67 ),
inference(avatar_component_clause,[],[f1886]) ).
fof(f1905,plain,
( aScalar0(sz0z00)
| ~ spl2_67 ),
inference(resolution,[],[f1888,f250]) ).
fof(f1911,plain,
( $false
| ~ spl2_67 ),
inference(forward_subsumption_resolution,[],[f1905,f228]) ).
fof(f1912,plain,
~ spl2_67,
inference(avatar_contradiction_clause,[],[f1911]) ).
fof(f2160,plain,
! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| aScalar0(sz0z00)
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,sz0z00)
| sz0z00 = X0 ),
inference(superposition,[],[f259,f390]) ).
fof(f2171,plain,
! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sdtlseqdt0(sz0z00,sz0z00)
| sz0z00 = X0 ),
inference(forward_subsumption_resolution,[],[f2160,f228]) ).
fof(f2173,plain,
( ! [X0] :
( sz0z00 != sdtasdt0(X0,X0)
| aScalar0(X0)
| sdtlseqdt0(sz0z00,X0)
| sz0z00 = X0 )
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f2171,f1887]) ).
fof(f2285,definition,
( spl2_80
<=> aScalar0(smndt0(xE)) ),
introduced(definition,[new_symbols(definition,[spl2_80])],[avatar_definition]) ).
fof(f2286,plain,
( ~ aScalar0(smndt0(xE))
| spl2_80 ),
inference(avatar_component_clause,[],[f2285]) ).
fof(f2287,plain,
( aScalar0(smndt0(xE))
| ~ spl2_80 ),
inference(avatar_component_clause,[],[f2285]) ).
fof(f2333,definition,
( spl2_86
<=> aScalar0(smndt0(xH)) ),
introduced(definition,[new_symbols(definition,[spl2_86])],[avatar_definition]) ).
fof(f2334,plain,
( ~ aScalar0(smndt0(xH))
| spl2_86 ),
inference(avatar_component_clause,[],[f2333]) ).
fof(f2335,plain,
( aScalar0(smndt0(xH))
| ~ spl2_86 ),
inference(avatar_component_clause,[],[f2333]) ).
fof(f2348,definition,
( spl2_88
<=> aScalar0(smndt0(xR)) ),
introduced(definition,[new_symbols(definition,[spl2_88])],[avatar_definition]) ).
fof(f2349,plain,
( ~ aScalar0(smndt0(xR))
| spl2_88 ),
inference(avatar_component_clause,[],[f2348]) ).
fof(f2350,plain,
( aScalar0(smndt0(xR))
| ~ spl2_88 ),
inference(avatar_component_clause,[],[f2348]) ).
fof(f2402,definition,
( spl2_90
<=> aScalar0(smndt0(xP)) ),
introduced(definition,[new_symbols(definition,[spl2_90])],[avatar_definition]) ).
fof(f2403,plain,
( ~ aScalar0(smndt0(xP))
| spl2_90 ),
inference(avatar_component_clause,[],[f2402]) ).
fof(f2404,plain,
( aScalar0(smndt0(xP))
| ~ spl2_90 ),
inference(avatar_component_clause,[],[f2402]) ).
fof(f2558,plain,
( aScalar0(xE)
| ~ spl2_80 ),
inference(resolution,[],[f2287,f231]) ).
fof(f2559,plain,
( $false
| ~ spl2_80 ),
inference(forward_subsumption_resolution,[],[f2558,f281]) ).
fof(f2560,plain,
~ spl2_80,
inference(avatar_contradiction_clause,[],[f2559]) ).
fof(f2695,plain,
( aScalar0(xH)
| ~ spl2_86 ),
inference(resolution,[],[f2335,f231]) ).
fof(f2696,plain,
( $false
| ~ spl2_86 ),
inference(forward_subsumption_resolution,[],[f2695,f284]) ).
fof(f2697,plain,
~ spl2_86,
inference(avatar_contradiction_clause,[],[f2696]) ).
fof(f2753,plain,
( aScalar0(xR)
| ~ spl2_88 ),
inference(resolution,[],[f2350,f231]) ).
fof(f2754,plain,
( $false
| ~ spl2_88 ),
inference(forward_subsumption_resolution,[],[f2753,f285]) ).
fof(f2755,plain,
~ spl2_88,
inference(avatar_contradiction_clause,[],[f2754]) ).
fof(f2903,plain,
( aScalar0(xP)
| ~ spl2_90 ),
inference(resolution,[],[f2404,f231]) ).
fof(f2904,plain,
( $false
| ~ spl2_90 ),
inference(forward_subsumption_resolution,[],[f2903,f286]) ).
fof(f2905,plain,
~ spl2_90,
inference(avatar_contradiction_clause,[],[f2904]) ).
fof(f3399,plain,
( sdtasdt0(xE,xH) = sdtasdt0(xH,xE)
| ~ spl2_1 ),
inference(resolution,[],[f587,f284]) ).
fof(f3404,plain,
( xP = sdtasdt0(xH,xE)
| ~ spl2_1 ),
inference(forward_demodulation,[],[f3399,f210]) ).
fof(f3709,plain,
( sdtasdt0(xP,xR) = sdtasdt0(xR,xP)
| ~ spl2_1 ),
inference(resolution,[],[f591,f286]) ).
fof(f3711,plain,
( sdtasdt0(xN,xR) = sdtasdt0(xR,xN)
| ~ spl2_1 ),
inference(resolution,[],[f591,f288]) ).
fof(f3750,plain,
( sdtasdt0(xN,xP) = sdtasdt0(xP,xN)
| ~ spl2_1 ),
inference(resolution,[],[f592,f288]) ).
fof(f5822,plain,
sdtasdt0(xR,smndt0(xP)) = smndt0(sdtasdt0(xR,xP)),
inference(resolution,[],[f668,f285]) ).
fof(f6873,plain,
sdtasdt0(smndt0(xH),xE) = smndt0(sdtasdt0(xH,xE)),
inference(resolution,[],[f697,f284]) ).
fof(f6878,plain,
( smndt0(xP) = sdtasdt0(smndt0(xH),xE)
| ~ spl2_1 ),
inference(forward_demodulation,[],[f6873,f3404]) ).
fof(f7168,definition,
( spl2_129
<=> sdtlseqdt0(sz0z00,smndt0(xE)) ),
introduced(definition,[new_symbols(definition,[spl2_129])],[avatar_definition]) ).
fof(f7170,plain,
( sdtlseqdt0(sz0z00,smndt0(xE))
| ~ spl2_129 ),
inference(avatar_component_clause,[],[f7168]) ).
fof(f8269,definition,
( spl2_135
<=> sdtlseqdt0(sz0z00,smndt0(xH)) ),
introduced(definition,[new_symbols(definition,[spl2_135])],[avatar_definition]) ).
fof(f8271,plain,
( sdtlseqdt0(sz0z00,smndt0(xH))
| ~ spl2_135 ),
inference(avatar_component_clause,[],[f8269]) ).
fof(f8306,plain,
sdtasdt0(xE,xH) = sdtasdt0(smndt0(xE),smndt0(xH)),
inference(resolution,[],[f734,f281]) ).
fof(f8314,plain,
xP = sdtasdt0(smndt0(xE),smndt0(xH)),
inference(forward_demodulation,[],[f8306,f210]) ).
fof(f8363,plain,
sdtasdt0(xR,xR) = sdtasdt0(smndt0(xR),smndt0(xR)),
inference(resolution,[],[f735,f285]) ).
fof(f8424,plain,
sdtasdt0(xP,xP) = sdtasdt0(smndt0(xP),smndt0(xP)),
inference(resolution,[],[f736,f286]) ).
fof(f8427,plain,
( xN = sdtasdt0(smndt0(xP),smndt0(xP))
| ~ spl2_17 ),
inference(forward_demodulation,[],[f8424,f771]) ).
fof(f8797,definition,
( spl2_139
<=> sdtlseqdt0(sz0z00,smndt0(xP)) ),
introduced(definition,[new_symbols(definition,[spl2_139])],[avatar_definition]) ).
fof(f9389,plain,
( aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| aScalar0(smndt0(xN))
| ~ spl2_49 ),
inference(resolution,[],[f1301,f229]) ).
fof(f9390,plain,
( aScalar0(sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)))
| spl2_10
| ~ spl2_49 ),
inference(forward_subsumption_resolution,[],[f9389,f474]) ).
fof(f15072,plain,
! [X0] :
( aScalar0(X0)
| sdtasdt0(sdtasdt0(X0,xN),xR) = sdtasdt0(X0,sdtasdt0(xN,xR)) ),
inference(resolution,[],[f1002,f288]) ).
fof(f17446,plain,
( ~ sdtlseqdt0(xN,sz0z00)
| aScalar0(xR)
| sdtlseqdt0(xS,sz0z00)
| sdtlseqdt0(xR,xR)
| aScalar0(sz0z00)
| spl2_25 ),
inference(superposition,[],[f1404,f400]) ).
fof(f17564,definition,
( spl2_157
<=> sdtlseqdt0(xR,xR) ),
introduced(definition,[new_symbols(definition,[spl2_157])],[avatar_definition]) ).
fof(f17565,plain,
( ~ sdtlseqdt0(xR,xR)
| spl2_157 ),
inference(avatar_component_clause,[],[f17564]) ).
fof(f17607,definition,
( spl2_167
<=> sdtlseqdt0(xN,xS) ),
introduced(definition,[new_symbols(definition,[spl2_167])],[avatar_definition]) ).
fof(f17609,plain,
( ~ sdtlseqdt0(xN,xS)
| spl2_167 ),
inference(avatar_component_clause,[],[f17607]) ).
fof(f17645,definition,
( spl2_175
<=> sdtlseqdt0(xS,xR) ),
introduced(definition,[new_symbols(definition,[spl2_175])],[avatar_definition]) ).
fof(f17654,definition,
( spl2_177
<=> sdtlseqdt0(xS,xN) ),
introduced(definition,[new_symbols(definition,[spl2_177])],[avatar_definition]) ).
fof(f17658,definition,
( spl2_178
<=> sdtlseqdt0(xN,sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_178])],[avatar_definition]) ).
fof(f17660,plain,
( ~ sdtlseqdt0(xN,sz0z00)
| spl2_178 ),
inference(avatar_component_clause,[],[f17658]) ).
fof(f17785,plain,
( ~ sdtlseqdt0(xS,xS)
| aScalar0(xF)
| sdtlseqdt0(xD,xD)
| sdtlseqdt0(xF,xF)
| aScalar0(xD) ),
inference(superposition,[],[f1405,f212]) ).
fof(f17817,plain,
( ~ sdtlseqdt0(xS,xS)
| aScalar0(xF)
| sdtlseqdt0(xF,xF)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f17785,f250]) ).
fof(f17890,plain,
( ~ sdtlseqdt0(xS,xS)
| aScalar0(xF)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f17817,f250]) ).
fof(f18014,plain,
( ~ sdtlseqdt0(xS,xS)
| aScalar0(xD) ),
inference(forward_subsumption_resolution,[],[f17890,f282]) ).
fof(f18034,definition,
( spl2_212
<=> sdtlseqdt0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl2_212])],[avatar_definition]) ).
fof(f18036,plain,
( ~ sdtlseqdt0(xS,xS)
| spl2_212 ),
inference(avatar_component_clause,[],[f18034]) ).
fof(f18114,plain,
~ sdtlseqdt0(xS,xS),
inference(forward_subsumption_resolution,[],[f18014,f280]) ).
fof(f18248,plain,
~ spl2_212,
inference(avatar_split_clause,[],[f18114,f18034]) ).
fof(f18256,plain,
( ~ spl2_177
| spl2_26
| ~ spl2_32 ),
inference(avatar_split_clause,[],[f1604,f1110,f892,f17654]) ).
fof(f18267,plain,
( ~ sdtlseqdt0(xN,sz0z00)
| sdtlseqdt0(xS,sz0z00)
| sdtlseqdt0(xR,xR)
| aScalar0(sz0z00)
| spl2_25 ),
inference(forward_subsumption_resolution,[],[f17446,f285]) ).
fof(f18344,plain,
( ~ sdtlseqdt0(xN,sz0z00)
| sdtlseqdt0(xS,sz0z00)
| sdtlseqdt0(xR,xR)
| spl2_25 ),
inference(forward_subsumption_resolution,[],[f18267,f228]) ).
fof(f18427,definition,
( spl2_244
<=> sdtlseqdt0(xR,xS) ),
introduced(definition,[new_symbols(definition,[spl2_244])],[avatar_definition]) ).
fof(f18429,plain,
( sdtlseqdt0(xR,xS)
| ~ spl2_244 ),
inference(avatar_component_clause,[],[f18427]) ).
fof(f18436,plain,
( spl2_157
| spl2_33
| ~ spl2_178
| spl2_25 ),
inference(avatar_split_clause,[],[f18344,f888,f17658,f1114,f17564]) ).
fof(f18588,plain,
( xR = sdtpldt0(xR,xS)
| ~ spl2_32 ),
inference(superposition,[],[f372,f1112]) ).
fof(f18647,plain,
( xS = sdtasdt0(smndt0(xS),xS)
| spl2_9
| ~ spl2_32 ),
inference(superposition,[],[f1425,f1112]) ).
fof(f19219,definition,
( spl2_294
<=> sdtlseqdt0(xE,xE) ),
introduced(definition,[new_symbols(definition,[spl2_294])],[avatar_definition]) ).
fof(f19220,plain,
( ~ sdtlseqdt0(xE,xE)
| spl2_294 ),
inference(avatar_component_clause,[],[f19219]) ).
fof(f19221,plain,
( sdtlseqdt0(xE,xE)
| ~ spl2_294 ),
inference(avatar_component_clause,[],[f19219]) ).
fof(f19404,plain,
( ~ sdtlseqdt0(xR,xR)
| aScalar0(xC)
| sdtlseqdt0(xG,xG)
| sdtlseqdt0(xC,xC)
| aScalar0(xG) ),
inference(superposition,[],[f1407,f208]) ).
fof(f19448,plain,
( ~ sdtlseqdt0(xR,xR)
| aScalar0(xC)
| sdtlseqdt0(xC,xC)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19404,f250]) ).
fof(f19521,plain,
( ~ sdtlseqdt0(xR,xR)
| aScalar0(xC)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19448,f250]) ).
fof(f19669,plain,
( ~ sdtlseqdt0(xR,xR)
| aScalar0(xG) ),
inference(forward_subsumption_resolution,[],[f19521,f279]) ).
fof(f19722,plain,
~ sdtlseqdt0(xR,xR),
inference(forward_subsumption_resolution,[],[f19669,f283]) ).
fof(f19780,plain,
~ spl2_157,
inference(avatar_split_clause,[],[f19722,f17564]) ).
fof(f20623,plain,
! [X0] :
( aScalar0(X0)
| sdtpldt0(sdtpldt0(X0,sz0z00),sz0z00) = sdtpldt0(X0,sdtpldt0(sz0z00,sz0z00)) ),
inference(resolution,[],[f985,f228]) ).
fof(f20705,plain,
! [X0] :
( sdtpldt0(X0,sz0z00) = sdtpldt0(sdtpldt0(X0,sz0z00),sz0z00)
| aScalar0(X0) ),
inference(forward_demodulation,[],[f20623,f362]) ).
fof(f20706,plain,
( ! [X0] :
( aScalar0(X0)
| sdtpldt0(X0,xS) = sdtpldt0(sdtpldt0(X0,xS),xS) )
| ~ spl2_32 ),
inference(forward_demodulation,[],[f20705,f1112]) ).
fof(f20714,definition,
( spl2_369
<=> xS = xN ),
introduced(definition,[new_symbols(definition,[spl2_369])],[avatar_definition]) ).
fof(f20715,plain,
( xS != xN
| spl2_369 ),
inference(avatar_component_clause,[],[f20714]) ).
fof(f20716,plain,
( xS = xN
| ~ spl2_369 ),
inference(avatar_component_clause,[],[f20714]) ).
fof(f21193,plain,
( ~ sdtlseqdt0(xN,xS)
| ~ spl2_32
| spl2_178 ),
inference(forward_demodulation,[],[f17660,f1112]) ).
fof(f21228,definition,
( spl2_382
<=> xN = sdtasdt0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl2_382])],[avatar_definition]) ).
fof(f21229,plain,
( xN = sdtasdt0(xS,xS)
| ~ spl2_382 ),
inference(avatar_component_clause,[],[f21228]) ).
fof(f21230,plain,
( xN != sdtasdt0(xS,xS)
| spl2_382 ),
inference(avatar_component_clause,[],[f21228]) ).
fof(f21235,definition,
( spl2_383
<=> xS = sdtasdt0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl2_383])],[avatar_definition]) ).
fof(f21236,plain,
( xS = sdtasdt0(xS,xS)
| ~ spl2_383 ),
inference(avatar_component_clause,[],[f21235]) ).
fof(f21239,definition,
( spl2_384
<=> xS = smndt0(xS) ),
introduced(definition,[new_symbols(definition,[spl2_384])],[avatar_definition]) ).
fof(f21241,plain,
( xS = smndt0(xS)
| ~ spl2_384 ),
inference(avatar_component_clause,[],[f21239]) ).
fof(f22043,definition,
( spl2_397
<=> xP = xN ),
introduced(definition,[new_symbols(definition,[spl2_397])],[avatar_definition]) ).
fof(f22044,plain,
( xP != xN
| spl2_397 ),
inference(avatar_component_clause,[],[f22043]) ).
fof(f29505,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),xN),xN)
| ~ spl2_384 ),
inference(superposition,[],[f224,f21241]) ).
fof(f29525,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),xS),xS)
| ~ spl2_369
| ~ spl2_384 ),
inference(forward_demodulation,[],[f29505,f20716]) ).
fof(f30597,plain,
! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| sdtlseqdt0(xN,X0)
| aScalar0(X0)
| aScalar0(xN)
| aScalar0(sdtasdt0(xP,xP))
| xN = X0 ),
inference(resolution,[],[f828,f290]) ).
fof(f30654,plain,
( ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(xS)
| aScalar0(sz0z00)
| aScalar0(X0)
| sz0z00 = xS )
| spl2_25 ),
inference(resolution,[],[f828,f889]) ).
fof(f30665,plain,
! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| sdtlseqdt0(xN,X0)
| aScalar0(xN)
| aScalar0(sdtasdt0(xP,xP))
| aScalar0(X0)
| xN = sdtasdt0(xP,xP) ),
inference(resolution,[],[f828,f290]) ).
fof(f30793,plain,
! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| sdtlseqdt0(xN,X0)
| aScalar0(X0)
| aScalar0(sdtasdt0(xP,xP))
| xN = X0 ),
inference(forward_subsumption_resolution,[],[f30597,f288]) ).
fof(f30867,plain,
( ! [X0] :
( sdtlseqdt0(X0,xN)
| sdtlseqdt0(xN,X0)
| aScalar0(X0)
| aScalar0(sdtasdt0(xP,xP))
| xN = X0 )
| ~ spl2_17 ),
inference(forward_demodulation,[],[f30793,f771]) ).
fof(f31336,plain,
( ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(sz0z00)
| aScalar0(X0)
| sz0z00 = xS )
| spl2_25 ),
inference(forward_subsumption_resolution,[],[f30654,f287]) ).
fof(f31553,plain,
( ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(X0)
| sz0z00 = xS )
| spl2_25 ),
inference(forward_subsumption_resolution,[],[f31336,f228]) ).
fof(f31601,definition,
( spl2_454
<=> ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| aScalar0(X0)
| sdtlseqdt0(xS,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_454])],[avatar_definition]) ).
fof(f31602,plain,
( ! [X0] :
( sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(X0) )
| ~ spl2_454 ),
inference(avatar_component_clause,[],[f31601]) ).
fof(f31603,plain,
( spl2_32
| spl2_454
| spl2_25 ),
inference(avatar_split_clause,[],[f31553,f888,f31601,f1110]) ).
fof(f31780,plain,
! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| sdtlseqdt0(xN,X0)
| aScalar0(sdtasdt0(xP,xP))
| aScalar0(X0)
| xN = sdtasdt0(xP,xP) ),
inference(forward_subsumption_resolution,[],[f30665,f288]) ).
fof(f31908,definition,
( spl2_473
<=> ! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| aScalar0(X0)
| sdtlseqdt0(xN,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_473])],[avatar_definition]) ).
fof(f31909,plain,
( ! [X0] :
( sdtlseqdt0(X0,sdtasdt0(xP,xP))
| aScalar0(X0)
| sdtlseqdt0(xN,X0) )
| ~ spl2_473 ),
inference(avatar_component_clause,[],[f31908]) ).
fof(f31910,plain,
( spl2_17
| spl2_18
| spl2_473 ),
inference(avatar_split_clause,[],[f31780,f31908,f773,f769]) ).
fof(f31939,plain,
( aScalar0(xP)
| aScalar0(xP)
| ~ spl2_18 ),
inference(resolution,[],[f775,f230]) ).
fof(f31940,plain,
( aScalar0(xP)
| ~ spl2_18 ),
inference(duplicate_literal_removal,[],[f31939]) ).
fof(f31941,plain,
( $false
| ~ spl2_18 ),
inference(forward_subsumption_resolution,[],[f31940,f286]) ).
fof(f31942,plain,
~ spl2_18,
inference(avatar_contradiction_clause,[],[f31941]) ).
fof(f31963,definition,
( spl2_476
<=> ! [X0] :
( sdtlseqdt0(X0,xN)
| xN = X0
| aScalar0(X0)
| sdtlseqdt0(xN,X0) ) ),
introduced(definition,[new_symbols(definition,[spl2_476])],[avatar_definition]) ).
fof(f31964,plain,
( ! [X0] :
( sdtlseqdt0(X0,xN)
| sdtlseqdt0(xN,X0)
| aScalar0(X0)
| xN = X0 )
| ~ spl2_476 ),
inference(avatar_component_clause,[],[f31963]) ).
fof(f32518,plain,
( ! [X0] :
( aScalar0(X0)
| aScalar0(xS)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(sz0z00) )
| ~ spl2_33 ),
inference(resolution,[],[f1116,f252]) ).
fof(f32520,plain,
( ! [X0] :
( aScalar0(X0)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0)
| aScalar0(sz0z00) )
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f32518,f287]) ).
fof(f32521,plain,
( ! [X0] :
( aScalar0(X0)
| sdtlseqdt0(X0,sz0z00)
| sdtlseqdt0(xS,X0) )
| ~ spl2_33 ),
inference(forward_subsumption_resolution,[],[f32520,f228]) ).
fof(f32522,plain,
( spl2_454
| ~ spl2_33 ),
inference(avatar_split_clause,[],[f32521,f1114,f31601]) ).
fof(f32616,plain,
( xS = sdtasdt0(xS,xS)
| spl2_9
| ~ spl2_32
| ~ spl2_384 ),
inference(forward_demodulation,[],[f18647,f21241]) ).
fof(f32701,plain,
( ~ spl2_167
| ~ spl2_32
| spl2_178 ),
inference(avatar_split_clause,[],[f21193,f17658,f1110,f17607]) ).
fof(f32979,plain,
( spl2_383
| spl2_9
| ~ spl2_32
| ~ spl2_384 ),
inference(avatar_split_clause,[],[f32616,f21239,f1110,f468,f21235]) ).
fof(f34223,definition,
( spl2_536
<=> sdtlseqdt0(xH,xH) ),
introduced(definition,[new_symbols(definition,[spl2_536])],[avatar_definition]) ).
fof(f34224,plain,
( sdtlseqdt0(xH,xH)
| ~ spl2_536 ),
inference(avatar_component_clause,[],[f34223]) ).
fof(f34225,plain,
( ~ sdtlseqdt0(xH,xH)
| spl2_536 ),
inference(avatar_component_clause,[],[f34223]) ).
fof(f39905,plain,
( aScalar0(xR)
| ~ sdtlseqdt0(xS,xR)
| aScalar0(xS)
| ~ spl2_244 ),
inference(resolution,[],[f18429,f255]) ).
fof(f43471,plain,
( ! [X0] :
( sdtlseqdt0(X0,xN)
| sdtlseqdt0(xN,X0)
| aScalar0(X0)
| xN = X0 )
| ~ spl2_17
| spl2_18 ),
inference(forward_subsumption_resolution,[],[f30867,f774]) ).
fof(f43527,plain,
( spl2_476
| ~ spl2_17
| spl2_18 ),
inference(avatar_split_clause,[],[f43471,f773,f769,f31963]) ).
fof(f55474,plain,
( sdtlseqdt0(sz0z00,xS)
| ~ spl2_22
| ~ spl2_384 ),
inference(forward_demodulation,[],[f869,f21241]) ).
fof(f55625,plain,
( $false
| ~ spl2_22
| spl2_25
| ~ spl2_384 ),
inference(forward_subsumption_resolution,[],[f55474,f889]) ).
fof(f55626,plain,
( ~ spl2_22
| spl2_25
| ~ spl2_384 ),
inference(avatar_contradiction_clause,[],[f55625]) ).
fof(f56401,plain,
( spl2_384
| ~ spl2_4
| ~ spl2_32 ),
inference(avatar_split_clause,[],[f1597,f1110,f303,f21239]) ).
fof(f56511,definition,
( spl2_641
<=> sdtlseqdt0(sdtasdt0(xS,xS),xN) ),
introduced(definition,[new_symbols(definition,[spl2_641])],[avatar_definition]) ).
fof(f56512,plain,
( sdtlseqdt0(sdtasdt0(xS,xS),xN)
| ~ spl2_641 ),
inference(avatar_component_clause,[],[f56511]) ).
fof(f56513,plain,
( ~ sdtlseqdt0(sdtasdt0(xS,xS),xN)
| spl2_641 ),
inference(avatar_component_clause,[],[f56511]) ).
fof(f86772,plain,
( sdtpldt0(sdtasdt0(xR,xR),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xS),xS)
| ~ spl2_32
| ~ spl2_369
| ~ spl2_384 ),
inference(superposition,[],[f29525,f18588]) ).
fof(f86793,plain,
( sdtpldt0(sdtasdt0(xR,xR),xS) != sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xS),xS)
| ~ spl2_32
| ~ spl2_369
| ~ spl2_383
| ~ spl2_384 ),
inference(forward_demodulation,[],[f86772,f21236]) ).
fof(f87139,definition,
( spl2_1094
<=> sdtlseqdt0(xP,sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl2_1094])],[avatar_definition]) ).
fof(f87140,plain,
( sdtlseqdt0(xP,sdtasdt0(xR,xR))
| ~ spl2_1094 ),
inference(avatar_component_clause,[],[f87139]) ).
fof(f91933,definition,
( spl2_1153
<=> sdtlseqdt0(smndt0(xP),sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl2_1153])],[avatar_definition]) ).
fof(f91934,plain,
( sdtlseqdt0(smndt0(xP),sdtasdt0(xR,xR))
| ~ spl2_1153 ),
inference(avatar_component_clause,[],[f91933]) ).
fof(f91935,plain,
( ~ sdtlseqdt0(smndt0(xP),sdtasdt0(xR,xR))
| spl2_1153 ),
inference(avatar_component_clause,[],[f91933]) ).
fof(f95225,definition,
( spl2_1248
<=> xP = smndt0(xP) ),
introduced(definition,[new_symbols(definition,[spl2_1248])],[avatar_definition]) ).
fof(f95226,plain,
( xP != smndt0(xP)
| spl2_1248 ),
inference(avatar_component_clause,[],[f95225]) ).
fof(f95227,plain,
( xP = smndt0(xP)
| ~ spl2_1248 ),
inference(avatar_component_clause,[],[f95225]) ).
fof(f96928,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xP))
| aScalar0(smndt0(xH))
| sdtlseqdt0(sz0z00,xE)
| sdtlseqdt0(sz0z00,smndt0(xH))
| aScalar0(xE)
| ~ spl2_1 ),
inference(superposition,[],[f257,f6878]) ).
fof(f96964,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xP))
| sdtlseqdt0(sz0z00,xE)
| sdtlseqdt0(sz0z00,smndt0(xH))
| aScalar0(xE)
| ~ spl2_1
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f96928,f2334]) ).
fof(f96973,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xP))
| sdtlseqdt0(sz0z00,xE)
| sdtlseqdt0(sz0z00,smndt0(xH))
| ~ spl2_1
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f96964,f281]) ).
fof(f97144,plain,
( aScalar0(xH)
| ~ spl2_536 ),
inference(resolution,[],[f34224,f250]) ).
fof(f97150,plain,
( $false
| ~ spl2_536 ),
inference(forward_subsumption_resolution,[],[f97144,f284]) ).
fof(f97151,plain,
~ spl2_536,
inference(avatar_contradiction_clause,[],[f97150]) ).
fof(f97434,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| aScalar0(smndt0(xE))
| sdtlseqdt0(sz0z00,smndt0(xH))
| sdtlseqdt0(sz0z00,smndt0(xE))
| aScalar0(smndt0(xH)) ),
inference(superposition,[],[f257,f8314]) ).
fof(f104376,definition,
( spl2_1370
<=> aScalar0(sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl2_1370])],[avatar_definition]) ).
fof(f104377,plain,
( ~ aScalar0(sdtasdt0(xR,xR))
| spl2_1370 ),
inference(avatar_component_clause,[],[f104376]) ).
fof(f104378,plain,
( aScalar0(sdtasdt0(xR,xR))
| ~ spl2_1370 ),
inference(avatar_component_clause,[],[f104376]) ).
fof(f105473,plain,
( aScalar0(xR)
| aScalar0(xR)
| ~ spl2_1370 ),
inference(resolution,[],[f104378,f230]) ).
fof(f105474,plain,
( aScalar0(xR)
| ~ spl2_1370 ),
inference(duplicate_literal_removal,[],[f105473]) ).
fof(f105475,plain,
( $false
| ~ spl2_1370 ),
inference(forward_subsumption_resolution,[],[f105474,f285]) ).
fof(f105476,plain,
~ spl2_1370,
inference(avatar_contradiction_clause,[],[f105475]) ).
fof(f130212,definition,
( spl2_1682
<=> xR = sdtasdt0(xR,xP) ),
introduced(definition,[new_symbols(definition,[spl2_1682])],[avatar_definition]) ).
fof(f130213,plain,
( xR != sdtasdt0(xR,xP)
| spl2_1682 ),
inference(avatar_component_clause,[],[f130212]) ).
fof(f130214,plain,
( xR = sdtasdt0(xR,xP)
| ~ spl2_1682 ),
inference(avatar_component_clause,[],[f130212]) ).
fof(f159018,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xR,xR))
| aScalar0(smndt0(xR)) ),
inference(superposition,[],[f258,f8363]) ).
fof(f159111,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xR,xR))
| spl2_88 ),
inference(forward_subsumption_resolution,[],[f159018,f2349]) ).
fof(f163161,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xP,xP))
| aScalar0(smndt0(xP)) ),
inference(superposition,[],[f258,f8424]) ).
fof(f163241,plain,
( ~ sdtlseqdt0(sz0z00,sdtasdt0(xP,xP))
| spl2_90 ),
inference(forward_subsumption_resolution,[],[f163161,f2403]) ).
fof(f163980,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| sdtlseqdt0(sz0z00,smndt0(xH))
| sdtlseqdt0(sz0z00,smndt0(xE))
| aScalar0(smndt0(xH))
| spl2_80 ),
inference(forward_subsumption_resolution,[],[f97434,f2286]) ).
fof(f164347,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| sdtlseqdt0(sz0z00,smndt0(xH))
| sdtlseqdt0(sz0z00,smndt0(xE))
| spl2_80
| spl2_86 ),
inference(forward_subsumption_resolution,[],[f163980,f2334]) ).
fof(f232658,plain,
( smndt0(xR) = sdtasdt0(xR,smndt0(xP))
| ~ spl2_1682 ),
inference(superposition,[],[f5822,f130214]) ).
fof(f305611,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xS) = sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,smndt0(xS)),sdtpldt0(xR,smndt0(xS))),xS),xS)
| ~ spl2_32
| spl2_39 ),
inference(resolution,[],[f20706,f1239]) ).
fof(f305788,plain,
( sdtpldt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),xS) = sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),xS),xS)
| ~ spl2_32
| spl2_39
| ~ spl2_384 ),
inference(forward_demodulation,[],[f305611,f21241]) ).
fof(f305833,plain,
( sdtpldt0(sdtasdt0(xR,xR),xS) = sdtpldt0(sdtpldt0(sdtasdt0(xR,xR),xS),xS)
| ~ spl2_32
| spl2_39
| ~ spl2_384 ),
inference(forward_demodulation,[],[f305788,f18588]) ).
fof(f305856,plain,
( $false
| ~ spl2_32
| spl2_39
| ~ spl2_369
| ~ spl2_383
| ~ spl2_384 ),
inference(forward_subsumption_resolution,[],[f305833,f86793]) ).
fof(f305857,plain,
( ~ spl2_32
| spl2_39
| ~ spl2_369
| ~ spl2_383
| ~ spl2_384 ),
inference(avatar_contradiction_clause,[],[f305856]) ).
fof(f307337,definition,
( spl2_2542
<=> sdtlseqdt0(smndt0(xN),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_2542])],[avatar_definition]) ).
fof(f307339,plain,
( ~ sdtlseqdt0(smndt0(xN),sz0z00)
| spl2_2542 ),
inference(avatar_component_clause,[],[f307337]) ).
fof(f307627,plain,
( spl2_135
| spl2_27
| ~ spl2_139
| ~ spl2_1
| spl2_86 ),
inference(avatar_split_clause,[],[f96973,f2333,f292,f8797,f898,f8269]) ).
fof(f308366,definition,
( spl2_2587
<=> sdtlseqdt0(sz0z00,sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl2_2587])],[avatar_definition]) ).
fof(f308376,plain,
( ~ spl2_2587
| spl2_88 ),
inference(avatar_split_clause,[],[f159111,f2348,f308366]) ).
fof(f308464,definition,
( spl2_2595
<=> sdtlseqdt0(sz0z00,sdtasdt0(xP,xP)) ),
introduced(definition,[new_symbols(definition,[spl2_2595])],[avatar_definition]) ).
fof(f308477,plain,
( ~ spl2_2595
| spl2_90 ),
inference(avatar_split_clause,[],[f163241,f2402,f308464]) ).
fof(f308486,plain,
( spl2_129
| spl2_135
| ~ spl2_29
| spl2_80
| spl2_86 ),
inference(avatar_split_clause,[],[f164347,f2333,f2285,f906,f8269,f7168]) ).
fof(f319058,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| aScalar0(sz0z00)
| aScalar0(xE)
| sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(superposition,[],[f1381,f396]) ).
fof(f319846,definition,
( spl2_2818
<=> sz0z00 = xN ),
introduced(definition,[new_symbols(definition,[spl2_2818])],[avatar_definition]) ).
fof(f319848,plain,
( sz0z00 = xN
| ~ spl2_2818 ),
inference(avatar_component_clause,[],[f319846]) ).
fof(f331858,definition,
( spl2_3236
<=> sz0z00 = xP ),
introduced(definition,[new_symbols(definition,[spl2_3236])],[avatar_definition]) ).
fof(f331860,plain,
( sz0z00 = xP
| ~ spl2_3236 ),
inference(avatar_component_clause,[],[f331858]) ).
fof(f333289,definition,
( spl2_3247
<=> sdtlseqdt0(xN,sdtasdt0(xR,xR)) ),
introduced(definition,[new_symbols(definition,[spl2_3247])],[avatar_definition]) ).
fof(f336101,plain,
( ~ sdtlseqdt0(xS,xR)
| aScalar0(xS)
| ~ spl2_244 ),
inference(forward_subsumption_resolution,[],[f39905,f285]) ).
fof(f336300,plain,
( ~ sdtlseqdt0(xS,xR)
| ~ spl2_244 ),
inference(forward_subsumption_resolution,[],[f336101,f287]) ).
fof(f336436,plain,
( ~ spl2_175
| ~ spl2_244 ),
inference(avatar_split_clause,[],[f336300,f18427,f17645]) ).
fof(f336762,plain,
( ~ sdtlseqdt0(sdtasdt0(xS,xS),sz0z00)
| spl2_641
| ~ spl2_2818 ),
inference(forward_demodulation,[],[f56513,f319848]) ).
fof(f337348,plain,
( sz0z00 != sdtasdt0(xS,xS)
| spl2_382
| ~ spl2_2818 ),
inference(forward_demodulation,[],[f21230,f319848]) ).
fof(f337490,definition,
( spl2_3334
<=> sdtlseqdt0(sdtasdt0(xS,xS),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_3334])],[avatar_definition]) ).
fof(f337492,plain,
( ~ sdtlseqdt0(sdtasdt0(xS,xS),sz0z00)
| spl2_3334 ),
inference(avatar_component_clause,[],[f337490]) ).
fof(f337582,plain,
( ~ spl2_3334
| spl2_641
| ~ spl2_2818 ),
inference(avatar_split_clause,[],[f336762,f319846,f56511,f337490]) ).
fof(f338469,definition,
( spl2_3350
<=> sz0z00 = sdtasdt0(xS,xS) ),
introduced(definition,[new_symbols(definition,[spl2_3350])],[avatar_definition]) ).
fof(f342704,definition,
( spl2_3507
<=> sdtlseqdt0(smndt0(xH),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_3507])],[avatar_definition]) ).
fof(f342728,definition,
( spl2_3510
<=> sdtlseqdt0(smndt0(xE),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_3510])],[avatar_definition]) ).
fof(f346053,plain,
( ~ spl2_3350
| spl2_382
| ~ spl2_2818 ),
inference(avatar_split_clause,[],[f337348,f319846,f21228,f338469]) ).
fof(f346115,plain,
( sdtlseqdt0(sz0z00,sz0z00)
| ~ spl2_29
| ~ spl2_3236 ),
inference(superposition,[],[f907,f331860]) ).
fof(f346177,plain,
( sz0z00 != xN
| spl2_397
| ~ spl2_3236 ),
inference(superposition,[],[f22044,f331860]) ).
fof(f346214,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(xR,xR))
| ~ spl2_1094
| ~ spl2_3236 ),
inference(superposition,[],[f87140,f331860]) ).
fof(f346247,plain,
( sz0z00 != smndt0(sz0z00)
| spl2_1248
| ~ spl2_3236 ),
inference(superposition,[],[f95226,f331860]) ).
fof(f346424,plain,
( $false
| ~ spl2_4
| spl2_1248
| ~ spl2_3236 ),
inference(forward_subsumption_resolution,[],[f346247,f305]) ).
fof(f346425,plain,
( ~ spl2_4
| spl2_1248
| ~ spl2_3236 ),
inference(avatar_contradiction_clause,[],[f346424]) ).
fof(f346456,plain,
( spl2_2587
| ~ spl2_1094
| ~ spl2_3236 ),
inference(avatar_split_clause,[],[f346214,f331858,f87139,f308366]) ).
fof(f346532,plain,
( $false
| ~ spl2_29
| spl2_67
| ~ spl2_3236 ),
inference(forward_subsumption_resolution,[],[f346115,f1887]) ).
fof(f346533,plain,
( ~ spl2_29
| spl2_67
| ~ spl2_3236 ),
inference(avatar_contradiction_clause,[],[f346532]) ).
fof(f347399,plain,
( aScalar0(sz0z00)
| ~ sdtlseqdt0(smndt0(xE),sz0z00)
| aScalar0(smndt0(xE))
| ~ spl2_129 ),
inference(resolution,[],[f7170,f255]) ).
fof(f347400,plain,
( ~ sdtlseqdt0(smndt0(xE),sz0z00)
| aScalar0(smndt0(xE))
| ~ spl2_129 ),
inference(forward_subsumption_resolution,[],[f347399,f228]) ).
fof(f347402,plain,
( ~ sdtlseqdt0(smndt0(xE),sz0z00)
| spl2_80
| ~ spl2_129 ),
inference(forward_subsumption_resolution,[],[f347400,f2286]) ).
fof(f347404,plain,
( ~ spl2_3510
| spl2_80
| ~ spl2_129 ),
inference(avatar_split_clause,[],[f347402,f7168,f2285,f342728]) ).
fof(f347448,plain,
( aScalar0(sz0z00)
| ~ sdtlseqdt0(smndt0(xH),sz0z00)
| aScalar0(smndt0(xH))
| ~ spl2_135 ),
inference(resolution,[],[f8271,f255]) ).
fof(f347449,plain,
( ~ sdtlseqdt0(smndt0(xH),sz0z00)
| aScalar0(smndt0(xH))
| ~ spl2_135 ),
inference(forward_subsumption_resolution,[],[f347448,f228]) ).
fof(f347451,plain,
( ~ sdtlseqdt0(smndt0(xH),sz0z00)
| spl2_86
| ~ spl2_135 ),
inference(forward_subsumption_resolution,[],[f347449,f2334]) ).
fof(f347453,plain,
( ~ spl2_3507
| spl2_86
| ~ spl2_135 ),
inference(avatar_split_clause,[],[f347451,f8269,f2333,f342704]) ).
fof(f347494,definition,
( spl2_3693
<=> sz0z00 = smndt0(xR) ),
introduced(definition,[new_symbols(definition,[spl2_3693])],[avatar_definition]) ).
fof(f347496,plain,
( sz0z00 = smndt0(xR)
| ~ spl2_3693 ),
inference(avatar_component_clause,[],[f347494]) ).
fof(f348896,plain,
( sz0z00 = sdtasdt0(smndt0(xP),smndt0(xP))
| ~ spl2_17
| ~ spl2_2818 ),
inference(forward_demodulation,[],[f8427,f319848]) ).
fof(f349227,plain,
( aScalar0(sdtasdt0(xR,xR))
| aScalar0(sdtasdt0(xS,xS))
| spl2_10
| ~ spl2_49 ),
inference(resolution,[],[f9390,f229]) ).
fof(f349228,plain,
( aScalar0(sdtasdt0(xS,xS))
| spl2_10
| ~ spl2_49
| spl2_1370 ),
inference(forward_subsumption_resolution,[],[f349227,f104377]) ).
fof(f349229,plain,
( $false
| spl2_10
| spl2_11
| ~ spl2_49
| spl2_1370 ),
inference(forward_subsumption_resolution,[],[f349228,f543]) ).
fof(f349230,plain,
( spl2_10
| spl2_11
| ~ spl2_49
| spl2_1370 ),
inference(avatar_contradiction_clause,[],[f349229]) ).
fof(f349883,definition,
( spl2_3744
<=> sz0z00 = smndt0(xP) ),
introduced(definition,[new_symbols(definition,[spl2_3744])],[avatar_definition]) ).
fof(f349885,plain,
( sz0z00 = smndt0(xP)
| ~ spl2_3744 ),
inference(avatar_component_clause,[],[f349883]) ).
fof(f350787,plain,
( smndt0(sz0z00) = xR
| ~ spl2_3693 ),
inference(superposition,[],[f428,f347496]) ).
fof(f350895,plain,
( sz0z00 = xR
| ~ spl2_4
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f350787,f305]) ).
fof(f370609,plain,
( aScalar0(xE)
| ~ spl2_294 ),
inference(resolution,[],[f19221,f250]) ).
fof(f370615,plain,
( $false
| ~ spl2_294 ),
inference(forward_subsumption_resolution,[],[f370609,f281]) ).
fof(f370616,plain,
~ spl2_294,
inference(avatar_contradiction_clause,[],[f370615]) ).
fof(f391095,plain,
( sdtpldt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(sz0z00,smndt0(xS)),sdtpldt0(sz0z00,smndt0(xS))),xN),xN)
| ~ spl2_4
| ~ spl2_3693 ),
inference(superposition,[],[f224,f350895]) ).
fof(f407393,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(xS,xS))
| aScalar0(sdtasdt0(xS,xS))
| aScalar0(sz0z00)
| sz0z00 = sdtasdt0(xS,xS)
| spl2_3334 ),
inference(resolution,[],[f337492,f251]) ).
fof(f407394,plain,
( aScalar0(sdtasdt0(xS,xS))
| aScalar0(sz0z00)
| sz0z00 = sdtasdt0(xS,xS)
| spl2_12
| spl2_3334 ),
inference(forward_subsumption_resolution,[],[f407393,f548]) ).
fof(f407399,plain,
( aScalar0(sz0z00)
| sz0z00 = sdtasdt0(xS,xS)
| spl2_11
| spl2_12
| spl2_3334 ),
inference(forward_subsumption_resolution,[],[f407394,f543]) ).
fof(f407404,plain,
( sz0z00 = sdtasdt0(xS,xS)
| spl2_11
| spl2_12
| spl2_3334 ),
inference(forward_subsumption_resolution,[],[f407399,f228]) ).
fof(f407410,plain,
( spl2_3350
| spl2_11
| spl2_12
| spl2_3334 ),
inference(avatar_split_clause,[],[f407404,f337490,f546,f541,f338469]) ).
fof(f417204,definition,
( spl2_3987
<=> sz0z00 = sdtasdt0(xR,xP) ),
introduced(definition,[new_symbols(definition,[spl2_3987])],[avatar_definition]) ).
fof(f417206,plain,
( sz0z00 = sdtasdt0(xR,xP)
| ~ spl2_3987 ),
inference(avatar_component_clause,[],[f417204]) ).
fof(f462726,definition,
( spl2_4230
<=> sdtlseqdt0(sdtasdt0(xR,xR),xN) ),
introduced(definition,[new_symbols(definition,[spl2_4230])],[avatar_definition]) ).
fof(f462727,plain,
( sdtlseqdt0(sdtasdt0(xR,xR),xN)
| ~ spl2_4230 ),
inference(avatar_component_clause,[],[f462726]) ).
fof(f462728,plain,
( ~ sdtlseqdt0(sdtasdt0(xR,xR),xN)
| spl2_4230 ),
inference(avatar_component_clause,[],[f462726]) ).
fof(f468434,plain,
( aScalar0(xS)
| aScalar0(xS)
| sdtlseqdt0(xS,xS)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xS,xR)
| ~ spl2_641 ),
inference(resolution,[],[f56512,f1379]) ).
fof(f502023,plain,
( sdtlseqdt0(xS,xN)
| aScalar0(xS)
| xS = xN
| spl2_167
| ~ spl2_476 ),
inference(resolution,[],[f31964,f17609]) ).
fof(f517429,plain,
( sz0z00 != xN
| aScalar0(smndt0(xP))
| sdtlseqdt0(sz0z00,smndt0(xP))
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67 ),
inference(superposition,[],[f2173,f8427]) ).
fof(f517436,plain,
( sz0z00 != xN
| aScalar0(xP)
| sdtlseqdt0(sz0z00,xP)
| sz0z00 = xP
| ~ spl2_17
| spl2_67 ),
inference(superposition,[],[f2173,f771]) ).
fof(f560410,plain,
( sz0z00 != xR
| spl2_1682
| ~ spl2_3987 ),
inference(superposition,[],[f130213,f417206]) ).
fof(f577298,definition,
( spl2_4901
<=> sz0z00 = xR ),
introduced(definition,[new_symbols(definition,[spl2_4901])],[avatar_definition]) ).
fof(f577308,plain,
( ~ spl2_4901
| spl2_1682
| ~ spl2_3987 ),
inference(avatar_split_clause,[],[f560410,f417204,f130212,f577298]) ).
fof(f654907,definition,
( spl2_5048
<=> xN = sdtasdt0(xR,xR) ),
introduced(definition,[new_symbols(definition,[spl2_5048])],[avatar_definition]) ).
fof(f654909,plain,
( xN = sdtasdt0(xR,xR)
| ~ spl2_5048 ),
inference(avatar_component_clause,[],[f654907]) ).
fof(f673787,plain,
( ! [X0] :
( aScalar0(X0)
| sdtasdt0(sdtasdt0(X0,xN),xR) = sdtasdt0(X0,sdtasdt0(xR,xN)) )
| ~ spl2_1 ),
inference(forward_demodulation,[],[f15072,f3711]) ).
fof(f686534,plain,
( sz0z00 != xN
| aScalar0(xS)
| sdtlseqdt0(sz0z00,xS)
| sz0z00 = xS
| spl2_67
| ~ spl2_382 ),
inference(superposition,[],[f2173,f21229]) ).
fof(f705232,plain,
( sz0z00 != xN
| aScalar0(xR)
| sdtlseqdt0(sz0z00,xR)
| sz0z00 = xR
| spl2_67
| ~ spl2_5048 ),
inference(superposition,[],[f2173,f654909]) ).
fof(f728991,plain,
( aScalar0(xR)
| aScalar0(xR)
| sdtlseqdt0(xR,xS)
| sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(xR,xR)
| ~ spl2_4230 ),
inference(resolution,[],[f462727,f1379]) ).
fof(f728994,plain,
( aScalar0(xR)
| sdtlseqdt0(xR,xS)
| sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(xR,xR)
| ~ spl2_4230 ),
inference(duplicate_literal_removal,[],[f728991]) ).
fof(f728996,plain,
( sdtlseqdt0(xR,xS)
| sdtlseqdt0(sz0z00,xR)
| sdtlseqdt0(xR,xR)
| ~ spl2_4230 ),
inference(forward_subsumption_resolution,[],[f728994,f285]) ).
fof(f729038,plain,
( sdtlseqdt0(xN,sdtasdt0(xR,xR))
| aScalar0(sdtasdt0(xR,xR))
| aScalar0(xN)
| xN = sdtasdt0(xR,xR)
| spl2_4230 ),
inference(resolution,[],[f462728,f251]) ).
fof(f731953,definition,
( spl2_5175
<=> xN = smndt0(xP) ),
introduced(definition,[new_symbols(definition,[spl2_5175])],[avatar_definition]) ).
fof(f731954,plain,
( xN != smndt0(xP)
| spl2_5175 ),
inference(avatar_component_clause,[],[f731953]) ).
fof(f731955,plain,
( xN = smndt0(xP)
| ~ spl2_5175 ),
inference(avatar_component_clause,[],[f731953]) ).
fof(f732290,plain,
( ~ sdtlseqdt0(xN,sdtasdt0(xR,xR))
| spl2_1153
| ~ spl2_5175 ),
inference(superposition,[],[f91935,f731955]) ).
fof(f732415,plain,
( ~ spl2_3247
| spl2_1153
| ~ spl2_5175 ),
inference(avatar_split_clause,[],[f732290,f731953,f91933,f333289]) ).
fof(f735071,definition,
( spl2_5198
<=> xP = sdtasdt0(xN,xP) ),
introduced(definition,[new_symbols(definition,[spl2_5198])],[avatar_definition]) ).
fof(f735072,plain,
( xP != sdtasdt0(xN,xP)
| spl2_5198 ),
inference(avatar_component_clause,[],[f735071]) ).
fof(f735073,plain,
( xP = sdtasdt0(xN,xP)
| ~ spl2_5198 ),
inference(avatar_component_clause,[],[f735071]) ).
fof(f739562,plain,
( xP != xN
| ~ spl2_1248
| spl2_5175 ),
inference(superposition,[],[f731954,f95227]) ).
fof(f744797,plain,
( sdtlseqdt0(xP,sdtasdt0(xR,xR))
| ~ spl2_1153
| ~ spl2_1248 ),
inference(forward_demodulation,[],[f91934,f95227]) ).
fof(f886854,plain,
( sdtasdt0(xP,sdtasdt0(xR,xN)) = sdtasdt0(sdtasdt0(xP,xN),xR)
| ~ spl2_1 ),
inference(resolution,[],[f673787,f286]) ).
fof(f886857,plain,
( sdtasdt0(sdtasdt0(xN,xP),xR) = sdtasdt0(xP,sdtasdt0(xR,xN))
| ~ spl2_1 ),
inference(forward_demodulation,[],[f886854,f3750]) ).
fof(f886907,plain,
( sdtasdt0(xP,xR) = sdtasdt0(xP,sdtasdt0(xR,xN))
| ~ spl2_1
| ~ spl2_5198 ),
inference(forward_demodulation,[],[f886857,f735073]) ).
fof(f886917,plain,
( sdtasdt0(xR,xP) = sdtasdt0(xP,sdtasdt0(xR,xN))
| ~ spl2_1
| ~ spl2_5198 ),
inference(forward_demodulation,[],[f886907,f3709]) ).
fof(f937577,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| aScalar0(xE)
| sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(forward_subsumption_resolution,[],[f319058,f228]) ).
fof(f938475,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(forward_subsumption_resolution,[],[f937577,f281]) ).
fof(f939077,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(xE,xE)
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f938475,f1887]) ).
fof(f939491,plain,
( ~ sdtlseqdt0(sz0z00,xP)
| sdtlseqdt0(sz0z00,xH)
| spl2_67
| spl2_294 ),
inference(forward_subsumption_resolution,[],[f939077,f19220]) ).
fof(f939663,plain,
( spl2_28
| ~ spl2_29
| spl2_67
| spl2_294 ),
inference(avatar_split_clause,[],[f939491,f19219,f1886,f906,f902]) ).
fof(f955000,plain,
( ~ spl2_397
| ~ spl2_1248
| spl2_5175 ),
inference(avatar_split_clause,[],[f739562,f731953,f95225,f22043]) ).
fof(f971628,plain,
( aScalar0(sz0z00)
| sdtlseqdt0(xN,sz0z00)
| aScalar0(xP)
| ~ spl2_473 ),
inference(resolution,[],[f31909,f258]) ).
fof(f996059,plain,
( sdtlseqdt0(xS,xN)
| xS = xN
| spl2_167
| ~ spl2_476 ),
inference(forward_subsumption_resolution,[],[f502023,f287]) ).
fof(f1000271,plain,
( sdtlseqdt0(xS,xN)
| spl2_167
| spl2_369
| ~ spl2_476 ),
inference(forward_subsumption_resolution,[],[f996059,f20715]) ).
fof(f1002539,plain,
( spl2_177
| spl2_167
| spl2_369
| ~ spl2_476 ),
inference(avatar_split_clause,[],[f1000271,f31963,f20714,f17607,f17654]) ).
fof(f1015406,plain,
( sdtlseqdt0(xN,sz0z00)
| aScalar0(xP)
| ~ spl2_473 ),
inference(forward_subsumption_resolution,[],[f971628,f228]) ).
fof(f1021969,plain,
( sdtlseqdt0(xN,sz0z00)
| ~ spl2_473 ),
inference(forward_subsumption_resolution,[],[f1015406,f286]) ).
fof(f1025306,plain,
( spl2_178
| ~ spl2_473 ),
inference(avatar_split_clause,[],[f1021969,f31908,f17658]) ).
fof(f1032056,plain,
( spl2_1094
| ~ spl2_1153
| ~ spl2_1248 ),
inference(avatar_split_clause,[],[f744797,f95225,f91933,f87139]) ).
fof(f1045822,plain,
( ~ spl2_2818
| spl2_397
| ~ spl2_3236 ),
inference(avatar_split_clause,[],[f346177,f331858,f22043,f319846]) ).
fof(f1048293,plain,
( ~ sdtlseqdt0(sz0z00,xE)
| aScalar0(smndt0(xE))
| aScalar0(xE)
| sdtlseqdt0(smndt0(xE),sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(superposition,[],[f1721,f488]) ).
fof(f1052710,plain,
( ~ sdtlseqdt0(sz0z00,xH)
| aScalar0(smndt0(xH))
| aScalar0(xH)
| sdtlseqdt0(smndt0(xH),sz0z00)
| sdtlseqdt0(xH,xH) ),
inference(superposition,[],[f1745,f491]) ).
fof(f1054852,plain,
( sz0z00 != xN
| sdtlseqdt0(sz0z00,smndt0(xP))
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67
| spl2_90 ),
inference(forward_subsumption_resolution,[],[f517429,f2403]) ).
fof(f1054853,plain,
( sz0z00 != xN
| sdtlseqdt0(sz0z00,xP)
| sz0z00 = xP
| ~ spl2_17
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f517436,f286]) ).
fof(f1074050,plain,
( sz0z00 != xN
| sdtlseqdt0(sz0z00,xR)
| sz0z00 = xR
| spl2_67
| ~ spl2_5048 ),
inference(forward_subsumption_resolution,[],[f705232,f285]) ).
fof(f1076487,plain,
( sdtlseqdt0(sz0z00,xP)
| sz0z00 != xN
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67
| spl2_90
| ~ spl2_1248 ),
inference(forward_demodulation,[],[f1054852,f95227]) ).
fof(f1076488,plain,
( sz0z00 != xN
| sz0z00 = xP
| ~ spl2_17
| spl2_29
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f1054853,f908]) ).
fof(f1085852,plain,
( sz0z00 != xN
| sz0z00 = xR
| spl2_23
| spl2_67
| ~ spl2_5048 ),
inference(forward_subsumption_resolution,[],[f1074050,f874]) ).
fof(f1087355,plain,
( sz0z00 != xN
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_29
| spl2_67
| spl2_90
| ~ spl2_1248 ),
inference(forward_subsumption_resolution,[],[f1076487,f908]) ).
fof(f1092218,plain,
( spl2_3744
| ~ spl2_2818
| ~ spl2_17
| spl2_29
| spl2_67
| spl2_90
| ~ spl2_1248 ),
inference(avatar_split_clause,[],[f1087355,f95225,f2402,f1886,f906,f769,f319846,f349883]) ).
fof(f1096560,plain,
( sz0z00 != xN
| sdtlseqdt0(sz0z00,xS)
| sz0z00 = xS
| spl2_67
| ~ spl2_382 ),
inference(forward_subsumption_resolution,[],[f686534,f287]) ).
fof(f1102900,plain,
( sz0z00 != xN
| sz0z00 = xS
| spl2_25
| spl2_67
| ~ spl2_382 ),
inference(forward_subsumption_resolution,[],[f1096560,f889]) ).
fof(f1105686,plain,
( sz0z00 != xN
| spl2_25
| spl2_32
| spl2_67
| ~ spl2_382 ),
inference(forward_subsumption_resolution,[],[f1102900,f1111]) ).
fof(f1107167,plain,
( ~ spl2_2818
| spl2_25
| spl2_32
| spl2_67
| ~ spl2_382 ),
inference(avatar_split_clause,[],[f1105686,f21228,f1886,f1110,f888,f319846]) ).
fof(f1108738,plain,
( sdtlseqdt0(xR,xS)
| sdtlseqdt0(xR,xR)
| spl2_23
| ~ spl2_4230 ),
inference(forward_subsumption_resolution,[],[f728996,f874]) ).
fof(f1108845,plain,
( ~ sdtlseqdt0(sz0z00,xE)
| aScalar0(xE)
| sdtlseqdt0(smndt0(xE),sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(forward_subsumption_resolution,[],[f1048293,f231]) ).
fof(f1109401,plain,
( sdtlseqdt0(xR,xS)
| spl2_23
| spl2_157
| ~ spl2_4230 ),
inference(forward_subsumption_resolution,[],[f1108738,f17565]) ).
fof(f1109432,plain,
( ~ sdtlseqdt0(sz0z00,xE)
| sdtlseqdt0(smndt0(xE),sz0z00)
| sdtlseqdt0(xE,xE) ),
inference(forward_subsumption_resolution,[],[f1108845,f281]) ).
fof(f1109671,plain,
( spl2_244
| spl2_23
| spl2_157
| ~ spl2_4230 ),
inference(avatar_split_clause,[],[f1109401,f462726,f17564,f873,f18427]) ).
fof(f1109682,plain,
( ~ sdtlseqdt0(sz0z00,xE)
| sdtlseqdt0(smndt0(xE),sz0z00)
| spl2_294 ),
inference(forward_subsumption_resolution,[],[f1109432,f19220]) ).
fof(f1109780,plain,
( spl2_3510
| ~ spl2_27
| spl2_294 ),
inference(avatar_split_clause,[],[f1109682,f19219,f898,f342728]) ).
fof(f1135672,plain,
( sz0z00 != sdtasdt0(xN,sz0z00)
| ~ spl2_3236
| spl2_5198 ),
inference(superposition,[],[f735072,f331860]) ).
fof(f1135828,plain,
( $false
| ~ spl2_3236
| spl2_5198 ),
inference(forward_subsumption_resolution,[],[f1135672,f403]) ).
fof(f1135829,plain,
( ~ spl2_3236
| spl2_5198 ),
inference(avatar_contradiction_clause,[],[f1135828]) ).
fof(f1139777,plain,
( ~ sdtlseqdt0(xS,sz0z00)
| aScalar0(xS)
| sdtlseqdt0(sz0z00,smndt0(xS))
| sdtlseqdt0(xS,xS)
| aScalar0(smndt0(xS)) ),
inference(superposition,[],[f1771,f494]) ).
fof(f1139788,plain,
( aScalar0(xS)
| sdtlseqdt0(sz0z00,smndt0(xS))
| sdtlseqdt0(xS,xS)
| aScalar0(smndt0(xS))
| ~ spl2_454 ),
inference(forward_subsumption_resolution,[],[f1139777,f31602]) ).
fof(f1139829,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| sdtlseqdt0(xS,xS)
| aScalar0(smndt0(xS))
| ~ spl2_454 ),
inference(forward_subsumption_resolution,[],[f1139788,f287]) ).
fof(f1139870,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| aScalar0(smndt0(xS))
| spl2_212
| ~ spl2_454 ),
inference(forward_subsumption_resolution,[],[f1139829,f18036]) ).
fof(f1139912,plain,
( sdtlseqdt0(sz0z00,smndt0(xS))
| spl2_9
| spl2_212
| ~ spl2_454 ),
inference(forward_subsumption_resolution,[],[f1139870,f469]) ).
fof(f1140692,definition,
( spl2_7538
<=> sdtlseqdt0(smndt0(xS),sz0z00) ),
introduced(definition,[new_symbols(definition,[spl2_7538])],[avatar_definition]) ).
fof(f1148062,plain,
( spl2_22
| spl2_9
| spl2_212
| ~ spl2_454 ),
inference(avatar_split_clause,[],[f1139912,f31601,f18034,f468,f867]) ).
fof(f1160498,plain,
( ~ spl2_7538
| spl2_9
| ~ spl2_22 ),
inference(avatar_split_clause,[],[f1650,f867,f468,f1140692]) ).
fof(f1162407,plain,
( xS = smndt0(xS)
| sdtlseqdt0(sz0z00,xS)
| aScalar0(xS)
| ~ spl2_34 ),
inference(equality_resolution,[],[f1188]) ).
fof(f1162408,plain,
( xS = smndt0(xS)
| aScalar0(xS)
| spl2_25
| ~ spl2_34 ),
inference(forward_subsumption_resolution,[],[f1162407,f889]) ).
fof(f1162413,plain,
( xS = smndt0(xS)
| spl2_25
| ~ spl2_34 ),
inference(forward_subsumption_resolution,[],[f1162408,f287]) ).
fof(f1162418,plain,
( spl2_384
| spl2_25
| ~ spl2_34 ),
inference(avatar_split_clause,[],[f1162413,f1187,f888,f21239]) ).
fof(f1163802,plain,
( ~ sdtlseqdt0(smndt0(xN),sz0z00)
| aScalar0(xR)
| sdtlseqdt0(smndt0(xS),sz0z00)
| sdtlseqdt0(xR,xR)
| aScalar0(sz0z00)
| ~ spl2_60 ),
inference(superposition,[],[f1414,f414]) ).
fof(f1164316,plain,
( ~ sdtlseqdt0(smndt0(xN),sz0z00)
| sdtlseqdt0(smndt0(xS),sz0z00)
| sdtlseqdt0(xR,xR)
| aScalar0(sz0z00)
| ~ spl2_60 ),
inference(forward_subsumption_resolution,[],[f1163802,f285]) ).
fof(f1164451,plain,
( ~ sdtlseqdt0(smndt0(xN),sz0z00)
| sdtlseqdt0(smndt0(xS),sz0z00)
| aScalar0(sz0z00)
| ~ spl2_60
| spl2_157 ),
inference(forward_subsumption_resolution,[],[f1164316,f17565]) ).
fof(f1164586,plain,
( ~ sdtlseqdt0(smndt0(xN),sz0z00)
| sdtlseqdt0(smndt0(xS),sz0z00)
| ~ spl2_60
| spl2_157 ),
inference(forward_subsumption_resolution,[],[f1164451,f228]) ).
fof(f1164760,plain,
( spl2_7538
| ~ spl2_2542
| ~ spl2_60
| spl2_157 ),
inference(avatar_split_clause,[],[f1164586,f17564,f1413,f307337,f1140692]) ).
fof(f1166389,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| sdtlseqdt0(smndt0(xS),smndt0(xS))
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,xR)
| aScalar0(smndt0(xS))
| aScalar0(sz0z00)
| spl2_9
| ~ spl2_56 ),
inference(superposition,[],[f1386,f1425]) ).
fof(f1179195,definition,
( spl2_8024
<=> sz0z00 = smndt0(xN) ),
introduced(definition,[new_symbols(definition,[spl2_8024])],[avatar_definition]) ).
fof(f1179197,plain,
( sz0z00 = smndt0(xN)
| ~ spl2_8024 ),
inference(avatar_component_clause,[],[f1179195]) ).
fof(f1181028,plain,
( sdtlseqdt0(sz0z00,smndt0(xN))
| aScalar0(sz0z00)
| aScalar0(smndt0(xN))
| sz0z00 = smndt0(xN)
| spl2_2542 ),
inference(resolution,[],[f307339,f251]) ).
fof(f1188967,plain,
( smndt0(sz0z00) = xN
| ~ spl2_8024 ),
inference(superposition,[],[f431,f1179197]) ).
fof(f1189131,plain,
( sz0z00 = xN
| ~ spl2_4
| ~ spl2_8024 ),
inference(forward_demodulation,[],[f1188967,f305]) ).
fof(f1189434,plain,
( sdtlseqdt0(sz0z00,smndt0(xN))
| aScalar0(smndt0(xN))
| sz0z00 = smndt0(xN)
| spl2_2542 ),
inference(forward_subsumption_resolution,[],[f1181028,f228]) ).
fof(f1189743,plain,
( sdtlseqdt0(sz0z00,smndt0(xN))
| sz0z00 = smndt0(xN)
| spl2_10
| spl2_2542 ),
inference(forward_subsumption_resolution,[],[f1189434,f474]) ).
fof(f1189972,plain,
( spl2_8024
| spl2_24
| spl2_10
| spl2_2542 ),
inference(avatar_split_clause,[],[f1189743,f307337,f472,f877,f1179195]) ).
fof(f1190539,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,xR)
| aScalar0(smndt0(xS))
| aScalar0(sz0z00)
| spl2_9
| ~ spl2_56 ),
inference(forward_subsumption_resolution,[],[f1166389,f250]) ).
fof(f1190723,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| sdtlseqdt0(sz0z00,xR)
| aScalar0(smndt0(xS))
| aScalar0(sz0z00)
| spl2_9
| ~ spl2_56
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f1190539,f1887]) ).
fof(f1190901,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| aScalar0(smndt0(xS))
| aScalar0(sz0z00)
| spl2_9
| spl2_23
| ~ spl2_56
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f1190723,f874]) ).
fof(f1190987,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| aScalar0(sz0z00)
| spl2_9
| spl2_23
| ~ spl2_56
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f1190901,f469]) ).
fof(f1191016,plain,
( ~ sdtlseqdt0(sz0z00,smndt0(xN))
| spl2_9
| spl2_23
| ~ spl2_56
| spl2_67 ),
inference(forward_subsumption_resolution,[],[f1190987,f228]) ).
fof(f1191023,plain,
( ~ spl2_24
| spl2_9
| spl2_23
| ~ spl2_56
| spl2_67 ),
inference(avatar_split_clause,[],[f1191016,f1886,f1385,f873,f468,f877]) ).
fof(f1191157,plain,
( aScalar0(xS)
| sdtlseqdt0(xS,xS)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xS,xR)
| ~ spl2_641 ),
inference(duplicate_literal_removal,[],[f468434]) ).
fof(f1194942,plain,
( sdtlseqdt0(xS,xS)
| sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xS,xR)
| ~ spl2_641 ),
inference(forward_subsumption_resolution,[],[f1191157,f287]) ).
fof(f1205935,plain,
( spl2_2818
| ~ spl2_4
| ~ spl2_8024 ),
inference(avatar_split_clause,[],[f1189131,f1179195,f303,f319846]) ).
fof(f1208100,plain,
( sdtlseqdt0(sz0z00,xS)
| sdtlseqdt0(xS,xR)
| spl2_212
| ~ spl2_641 ),
inference(forward_subsumption_resolution,[],[f1194942,f18036]) ).
fof(f1215874,plain,
( sdtlseqdt0(xS,xR)
| spl2_25
| spl2_212
| ~ spl2_641 ),
inference(forward_subsumption_resolution,[],[f1208100,f889]) ).
fof(f1225211,plain,
( sdtlseqdt0(xN,sdtasdt0(xR,xR))
| aScalar0(xN)
| xN = sdtasdt0(xR,xR)
| spl2_1370
| spl2_4230 ),
inference(forward_subsumption_resolution,[],[f729038,f104377]) ).
fof(f1227859,plain,
( spl2_175
| spl2_25
| spl2_212
| ~ spl2_641 ),
inference(avatar_split_clause,[],[f1215874,f56511,f18034,f888,f17645]) ).
fof(f1228351,plain,
( ~ sdtlseqdt0(sz0z00,xH)
| aScalar0(xH)
| sdtlseqdt0(smndt0(xH),sz0z00)
| sdtlseqdt0(xH,xH) ),
inference(forward_subsumption_resolution,[],[f1052710,f231]) ).
fof(f1230001,plain,
( sdtlseqdt0(xN,sdtasdt0(xR,xR))
| xN = sdtasdt0(xR,xR)
| spl2_1370
| spl2_4230 ),
inference(forward_subsumption_resolution,[],[f1225211,f288]) ).
fof(f1231556,plain,
( ~ sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(smndt0(xH),sz0z00)
| sdtlseqdt0(xH,xH) ),
inference(forward_subsumption_resolution,[],[f1228351,f284]) ).
fof(f1232217,plain,
( spl2_5048
| spl2_3247
| spl2_1370
| spl2_4230 ),
inference(avatar_split_clause,[],[f1230001,f462726,f104376,f333289,f654907]) ).
fof(f1233327,plain,
( ~ sdtlseqdt0(sz0z00,xH)
| sdtlseqdt0(smndt0(xH),sz0z00)
| spl2_536 ),
inference(forward_subsumption_resolution,[],[f1231556,f34225]) ).
fof(f1234224,plain,
( spl2_3507
| ~ spl2_28
| spl2_536 ),
inference(avatar_split_clause,[],[f1233327,f34223,f902,f342704]) ).
fof(f1241397,plain,
( sdtlseqdt0(sz0z00,sdtasdt0(xP,xP))
| ~ spl2_19
| ~ spl2_2818 ),
inference(superposition,[],[f779,f319848]) ).
fof(f1241852,plain,
( spl2_2595
| ~ spl2_19
| ~ spl2_2818 ),
inference(avatar_split_clause,[],[f1241397,f319846,f777,f308464]) ).
fof(f1259709,plain,
( sz0z00 != sz0z00
| aScalar0(smndt0(xP))
| sdtlseqdt0(sz0z00,smndt0(xP))
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67
| ~ spl2_2818 ),
inference(superposition,[],[f2173,f348896]) ).
fof(f1259752,plain,
( aScalar0(smndt0(xP))
| sdtlseqdt0(sz0z00,smndt0(xP))
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67
| ~ spl2_2818 ),
inference(trivial_inequality_removal,[],[f1259709]) ).
fof(f1259761,plain,
( sdtlseqdt0(sz0z00,smndt0(xP))
| sz0z00 = smndt0(xP)
| ~ spl2_17
| spl2_67
| spl2_90
| ~ spl2_2818 ),
inference(forward_subsumption_resolution,[],[f1259752,f2403]) ).
fof(f1259770,plain,
( spl2_3744
| spl2_139
| ~ spl2_17
| spl2_67
| spl2_90
| ~ spl2_2818 ),
inference(avatar_split_clause,[],[f1259761,f319846,f2402,f1886,f769,f8797,f349883]) ).
fof(f1276993,plain,
( smndt0(sz0z00) = xP
| ~ spl2_3744 ),
inference(superposition,[],[f429,f349885]) ).
fof(f1277185,plain,
( sz0z00 = xP
| ~ spl2_4
| ~ spl2_3744 ),
inference(forward_demodulation,[],[f1276993,f305]) ).
fof(f1277594,plain,
( sz0z00 = xP
| ~ spl2_17
| spl2_29
| spl2_67
| ~ spl2_2818 ),
inference(forward_subsumption_resolution,[],[f1076488,f319848]) ).
fof(f1284043,plain,
( sdtasdt0(xR,sz0z00) = smndt0(xR)
| ~ spl2_1682
| ~ spl2_3744 ),
inference(forward_demodulation,[],[f232658,f349885]) ).
fof(f1292535,plain,
( sdtpldt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(sdtpldt0(sz0z00,smndt0(xS)),sdtpldt0(sz0z00,smndt0(xS))),sz0z00),sz0z00)
| ~ spl2_4
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f391095,f319848]) ).
fof(f1295136,plain,
( sz0z00 = xR
| spl2_23
| spl2_67
| ~ spl2_2818
| ~ spl2_5048 ),
inference(forward_subsumption_resolution,[],[f1085852,f319848]) ).
fof(f1295457,plain,
( sdtasdt0(xR,xP) = sdtasdt0(xP,sdtasdt0(xR,sz0z00))
| ~ spl2_1
| ~ spl2_2818
| ~ spl2_5198 ),
inference(forward_demodulation,[],[f886917,f319848]) ).
fof(f1296100,plain,
( spl2_3236
| ~ spl2_4
| ~ spl2_3744 ),
inference(avatar_split_clause,[],[f1277185,f349883,f303,f331858]) ).
fof(f1297532,plain,
( spl2_3236
| ~ spl2_17
| spl2_29
| spl2_67
| ~ spl2_2818 ),
inference(avatar_split_clause,[],[f1277594,f319846,f1886,f906,f769,f331858]) ).
fof(f1300584,plain,
( sz0z00 = smndt0(xR)
| ~ spl2_1682
| ~ spl2_3744 ),
inference(forward_demodulation,[],[f1284043,f400]) ).
fof(f1305688,plain,
( sdtpldt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(smndt0(xS),smndt0(xS)),sz0z00),sz0z00)
| ~ spl2_4
| spl2_9
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f1292535,f1424]) ).
fof(f1307109,plain,
( spl2_4901
| spl2_23
| spl2_67
| ~ spl2_2818
| ~ spl2_5048 ),
inference(avatar_split_clause,[],[f1295136,f654907,f319846,f1886,f873,f577298]) ).
fof(f1307337,plain,
( sdtasdt0(xP,sz0z00) = sdtasdt0(xR,xP)
| ~ spl2_1
| ~ spl2_2818
| ~ spl2_5198 ),
inference(forward_demodulation,[],[f1295457,f400]) ).
fof(f1309852,plain,
( spl2_3693
| ~ spl2_1682
| ~ spl2_3744 ),
inference(avatar_split_clause,[],[f1300584,f349883,f130212,f347494]) ).
fof(f1312691,plain,
( sdtpldt0(sdtpldt0(sdtasdt0(xS,xS),sz0z00),sz0z00) != sdtpldt0(sdtasdt0(sz0z00,sz0z00),sdtasdt0(xS,xS))
| ~ spl2_4
| spl2_9
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f1305688,f218]) ).
fof(f1313559,plain,
( sz0z00 = sdtasdt0(xR,xP)
| ~ spl2_1
| ~ spl2_2818
| ~ spl2_5198 ),
inference(forward_demodulation,[],[f1307337,f401]) ).
fof(f1316374,plain,
( sdtpldt0(sz0z00,sdtasdt0(xS,xS)) != sdtpldt0(sdtpldt0(sdtasdt0(xS,xS),sz0z00),sz0z00)
| ~ spl2_4
| spl2_9
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f1312691,f390]) ).
fof(f1316814,plain,
( spl2_3987
| ~ spl2_1
| ~ spl2_2818
| ~ spl2_5198 ),
inference(avatar_split_clause,[],[f1313559,f735071,f319846,f292,f417204]) ).
fof(f1318198,plain,
( sdtpldt0(sdtasdt0(xS,xS),sz0z00) != sdtpldt0(sz0z00,sdtasdt0(xS,xS))
| ~ spl2_4
| spl2_9
| spl2_11
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f1316374,f830]) ).
fof(f1319006,plain,
( sdtasdt0(xS,xS) != sdtpldt0(sdtasdt0(xS,xS),sz0z00)
| ~ spl2_4
| spl2_9
| spl2_11
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_demodulation,[],[f1318198,f831]) ).
fof(f1319349,plain,
( $false
| ~ spl2_4
| spl2_9
| spl2_11
| ~ spl2_2818
| ~ spl2_3693 ),
inference(forward_subsumption_resolution,[],[f1319006,f830]) ).
fof(f1319350,plain,
( ~ spl2_4
| spl2_9
| spl2_11
| ~ spl2_2818
| ~ spl2_3693 ),
inference(avatar_contradiction_clause,[],[f1319349]) ).
cnf(s1,plain,
( spl2_1
| spl2_2 ),
inference(sat_conversion,[],[f297]) ).
cnf(s3,plain,
( spl2_2
| spl2_4 ),
inference(sat_conversion,[],[f306]) ).
cnf(s16,plain,
~ spl2_2,
inference(sat_conversion,[],[f332]) ).
cnf(s21,plain,
( spl2_9
| ~ spl2_10 ),
inference(sat_conversion,[],[f476]) ).
cnf(s23,plain,
( spl2_9
| ~ spl2_11 ),
inference(sat_conversion,[],[f544]) ).
cnf(s24,plain,
( spl2_9
| ~ spl2_12 ),
inference(sat_conversion,[],[f549]) ).
cnf(s28,plain,
( spl2_17
| spl2_18
| spl2_19 ),
inference(sat_conversion,[],[f781]) ).
cnf(s34,plain,
( spl2_23
| spl2_25
| ~ spl2_26 ),
inference(sat_conversion,[],[f895]) ).
cnf(s37,plain,
~ spl2_25,
inference(sat_conversion,[],[f922]) ).
cnf(s38,plain,
~ spl2_23,
inference(sat_conversion,[],[f923]) ).
cnf(s42,plain,
( spl2_9
| spl2_22
| spl2_34 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s66,plain,
( spl2_9
| spl2_56 ),
inference(sat_conversion,[],[f1387]) ).
cnf(s70,plain,
( spl2_9
| spl2_23
| spl2_60 ),
inference(sat_conversion,[],[f1415]) ).
cnf(s71,plain,
~ spl2_9,
inference(sat_conversion,[],[f1418]) ).
cnf(s72,plain,
( spl2_10
| ~ spl2_39
| spl2_49 ),
inference(sat_conversion,[],[f1419]) ).
cnf(s83,plain,
~ spl2_67,
inference(sat_conversion,[],[f1912]) ).
cnf(s103,plain,
~ spl2_80,
inference(sat_conversion,[],[f2560]) ).
cnf(s107,plain,
~ spl2_86,
inference(sat_conversion,[],[f2697]) ).
cnf(s108,plain,
~ spl2_88,
inference(sat_conversion,[],[f2755]) ).
cnf(s111,plain,
~ spl2_90,
inference(sat_conversion,[],[f2905]) ).
cnf(s283,plain,
~ spl2_212,
inference(sat_conversion,[],[f18248]) ).
cnf(s291,plain,
( spl2_26
| ~ spl2_32
| ~ spl2_177 ),
inference(sat_conversion,[],[f18256]) ).
cnf(s303,plain,
( spl2_25
| spl2_33
| spl2_157
| ~ spl2_178 ),
inference(sat_conversion,[],[f18436]) ).
cnf(s505,plain,
~ spl2_157,
inference(sat_conversion,[],[f19780]) ).
cnf(s811,plain,
( spl2_25
| spl2_32
| spl2_454 ),
inference(sat_conversion,[],[f31603]) ).
cnf(s923,plain,
( spl2_17
| spl2_18
| spl2_473 ),
inference(sat_conversion,[],[f31910]) ).
cnf(s931,plain,
~ spl2_18,
inference(sat_conversion,[],[f31942]) ).
cnf(s940,plain,
( ~ spl2_33
| spl2_454 ),
inference(sat_conversion,[],[f32522]) ).
cnf(s1024,plain,
( ~ spl2_32
| ~ spl2_167
| spl2_178 ),
inference(sat_conversion,[],[f32701]) ).
cnf(s1040,plain,
( spl2_9
| ~ spl2_32
| spl2_383
| ~ spl2_384 ),
inference(sat_conversion,[],[f32979]) ).
cnf(s1601,plain,
( ~ spl2_17
| spl2_18
| spl2_476 ),
inference(sat_conversion,[],[f43527]) ).
cnf(s1684,plain,
( ~ spl2_22
| spl2_25
| ~ spl2_384 ),
inference(sat_conversion,[],[f55626]) ).
cnf(s1782,plain,
( ~ spl2_4
| ~ spl2_32
| spl2_384 ),
inference(sat_conversion,[],[f56401]) ).
cnf(s5401,plain,
~ spl2_536,
inference(sat_conversion,[],[f97151]) ).
cnf(s5901,plain,
~ spl2_1370,
inference(sat_conversion,[],[f105476]) ).
cnf(s10265,plain,
( ~ spl2_32
| spl2_39
| ~ spl2_369
| ~ spl2_383
| ~ spl2_384 ),
inference(sat_conversion,[],[f305857]) ).
cnf(s10494,plain,
( ~ spl2_1
| spl2_27
| spl2_86
| spl2_135
| ~ spl2_139 ),
inference(sat_conversion,[],[f307627]) ).
cnf(s10572,plain,
( spl2_88
| ~ spl2_2587 ),
inference(sat_conversion,[],[f308376]) ).
cnf(s10583,plain,
( spl2_90
| ~ spl2_2595 ),
inference(sat_conversion,[],[f308477]) ).
cnf(s10588,plain,
( ~ spl2_29
| spl2_80
| spl2_86
| spl2_129
| spl2_135 ),
inference(sat_conversion,[],[f308486]) ).
cnf(s12988,plain,
( ~ spl2_175
| ~ spl2_244 ),
inference(sat_conversion,[],[f336436]) ).
cnf(s13173,plain,
( spl2_641
| ~ spl2_2818
| ~ spl2_3334 ),
inference(sat_conversion,[],[f337582]) ).
cnf(s14577,plain,
( spl2_382
| ~ spl2_2818
| ~ spl2_3350 ),
inference(sat_conversion,[],[f346053]) ).
cnf(s14591,plain,
( ~ spl2_4
| spl2_1248
| ~ spl2_3236 ),
inference(sat_conversion,[],[f346425]) ).
cnf(s14604,plain,
( ~ spl2_1094
| spl2_2587
| ~ spl2_3236 ),
inference(sat_conversion,[],[f346456]) ).
cnf(s14617,plain,
( ~ spl2_29
| spl2_67
| ~ spl2_3236 ),
inference(sat_conversion,[],[f346533]) ).
cnf(s14702,plain,
( spl2_80
| ~ spl2_129
| ~ spl2_3510 ),
inference(sat_conversion,[],[f347404]) ).
cnf(s14707,plain,
( spl2_86
| ~ spl2_135
| ~ spl2_3507 ),
inference(sat_conversion,[],[f347453]) ).
cnf(s14943,plain,
( spl2_10
| spl2_11
| ~ spl2_49
| spl2_1370 ),
inference(sat_conversion,[],[f349230]) ).
cnf(s17064,plain,
~ spl2_294,
inference(sat_conversion,[],[f370616]) ).
cnf(s18109,plain,
( spl2_11
| spl2_12
| spl2_3334
| spl2_3350 ),
inference(sat_conversion,[],[f407410]) ).
cnf(s24784,plain,
( spl2_1682
| ~ spl2_3987
| ~ spl2_4901 ),
inference(sat_conversion,[],[f577308]) ).
cnf(s28886,plain,
( spl2_1153
| ~ spl2_3247
| ~ spl2_5175 ),
inference(sat_conversion,[],[f732415]) ).
cnf(s35293,plain,
( spl2_28
| ~ spl2_29
| spl2_67
| spl2_294 ),
inference(sat_conversion,[],[f939663]) ).
cnf(s39858,plain,
( ~ spl2_397
| ~ spl2_1248
| spl2_5175 ),
inference(sat_conversion,[],[f955000]) ).
cnf(s52900,plain,
( spl2_167
| spl2_177
| spl2_369
| ~ spl2_476 ),
inference(sat_conversion,[],[f1002539]) ).
cnf(s58758,plain,
( spl2_178
| ~ spl2_473 ),
inference(sat_conversion,[],[f1025306]) ).
cnf(s62412,plain,
( spl2_1094
| ~ spl2_1153
| ~ spl2_1248 ),
inference(sat_conversion,[],[f1032056]) ).
cnf(s67775,plain,
( spl2_397
| ~ spl2_2818
| ~ spl2_3236 ),
inference(sat_conversion,[],[f1045822]) ).
cnf(s78601,plain,
( ~ spl2_17
| spl2_29
| spl2_67
| spl2_90
| ~ spl2_1248
| ~ spl2_2818
| spl2_3744 ),
inference(sat_conversion,[],[f1092218]) ).
cnf(s87170,plain,
( spl2_25
| spl2_32
| spl2_67
| ~ spl2_382
| ~ spl2_2818 ),
inference(sat_conversion,[],[f1107167]) ).
cnf(s88854,plain,
( spl2_23
| spl2_157
| spl2_244
| ~ spl2_4230 ),
inference(sat_conversion,[],[f1109671]) ).
cnf(s88944,plain,
( ~ spl2_27
| spl2_294
| spl2_3510 ),
inference(sat_conversion,[],[f1109780]) ).
cnf(s96316,plain,
( ~ spl2_3236
| spl2_5198 ),
inference(sat_conversion,[],[f1135829]) ).
cnf(s96715,plain,
( spl2_9
| spl2_22
| spl2_212
| ~ spl2_454 ),
inference(sat_conversion,[],[f1148062]) ).
cnf(s97228,plain,
( spl2_9
| ~ spl2_22
| ~ spl2_7538 ),
inference(sat_conversion,[],[f1160498]) ).
cnf(s97657,plain,
( spl2_25
| ~ spl2_34
| spl2_384 ),
inference(sat_conversion,[],[f1162418]) ).
cnf(s97835,plain,
( ~ spl2_60
| spl2_157
| ~ spl2_2542
| spl2_7538 ),
inference(sat_conversion,[],[f1164760]) ).
cnf(s99781,plain,
( spl2_10
| spl2_24
| spl2_2542
| spl2_8024 ),
inference(sat_conversion,[],[f1189972]) ).
cnf(s99994,plain,
( spl2_9
| spl2_23
| ~ spl2_24
| ~ spl2_56
| spl2_67 ),
inference(sat_conversion,[],[f1191023]) ).
cnf(s100340,plain,
( ~ spl2_4
| spl2_2818
| ~ spl2_8024 ),
inference(sat_conversion,[],[f1205935]) ).
cnf(s104740,plain,
( spl2_25
| spl2_175
| spl2_212
| ~ spl2_641 ),
inference(sat_conversion,[],[f1227859]) ).
cnf(s107003,plain,
( spl2_1370
| spl2_3247
| spl2_4230
| spl2_5048 ),
inference(sat_conversion,[],[f1232217]) ).
cnf(s107854,plain,
( ~ spl2_28
| spl2_536
| spl2_3507 ),
inference(sat_conversion,[],[f1234224]) ).
cnf(s109766,plain,
( ~ spl2_19
| spl2_2595
| ~ spl2_2818 ),
inference(sat_conversion,[],[f1241852]) ).
cnf(s112130,plain,
( ~ spl2_17
| spl2_67
| spl2_90
| spl2_139
| ~ spl2_2818
| spl2_3744 ),
inference(sat_conversion,[],[f1259770]) ).
cnf(s115728,plain,
( ~ spl2_4
| spl2_3236
| ~ spl2_3744 ),
inference(sat_conversion,[],[f1296100]) ).
cnf(s116176,plain,
( ~ spl2_17
| spl2_29
| spl2_67
| ~ spl2_2818
| spl2_3236 ),
inference(sat_conversion,[],[f1297532]) ).
cnf(s117663,plain,
( spl2_23
| spl2_67
| ~ spl2_2818
| spl2_4901
| ~ spl2_5048 ),
inference(sat_conversion,[],[f1307109]) ).
cnf(s118585,plain,
( ~ spl2_1682
| spl2_3693
| ~ spl2_3744 ),
inference(sat_conversion,[],[f1309852]) ).
cnf(s119437,plain,
( ~ spl2_1
| ~ spl2_2818
| spl2_3987
| ~ spl2_5198 ),
inference(sat_conversion,[],[f1316814]) ).
cnf(s120031,plain,
( ~ spl2_4
| spl2_9
| spl2_11
| ~ spl2_2818
| ~ spl2_3693 ),
inference(sat_conversion,[],[f1319350]) ).
cnf(s120308,plain,
( spl2_17
| spl2_473 ),
inference(rat,[],[s923,s931]) ).
cnf(s120318,plain,
( spl2_25
| spl2_33
| ~ spl2_178 ),
inference(rat,[],[s303,s505]) ).
cnf(s120321,plain,
~ spl2_2595,
inference(rat,[],[s10583,s111]) ).
cnf(s120325,plain,
~ spl2_2587,
inference(rat,[],[s10572,s108]) ).
cnf(s120428,plain,
( spl2_23
| spl2_60 ),
inference(rat,[],[s70,s71]) ).
cnf(s120430,plain,
spl2_56,
inference(rat,[],[s66,s71]) ).
cnf(s120434,plain,
( spl2_22
| spl2_34 ),
inference(rat,[],[s42,s71]) ).
cnf(s120436,plain,
~ spl2_24,
inference(rat,[],[s99994,s83,s120430,s71,s38]) ).
cnf(s120437,plain,
spl2_60,
inference(rat,[],[s120428,s38]) ).
cnf(s120439,plain,
~ spl2_26,
inference(rat,[],[s34,s37,s38]) ).
cnf(s120441,plain,
( spl2_17
| spl2_19 ),
inference(rat,[],[s28,s931]) ).
cnf(s120443,plain,
~ spl2_12,
inference(rat,[],[s24,s71]) ).
cnf(s120444,plain,
~ spl2_11,
inference(rat,[],[s23,s71]) ).
cnf(s120446,plain,
~ spl2_10,
inference(rat,[],[s21,s71]) ).
cnf(s120470,plain,
~ spl2_49,
inference(rat,[],[s14943,s5901,s120444,s120446]) ).
cnf(s120475,plain,
~ spl2_39,
inference(rat,[],[s72,s120470,s120446]) ).
cnf(s120486,plain,
spl2_4,
inference(rat,[],[s3,s16]) ).
cnf(s120494,plain,
spl2_1,
inference(rat,[],[s1,s16]) ).
cnf(s120509,plain,
spl2_17,
inference(rat,[],[s97228,s97835,s96715,s99781,s940,s100340,s120318,s109766,s58758,s120441,s120308,s71,s505,s120437,s283,s120436,s120446,s120486,s37,s120321]) ).
cnf(s120510,plain,
spl2_476,
inference(rat,[],[s1601,s931,s120509]) ).
cnf(s120513,plain,
( spl2_29
| ~ spl2_22 ),
inference(rat,[],[s117663,s24784,s107003,s118585,s28886,s39858,s78601,s62412,s119437,s67775,s14591,s14604,s96316,s116176,s120031,s88854,s12988,s104740,s13173,s18109,s14577,s87170,s1782,s1684,s100340,s99781,s97835,s97228,s83,s38,s5901,s111,s120509,s120494,s120486,s120325,s505,s37,s283,s120446,s120436,s120437,s71,s120444,s120443]) ).
cnf(s120514,plain,
~ spl2_22,
inference(rat,[],[s88944,s14702,s10494,s10588,s112130,s14707,s115728,s107854,s14617,s35293,s120513,s100340,s99781,s97835,s97228,s17064,s103,s107,s120494,s111,s83,s120509,s120486,s5401,s120436,s120446,s505,s120437,s71]) ).
cnf(s120516,plain,
~ spl2_454,
inference(rat,[],[s96715,s71,s283,s120514]) ).
cnf(s120522,plain,
spl2_34,
inference(rat,[],[s120434,s120514]) ).
cnf(s120523,plain,
~ spl2_33,
inference(rat,[],[s940,s120516]) ).
cnf(s120524,plain,
spl2_32,
inference(rat,[],[s811,s37,s120516]) ).
cnf(s120526,plain,
spl2_384,
inference(rat,[],[s97657,s37,s120522]) ).
cnf(s120527,plain,
~ spl2_178,
inference(rat,[],[s120318,s37,s120523]) ).
cnf(s120536,plain,
spl2_383,
inference(rat,[],[s1040,s120526,s71,s120524]) ).
cnf(s120537,plain,
~ spl2_167,
inference(rat,[],[s1024,s120527,s120524]) ).
cnf(s120540,plain,
~ spl2_177,
inference(rat,[],[s291,s120439,s120524]) ).
cnf(s120612,plain,
~ spl2_369,
inference(rat,[],[s10265,s120526,s120524,s120475,s120536]) ).
cnf(s120613,plain,
$false,
inference(rat,[],[s52900,s120510,s120612,s120540,s120537]) ).
fof(f1319568,plain,
$false,
inference(avatar_sat_refutation,[],[s120613]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG063+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n010.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:04:47 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.98/2.48 % (1408963)Will run a generic schedule for satisfiability detection.
% 13.98/2.48 % (1408968)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3213196316_2999 on theBenchmark for (2999ds/0Mi)
% 13.98/2.48 % (1408969)% WARNING: option uhcvi not known.
% 13.98/2.48 % TRYING [1]
% 13.98/2.48 % TRYING [2]
% 13.98/2.48 % (1408969)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3388694851:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.98/2.48 % (1408970)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3340404194:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.98/2.48 % (1408971)dis+10_1_sil=32000:sp=arity:random_seed=960098030:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.98/2.48 % TRYING [3]
% 13.98/2.48 % (1408973)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3344811424:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.98/2.48 % (1408972)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1262076247:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.98/2.48 % (1408974)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1506768424:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.98/2.48 % TRYING [4]
% 13.98/2.48 % TRYING [5]
% 13.98/2.48 % (1408971)Instruction limit reached!
% 13.98/2.48 % (1408971)------------------------------
% 13.98/2.48 % (1408971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/2.48 % (1408971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/2.48 % (1408971)CaDiCaL version: 2.1.3
% 13.98/2.48 % (1408971)Termination reason: Instruction limit
% 13.98/2.48 % (1408971)Termination phase: Saturation
% 13.98/2.48 % (1408971)Time elapsed: 0.062 s
% 13.98/2.48 % (1408971)Peak memory usage: 13 MB
% 13.98/2.48 % (1408971)Instructions burned: 104 (million)
% 13.98/2.48 % (1408972)Instruction limit reached!
% 13.98/2.48 % (1408972)------------------------------
% 13.98/2.48 % (1408972)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/2.48 % (1408972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/2.48 % (1408972)CaDiCaL version: 2.1.3
% 13.98/2.48 % (1408972)Termination reason: Instruction limit
% 13.98/2.48 % (1408972)Termination phase: Saturation
% 13.98/2.48 % (1408972)Time elapsed: 0.066 s
% 13.98/2.48 % (1408972)Peak memory usage: 13 MB
% 13.98/2.48 % (1408972)Instructions burned: 116 (million)
% 13.98/2.48 % (1408973)Instruction limit reached!
% 13.98/2.48 % (1408973)------------------------------
% 13.98/2.48 % (1408973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/2.48 % (1408973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/2.48 % (1408973)CaDiCaL version: 2.1.3
% 13.98/2.48 % (1408973)Termination reason: Instruction limit
% 13.98/2.48 % (1408973)Termination phase: Saturation
% 13.98/2.48 % (1408973)Time elapsed: 0.068 s
% 13.98/2.48 % (1408973)Peak memory usage: 13 MB
% 13.98/2.48 % (1408973)Instructions burned: 132 (million)
% 13.98/2.48 % (1408982)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=830415729:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.98/2.48 % (1408983)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=242151919:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.98/2.48 % (1408984)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2362627831:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.98/2.48 % TRYING [1]
% 13.98/2.48 % TRYING [2]
% 13.98/2.48 % TRYING [3]
% 13.98/2.48 % (1408974)Instruction limit reached!
% 13.98/2.48 % (1408974)------------------------------
% 13.98/2.48 % (1408974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.98/2.48 % (1408974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.98/2.48 % (1408974)CaDiCaL version: 2.1.3
% 13.98/2.48 % (1408974)Termination reason: Instruction limit
% 13.98/2.48 % (1408974)Termination phase: Saturation
% 13.98/2.48 % (1408974)Time elapsed: 0.100 s
% 13.98/2.48 % (1408974)Peak memory usage: 14 MB
% 13.98/2.48 % (1408974)Instructions burned: 159 (million)
% 13.98/2.48 % TRYING [4]
% 13.98/2.48 % (1408988)ott-21_1_sil=16000:fs=off:random_seed=3493101917:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.98/2.48 % TRYING [6]
% 13.98/2.48 % (1408983)Instruction limit reached!
% 13.98/2.48 % (1408983)------------------------------
% 13.98/2.48 % (1408983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408983)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408983)Termination reason: Instruction limit
% 41.65/6.34 % (1408983)Termination phase: Saturation
% 41.65/6.34 % (1408983)Time elapsed: 0.059 s
% 41.65/6.34 % (1408983)Peak memory usage: 12 MB
% 41.65/6.34 % (1408983)Instructions burned: 132 (million)
% 41.65/6.34 % (1408990)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3870159805:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 41.65/6.34 % TRYING [5]
% 41.65/6.34 % (1408988)Instruction limit reached!
% 41.65/6.34 % (1408988)------------------------------
% 41.65/6.34 % (1408988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408988)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408988)Termination reason: Instruction limit
% 41.65/6.34 % (1408988)Termination phase: Saturation
% 41.65/6.34 % (1408988)Time elapsed: 0.088 s
% 41.65/6.34 % (1408988)Peak memory usage: 13 MB
% 41.65/6.34 % (1408988)Instructions burned: 181 (million)
% 41.65/6.34 % (1408992)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1701080194:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 41.65/6.34 % TRYING [1]
% 41.65/6.34 % TRYING [2]
% 41.65/6.34 % TRYING [3]
% 41.65/6.34 % TRYING [4]
% 41.65/6.34 % TRYING [6]
% 41.65/6.34 % TRYING [7]
% 41.65/6.34 % (1408982)Instruction limit reached!
% 41.65/6.34 % (1408982)------------------------------
% 41.65/6.34 % (1408982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408982)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408982)Termination reason: Instruction limit
% 41.65/6.34 % (1408982)Termination phase: Finite model building constraint generation
% 41.65/6.34 % (1408982)Time elapsed: 0.266 s
% 41.65/6.34 % (1408982)Peak memory usage: 37 MB
% 41.65/6.34 % (1408982)Instructions burned: 717 (million)
% 41.65/6.34 % (1408994)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1765565573:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 41.65/6.34 % (1408990)Instruction limit reached!
% 41.65/6.34 % (1408990)------------------------------
% 41.65/6.34 % (1408990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408990)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408990)Termination reason: Instruction limit
% 41.65/6.34 % (1408990)Termination phase: Saturation
% 41.65/6.34 % (1408990)Time elapsed: 0.287 s
% 41.65/6.34 % (1408990)Peak memory usage: 14 MB
% 41.65/6.34 % (1408990)Instructions burned: 478 (million)
% 41.65/6.34 % (1408984)Instruction limit reached!
% 41.65/6.34 % (1408984)------------------------------
% 41.65/6.34 % (1408984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408984)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408984)Termination reason: Instruction limit
% 41.65/6.34 % (1408984)Termination phase: Saturation
% 41.65/6.34 % (1408984)Time elapsed: 0.381 s
% 41.65/6.34 % (1408984)Peak memory usage: 20 MB
% 41.65/6.34 % (1408984)Instructions burned: 685 (million)
% 41.65/6.34 % (1408996)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3153976683:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 41.65/6.34 % (1408997)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=788143015:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 41.65/6.34 % TRYING [5]
% 41.65/6.34 % (1408992)Instruction limit reached!
% 41.65/6.34 % (1408992)------------------------------
% 41.65/6.34 % (1408992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.65/6.34 % (1408992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.65/6.34 % (1408992)CaDiCaL version: 2.1.3
% 41.65/6.34 % (1408992)Termination reason: Instruction limit
% 41.65/6.34 % (1408992)Termination phase: Finite model building constraint generation
% 41.65/6.34 % (1408992)Time elapsed: 0.332 s
% 41.65/6.34 % (1408992)Peak memory usage: 21 MB
% 41.65/6.34 % (1408992)Instructions burned: 865 (million)
% 41.65/6.34 % (1409000)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=41265633:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 41.65/6.34 % (1408996)Instruction limit reached!
% 91.30/13.37 % (1408996)------------------------------
% 91.30/13.37 % (1408996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1408996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1408996)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1408996)Termination reason: Instruction limit
% 91.30/13.37 % (1408996)Termination phase: Finite model building constraint generation
% 91.30/13.37 % (1408996)Time elapsed: 0.410 s
% 91.30/13.37 % (1408996)Peak memory usage: 106 MB
% 91.30/13.37 % (1408996)Instructions burned: 889 (million)
% 91.30/13.37 % (1408997)Instruction limit reached!
% 91.30/13.37 % (1408997)------------------------------
% 91.30/13.37 % (1408997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1408997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1408997)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1408997)Termination reason: Instruction limit
% 91.30/13.37 % (1408997)Termination phase: Saturation
% 91.30/13.37 % (1408997)Time elapsed: 0.395 s
% 91.30/13.37 % (1408997)Peak memory usage: 23 MB
% 91.30/13.37 % (1408997)Instructions burned: 693 (million)
% 91.30/13.37 % TRYING [8]
% 91.30/13.37 % (1409002)fmb+10_1_sil=64000:random_seed=2463230944:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 91.30/13.37 % (1409003)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1157072203:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 91.30/13.37 % TRYING [1]
% 91.30/13.37 % TRYING [2]
% 91.30/13.37 % TRYING [20]
% 91.30/13.37 % TRYING [3]
% 91.30/13.37 % (1408994)Instruction limit reached!
% 91.30/13.37 % (1408994)------------------------------
% 91.30/13.37 % (1408994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1408994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1408994)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1408994)Termination reason: Instruction limit
% 91.30/13.37 % (1408994)Termination phase: Saturation
% 91.30/13.37 % (1408994)Time elapsed: 0.615 s
% 91.30/13.37 % (1408994)Peak memory usage: 29 MB
% 91.30/13.37 % (1408994)Instructions burned: 1179 (million)
% 91.30/13.37 % TRYING [4]
% 91.30/13.37 % (1409006)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1234139179:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 91.30/13.37 % TRYING [8]
% 91.30/13.37 % (1409000)Instruction limit reached!
% 91.30/13.37 % (1409000)------------------------------
% 91.30/13.37 % (1409000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1409000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1409000)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1409000)Termination reason: Instruction limit
% 91.30/13.37 % (1409000)Termination phase: Saturation
% 91.30/13.37 % (1409000)Time elapsed: 0.497 s
% 91.30/13.37 % (1409000)Peak memory usage: 20 MB
% 91.30/13.37 % (1409000)Instructions burned: 880 (million)
% 91.30/13.37 % (1409008)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1886157690:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 91.30/13.37 % TRYING [5]
% 91.30/13.37 % (1409006)Instruction limit reached!
% 91.30/13.37 % (1409006)------------------------------
% 91.30/13.37 % (1409006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1409006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1409006)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1409006)Termination reason: Instruction limit
% 91.30/13.37 % (1409006)Termination phase: Finite model building constraint generation
% 91.30/13.37 % (1409006)Time elapsed: 0.305 s
% 91.30/13.37 % (1409006)Peak memory usage: 64 MB
% 91.30/13.37 % (1409006)Instructions burned: 923 (million)
% 91.30/13.37 % (1409011)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1973787967:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 91.30/13.37 % (1409011)Instruction limit reached!
% 91.30/13.37 % (1409011)------------------------------
% 91.30/13.37 % (1409011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.30/13.37 % (1409011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.30/13.37 % (1409011)CaDiCaL version: 2.1.3
% 91.30/13.37 % (1409011)Termination reason: Instruction limit
% 91.30/13.37 % (1409011)Termination phase: Saturation
% 91.30/13.37 % (1409011)Time elapsed: 0.652 s
% 91.30/13.37 % (1409011)Peak memory usage: 17 MB
% 91.30/13.37 % (1409011)Instructions burned: 1473 (million)
% 91.30/13.37 % (1409013)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3693911102:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 223.09/31.91 % (1409013)Cannot represent all propositional literals internally
% 223.09/31.91 % (1409013)Refutation not found, incomplete strategy
% 223.09/31.91 % (1409013)------------------------------
% 223.09/31.91 % (1409013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409013)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409013)Termination reason: Refutation not found, incomplete strategy
% 223.09/31.91 % (1409013)Time elapsed: 0.009 s
% 223.09/31.91 % (1409013)Peak memory usage: 11 MB
% 223.09/31.91 % (1409013)Instructions burned: 17 (million)
% 223.09/31.91 % (1409013)------------------------------
% 223.09/31.91 % (1409013)------------------------------
% 223.09/31.91 % TRYING [6]
% 223.09/31.91 % (1409015)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2949490936:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 223.09/31.91 % TRYING [16]
% 223.09/31.91 % TRYING [9]
% 223.09/31.91 % (1409015)Instruction limit reached!
% 223.09/31.91 % (1409015)------------------------------
% 223.09/31.91 % (1409015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409015)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409015)Termination reason: Instruction limit
% 223.09/31.91 % (1409015)Termination phase: Finite model building constraint generation
% 223.09/31.91 % (1409015)Time elapsed: 0.767 s
% 223.09/31.91 % (1409015)Peak memory usage: 146 MB
% 223.09/31.91 % (1409015)Instructions burned: 2175 (million)
% 223.09/31.91 % (1409017)ott-2_1_sil=16000:newcnf=on:random_seed=1056114864:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi)
% 223.09/31.91 % (1409017)Instruction limit reached!
% 223.09/31.91 % (1409017)------------------------------
% 223.09/31.91 % (1409017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409017)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409017)Termination reason: Instruction limit
% 223.09/31.91 % (1409017)Termination phase: Saturation
% 223.09/31.91 % (1409017)Time elapsed: 0.434 s
% 223.09/31.91 % (1409017)Peak memory usage: 26 MB
% 223.09/31.91 % (1409017)Instructions burned: 870 (million)
% 223.09/31.91 % (1409019)ott+10_1_sil=32000:tgt=ground:random_seed=3612763497:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 223.09/31.91 % (1409008)Instruction limit reached!
% 223.09/31.91 % (1409008)------------------------------
% 223.09/31.91 % (1409008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409008)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409008)Termination reason: Instruction limit
% 223.09/31.91 % (1409008)Termination phase: Saturation
% 223.09/31.91 % (1409008)Time elapsed: 2.501 s
% 223.09/31.91 % (1409008)Peak memory usage: 58 MB
% 223.09/31.91 % (1409008)Instructions burned: 5131 (million)
% 223.09/31.91 % (1409021)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=704754004:i=54282_2963 on theBenchmark for (2963ds/54282Mi)
% 223.09/31.91 % TRYING [1]
% 223.09/31.91 % TRYING [2]
% 223.09/31.91 % TRYING [3]
% 223.09/31.91 % TRYING [4]
% 223.09/31.91 % TRYING [5]
% 223.09/31.91 % TRYING [6]
% 223.09/31.91 % (1409003)Instruction limit reached!
% 223.09/31.91 % (1409003)------------------------------
% 223.09/31.91 % (1409003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409003)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409003)Termination reason: Instruction limit
% 223.09/31.91 % (1409003)Termination phase: Finite model building constraint generation
% 223.09/31.91 % (1409003)Time elapsed: 3.096 s
% 223.09/31.91 % (1409003)Peak memory usage: 484 MB
% 223.09/31.91 % (1409003)Instructions burned: 9515 (million)
% 223.09/31.91 % (1409023)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2866816346:i=3512:aac=none_2958 on theBenchmark for (2958ds/3512Mi)
% 223.09/31.91 % TRYING [7]
% 223.09/31.91 % TRYING [7]
% 223.09/31.91 % TRYING [8]
% 223.09/31.91 % (1409023)Instruction limit reached!
% 223.09/31.91 % (1409023)------------------------------
% 223.09/31.91 % (1409023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.09/31.91 % (1409023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.09/31.91 % (1409023)CaDiCaL version: 2.1.3
% 223.09/31.91 % (1409023)Termination reason: Instruction limit
% 223.09/31.91 % (1409023)Termination phase: Saturation
% 223.09/31.91 % (1409023)Time elapsed: 1.787 s
% 216.37/36.07 % (1409023)Peak memory usage: 40 MB
% 216.37/36.07 % (1409023)Instructions burned: 3514 (million)
% 216.37/36.07 % (1409025)dis+21_1_sil=32000:sas=cadical:random_seed=2620009899:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 216.37/36.07 % (1409019)Instruction limit reached!
% 216.37/36.07 % (1409019)------------------------------
% 216.37/36.07 % (1409019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409019)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409019)Termination reason: Instruction limit
% 216.37/36.07 % (1409019)Termination phase: Saturation
% 216.37/36.07 % (1409019)Time elapsed: 2.791 s
% 216.37/36.07 % (1409019)Peak memory usage: 76 MB
% 216.37/36.07 % (1409019)Instructions burned: 5116 (million)
% 216.37/36.07 % (1409027)ott+11_1_sil=16000:gs=on:random_seed=2431994999:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2938 on theBenchmark for (2938ds/2251Mi)
% 216.37/36.07 % (1409027)Instruction limit reached!
% 216.37/36.07 % (1409027)------------------------------
% 216.37/36.07 % (1409027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409027)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409027)Termination reason: Instruction limit
% 216.37/36.07 % (1409027)Termination phase: Saturation
% 216.37/36.07 % (1409027)Time elapsed: 0.923 s
% 216.37/36.07 % (1409027)Peak memory usage: 17 MB
% 216.37/36.07 % (1409027)Instructions burned: 2251 (million)
% 216.37/36.07 % (1409029)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3686202166:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi)
% 216.37/36.07 % TRYING [7]
% 216.37/36.07 % (1409025)Instruction limit reached!
% 216.37/36.07 % (1409025)------------------------------
% 216.37/36.07 % (1409025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409025)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409025)Termination reason: Instruction limit
% 216.37/36.07 % (1409025)Termination phase: Saturation
% 216.37/36.07 % (1409025)Time elapsed: 2.085 s
% 216.37/36.07 % (1409025)Peak memory usage: 46 MB
% 216.37/36.07 % (1409025)Instructions burned: 3774 (million)
% 216.37/36.07 % (1409031)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1477162982:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2919 on theBenchmark for (2919ds/4591Mi)
% 216.37/36.07 % TRYING [9]
% 216.37/36.07 % (1409002)Instruction limit reached!
% 216.37/36.07 % (1409002)------------------------------
% 216.37/36.07 % (1409002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409002)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409002)Termination reason: Instruction limit
% 216.37/36.07 % (1409002)Termination phase: Finite model building SAT solving
% 216.37/36.07 % (1409002)Time elapsed: 8.053 s
% 216.37/36.07 % (1409002)Peak memory usage: 152 MB
% 216.37/36.07 % (1409002)Instructions burned: 22061 (million)
% 216.37/36.07 % (1409033)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3630812354:i=29340_2909 on theBenchmark for (2909ds/29340Mi)
% 216.37/36.07 % (1409031)Instruction limit reached!
% 216.37/36.07 % (1409031)------------------------------
% 216.37/36.07 % (1409031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409031)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409031)Termination reason: Instruction limit
% 216.37/36.07 % (1409031)Termination phase: Saturation
% 216.37/36.07 % (1409031)Time elapsed: 2.076 s
% 216.37/36.07 % (1409031)Peak memory usage: 60 MB
% 216.37/36.07 % (1409031)Instructions burned: 4593 (million)
% 216.37/36.07 % (1409035)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1728500157:i=5211_2898 on theBenchmark for (2898ds/5211Mi)
% 216.37/36.07 % TRYING [8]
% 216.37/36.07 % (1409035)Instruction limit reached!
% 216.37/36.07 % (1409035)------------------------------
% 216.37/36.07 % (1409035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409035)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409035)Termination reason: Instruction limit
% 216.37/36.07 % (1409035)Termination phase: Saturation
% 216.37/36.07 % (1409035)Time elapsed: 2.773 s
% 216.37/36.07 % (1409035)Peak memory usage: 60 MB
% 216.37/36.07 % (1409035)Instructions burned: 5212 (million)
% 216.37/36.07 % (1409037)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=372614627:i=5497:nm=2_2870 on theBenchmark for (2870ds/5497Mi)
% 216.37/36.07 % TRYING [17]
% 216.37/36.07 % (1409037)Instruction limit reached!
% 216.37/36.07 % (1409037)------------------------------
% 216.37/36.07 % (1409037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409037)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409037)Termination reason: Instruction limit
% 216.37/36.07 % (1409037)Termination phase: Finite model building constraint generation
% 216.37/36.07 % (1409037)Time elapsed: 1.840 s
% 216.37/36.07 % (1409037)Peak memory usage: 309 MB
% 216.37/36.07 % (1409037)Instructions burned: 5498 (million)
% 216.37/36.07 % (1409039)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2556508654:fmbsr=2:i=46332_2851 on theBenchmark for (2851ds/46332Mi)
% 216.37/36.07 % TRYING [15]
% 216.37/36.07 % TRYING [9]
% 216.37/36.07 % (1409033)Instruction limit reached!
% 216.37/36.07 % (1409033)------------------------------
% 216.37/36.07 % (1409033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409033)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409033)Termination reason: Instruction limit
% 216.37/36.07 % (1409033)Termination phase: Saturation
% 216.37/36.07 % (1409033)Time elapsed: 14.013 s
% 216.37/36.07 % (1409033)Peak memory usage: 378 MB
% 216.37/36.07 % (1409033)Instructions burned: 29341 (million)
% 216.37/36.07 % (1409041)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=334319093:i=14071_2768 on theBenchmark for (2768ds/14071Mi)
% 216.37/36.07 % TRYING [12]
% 216.37/36.07 % TRYING [10]
% 216.37/36.07 % (1409021)Instruction limit reached!
% 216.37/36.07 % (1409021)------------------------------
% 216.37/36.07 % (1409021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409021)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409021)Termination reason: Instruction limit
% 216.37/36.07 % (1409021)Termination phase: Finite model building SAT solving
% 216.37/36.07 % (1409021)Time elapsed: 23.797 s
% 216.37/36.07 % (1409021)Peak memory usage: 826 MB
% 216.37/36.07 % (1409021)Instructions burned: 54282 (million)
% 216.37/36.07 % (1409043)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2657359716:i=22565:add=on:rawr=on_2724 on theBenchmark for (2724ds/22565Mi)
% 216.37/36.07 % (1409041)Instruction limit reached!
% 216.37/36.07 % (1409041)------------------------------
% 216.37/36.07 % (1409041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409041)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409041)Termination reason: Instruction limit
% 216.37/36.07 % (1409041)Termination phase: Finite model building constraint generation
% 216.37/36.07 % (1409041)Time elapsed: 4.990 s
% 216.37/36.07 % (1409041)Peak memory usage: 967 MB
% 216.37/36.07 % (1409041)Instructions burned: 14074 (million)
% 216.37/36.07 % (1409045)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1555787104:i=8173:av=off_2717 on theBenchmark for (2717ds/8173Mi)
% 216.37/36.07 % (1409045)Instruction limit reached!
% 216.37/36.07 % (1409045)------------------------------
% 216.37/36.07 % (1409045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409045)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409045)Termination reason: Instruction limit
% 216.37/36.07 % (1409045)Termination phase: Saturation
% 216.37/36.07 % (1409045)Time elapsed: 2.999 s
% 216.37/36.07 % (1409045)Peak memory usage: 52 MB
% 216.37/36.07 % (1409045)Instructions burned: 8174 (million)
% 216.37/36.07 % (1409047)dis+10_16:1_sil=16000:random_seed=1313421208:i=9155:fsr=off_2687 on theBenchmark for (2687ds/9155Mi)
% 216.37/36.07 % (1409039)Instruction limit reached!
% 216.37/36.07 % (1409039)------------------------------
% 216.37/36.07 % (1409039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409039)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409039)Termination reason: Instruction limit
% 216.37/36.07 % (1409039)Termination phase: Finite model building constraint generation
% 216.37/36.07 % (1409039)Time elapsed: 16.612 s
% 216.37/36.07 % (1409039)Peak memory usage: 3046 MB
% 216.37/36.07 % (1409039)Instructions burned: 46332 (million)
% 216.37/36.07 % (1409049)ott-3_8_sil=64000:random_seed=455366172:i=20139:bs=on_2680 on theBenchmark for (2680ds/20139Mi)
% 216.37/36.07 % (1409029)Instruction limit reached!
% 216.37/36.07 % (1409029)------------------------------
% 216.37/36.07 % (1409029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.07 % (1409029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.07 % (1409029)CaDiCaL version: 2.1.3
% 216.37/36.07 % (1409029)Termination reason: Instruction limit
% 216.37/36.07 % (1409029)Termination phase: Finite model building SAT solving
% 216.37/36.07 % (1409029)Time elapsed: 26.411 s
% 216.37/36.07 % (1409029)Peak memory usage: 468 MB
% 216.37/36.07 % (1409029)Instructions burned: 67535 (million)
% 216.37/36.07 % (1409051)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=451042983:fmbsr=2:i=32576_2663 on theBenchmark for (2663ds/32576Mi)
% 216.37/36.07 % TRYING [9]
% 216.37/36.07 % (1408969) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1408963-1408969"...
% 216.37/36.07 % (1408969)...printing done.
% 216.37/36.07 % (1408969)Refutation found. Thanks to Tanya!
% 216.37/36.07 % SZS status Theorem for theBenchmark
% 216.37/36.07 % SZS output start Proof for theBenchmark
% See solution above
% 216.37/36.08 % (1408969)------------------------------
% 216.37/36.08 % (1408969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.37/36.08 % (1408969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.37/36.08 % (1408969)CaDiCaL version: 2.1.3
% 216.37/36.08 % (1408969)Termination reason: Refutation
% 216.37/36.08 % (1408969)Time elapsed: 35.410 s
% 216.37/36.08 % (1408969)Peak memory usage: 478 MB
% 216.37/36.08 % (1408969)Instructions burned: 65614 (million)
% 216.37/36.08 % (1408963)Success in time 35.648 s
% 216.37/36.08 % Vampire exiting
%------------------------------------------------------------------------------