%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM509+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:15:31 PM UTC 2026
% Result : Theorem 13.92s 2.84s
% Output : Refutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 49
% Syntax : Number of formulae : 400 ( 78 unt; 24 def)
% Number of atoms : 1586 ( 422 equ)
% Maximal formula atoms : 22 ( 3 avg)
% Number of connectives : 1946 ( 760 ~; 823 |; 294 &)
% ( 26 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 21 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 15 con; 0-2 aty)
% Number of variables : 350 ( 0 sgn 286 !; 64 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f9,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
fof(f15,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 != sz00
=> ! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtasdt0(X0,X1) = sdtasdt0(X0,X2)
| sdtasdt0(X1,X0) = sdtasdt0(X2,X0) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulCanc) ).
fof(f21,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEAsym) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETran) ).
fof(f24,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != X1
& sdtlseqdt0(X0,X1) )
=> ! [X2] :
( aNaturalNumber0(X2)
=> ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonAdd) ).
fof(f27,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( X0 != sz00
=> sdtlseqdt0(X1,sdtasdt0(X1,X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonMul2) ).
fof(f29,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != X1
& sdtlseqdt0(X0,X1) )
=> iLess0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH_03) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
fof(f35,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( doDivides0(X0,X1)
& X1 != sz00 )
=> sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDivLE) ).
fof(f36,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( aNaturalNumber0(X2)
=> sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDivAsso) ).
fof(f39,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(f40,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( ( ( X2 != sz00
& X2 != sz10
& ! [X3] :
( ( aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) )
=> ( X3 = sz10
| X3 = X2 ) ) )
| isPrime0(X2) )
& ( ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X0,X1) = sdtasdt0(X2,X3) )
| doDivides0(X2,sdtasdt0(X0,X1)) ) )
=> ( iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
=> ( ( ? [X3] :
( aNaturalNumber0(X3)
& X0 = sdtasdt0(X2,X3) )
& doDivides0(X2,X0) )
| ( ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1799) ).
fof(f41,axiom,
( xp != sz00
& xp != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtasdt0(X0,X1) )
| doDivides0(X0,xp) ) )
=> ( X0 = sz10
| X0 = xp ) )
& isPrime0(xp)
& ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X0) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1860) ).
fof(f44,axiom,
( xn != xp
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xn,X0) = xp )
& sdtlseqdt0(xn,xp)
& xm != xp
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xm,X0) = xp )
& sdtlseqdt0(xm,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2287) ).
fof(f45,axiom,
( aNaturalNumber0(xk)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2306) ).
fof(f48,axiom,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xr = sdtasdt0(X0,X1) )
| doDivides0(X0,xr) ) )
=> ( X0 = sz10
| X0 = xr ) )
& isPrime0(xr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2342) ).
fof(f49,axiom,
( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xr,X0) = xk )
& ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xn,xm) = sdtasdt0(xr,X0) )
& doDivides0(xr,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2362) ).
fof(f52,conjecture,
( ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) )
=> ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
| doDivides0(xp,xn)
| ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
| doDivides0(xp,xm) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f53,negated_conjecture,
~ ( ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) )
=> ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
| doDivides0(xp,xn)
| ? [X0] :
( aNaturalNumber0(X0)
& xm = sdtasdt0(xp,X0) )
| doDivides0(xp,xm) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( ( ( X2 != sz00
& X2 != sz10
& ! [X3] :
( ( aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) )
=> ( X3 = sz10
| X3 = X2 ) ) )
| isPrime0(X2) )
& ( ? [X5] :
( aNaturalNumber0(X5)
& sdtasdt0(X0,X1) = sdtasdt0(X2,X5) )
| doDivides0(X2,sdtasdt0(X0,X1)) ) )
=> ( iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
=> ( ( ? [X6] :
( aNaturalNumber0(X6)
& sdtasdt0(X2,X6) = X0 )
& doDivides0(X2,X0) )
| ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X2,X7) = X1 )
& doDivides0(X2,X1) ) ) ) ) ),
inference(rectify,[],[f40]) ).
fof(f57,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtasdt0(X0,X1) )
| doDivides0(X0,xp) ) )
=> ( X0 = sz10
| X0 = xp ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(rectify,[],[f41]) ).
fof(f58,plain,
( xn != xp
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xn,X0) = xp )
& sdtlseqdt0(xn,xp)
& xm != xp
& ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtpldt0(xm,X1) )
& sdtlseqdt0(xm,xp) ),
inference(rectify,[],[f44]) ).
fof(f59,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& ( ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(X1,X2) = xr )
| doDivides0(X1,xr) ) )
=> ( sz10 = X1
| xr = X1 ) )
& isPrime0(xr) ),
inference(rectify,[],[f48]) ).
fof(f60,plain,
( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xr,X0) = xk )
& ? [X1] :
( aNaturalNumber0(X1)
& sdtasdt0(xn,xm) = sdtasdt0(xr,X1) )
& doDivides0(xr,sdtasdt0(xn,xm)) ),
inference(rectify,[],[f49]) ).
fof(f62,plain,
~ ( ( ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) )
=> ( ? [X1] :
( aNaturalNumber0(X1)
& xn = sdtasdt0(xp,X1) )
| doDivides0(xp,xn)
| ? [X2] :
( aNaturalNumber0(X2)
& xm = sdtasdt0(xp,X2) )
| doDivides0(xp,xm) ) ),
inference(rectify,[],[f53]) ).
fof(f63,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f64,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f63]) ).
fof(f65,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f66,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f65]) ).
fof(f72,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f73,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f72]) ).
fof(f76,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f77,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f82,plain,
! [X0] :
( ! [X1,X2] :
( X1 = X2
| ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f83,plain,
! [X0] :
( ! [X1,X2] :
( X1 = X2
| ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0) )
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(flattening,[],[f82]) ).
fof(f93,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f94,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f93]) ).
fof(f95,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f96,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f95]) ).
fof(f99,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2) )
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f100,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2) )
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f99]) ).
fof(f105,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f106,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f105]) ).
fof(f107,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f108,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f107]) ).
fof(f109,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f110,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f109]) ).
fof(f111,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f31]) ).
fof(f112,plain,
! [X0,X1] :
( ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f111]) ).
fof(f119,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f120,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f119]) ).
fof(f121,plain,
! [X0,X1] :
( ! [X2] :
( sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f36]) ).
fof(f122,plain,
! [X0,X1] :
( ! [X2] :
( sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0)
| ~ aNaturalNumber0(X2) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f121]) ).
fof(f127,plain,
! [X0,X1,X2] :
( ( ? [X6] :
( aNaturalNumber0(X6)
& sdtasdt0(X2,X6) = X0 )
& doDivides0(X2,X0) )
| ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X2,X7) = X1 )
& doDivides0(X2,X1) )
| ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| ( ( sz00 = X2
| sz10 = X2
| ? [X3] :
( sz10 != X3
& X2 != X3
& aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) ) )
& ~ isPrime0(X2) )
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| sdtasdt0(X0,X1) != sdtasdt0(X2,X5) )
& ~ doDivides0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f56]) ).
fof(f128,plain,
! [X0,X1,X2] :
( ( ? [X6] :
( aNaturalNumber0(X6)
& sdtasdt0(X2,X6) = X0 )
& doDivides0(X2,X0) )
| ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X2,X7) = X1 )
& doDivides0(X2,X1) )
| ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| ( ( sz00 = X2
| sz10 = X2
| ? [X3] :
( sz10 != X3
& X2 != X3
& aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) ) )
& ~ isPrime0(X2) )
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| sdtasdt0(X0,X1) != sdtasdt0(X2,X5) )
& ~ doDivides0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f127]) ).
fof(f129,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(ennf_transformation,[],[f57]) ).
fof(f130,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(xn,xm) = sdtasdt0(xp,X2) )
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(flattening,[],[f129]) ).
fof(f134,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( sz10 = X1
| xr = X1
| ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != xr )
& ~ doDivides0(X1,xr) ) )
& isPrime0(xr) ),
inference(ennf_transformation,[],[f59]) ).
fof(f135,plain,
( aNaturalNumber0(xr)
& ? [X0] :
( aNaturalNumber0(X0)
& xk = sdtasdt0(xr,X0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( sz10 = X1
| xr = X1
| ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != xr )
& ~ doDivides0(X1,xr) ) )
& isPrime0(xr) ),
inference(flattening,[],[f134]) ).
fof(f136,plain,
( ! [X1] :
( ~ aNaturalNumber0(X1)
| xn != sdtasdt0(xp,X1) )
& ~ doDivides0(xp,xn)
& ! [X2] :
( ~ aNaturalNumber0(X2)
| xm != sdtasdt0(xp,X2) )
& ~ doDivides0(xp,xm)
& ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) ),
inference(ennf_transformation,[],[f62]) ).
fof(f137,plain,
( ! [X1] :
( ~ aNaturalNumber0(X1)
| xn != sdtasdt0(xp,X1) )
& ~ doDivides0(xp,xn)
& ! [X2] :
( ~ aNaturalNumber0(X2)
| xm != sdtasdt0(xp,X2) )
& ~ doDivides0(xp,xm)
& ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xr,X0) )
& doDivides0(xr,xn) ),
inference(flattening,[],[f136]) ).
fof(f138,definition,
! [X2] :
( ( ( sz00 = X2
| sz10 = X2
| ? [X3] :
( sz10 != X3
& X2 != X3
& aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) ) )
& ~ isPrime0(X2) )
| ~ sP0(X2) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f139,definition,
! [X1,X2] :
( ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X2,X7) = X1 )
& doDivides0(X2,X1) )
| ~ sP1(X1,X2) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f140,plain,
! [X0,X1,X2] :
( ( ? [X6] :
( aNaturalNumber0(X6)
& sdtasdt0(X2,X6) = X0 )
& doDivides0(X2,X0) )
| sP1(X1,X2)
| ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| sP0(X2)
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| sdtasdt0(X0,X1) != sdtasdt0(X2,X5) )
& ~ doDivides0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(definition_folding,[],[f128,f139,f138]) ).
fof(f148,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(nnf_transformation,[],[f110]) ).
fof(f149,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X0,X3) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(rectify,[],[f148]) ).
fof(f150,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ( aNaturalNumber0(sK4(X0,X1))
& sdtasdt0(X0,sK4(X0,X1)) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X3,sK4(X0,X1))],[f149]) ).
fof(f151,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = sdtsldt0(X1,X0)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 )
& ( ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| sdtsldt0(X1,X0) != X2 ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(nnf_transformation,[],[f112]) ).
fof(f152,plain,
! [X0,X1] :
( ! [X2] :
( ( X2 = sdtsldt0(X1,X0)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 )
& ( ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) )
| sdtsldt0(X1,X0) != X2 ) )
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f151]) ).
fof(f158,plain,
! [X1,X2] :
( ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X2,X7) = X1 )
& doDivides0(X2,X1) )
| ~ sP1(X1,X2) ),
inference(nnf_transformation,[],[f139]) ).
fof(f159,plain,
! [X0,X1] :
( ( ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(X1,X2) = X0 )
& doDivides0(X1,X0) )
| ~ sP1(X0,X1) ),
inference(rectify,[],[f158]) ).
fof(f160,plain,
! [X0,X1] :
( ( aNaturalNumber0(sK7(X0,X1))
& sdtasdt0(X1,sK7(X0,X1)) = X0
& doDivides0(X1,X0) )
| ~ sP1(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f159]) ).
fof(f161,plain,
! [X2] :
( ( ( sz00 = X2
| sz10 = X2
| ? [X3] :
( sz10 != X3
& X2 != X3
& aNaturalNumber0(X3)
& ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
& doDivides0(X3,X2) ) )
& ~ isPrime0(X2) )
| ~ sP0(X2) ),
inference(nnf_transformation,[],[f138]) ).
fof(f162,plain,
! [X0] :
( ( ( sz00 = X0
| sz10 = X0
| ? [X1] :
( sz10 != X1
& X0 != X1
& aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& sdtasdt0(X1,X2) = X0 )
& doDivides0(X1,X0) ) )
& ~ isPrime0(X0) )
| ~ sP0(X0) ),
inference(rectify,[],[f161]) ).
fof(f163,plain,
! [X0] :
( ( ( sz00 = X0
| sz10 = X0
| ( sz10 != sK8(X0)
& sK8(X0) != X0
& aNaturalNumber0(sK8(X0))
& aNaturalNumber0(sK9(X0))
& sdtasdt0(sK8(X0),sK9(X0)) = X0
& doDivides0(sK8(X0),X0) ) )
& ~ isPrime0(X0) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0))],[f162]) ).
fof(f164,plain,
! [X0,X1,X2] :
( ( ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X2,X3) = X0 )
& doDivides0(X2,X0) )
| sP1(X1,X2)
| ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| sP0(X2)
| ( ! [X4] :
( ~ aNaturalNumber0(X4)
| sdtasdt0(X0,X1) != sdtasdt0(X2,X4) )
& ~ doDivides0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(rectify,[],[f140]) ).
fof(f165,plain,
! [X0,X1,X2] :
( ( aNaturalNumber0(sK10(X0,X2))
& sdtasdt0(X2,sK10(X0,X2)) = X0
& doDivides0(X2,X0) )
| sP1(X1,X2)
| ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| sP0(X2)
| ( ! [X4] :
( ~ aNaturalNumber0(X4)
| sdtasdt0(X0,X1) != sdtasdt0(X2,X4) )
& ~ doDivides0(X2,sdtasdt0(X0,X1)) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(X3,sK10(X0,X2))],[f164]) ).
fof(f166,plain,
( xp != sz00
& xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp)
& aNaturalNumber0(sK11)
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK11)
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X2,sK11)],[f130]) ).
fof(f167,plain,
( xn != xp
& aNaturalNumber0(sK12)
& xp = sdtpldt0(xn,sK12)
& sdtlseqdt0(xn,xp)
& xm != xp
& aNaturalNumber0(sK13)
& xp = sdtpldt0(xm,sK13)
& sdtlseqdt0(xm,xp) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12,sK13]),skolemize(X0,sK12),skolemize(X1,sK13)],[f58]) ).
fof(f168,plain,
( aNaturalNumber0(xr)
& aNaturalNumber0(sK14)
& xk = sdtasdt0(xr,sK14)
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [X1] :
( sz10 = X1
| xr = X1
| ~ aNaturalNumber0(X1)
| ( ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X1,X2) != xr )
& ~ doDivides0(X1,xr) ) )
& isPrime0(xr) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X0,sK14)],[f135]) ).
fof(f169,plain,
( aNaturalNumber0(sK15)
& xk = sdtpldt0(xr,sK15)
& aNaturalNumber0(sK16)
& sdtasdt0(xn,xm) = sdtasdt0(xr,sK16)
& doDivides0(xr,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X0,sK15),skolemize(X1,sK16)],[f60]) ).
fof(f175,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtasdt0(xp,X0) )
& ~ doDivides0(xp,xn)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| xm != sdtasdt0(xp,X1) )
& ~ doDivides0(xp,xm)
& ? [X2] :
( aNaturalNumber0(X2)
& xn = sdtasdt0(xr,X2) )
& doDivides0(xr,xn) ),
inference(rectify,[],[f137]) ).
fof(f176,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtasdt0(xp,X0) )
& ~ doDivides0(xp,xn)
& ! [X1] :
( ~ aNaturalNumber0(X1)
| xm != sdtasdt0(xp,X1) )
& ~ doDivides0(xp,xm)
& aNaturalNumber0(sK20)
& xn = sdtasdt0(xr,sK20)
& doDivides0(xr,xn) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X2,sK20)],[f175]) ).
fof(f177,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f179,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f180,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f64]) ).
fof(f181,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f66]) ).
fof(f186,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f189,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f76]) ).
fof(f191,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f77]) ).
fof(f197,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f208,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f209,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f96]) ).
fof(f212,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X2)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f213,plain,
! [X2,X0,X1] :
( sdtpldt0(X1,X2) != sdtpldt0(X0,X2)
| ~ aNaturalNumber0(X2)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f100]) ).
fof(f222,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f223,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| X0 = X1
| iLess0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f108]) ).
fof(f226,plain,
! [X2,X0,X1] :
( doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f150]) ).
fof(f228,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X2)
| sdtsldt0(X1,X0) != X2
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f229,plain,
! [X2,X0,X1] :
( sdtsldt0(X1,X0) = X2
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f152]) ).
fof(f233,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| sdtlseqdt0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f120]) ).
fof(f234,plain,
! [X2,X0,X1] :
( ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| sz00 = X0
| sdtasdt0(X2,sdtsldt0(X1,X0)) = sdtsldt0(sdtasdt0(X2,X1),X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f122]) ).
fof(f245,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f39]) ).
fof(f246,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f39]) ).
fof(f247,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f39]) ).
fof(f248,plain,
! [X0,X1] :
( ~ sP1(X0,X1)
| doDivides0(X1,X0) ),
inference(cnf_transformation,[],[f160]) ).
fof(f251,plain,
! [X0] :
( ~ sP0(X0)
| ~ isPrime0(X0) ),
inference(cnf_transformation,[],[f163]) ).
fof(f258,plain,
! [X2,X0,X1] :
( ~ iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp))
| sP1(X1,X2)
| doDivides0(X2,X0)
| sP0(X2)
| ~ doDivides0(X2,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f165]) ).
fof(f267,plain,
isPrime0(xp),
inference(cnf_transformation,[],[f166]) ).
fof(f280,plain,
sdtlseqdt0(xn,xp),
inference(cnf_transformation,[],[f167]) ).
fof(f285,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(cnf_transformation,[],[f45]) ).
fof(f286,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[],[f45]) ).
fof(f294,plain,
sz10 != xr,
inference(cnf_transformation,[],[f168]) ).
fof(f295,plain,
sz00 != xr,
inference(cnf_transformation,[],[f168]) ).
fof(f296,plain,
doDivides0(xr,xk),
inference(cnf_transformation,[],[f168]) ).
fof(f299,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[],[f168]) ).
fof(f300,plain,
doDivides0(xr,sdtasdt0(xn,xm)),
inference(cnf_transformation,[],[f169]) ).
fof(f301,plain,
sdtasdt0(xn,xm) = sdtasdt0(xr,sK16),
inference(cnf_transformation,[],[f169]) ).
fof(f302,plain,
aNaturalNumber0(sK16),
inference(cnf_transformation,[],[f169]) ).
fof(f315,plain,
doDivides0(xr,xn),
inference(cnf_transformation,[],[f176]) ).
fof(f316,plain,
xn = sdtasdt0(xr,sK20),
inference(cnf_transformation,[],[f176]) ).
fof(f317,plain,
aNaturalNumber0(sK20),
inference(cnf_transformation,[],[f176]) ).
fof(f318,plain,
~ doDivides0(xp,xm),
inference(cnf_transformation,[],[f176]) ).
fof(f320,plain,
~ doDivides0(xp,xn),
inference(cnf_transformation,[],[f176]) ).
fof(f321,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtasdt0(xp,X0) ),
inference(cnf_transformation,[],[f176]) ).
fof(f328,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f226]) ).
fof(f329,plain,
! [X2,X0] :
( ~ doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| sz00 = X0
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f229]) ).
fof(f330,plain,
! [X0,X1] :
( aNaturalNumber0(sdtsldt0(X1,X0))
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(equality_resolution,[],[f228]) ).
fof(f334,definition,
! [X0] : sF21(X0) = sdtasdt0(xp,X0),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f335,plain,
! [X0] : sdtasdt0(xp,X0) = sF21(X0),
inference(reorient_equations,[],[f334]) ).
fof(f336,plain,
! [X0] :
( xn != sF21(X0)
| ~ aNaturalNumber0(X0) ),
inference(definition_folding,[],[f321,f335]) ).
fof(f338,definition,
sF22 = sdtasdt0(xr,sK20),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f339,plain,
sdtasdt0(xr,sK20) = sF22,
inference(reorient_equations,[],[f338]) ).
fof(f340,plain,
xn = sF22,
inference(definition_folding,[],[f316,f339]) ).
fof(f374,definition,
( spl23_7
<=> aNaturalNumber0(sz10) ),
introduced(definition,[new_symbols(definition,[spl23_7])],[avatar_definition]) ).
fof(f375,plain,
( aNaturalNumber0(sz10)
| ~ spl23_7 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f383,definition,
( spl23_9
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[spl23_9])],[avatar_definition]) ).
fof(f384,plain,
( aNaturalNumber0(sz00)
| ~ spl23_9 ),
inference(avatar_component_clause,[],[f383]) ).
fof(f391,plain,
spl23_7,
inference(avatar_split_clause,[],[f179,f374]) ).
fof(f392,plain,
spl23_9,
inference(avatar_split_clause,[],[f177,f383]) ).
fof(f393,plain,
xn = sdtasdt0(xr,sK20),
inference(forward_demodulation,[],[f339,f340]) ).
fof(f398,plain,
! [X0] :
( doDivides0(xp,sF21(X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sF21(X0)) ),
inference(superposition,[],[f328,f335]) ).
fof(f399,plain,
! [X0] :
( doDivides0(xp,sF21(X0))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sF21(X0)) ),
inference(forward_subsumption_resolution,[],[f398,f245]) ).
fof(f405,plain,
( aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sK16) ),
inference(superposition,[],[f181,f301]) ).
fof(f407,plain,
( aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(sK16) ),
inference(forward_subsumption_resolution,[],[f405,f299]) ).
fof(f408,plain,
aNaturalNumber0(sdtasdt0(xn,xm)),
inference(forward_subsumption_resolution,[],[f407,f302]) ).
fof(f409,plain,
aNaturalNumber0(sdtasdt0(xp,xk)),
inference(forward_demodulation,[],[f408,f285]) ).
fof(f410,plain,
aNaturalNumber0(sF21(xk)),
inference(forward_demodulation,[],[f409,f335]) ).
fof(f431,plain,
( ~ doDivides0(xr,xn)
| ~ aNaturalNumber0(sK20)
| sz00 = xr
| sK20 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[],[f329,f393]) ).
fof(f433,plain,
( ~ doDivides0(xr,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(sK16)
| sz00 = xr
| sK16 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(superposition,[],[f329,f301]) ).
fof(f439,plain,
( ~ aNaturalNumber0(sK16)
| sz00 = xr
| sK16 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f433,f300]) ).
fof(f441,plain,
( ~ aNaturalNumber0(sK20)
| sz00 = xr
| sK20 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f431,f315]) ).
fof(f445,plain,
( sz00 = xr
| sK16 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f439,f302]) ).
fof(f447,plain,
( sz00 = xr
| sK20 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f441,f317]) ).
fof(f450,plain,
( sK16 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f445,f295]) ).
fof(f452,plain,
( sK20 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f447,f295]) ).
fof(f455,plain,
( sK16 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f450,f299]) ).
fof(f457,plain,
( sK20 = sdtsldt0(xn,xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f452,f299]) ).
fof(f459,plain,
( sK16 = sdtsldt0(sdtasdt0(xp,xk),xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_demodulation,[],[f455,f285]) ).
fof(f461,plain,
sK20 = sdtsldt0(xn,xr),
inference(forward_subsumption_resolution,[],[f457,f247]) ).
fof(f463,plain,
( sK16 = sdtsldt0(sF21(xk),xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_demodulation,[],[f459,f335]) ).
fof(f466,plain,
( ~ aNaturalNumber0(sdtasdt0(xp,xk))
| sK16 = sdtsldt0(sF21(xk),xr) ),
inference(forward_demodulation,[],[f463,f285]) ).
fof(f468,definition,
( spl23_11
<=> sz00 = xn ),
introduced(definition,[new_symbols(definition,[spl23_11])],[avatar_definition]) ).
fof(f469,plain,
( sz00 != xn
| spl23_11 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( sz00 = xn
| ~ spl23_11 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f476,plain,
( ~ aNaturalNumber0(sF21(xk))
| sK16 = sdtsldt0(sF21(xk),xr) ),
inference(forward_demodulation,[],[f466,f335]) ).
fof(f477,plain,
sK16 = sdtsldt0(sF21(xk),xr),
inference(forward_subsumption_resolution,[],[f476,f410]) ).
fof(f506,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xn) = sdtasdt0(xn,X0) ),
inference(resolution,[],[f186,f247]) ).
fof(f507,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xm) = sdtasdt0(xm,X0) ),
inference(resolution,[],[f186,f246]) ).
fof(f510,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(xr,X0) = sdtasdt0(X0,xr) ),
inference(resolution,[],[f186,f299]) ).
fof(f728,definition,
( spl23_13
<=> sP0(xp) ),
introduced(definition,[new_symbols(definition,[spl23_13])],[avatar_definition]) ).
fof(f729,plain,
( ~ sP0(xp)
| spl23_13 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f730,plain,
( sP0(xp)
| ~ spl23_13 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f868,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = xr
| sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtsldt0(sdtasdt0(X0,xn),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(resolution,[],[f234,f315]) ).
fof(f869,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = xr
| sdtasdt0(X0,sdtsldt0(xk,xr)) = sdtsldt0(sdtasdt0(X0,xk),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk) ),
inference(resolution,[],[f234,f296]) ).
fof(f878,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xk,xr)) = sdtsldt0(sdtasdt0(X0,xk),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk) ),
inference(forward_subsumption_resolution,[],[f869,f295]) ).
fof(f879,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtsldt0(sdtasdt0(X0,xn),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f868,f295]) ).
fof(f890,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xk,xr)) = sdtsldt0(sdtasdt0(X0,xk),xr)
| ~ aNaturalNumber0(xk) ),
inference(forward_subsumption_resolution,[],[f878,f299]) ).
fof(f891,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtsldt0(sdtasdt0(X0,xn),xr)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f879,f299]) ).
fof(f897,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xk,xr)) = sdtsldt0(sdtasdt0(X0,xk),xr) ),
inference(forward_subsumption_resolution,[],[f890,f286]) ).
fof(f898,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtsldt0(sdtasdt0(X0,xn),xr) ),
inference(forward_subsumption_resolution,[],[f891,f247]) ).
fof(f913,plain,
sdtsldt0(sdtasdt0(xp,xk),xr) = sdtasdt0(xp,sdtsldt0(xk,xr)),
inference(resolution,[],[f897,f245]) ).
fof(f924,plain,
sdtsldt0(sdtasdt0(xp,xk),xr) = sF21(sdtsldt0(xk,xr)),
inference(forward_demodulation,[],[f913,f335]) ).
fof(f928,plain,
sdtsldt0(sF21(xk),xr) = sF21(sdtsldt0(xk,xr)),
inference(forward_demodulation,[],[f924,f335]) ).
fof(f929,plain,
sK16 = sF21(sdtsldt0(xk,xr)),
inference(forward_demodulation,[],[f928,f477]) ).
fof(f931,plain,
( doDivides0(xp,sK16)
| ~ aNaturalNumber0(sdtsldt0(xk,xr))
| ~ aNaturalNumber0(sK16) ),
inference(superposition,[],[f399,f929]) ).
fof(f935,definition,
( spl23_25
<=> aNaturalNumber0(sdtsldt0(xk,xr)) ),
introduced(definition,[new_symbols(definition,[spl23_25])],[avatar_definition]) ).
fof(f937,plain,
( ~ aNaturalNumber0(sdtsldt0(xk,xr))
| spl23_25 ),
inference(avatar_component_clause,[],[f935]) ).
fof(f948,plain,
( doDivides0(xp,sK16)
| ~ aNaturalNumber0(sdtsldt0(xk,xr)) ),
inference(forward_subsumption_resolution,[],[f931,f302]) ).
fof(f950,definition,
( spl23_28
<=> doDivides0(xp,sK16) ),
introduced(definition,[new_symbols(definition,[spl23_28])],[avatar_definition]) ).
fof(f952,plain,
( doDivides0(xp,sK16)
| ~ spl23_28 ),
inference(avatar_component_clause,[],[f950]) ).
fof(f953,plain,
( ~ spl23_25
| spl23_28 ),
inference(avatar_split_clause,[],[f948,f950,f935]) ).
fof(f989,plain,
( sz00 = xr
| ~ doDivides0(xr,xk)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| spl23_25 ),
inference(resolution,[],[f330,f937]) ).
fof(f1005,plain,
( ~ doDivides0(xr,xk)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| spl23_25 ),
inference(forward_subsumption_resolution,[],[f989,f295]) ).
fof(f1007,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| spl23_25 ),
inference(forward_subsumption_resolution,[],[f1005,f296]) ).
fof(f1021,plain,
( ~ aNaturalNumber0(xk)
| spl23_25 ),
inference(forward_subsumption_resolution,[],[f1007,f299]) ).
fof(f1022,plain,
( $false
| spl23_25 ),
inference(forward_subsumption_resolution,[],[f1021,f286]) ).
fof(f1023,plain,
spl23_25,
inference(avatar_contradiction_clause,[],[f1022]) ).
fof(f1192,definition,
( spl23_43
<=> sz00 = sF21(xk) ),
introduced(definition,[new_symbols(definition,[spl23_43])],[avatar_definition]) ).
fof(f1193,plain,
( sz00 != sF21(xk)
| spl23_43 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1194,plain,
( sz00 = sF21(xk)
| ~ spl23_43 ),
inference(avatar_component_clause,[],[f1192]) ).
fof(f1355,plain,
sdtasdt0(xr,sK20) = sdtasdt0(sK20,xr),
inference(resolution,[],[f510,f317]) ).
fof(f1482,definition,
( spl23_59
<=> sz00 = sK16 ),
introduced(definition,[new_symbols(definition,[spl23_59])],[avatar_definition]) ).
fof(f1483,plain,
( sz00 != sK16
| spl23_59 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1484,plain,
( sz00 = sK16
| ~ spl23_59 ),
inference(avatar_component_clause,[],[f1482]) ).
fof(f1585,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X2,X1)
| iLess0(sdtpldt0(X0,X1),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X1)
| X0 = X2
| ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2) ),
inference(resolution,[],[f223,f212]) ).
fof(f1595,plain,
! [X2,X0,X1] :
( iLess0(sdtpldt0(X0,X1),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X1)
| X0 = X2
| ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2) ),
inference(forward_subsumption_resolution,[],[f1585,f213]) ).
fof(f1601,plain,
! [X2,X0,X1] :
( iLess0(sdtpldt0(X0,X1),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X1)
| X0 = X2
| ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2) ),
inference(forward_subsumption_resolution,[],[f1595,f180]) ).
fof(f1606,plain,
! [X2,X0,X1] :
( iLess0(sdtpldt0(X0,X1),sdtpldt0(X2,X1))
| ~ aNaturalNumber0(X1)
| X0 = X2
| ~ sdtlseqdt0(X0,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2) ),
inference(forward_subsumption_resolution,[],[f1601,f180]) ).
fof(f1861,plain,
! [X0,X1] :
( ~ aNaturalNumber0(xp)
| sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sP1(X1,xp)
| doDivides0(xp,X0)
| sP0(xp)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[],[f1606,f258]) ).
fof(f1868,plain,
! [X0,X1] :
( ~ aNaturalNumber0(xp)
| sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sP1(X1,xp)
| doDivides0(xp,X0)
| sP0(xp)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(duplicate_literal_removal,[],[f1861]) ).
fof(f2040,definition,
( spl23_94
<=> doDivides0(xn,xn) ),
introduced(definition,[new_symbols(definition,[spl23_94])],[avatar_definition]) ).
fof(f2042,plain,
( doDivides0(xn,xn)
| ~ spl23_94 ),
inference(avatar_component_clause,[],[f2040]) ).
fof(f2412,plain,
xn = sdtasdt0(xn,sz10),
inference(resolution,[],[f189,f247]) ).
fof(f2437,plain,
( doDivides0(xn,xn)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[],[f328,f2412]) ).
fof(f2438,plain,
( ~ doDivides0(xn,xn)
| ~ aNaturalNumber0(sz10)
| sz00 = xn
| sz10 = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[],[f329,f2412]) ).
fof(f2441,plain,
( ~ doDivides0(xn,xn)
| ~ aNaturalNumber0(sz10)
| sz00 = xn
| sz10 = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn) ),
inference(duplicate_literal_removal,[],[f2438]) ).
fof(f2442,plain,
( doDivides0(xn,xn)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xn) ),
inference(duplicate_literal_removal,[],[f2437]) ).
fof(f2443,plain,
( ~ doDivides0(xn,xn)
| sz00 = xn
| sz10 = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_7 ),
inference(forward_subsumption_resolution,[],[f2441,f375]) ).
fof(f2444,plain,
( doDivides0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_7 ),
inference(forward_subsumption_resolution,[],[f2442,f375]) ).
fof(f2452,plain,
( ~ doDivides0(xn,xn)
| sz10 = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_7
| spl23_11 ),
inference(forward_subsumption_resolution,[],[f2443,f469]) ).
fof(f2453,plain,
( doDivides0(xn,xn)
| ~ spl23_7 ),
inference(forward_subsumption_resolution,[],[f2444,f247]) ).
fof(f2461,plain,
( ~ doDivides0(xn,xn)
| sz10 = sdtsldt0(xn,xn)
| ~ spl23_7
| spl23_11 ),
inference(forward_subsumption_resolution,[],[f2452,f247]) ).
fof(f2462,plain,
( spl23_94
| ~ spl23_7 ),
inference(avatar_split_clause,[],[f2453,f374,f2040]) ).
fof(f2470,definition,
( spl23_110
<=> sz10 = sdtsldt0(xn,xn) ),
introduced(definition,[new_symbols(definition,[spl23_110])],[avatar_definition]) ).
fof(f2472,plain,
( sz10 = sdtsldt0(xn,xn)
| ~ spl23_110 ),
inference(avatar_component_clause,[],[f2470]) ).
fof(f2473,plain,
( spl23_110
| ~ spl23_94
| ~ spl23_7
| spl23_11 ),
inference(avatar_split_clause,[],[f2461,f468,f374,f2040,f2470]) ).
fof(f2759,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xn)
| sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(resolution,[],[f209,f280]) ).
fof(f2770,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xn)
| sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(forward_subsumption_resolution,[],[f2759,f247]) ).
fof(f2781,plain,
! [X0] :
( ~ sdtlseqdt0(X0,xn)
| sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f2770,f245]) ).
fof(f2987,plain,
( sz00 != xn
| ~ aNaturalNumber0(xk)
| ~ spl23_43 ),
inference(superposition,[],[f336,f1194]) ).
fof(f3126,plain,
! [X0] :
( xn != sdtasdt0(xr,X0)
| sK20 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK20)
| sz00 = xr
| ~ aNaturalNumber0(xr) ),
inference(superposition,[],[f197,f393]) ).
fof(f3131,plain,
! [X0] :
( xn != sdtasdt0(xr,X0)
| sK20 = X0
| ~ aNaturalNumber0(X0)
| sz00 = xr
| ~ aNaturalNumber0(xr) ),
inference(forward_subsumption_resolution,[],[f3126,f317]) ).
fof(f3153,plain,
! [X0] :
( xn != sdtasdt0(xr,X0)
| sK20 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xr) ),
inference(forward_subsumption_resolution,[],[f3131,f295]) ).
fof(f3175,plain,
! [X0] :
( xn != sdtasdt0(xr,X0)
| sK20 = X0
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f3153,f299]) ).
fof(f3539,plain,
sz00 = sdtasdt0(xm,sz00),
inference(resolution,[],[f191,f246]) ).
fof(f3542,plain,
sz00 = sdtasdt0(xr,sz00),
inference(resolution,[],[f191,f299]) ).
fof(f3629,plain,
( ~ aNaturalNumber0(xk)
| ~ spl23_11
| ~ spl23_43 ),
inference(forward_subsumption_resolution,[],[f2987,f470]) ).
fof(f3630,plain,
( $false
| ~ spl23_11
| ~ spl23_43 ),
inference(forward_subsumption_resolution,[],[f3629,f286]) ).
fof(f3631,plain,
( ~ spl23_11
| ~ spl23_43 ),
inference(avatar_contradiction_clause,[],[f3630]) ).
fof(f3981,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xr,sz00)
| ~ spl23_59 ),
inference(superposition,[],[f301,f1484]) ).
fof(f3982,plain,
( sz00 = sdtasdt0(xn,xm)
| ~ spl23_59 ),
inference(forward_demodulation,[],[f3981,f3542]) ).
fof(f3983,plain,
( sz00 = sdtasdt0(xp,xk)
| ~ spl23_59 ),
inference(forward_demodulation,[],[f3982,f285]) ).
fof(f3984,plain,
( sz00 = sF21(xk)
| ~ spl23_59 ),
inference(forward_demodulation,[],[f3983,f335]) ).
fof(f3985,plain,
( $false
| spl23_43
| ~ spl23_59 ),
inference(forward_subsumption_resolution,[],[f3984,f1193]) ).
fof(f3986,plain,
( spl23_43
| ~ spl23_59 ),
inference(avatar_contradiction_clause,[],[f3985]) ).
fof(f4157,plain,
sdtasdt0(xn,xm) = sdtasdt0(xm,xn),
inference(resolution,[],[f506,f246]) ).
fof(f4281,plain,
sdtasdt0(xp,xk) = sdtasdt0(xm,xn),
inference(forward_demodulation,[],[f4157,f285]) ).
fof(f4309,plain,
sF21(xk) = sdtasdt0(xm,xn),
inference(forward_demodulation,[],[f4281,f335]) ).
fof(f5239,plain,
( ~ isPrime0(xp)
| ~ spl23_13 ),
inference(resolution,[],[f730,f251]) ).
fof(f5240,plain,
( $false
| ~ spl23_13 ),
inference(forward_subsumption_resolution,[],[f5239,f267]) ).
fof(f5241,plain,
~ spl23_13,
inference(avatar_contradiction_clause,[],[f5240]) ).
fof(f5243,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sP1(X1,xp)
| doDivides0(xp,X0)
| sP0(xp)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(forward_subsumption_resolution,[],[f1868,f245]) ).
fof(f5247,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sP1(X1,xp)
| doDivides0(xp,X0)
| sP0(xp)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(forward_subsumption_resolution,[],[f5243,f180]) ).
fof(f5251,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| sP1(X1,xp)
| doDivides0(xp,X0)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) )
| spl23_13 ),
inference(forward_subsumption_resolution,[],[f5247,f729]) ).
fof(f5253,definition,
( spl23_163
<=> aNaturalNumber0(sdtpldt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[spl23_163])],[avatar_definition]) ).
fof(f5255,plain,
( ~ aNaturalNumber0(sdtpldt0(xn,xm))
| spl23_163 ),
inference(avatar_component_clause,[],[f5253]) ).
fof(f5270,definition,
( spl23_167
<=> sP1(xm,xp) ),
introduced(definition,[new_symbols(definition,[spl23_167])],[avatar_definition]) ).
fof(f5272,plain,
( sP1(xm,xp)
| ~ spl23_167 ),
inference(avatar_component_clause,[],[f5270]) ).
fof(f5278,definition,
( spl23_169
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(xn,xm)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| doDivides0(xp,X0)
| sP1(X1,xp)
| ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm)) ) ),
introduced(definition,[new_symbols(definition,[spl23_169])],[avatar_definition]) ).
fof(f5279,plain,
( ! [X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X0,X1),sdtpldt0(xn,xm))
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,X1))
| doDivides0(xp,X0)
| sP1(X1,xp)
| sdtpldt0(X0,X1) = sdtpldt0(xn,xm) )
| ~ spl23_169 ),
inference(avatar_component_clause,[],[f5278]) ).
fof(f5280,plain,
( ~ spl23_163
| spl23_169
| spl23_13 ),
inference(avatar_split_clause,[],[f5251,f728,f5278,f5253]) ).
fof(f5290,plain,
( ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm)
| spl23_163 ),
inference(resolution,[],[f5255,f180]) ).
fof(f5291,plain,
( ~ aNaturalNumber0(xm)
| spl23_163 ),
inference(forward_subsumption_resolution,[],[f5290,f247]) ).
fof(f5292,plain,
( $false
| spl23_163 ),
inference(forward_subsumption_resolution,[],[f5291,f246]) ).
fof(f5293,plain,
spl23_163,
inference(avatar_contradiction_clause,[],[f5292]) ).
fof(f5294,plain,
( ! [X0] :
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm))
| doDivides0(xp,X0)
| sP1(xm,xp)
| sdtpldt0(xn,xm) = sdtpldt0(X0,xm)
| ~ aNaturalNumber0(xm)
| xn = X0
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xn) )
| ~ spl23_169 ),
inference(resolution,[],[f5279,f212]) ).
fof(f5303,plain,
( ! [X0] :
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm))
| doDivides0(xp,X0)
| sP1(xm,xp)
| sdtpldt0(xn,xm) = sdtpldt0(X0,xm)
| xn = X0
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(xn) )
| ~ spl23_169 ),
inference(duplicate_literal_removal,[],[f5294]) ).
fof(f5310,plain,
( ! [X0] :
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm))
| doDivides0(xp,X0)
| sP1(xm,xp)
| xn = X0
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(xn) )
| ~ spl23_169 ),
inference(forward_subsumption_resolution,[],[f5303,f213]) ).
fof(f5317,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm))
| doDivides0(xp,X0)
| sP1(xm,xp)
| xn = X0
| ~ sdtlseqdt0(X0,xn)
| ~ aNaturalNumber0(xn) )
| ~ spl23_169 ),
inference(forward_subsumption_resolution,[],[f5310,f246]) ).
fof(f5344,plain,
( ! [X0] :
( ~ aNaturalNumber0(X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm))
| doDivides0(xp,X0)
| sP1(xm,xp)
| xn = X0
| ~ sdtlseqdt0(X0,xn) )
| ~ spl23_169 ),
inference(forward_subsumption_resolution,[],[f5317,f247]) ).
fof(f5359,definition,
( spl23_179
<=> ! [X0] :
( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,xn)
| xn = X0
| doDivides0(xp,X0)
| ~ doDivides0(xp,sdtasdt0(X0,xm)) ) ),
introduced(definition,[new_symbols(definition,[spl23_179])],[avatar_definition]) ).
fof(f5360,plain,
( ! [X0] :
( ~ doDivides0(xp,sdtasdt0(X0,xm))
| ~ sdtlseqdt0(X0,xn)
| xn = X0
| doDivides0(xp,X0)
| ~ aNaturalNumber0(X0) )
| ~ spl23_179 ),
inference(avatar_component_clause,[],[f5359]) ).
fof(f5361,plain,
( spl23_167
| spl23_179
| ~ spl23_169 ),
inference(avatar_split_clause,[],[f5344,f5278,f5359,f5270]) ).
fof(f5396,plain,
( doDivides0(xp,xm)
| ~ spl23_167 ),
inference(resolution,[],[f5272,f248]) ).
fof(f5397,plain,
( $false
| ~ spl23_167 ),
inference(forward_subsumption_resolution,[],[f5396,f318]) ).
fof(f5398,plain,
~ spl23_167,
inference(avatar_contradiction_clause,[],[f5397]) ).
fof(f5685,plain,
sdtasdt0(sK20,xm) = sdtasdt0(xm,sK20),
inference(resolution,[],[f507,f317]) ).
fof(f6419,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sK20) = sdtsldt0(sdtasdt0(X0,xn),xr) ),
inference(forward_demodulation,[],[f898,f461]) ).
fof(f6422,plain,
xn = sdtasdt0(sK20,xr),
inference(forward_demodulation,[],[f1355,f393]) ).
fof(f6424,definition,
( spl23_251
<=> sz00 = sK20 ),
introduced(definition,[new_symbols(definition,[spl23_251])],[avatar_definition]) ).
fof(f6425,plain,
( sz00 != sK20
| spl23_251 ),
inference(avatar_component_clause,[],[f6424]) ).
fof(f6426,plain,
( sz00 = sK20
| ~ spl23_251 ),
inference(avatar_component_clause,[],[f6424]) ).
fof(f6612,plain,
( xn = sdtasdt0(xr,sz00)
| ~ spl23_251 ),
inference(superposition,[],[f393,f6426]) ).
fof(f6613,plain,
( sz00 = xn
| ~ spl23_251 ),
inference(forward_demodulation,[],[f6612,f3542]) ).
fof(f6614,plain,
( $false
| spl23_11
| ~ spl23_251 ),
inference(forward_subsumption_resolution,[],[f6613,f469]) ).
fof(f6615,plain,
( spl23_11
| ~ spl23_251 ),
inference(avatar_contradiction_clause,[],[f6614]) ).
fof(f6801,plain,
( sdtlseqdt0(sK20,xn)
| sz00 = xr
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sK20) ),
inference(superposition,[],[f222,f6422]) ).
fof(f6805,plain,
( doDivides0(sK20,xn)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sK20)
| ~ aNaturalNumber0(xn) ),
inference(superposition,[],[f328,f6422]) ).
fof(f6829,plain,
( doDivides0(sK20,xn)
| ~ aNaturalNumber0(sK20)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f6805,f299]) ).
fof(f6832,plain,
( sdtlseqdt0(sK20,xn)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sK20) ),
inference(forward_subsumption_resolution,[],[f6801,f295]) ).
fof(f6855,plain,
( doDivides0(sK20,xn)
| ~ aNaturalNumber0(xn) ),
inference(forward_subsumption_resolution,[],[f6829,f317]) ).
fof(f6858,plain,
( sdtlseqdt0(sK20,xn)
| ~ aNaturalNumber0(sK20) ),
inference(forward_subsumption_resolution,[],[f6832,f299]) ).
fof(f6881,plain,
doDivides0(sK20,xn),
inference(forward_subsumption_resolution,[],[f6855,f247]) ).
fof(f6891,plain,
sdtlseqdt0(sK20,xn),
inference(forward_subsumption_resolution,[],[f6858,f317]) ).
fof(f6905,definition,
( spl23_292
<=> sdtlseqdt0(xp,sK20) ),
introduced(definition,[new_symbols(definition,[spl23_292])],[avatar_definition]) ).
fof(f6906,plain,
( sdtlseqdt0(xp,sK20)
| ~ spl23_292 ),
inference(avatar_component_clause,[],[f6905]) ).
fof(f6907,plain,
( ~ sdtlseqdt0(xp,sK20)
| spl23_292 ),
inference(avatar_component_clause,[],[f6905]) ).
fof(f6909,definition,
( spl23_293
<=> xp = sK20 ),
introduced(definition,[new_symbols(definition,[spl23_293])],[avatar_definition]) ).
fof(f6910,plain,
( xp != sK20
| spl23_293 ),
inference(avatar_component_clause,[],[f6909]) ).
fof(f6911,plain,
( xp = sK20
| ~ spl23_293 ),
inference(avatar_component_clause,[],[f6909]) ).
fof(f6920,plain,
sdtsldt0(sdtasdt0(xm,xn),xr) = sdtasdt0(xm,sK20),
inference(resolution,[],[f6419,f246]) ).
fof(f6940,plain,
sdtsldt0(sF21(xk),xr) = sdtasdt0(xm,sK20),
inference(forward_demodulation,[],[f6920,f4309]) ).
fof(f6944,plain,
sK16 = sdtasdt0(xm,sK20),
inference(forward_demodulation,[],[f6940,f477]) ).
fof(f7255,plain,
( sz00 != xn
| sz00 = sK20
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[],[f3175,f3542]) ).
fof(f7373,definition,
( spl23_306
<=> doDivides0(xp,sK20) ),
introduced(definition,[new_symbols(definition,[spl23_306])],[avatar_definition]) ).
fof(f7375,plain,
( doDivides0(xp,sK20)
| ~ spl23_306 ),
inference(avatar_component_clause,[],[f7373]) ).
fof(f8407,definition,
( spl23_354
<=> sdtlseqdt0(sK20,xp) ),
introduced(definition,[new_symbols(definition,[spl23_354])],[avatar_definition]) ).
fof(f8408,plain,
( sdtlseqdt0(sK20,xp)
| ~ spl23_354 ),
inference(avatar_component_clause,[],[f8407]) ).
fof(f8409,plain,
( ~ sdtlseqdt0(sK20,xp)
| spl23_354 ),
inference(avatar_component_clause,[],[f8407]) ).
fof(f8851,definition,
( spl23_367
<=> xn = sK20 ),
introduced(definition,[new_symbols(definition,[spl23_367])],[avatar_definition]) ).
fof(f8852,plain,
( xn != sK20
| spl23_367 ),
inference(avatar_component_clause,[],[f8851]) ).
fof(f8853,plain,
( xn = sK20
| ~ spl23_367 ),
inference(avatar_component_clause,[],[f8851]) ).
fof(f10264,plain,
( xn = sdtasdt0(xn,xr)
| ~ spl23_367 ),
inference(superposition,[],[f6422,f8853]) ).
fof(f10320,plain,
( ~ doDivides0(xn,xn)
| ~ aNaturalNumber0(xr)
| sz00 = xn
| xr = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_367 ),
inference(superposition,[],[f329,f10264]) ).
fof(f10333,plain,
( ~ doDivides0(xn,xn)
| ~ aNaturalNumber0(xr)
| sz00 = xn
| xr = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_367 ),
inference(duplicate_literal_removal,[],[f10320]) ).
fof(f10343,plain,
( ~ aNaturalNumber0(xr)
| sz00 = xn
| xr = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_94
| ~ spl23_367 ),
inference(forward_subsumption_resolution,[],[f10333,f2042]) ).
fof(f10365,plain,
( sz00 = xn
| xr = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| ~ spl23_94
| ~ spl23_367 ),
inference(forward_subsumption_resolution,[],[f10343,f299]) ).
fof(f10386,plain,
( xr = sdtsldt0(xn,xn)
| ~ aNaturalNumber0(xn)
| spl23_11
| ~ spl23_94
| ~ spl23_367 ),
inference(forward_subsumption_resolution,[],[f10365,f469]) ).
fof(f10399,plain,
( xr = sdtsldt0(xn,xn)
| spl23_11
| ~ spl23_94
| ~ spl23_367 ),
inference(forward_subsumption_resolution,[],[f10386,f247]) ).
fof(f10400,plain,
( sz10 = xr
| spl23_11
| ~ spl23_94
| ~ spl23_110
| ~ spl23_367 ),
inference(forward_demodulation,[],[f10399,f2472]) ).
fof(f10401,plain,
( $false
| spl23_11
| ~ spl23_94
| ~ spl23_110
| ~ spl23_367 ),
inference(forward_subsumption_resolution,[],[f10400,f294]) ).
fof(f10402,plain,
( spl23_11
| ~ spl23_94
| ~ spl23_110
| ~ spl23_367 ),
inference(avatar_contradiction_clause,[],[f10401]) ).
fof(f10849,plain,
( ~ doDivides0(xp,sdtasdt0(xm,sK20))
| ~ sdtlseqdt0(sK20,xn)
| xn = sK20
| doDivides0(xp,sK20)
| ~ aNaturalNumber0(sK20)
| ~ spl23_179 ),
inference(superposition,[],[f5360,f5685]) ).
fof(f10908,plain,
( ~ doDivides0(xp,sdtasdt0(xm,sK20))
| xn = sK20
| doDivides0(xp,sK20)
| ~ aNaturalNumber0(sK20)
| ~ spl23_179 ),
inference(forward_subsumption_resolution,[],[f10849,f6891]) ).
fof(f10935,plain,
( ~ doDivides0(xp,sdtasdt0(xm,sK20))
| doDivides0(xp,sK20)
| ~ aNaturalNumber0(sK20)
| ~ spl23_179
| spl23_367 ),
inference(forward_subsumption_resolution,[],[f10908,f8852]) ).
fof(f10962,plain,
( ~ doDivides0(xp,sdtasdt0(xm,sK20))
| doDivides0(xp,sK20)
| ~ spl23_179
| spl23_367 ),
inference(forward_subsumption_resolution,[],[f10935,f317]) ).
fof(f10988,plain,
( ~ doDivides0(xp,sK16)
| doDivides0(xp,sK20)
| ~ spl23_179
| spl23_367 ),
inference(forward_demodulation,[],[f10962,f6944]) ).
fof(f10992,plain,
( doDivides0(xp,sK20)
| ~ spl23_28
| ~ spl23_179
| spl23_367 ),
inference(forward_subsumption_resolution,[],[f10988,f952]) ).
fof(f10994,plain,
( spl23_306
| ~ spl23_28
| ~ spl23_179
| spl23_367 ),
inference(avatar_split_clause,[],[f10992,f8851,f5359,f950,f7373]) ).
fof(f10998,plain,
( sdtlseqdt0(xp,sK20)
| sz00 = sK20
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK20)
| ~ spl23_306 ),
inference(resolution,[],[f7375,f233]) ).
fof(f11004,plain,
( sz00 = sK20
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK20)
| spl23_292
| ~ spl23_306 ),
inference(forward_subsumption_resolution,[],[f10998,f6907]) ).
fof(f11008,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK20)
| spl23_251
| spl23_292
| ~ spl23_306 ),
inference(forward_subsumption_resolution,[],[f11004,f6425]) ).
fof(f11011,plain,
( ~ aNaturalNumber0(sK20)
| spl23_251
| spl23_292
| ~ spl23_306 ),
inference(forward_subsumption_resolution,[],[f11008,f245]) ).
fof(f11013,plain,
( $false
| spl23_251
| spl23_292
| ~ spl23_306 ),
inference(forward_subsumption_resolution,[],[f11011,f317]) ).
fof(f11014,plain,
( spl23_251
| spl23_292
| ~ spl23_306 ),
inference(avatar_contradiction_clause,[],[f11013]) ).
fof(f11110,plain,
( ~ sdtlseqdt0(sK20,xp)
| xp = sK20
| ~ aNaturalNumber0(sK20)
| ~ aNaturalNumber0(xp)
| ~ spl23_292 ),
inference(resolution,[],[f6906,f208]) ).
fof(f11400,plain,
( sdtlseqdt0(sK20,xp)
| ~ aNaturalNumber0(sK20) ),
inference(resolution,[],[f2781,f6891]) ).
fof(f11403,plain,
( ~ aNaturalNumber0(sK20)
| spl23_354 ),
inference(forward_subsumption_resolution,[],[f11400,f8409]) ).
fof(f11404,plain,
( $false
| spl23_354 ),
inference(forward_subsumption_resolution,[],[f11403,f317]) ).
fof(f11405,plain,
spl23_354,
inference(avatar_contradiction_clause,[],[f11404]) ).
fof(f11428,plain,
( doDivides0(xp,xn)
| ~ spl23_293 ),
inference(superposition,[],[f6881,f6911]) ).
fof(f11467,plain,
( $false
| ~ spl23_293 ),
inference(forward_subsumption_resolution,[],[f11428,f320]) ).
fof(f11468,plain,
~ spl23_293,
inference(avatar_contradiction_clause,[],[f11467]) ).
fof(f11496,plain,
( xp = sK20
| ~ aNaturalNumber0(sK20)
| ~ aNaturalNumber0(xp)
| ~ spl23_292
| ~ spl23_354 ),
inference(forward_subsumption_resolution,[],[f11110,f8408]) ).
fof(f11500,plain,
( ~ aNaturalNumber0(sK20)
| ~ aNaturalNumber0(xp)
| ~ spl23_292
| spl23_293
| ~ spl23_354 ),
inference(forward_subsumption_resolution,[],[f11496,f6910]) ).
fof(f11504,plain,
( ~ aNaturalNumber0(xp)
| ~ spl23_292
| spl23_293
| ~ spl23_354 ),
inference(forward_subsumption_resolution,[],[f11500,f317]) ).
fof(f11509,plain,
( $false
| ~ spl23_292
| spl23_293
| ~ spl23_354 ),
inference(forward_subsumption_resolution,[],[f11504,f245]) ).
fof(f11510,plain,
( ~ spl23_292
| spl23_293
| ~ spl23_354 ),
inference(avatar_contradiction_clause,[],[f11509]) ).
fof(f11538,plain,
( sz00 = sK20
| ~ aNaturalNumber0(sz00)
| ~ spl23_11 ),
inference(forward_subsumption_resolution,[],[f7255,f470]) ).
fof(f11554,plain,
( ~ aNaturalNumber0(sz00)
| ~ spl23_11
| spl23_251 ),
inference(forward_subsumption_resolution,[],[f11538,f6425]) ).
fof(f11562,plain,
( $false
| ~ spl23_9
| ~ spl23_11
| spl23_251 ),
inference(forward_subsumption_resolution,[],[f11554,f384]) ).
fof(f11563,plain,
( ~ spl23_9
| ~ spl23_11
| spl23_251 ),
inference(avatar_contradiction_clause,[],[f11562]) ).
fof(f11608,plain,
( sK16 = sdtasdt0(xm,sz00)
| ~ spl23_251 ),
inference(superposition,[],[f6944,f6426]) ).
fof(f11631,plain,
( sz00 = sK16
| ~ spl23_251 ),
inference(forward_demodulation,[],[f11608,f3539]) ).
fof(f11647,plain,
( $false
| spl23_59
| ~ spl23_251 ),
inference(forward_subsumption_resolution,[],[f11631,f1483]) ).
fof(f11648,plain,
( spl23_59
| ~ spl23_251 ),
inference(avatar_contradiction_clause,[],[f11647]) ).
cnf(s8,plain,
spl23_7,
inference(sat_conversion,[],[f391]) ).
cnf(s9,plain,
spl23_9,
inference(sat_conversion,[],[f392]) ).
cnf(s24,plain,
( ~ spl23_25
| spl23_28 ),
inference(sat_conversion,[],[f953]) ).
cnf(s26,plain,
spl23_25,
inference(sat_conversion,[],[f1023]) ).
cnf(s87,plain,
( ~ spl23_7
| spl23_94 ),
inference(sat_conversion,[],[f2462]) ).
cnf(s88,plain,
( ~ spl23_7
| spl23_11
| ~ spl23_94
| spl23_110 ),
inference(sat_conversion,[],[f2473]) ).
cnf(s117,plain,
( ~ spl23_11
| ~ spl23_43 ),
inference(sat_conversion,[],[f3631]) ).
cnf(s126,plain,
( spl23_43
| ~ spl23_59 ),
inference(sat_conversion,[],[f3986]) ).
cnf(s168,plain,
~ spl23_13,
inference(sat_conversion,[],[f5241]) ).
cnf(s171,plain,
( spl23_13
| ~ spl23_163
| spl23_169 ),
inference(sat_conversion,[],[f5280]) ).
cnf(s173,plain,
spl23_163,
inference(sat_conversion,[],[f5293]) ).
cnf(s176,plain,
( spl23_167
| ~ spl23_169
| spl23_179 ),
inference(sat_conversion,[],[f5361]) ).
cnf(s180,plain,
~ spl23_167,
inference(sat_conversion,[],[f5398]) ).
cnf(s251,plain,
( spl23_11
| ~ spl23_251 ),
inference(sat_conversion,[],[f6615]) ).
cnf(s342,plain,
( spl23_11
| ~ spl23_94
| ~ spl23_110
| ~ spl23_367 ),
inference(sat_conversion,[],[f10402]) ).
cnf(s355,plain,
( ~ spl23_28
| ~ spl23_179
| spl23_306
| spl23_367 ),
inference(sat_conversion,[],[f10994]) ).
cnf(s356,plain,
( spl23_251
| spl23_292
| ~ spl23_306 ),
inference(sat_conversion,[],[f11014]) ).
cnf(s380,plain,
spl23_354,
inference(sat_conversion,[],[f11405]) ).
cnf(s386,plain,
~ spl23_293,
inference(sat_conversion,[],[f11468]) ).
cnf(s392,plain,
( ~ spl23_292
| spl23_293
| ~ spl23_354 ),
inference(sat_conversion,[],[f11510]) ).
cnf(s398,plain,
( ~ spl23_9
| ~ spl23_11
| spl23_251 ),
inference(sat_conversion,[],[f11563]) ).
cnf(s405,plain,
( spl23_59
| ~ spl23_251 ),
inference(sat_conversion,[],[f11648]) ).
cnf(s408,plain,
~ spl23_292,
inference(rat,[],[s392,s386,s380]) ).
cnf(s411,plain,
( spl23_251
| ~ spl23_306 ),
inference(rat,[],[s356,s408]) ).
cnf(s424,plain,
( ~ spl23_169
| spl23_179 ),
inference(rat,[],[s176,s180]) ).
cnf(s425,plain,
( spl23_13
| spl23_169 ),
inference(rat,[],[s171,s173]) ).
cnf(s428,plain,
spl23_169,
inference(rat,[],[s425,s168]) ).
cnf(s429,plain,
spl23_179,
inference(rat,[],[s424,s428]) ).
cnf(s458,plain,
spl23_28,
inference(rat,[],[s24,s26]) ).
cnf(s471,plain,
spl23_94,
inference(rat,[],[s87,s8]) ).
cnf(s475,plain,
spl23_11,
inference(rat,[],[s355,s342,s411,s88,s251,s429,s458,s471,s8]) ).
cnf(s476,plain,
spl23_251,
inference(rat,[],[s398,s9,s475]) ).
cnf(s477,plain,
~ spl23_43,
inference(rat,[],[s117,s475]) ).
cnf(s482,plain,
spl23_59,
inference(rat,[],[s405,s476]) ).
cnf(s490,plain,
$false,
inference(rat,[],[s126,s482,s477]) ).
fof(f11656,plain,
$false,
inference(avatar_sat_refutation,[],[s490]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM509+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.39 % Computer : n017.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 20:10:51 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.89/2.57 % (2904839)Detected formulas, will run a generic FOF schedule.
% 11.89/2.57 % (2904850)dis-21_1_sil=8000:lcm=predicate:random_seed=1167028820:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.89/2.57 % (2904849)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3301619200:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.89/2.57 % (2904848)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2876822787:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.89/2.57 % (2904845)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4260558173:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.89/2.57 % (2904847)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=550466020:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.89/2.57 % (2904844)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1433779928:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.89/2.57 % (2904846)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3228436035:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.89/2.57 % (2904850)Instruction limit reached!
% 11.89/2.57 % (2904850)------------------------------
% 11.89/2.57 % (2904850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.57 % (2904850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.57 % (2904850)CaDiCaL version: 2.1.3
% 11.89/2.57 % (2904850)Termination reason: Instruction limit
% 11.89/2.57 % (2904850)Termination phase: Saturation
% 11.89/2.57 % (2904850)Time elapsed: 0.043 s
% 11.89/2.57 % (2904850)Peak memory usage: 91 MB
% 11.89/2.57 % (2904850)Instructions burned: 129 (million)
% 11.89/2.57 % (2904847)Instruction limit reached!
% 11.89/2.57 % (2904847)------------------------------
% 11.89/2.57 % (2904847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.57 % (2904847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.57 % (2904847)CaDiCaL version: 2.1.3
% 11.89/2.57 % (2904847)Termination reason: Instruction limit
% 11.89/2.57 % (2904847)Termination phase: Saturation
% 11.89/2.57 % (2904847)Time elapsed: 0.063 s
% 11.89/2.57 % (2904847)Peak memory usage: 89 MB
% 11.89/2.57 % (2904847)Instructions burned: 110 (million)
% 11.89/2.57 % (2904848)Instruction limit reached!
% 11.89/2.57 % (2904848)------------------------------
% 11.89/2.57 % (2904848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.57 % (2904848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.57 % (2904848)CaDiCaL version: 2.1.3
% 11.89/2.57 % (2904848)Termination reason: Instruction limit
% 11.89/2.57 % (2904848)Termination phase: Saturation
% 11.89/2.57 % (2904848)Time elapsed: 0.067 s
% 11.89/2.57 % (2904848)Peak memory usage: 89 MB
% 11.89/2.57 % (2904848)Instructions burned: 120 (million)
% 11.89/2.57 % (2904849)Instruction limit reached!
% 11.89/2.57 % (2904849)------------------------------
% 11.89/2.57 % (2904849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.57 % (2904849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.57 % (2904849)CaDiCaL version: 2.1.3
% 11.89/2.57 % (2904849)Termination reason: Instruction limit
% 11.89/2.57 % (2904849)Termination phase: Saturation
% 11.89/2.57 % (2904849)Time elapsed: 0.092 s
% 11.89/2.57 % (2904849)Peak memory usage: 90 MB
% 11.89/2.57 % (2904849)Instructions burned: 140 (million)
% 11.89/2.57 % (2904858)lrs+10_1_sil=8000:sp=occurrence:random_seed=341901152:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.89/2.57 % (2904858)Instruction limit reached!
% 11.89/2.57 % (2904858)------------------------------
% 11.89/2.57 % (2904858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.89/2.57 % (2904858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.89/2.57 % (2904858)CaDiCaL version: 2.1.3
% 11.89/2.57 % (2904858)Termination reason: Instruction limit
% 11.89/2.57 % (2904858)Termination phase: Saturation
% 11.89/2.57 % (2904858)Time elapsed: 0.085 s
% 11.89/2.57 % (2904858)Peak memory usage: 91 MB
% 11.89/2.57 % (2904858)Instructions burned: 285 (million)
% 13.92/2.84 % (2904859)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2287984088:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.92/2.84 % (2904860)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2989137631:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.92/2.84 % (2904862)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=4001858945:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.92/2.84 % (2904863)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3025636658:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 13.92/2.84 % (2904859)Instruction limit reached!
% 13.92/2.84 % (2904859)------------------------------
% 13.92/2.84 % (2904859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904859)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904859)Termination reason: Instruction limit
% 13.92/2.84 % (2904859)Termination phase: Saturation
% 13.92/2.84 % (2904859)Time elapsed: 0.076 s
% 13.92/2.84 % (2904859)Peak memory usage: 92 MB
% 13.92/2.84 % (2904859)Instructions burned: 159 (million)
% 13.92/2.84 % (2904862)Instruction limit reached!
% 13.92/2.84 % (2904862)------------------------------
% 13.92/2.84 % (2904862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904862)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904862)Termination reason: Instruction limit
% 13.92/2.84 % (2904862)Termination phase: Saturation
% 13.92/2.84 % (2904862)Time elapsed: 0.116 s
% 13.92/2.84 % (2904862)Peak memory usage: 94 MB
% 13.92/2.84 % (2904862)Instructions burned: 249 (million)
% 13.92/2.84 % (2904863)Instruction limit reached!
% 13.92/2.84 % (2904863)------------------------------
% 13.92/2.84 % (2904863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904863)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904863)Termination reason: Instruction limit
% 13.92/2.84 % (2904863)Termination phase: Saturation
% 13.92/2.84 % (2904863)Time elapsed: 0.086 s
% 13.92/2.84 % (2904863)Peak memory usage: 89 MB
% 13.92/2.84 % (2904863)Instructions burned: 295 (million)
% 13.92/2.84 % (2904868)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2067916449:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 13.92/2.84 % (2904860)Instruction limit reached!
% 13.92/2.84 % (2904860)------------------------------
% 13.92/2.84 % (2904860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904860)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904860)Termination reason: Instruction limit
% 13.92/2.84 % (2904860)Termination phase: Saturation
% 13.92/2.84 % (2904860)Time elapsed: 0.202 s
% 13.92/2.84 % (2904860)Peak memory usage: 92 MB
% 13.92/2.84 % (2904860)Instructions burned: 326 (million)
% 13.92/2.84 % (2904870)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1252511807:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 13.92/2.84 % (2904869)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3544888205:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 13.92/2.84 % (2904870)Instruction limit reached!
% 13.92/2.84 % (2904870)------------------------------
% 13.92/2.84 % (2904870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904870)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904870)Termination reason: Instruction limit
% 13.92/2.84 % (2904870)Termination phase: Saturation
% 13.92/2.84 % (2904870)Time elapsed: 0.035 s
% 13.92/2.84 % (2904870)Peak memory usage: 89 MB
% 13.92/2.84 % (2904870)Instructions burned: 129 (million)
% 13.92/2.84 % (2904869)Instruction limit reached!
% 13.92/2.84 % (2904869)------------------------------
% 13.92/2.84 % (2904869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904869)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904869)Termination reason: Instruction limit
% 13.92/2.84 % (2904869)Termination phase: Saturation
% 13.92/2.84 % (2904869)Time elapsed: 0.068 s
% 13.92/2.84 % (2904869)Peak memory usage: 91 MB
% 13.92/2.84 % (2904869)Instructions burned: 114 (million)
% 13.92/2.84 % (2904872)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2145060000:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 13.92/2.84 % (2904875)lrs+10_1_sil=8000:sp=occurrence:random_seed=1489001628:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2993 on theBenchmark for (2993ds/907Mi)
% 13.92/2.84 % (2904872)Instruction limit reached!
% 13.92/2.84 % (2904872)------------------------------
% 13.92/2.84 % (2904872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904872)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904872)Termination reason: Instruction limit
% 13.92/2.84 % (2904872)Termination phase: Saturation
% 13.92/2.84 % (2904872)Time elapsed: 0.063 s
% 13.92/2.84 % (2904872)Peak memory usage: 89 MB
% 13.92/2.84 % (2904872)Instructions burned: 114 (million)
% 13.92/2.84 % (2904877)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1708121649:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 13.92/2.84 % (2904879)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3427272836:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 13.92/2.84 % (2904875)Instruction limit reached!
% 13.92/2.84 % (2904875)------------------------------
% 13.92/2.84 % (2904875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904875)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904875)Termination reason: Instruction limit
% 13.92/2.84 % (2904875)Termination phase: Saturation
% 13.92/2.84 % (2904875)Time elapsed: 0.277 s
% 13.92/2.84 % (2904875)Peak memory usage: 98 MB
% 13.92/2.84 % (2904875)Instructions burned: 910 (million)
% 13.92/2.84 % (2904877)Instruction limit reached!
% 13.92/2.84 % (2904877)------------------------------
% 13.92/2.84 % (2904877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904877)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904877)Termination reason: Instruction limit
% 13.92/2.84 % (2904877)Termination phase: Saturation
% 13.92/2.84 % (2904877)Time elapsed: 0.255 s
% 13.92/2.84 % (2904877)Peak memory usage: 92 MB
% 13.92/2.84 % (2904877)Instructions burned: 438 (million)
% 13.92/2.84 % (2904882)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1080435757:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2990 on theBenchmark for (2990ds/134Mi)
% 13.92/2.84 % (2904882)Instruction limit reached!
% 13.92/2.84 % (2904882)------------------------------
% 13.92/2.84 % (2904882)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904882)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904882)Termination reason: Instruction limit
% 13.92/2.84 % (2904882)Termination phase: Saturation
% 13.92/2.84 % (2904882)Time elapsed: 0.036 s
% 13.92/2.84 % (2904882)Peak memory usage: 93 MB
% 13.92/2.84 % (2904882)Instructions burned: 135 (million)
% 13.92/2.84 % (2904883)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2035739759:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi)
% 13.92/2.84 % (2904885)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1396452012:st=3:i=13193:sd=3:ss=axioms_2988 on theBenchmark for (2988ds/13193Mi)
% 13.92/2.84 % (2904883)Instruction limit reached!
% 13.92/2.84 % (2904883)------------------------------
% 13.92/2.84 % (2904883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904883)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904883)Termination reason: Instruction limit
% 13.92/2.84 % (2904883)Termination phase: Saturation
% 13.92/2.84 % (2904883)Time elapsed: 0.367 s
% 13.92/2.84 % (2904883)Peak memory usage: 95 MB
% 13.92/2.84 % (2904883)Instructions burned: 593 (million)
% 13.92/2.84 % (2904888)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3572108095:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/125Mi)
% 13.92/2.84 % (2904844)First to succeed.
% 13.92/2.84 % (2904844)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2904839"
% 13.92/2.84 % (2904888)Instruction limit reached!
% 13.92/2.84 % (2904888)------------------------------
% 13.92/2.84 % (2904888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.92/2.84 % (2904888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.92/2.84 % (2904888)CaDiCaL version: 2.1.3
% 13.92/2.84 % (2904888)Termination reason: Instruction limit
% 13.92/2.84 % (2904888)Termination phase: Saturation
% 13.92/2.84 % (2904888)Time elapsed: 0.071 s
% 13.92/2.84 % (2904888)Peak memory usage: 90 MB
% 13.92/2.84 % (2904888)Instructions burned: 127 (million)
% 13.92/2.84 % (2904890)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4275695284:i=134:gtgl=5:slsql=off:gtg=exists_sym_2982 on theBenchmark for (2982ds/134Mi)
% 13.92/2.84 % (2904844)Refutation found. Thanks to Tanya!
% 13.92/2.84 % SZS status Theorem for theBenchmark
% 13.92/2.84 % SZS output start Proof for theBenchmark
% See solution above
% 0.16/3.03 % (2904844)------------------------------
% 0.16/3.03 % (2904844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.16/3.03 % (2904844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.16/3.03 % (2904844)CaDiCaL version: 2.1.3
% 0.16/3.03 % (2904844)Termination reason: Refutation
% 0.16/3.03 % (2904844)Time elapsed: 1.568 s
% 0.16/3.03 % (2904844)Peak memory usage: 142 MB
% 0.16/3.03 % (2904844)Instructions burned: 2473 (million)
% 0.16/3.03 % (2904844)------------------------------
% 0.16/3.03 % (2904844)------------------------------
% 0.16/3.03 % (2904839)Success in time 1.972 s
% 0.16/3.03 % Vampire exiting
%------------------------------------------------------------------------------