%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:36 PM UTC 2026
% Result : Theorem 2.73s 1.34s
% Output : Refutation 4.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 31
% Syntax : Number of formulae : 252 ( 36 unt; 11 def)
% Number of atoms : 963 ( 269 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 1220 ( 509 ~; 571 |; 101 &)
% ( 17 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 12 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 160 ( 0 sgn 142 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mMulCanc) ).
fof(f17,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( sdtasdt0(X0,X1) = sz00
=> ( X0 = sz00
| X1 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroMul) ).
fof(f21,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEAsym) ).
fof(f23,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETotal) ).
fof(f25,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( X0 != sz00
& X1 != X2
& sdtlseqdt0(X1,X2) )
=> ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul) ).
fof(f27,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( X0 != sz00
=> sdtlseqdt0(X1,sdtasdt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul2) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mDefQuot) ).
fof(f40,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp)
& xn != sz00
& xm != sz00
& xp != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2987) ).
fof(f42,axiom,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3014) ).
fof(f43,axiom,
( xp != sz10
& ! [X0] :
( ( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xp = sdtasdt0(X0,X1) )
| doDivides0(X0,xp) ) )
=> ( X0 = sz10
| X0 = xp ) )
& isPrime0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3025) ).
fof(f44,axiom,
( ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xn,xn) = sdtasdt0(xp,X0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [X0] :
( aNaturalNumber0(X0)
& xn = sdtasdt0(xp,X0) )
& doDivides0(xp,xn) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3046) ).
fof(f45,axiom,
( aNaturalNumber0(xq)
& xn = sdtasdt0(xp,xq)
& xq = sdtsldt0(xn,xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3059) ).
fof(f46,axiom,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3082) ).
fof(f47,axiom,
( ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xn,X0) = xm )
| sdtlseqdt0(xn,xm) )
=> ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtasdt0(xn,xn),X0) = sdtasdt0(xm,xm) )
& sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__3152) ).
fof(f48,conjecture,
( xm != xn
& ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xm,X0) = xn )
| sdtlseqdt0(xm,xn) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f49,negated_conjecture,
~ ( xm != xn
& ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xm,X0) = xn )
| sdtlseqdt0(xm,xn) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f50,plain,
( ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xn,xn) = sdtasdt0(xp,X0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [X1] :
( aNaturalNumber0(X1)
& xn = sdtasdt0(xp,X1) )
& doDivides0(xp,xn) ),
inference(rectify,[],[f44]) ).
fof(f51,plain,
( ( ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(xn,X0) = xm )
| sdtlseqdt0(xn,xm) )
=> ( ? [X1] :
( aNaturalNumber0(X1)
& sdtasdt0(xm,xm) = sdtpldt0(sdtasdt0(xn,xn),X1) )
& sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ) ),
inference(rectify,[],[f47]) ).
fof(f56,plain,
( xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp) ),
inference(ennf_transformation,[],[f43]) ).
fof(f57,plain,
( xp != sz10
& ! [X0] :
( X0 = sz10
| X0 = xp
| ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xp )
& ~ doDivides0(X0,xp) ) )
& isPrime0(xp) ),
inference(flattening,[],[f56]) ).
fof(f58,plain,
( ( ? [X1] :
( aNaturalNumber0(X1)
& sdtasdt0(xm,xm) = sdtpldt0(sdtasdt0(xn,xn),X1) )
& sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) )
| ( ! [X0] :
( ~ aNaturalNumber0(X0)
| xm != sdtpldt0(xn,X0) )
& ~ sdtlseqdt0(xn,xm) ) ),
inference(ennf_transformation,[],[f51]) ).
fof(f59,plain,
( xn = xm
| ( ! [X0] :
( ~ aNaturalNumber0(X0)
| xn != sdtpldt0(xm,X0) )
& ~ sdtlseqdt0(xm,xn) ) ),
inference(ennf_transformation,[],[f49]) ).
fof(f60,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f61,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f60]) ).
fof(f62,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(f63,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,[],[f62]) ).
fof(f64,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f71,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f78,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f79,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f78]) ).
fof(f88,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f89,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f88]) ).
fof(f94,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(f95,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,[],[f94]) ).
fof(f96,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f97,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f96]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f25]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
& sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
& sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) )
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f98]) ).
fof(f102,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f103,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f102]) ).
fof(f106,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f107,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f106]) ).
fof(f125,plain,
( aNaturalNumber0(sK2)
& sdtasdt0(xn,xn) = sdtasdt0(xp,sK2)
& doDivides0(xp,sdtasdt0(xn,xn))
& aNaturalNumber0(sK3)
& xn = sdtasdt0(xp,sK3)
& doDivides0(xp,xn) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2),skolemize(X1,sK3)],[f50]) ).
fof(f126,plain,
( ( ? [X0] :
( aNaturalNumber0(X0)
& sdtasdt0(xm,xm) = sdtpldt0(sdtasdt0(xn,xn),X0) )
& sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) )
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| xm != sdtpldt0(xn,X1) )
& ~ sdtlseqdt0(xn,xm) ) ),
inference(rectify,[],[f58]) ).
fof(f127,plain,
( ( aNaturalNumber0(sK4)
& sdtasdt0(xm,xm) = sdtpldt0(sdtasdt0(xn,xn),sK4)
& sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) )
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| xm != sdtpldt0(xn,X1) )
& ~ sdtlseqdt0(xn,xm) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X0,sK4)],[f126]) ).
fof(f133,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,[],[f89]) ).
fof(f134,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,[],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ( aNaturalNumber0(sK7(X0,X1))
& sdtasdt0(X0,sK7(X0,X1)) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1))],[f134]) ).
fof(f136,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,[],[f95]) ).
fof(f137,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,[],[f136]) ).
fof(f141,plain,
sz00 != xp,
inference(cnf_transformation,[],[f40]) ).
fof(f143,plain,
sz00 != xn,
inference(cnf_transformation,[],[f40]) ).
fof(f144,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f40]) ).
fof(f145,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f40]) ).
fof(f146,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f40]) ).
fof(f154,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(cnf_transformation,[],[f42]) ).
fof(f158,plain,
sz10 != xp,
inference(cnf_transformation,[],[f57]) ).
fof(f162,plain,
doDivides0(xp,sdtasdt0(xn,xn)),
inference(cnf_transformation,[],[f125]) ).
fof(f163,plain,
sdtasdt0(xn,xn) = sdtasdt0(xp,sK2),
inference(cnf_transformation,[],[f125]) ).
fof(f164,plain,
aNaturalNumber0(sK2),
inference(cnf_transformation,[],[f125]) ).
fof(f166,plain,
xn = sdtasdt0(xp,xq),
inference(cnf_transformation,[],[f45]) ).
fof(f167,plain,
aNaturalNumber0(xq),
inference(cnf_transformation,[],[f45]) ).
fof(f168,plain,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
inference(cnf_transformation,[],[f46]) ).
fof(f169,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(xn,xm) ),
inference(cnf_transformation,[],[f127]) ).
fof(f175,plain,
( xn = xm
| ~ sdtlseqdt0(xm,xn) ),
inference(cnf_transformation,[],[f59]) ).
fof(f177,plain,
! [X0,X1] :
( sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f61]) ).
fof(f178,plain,
! [X2,X0,X1] :
( sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f179,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| X1 = X2
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f181,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f64]) ).
fof(f195,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(sz10,X0) = X0 ),
inference(cnf_transformation,[],[f71]) ).
fof(f198,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f202,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f209,plain,
! [X2,X0,X1] :
( doDivides0(X0,X1)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f135]) ).
fof(f214,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,[],[f137]) ).
fof(f215,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f97]) ).
fof(f216,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f218,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| sz00 = X0
| X1 = X2
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f99]) ).
fof(f224,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f103]) ).
fof(f227,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f107]) ).
fof(f246,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f209]) ).
fof(f247,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,[],[f214]) ).
fof(f266,definition,
( spl9_3
<=> sdtlseqdt0(xm,xn) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f268,plain,
( ~ sdtlseqdt0(xm,xn)
| spl9_3 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f270,definition,
( spl9_4
<=> xn = xm ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f272,plain,
( xn = xm
| ~ spl9_4 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f273,plain,
( ~ spl9_3
| spl9_4 ),
inference(avatar_split_clause,[],[f175,f270,f266]) ).
fof(f279,definition,
( spl9_6
<=> sdtlseqdt0(xn,xm) ),
introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition]) ).
fof(f281,plain,
( ~ sdtlseqdt0(xn,xm)
| spl9_6 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f283,definition,
( spl9_7
<=> sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
fof(f285,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f286,plain,
( ~ spl9_6
| spl9_7 ),
inference(avatar_split_clause,[],[f169,f283,f279]) ).
fof(f327,plain,
sz00 = sdtasdt0(xp,sz00),
inference(resolution,[],[f181,f144]) ).
fof(f337,plain,
xp = sdtasdt0(sz10,xp),
inference(resolution,[],[f195,f144]) ).
fof(f381,plain,
( aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK2) ),
inference(superposition,[],[f202,f163]) ).
fof(f387,plain,
( aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK2) ),
inference(forward_subsumption_resolution,[],[f381,f144]) ).
fof(f388,plain,
aNaturalNumber0(sdtasdt0(xn,xn)),
inference(forward_subsumption_resolution,[],[f387,f164]) ).
fof(f406,plain,
( aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) ),
inference(superposition,[],[f202,f168]) ).
fof(f407,plain,
( aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) ),
inference(forward_subsumption_resolution,[],[f406,f144]) ).
fof(f505,plain,
( sdtlseqdt0(sz10,xp)
| sz00 = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(superposition,[],[f215,f337]) ).
fof(f524,plain,
( sdtlseqdt0(sz10,xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sz10) ),
inference(forward_subsumption_resolution,[],[f505,f141]) ).
fof(f535,plain,
( sdtlseqdt0(sz10,xp)
| ~ aNaturalNumber0(sz10) ),
inference(forward_subsumption_resolution,[],[f524,f144]) ).
fof(f556,definition,
( spl9_17
<=> sz00 = xq ),
introduced(definition,[new_symbols(definition,[spl9_17])],[avatar_definition]) ).
fof(f557,plain,
( sz00 != xq
| spl9_17 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( sz00 = xq
| ~ spl9_17 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f561,definition,
( spl9_18
<=> aNaturalNumber0(sdtasdt0(xq,xq)) ),
introduced(definition,[new_symbols(definition,[spl9_18])],[avatar_definition]) ).
fof(f562,plain,
( aNaturalNumber0(sdtasdt0(xq,xq))
| ~ spl9_18 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f563,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| spl9_18 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f565,definition,
( spl9_19
<=> sz00 = sdtasdt0(xq,xq) ),
introduced(definition,[new_symbols(definition,[spl9_19])],[avatar_definition]) ).
fof(f566,plain,
( sz00 != sdtasdt0(xq,xq)
| spl9_19 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f567,plain,
( sz00 = sdtasdt0(xq,xq)
| ~ spl9_19 ),
inference(avatar_component_clause,[],[f565]) ).
fof(f590,plain,
sdtlseqdt0(sz10,xp),
inference(forward_subsumption_resolution,[],[f535,f198]) ).
fof(f690,plain,
( xn = sdtasdt0(xp,sz00)
| ~ spl9_17 ),
inference(superposition,[],[f166,f558]) ).
fof(f697,plain,
( sz00 = xn
| ~ spl9_17 ),
inference(forward_demodulation,[],[f690,f327]) ).
fof(f699,plain,
( $false
| ~ spl9_17 ),
inference(forward_subsumption_resolution,[],[f697,f143]) ).
fof(f700,plain,
~ spl9_17,
inference(avatar_contradiction_clause,[],[f699]) ).
fof(f720,plain,
( doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(superposition,[],[f246,f168]) ).
fof(f751,plain,
( doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(forward_subsumption_resolution,[],[f720,f144]) ).
fof(f1087,definition,
( spl9_41
<=> aNaturalNumber0(sdtasdt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[spl9_41])],[avatar_definition]) ).
fof(f1089,plain,
( aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_41 ),
inference(avatar_component_clause,[],[f1087]) ).
fof(f1090,plain,
( ~ spl9_18
| spl9_41 ),
inference(avatar_split_clause,[],[f407,f1087,f561]) ).
fof(f1097,definition,
( spl9_43
<=> doDivides0(xp,sdtasdt0(xm,xm)) ),
introduced(definition,[new_symbols(definition,[spl9_43])],[avatar_definition]) ).
fof(f1099,plain,
( doDivides0(xp,sdtasdt0(xm,xm))
| ~ spl9_43 ),
inference(avatar_component_clause,[],[f1097]) ).
fof(f1100,plain,
( ~ spl9_41
| ~ spl9_18
| spl9_43 ),
inference(avatar_split_clause,[],[f751,f1097,f561,f1087]) ).
fof(f1107,plain,
( sdtlseqdt0(xn,xm)
| ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn)
| spl9_3 ),
inference(resolution,[],[f268,f224]) ).
fof(f1109,plain,
( ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq)
| spl9_18 ),
inference(resolution,[],[f563,f202]) ).
fof(f1110,plain,
( ~ aNaturalNumber0(xq)
| spl9_18 ),
inference(duplicate_literal_removal,[],[f1109]) ).
fof(f1111,plain,
( $false
| spl9_18 ),
inference(forward_subsumption_resolution,[],[f1110,f167]) ).
fof(f1112,plain,
spl9_18,
inference(avatar_contradiction_clause,[],[f1111]) ).
fof(f1142,plain,
( sdtasdt0(xq,xq) = sdtasdt0(sz10,sdtasdt0(xq,xq))
| ~ spl9_18 ),
inference(resolution,[],[f562,f195]) ).
fof(f1169,plain,
( ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_7 ),
inference(resolution,[],[f285,f227]) ).
fof(f1189,plain,
( sz00 != sz00
| sz00 = xq
| sz00 = xq
| ~ aNaturalNumber0(xq)
| ~ aNaturalNumber0(xq)
| ~ spl9_19 ),
inference(superposition,[],[f177,f567]) ).
fof(f1198,plain,
( sz00 != sz00
| sz00 = xq
| ~ aNaturalNumber0(xq)
| ~ spl9_19 ),
inference(duplicate_literal_removal,[],[f1189]) ).
fof(f1199,plain,
( sz00 = xq
| ~ aNaturalNumber0(xq)
| ~ spl9_19 ),
inference(trivial_inequality_removal,[],[f1198]) ).
fof(f1201,plain,
( ~ aNaturalNumber0(xq)
| spl9_17
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f1199,f557]) ).
fof(f1204,plain,
( $false
| spl9_17
| ~ spl9_19 ),
inference(forward_subsumption_resolution,[],[f1201,f167]) ).
fof(f1205,plain,
( spl9_17
| ~ spl9_19 ),
inference(avatar_contradiction_clause,[],[f1204]) ).
fof(f1263,plain,
( ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_7
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f1169,f1089]) ).
fof(f1267,plain,
( ~ aNaturalNumber0(xm)
| ~ aNaturalNumber0(xn)
| spl9_3
| spl9_6 ),
inference(forward_subsumption_resolution,[],[f1107,f281]) ).
fof(f1270,plain,
( ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ spl9_7
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f1263,f388]) ).
fof(f1272,plain,
( ~ aNaturalNumber0(xn)
| spl9_3
| spl9_6 ),
inference(forward_subsumption_resolution,[],[f1267,f145]) ).
fof(f1277,plain,
( $false
| spl9_3
| spl9_6 ),
inference(forward_subsumption_resolution,[],[f1272,f146]) ).
fof(f1278,plain,
( spl9_3
| spl9_6 ),
inference(avatar_contradiction_clause,[],[f1277]) ).
fof(f1284,definition,
( spl9_51
<=> sdtasdt0(xm,xm) = sdtasdt0(xn,xn) ),
introduced(definition,[new_symbols(definition,[spl9_51])],[avatar_definition]) ).
fof(f1286,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xn,xn)
| ~ spl9_51 ),
inference(avatar_component_clause,[],[f1284]) ).
fof(f1289,definition,
( spl9_52
<=> sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)) ),
introduced(definition,[new_symbols(definition,[spl9_52])],[avatar_definition]) ).
fof(f1291,plain,
( ~ sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| spl9_52 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1292,plain,
( spl9_51
| ~ spl9_52
| ~ spl9_7
| ~ spl9_41 ),
inference(avatar_split_clause,[],[f1270,f1087,f283,f1289,f1284]) ).
fof(f1300,plain,
( sdtasdt0(xn,xn) = sdtasdt0(xp,sdtasdt0(xn,xn))
| ~ spl9_4 ),
inference(superposition,[],[f154,f272]) ).
fof(f1508,plain,
! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(X0,sdtasdt0(xq,xq))
| xp = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp)
| sz00 = sdtasdt0(xq,xq)
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) ),
inference(superposition,[],[f178,f168]) ).
fof(f1517,plain,
! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(X0,sdtasdt0(xq,xq))
| xp = X0
| ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(xq,xq)
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) ),
inference(forward_subsumption_resolution,[],[f1508,f144]) ).
fof(f1537,plain,
( ! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(X0,sdtasdt0(xq,xq))
| xp = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(xq,xq)) )
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f1517,f566]) ).
fof(f1557,plain,
( ! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(X0,sdtasdt0(xq,xq))
| xp = X0
| ~ aNaturalNumber0(X0) )
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f1537,f562]) ).
fof(f1574,plain,
( ! [X0] :
( sdtasdt0(xn,xn) != sdtasdt0(X0,sdtasdt0(xq,xq))
| xp = X0
| ~ aNaturalNumber0(X0) )
| ~ spl9_4
| ~ spl9_18
| spl9_19 ),
inference(forward_demodulation,[],[f1557,f272]) ).
fof(f1611,plain,
! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(xp,X0)
| sdtasdt0(xq,xq) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| sz00 = xp
| ~ aNaturalNumber0(xp) ),
inference(superposition,[],[f179,f168]) ).
fof(f1624,plain,
( ! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(xp,X0)
| sdtasdt0(xq,xq) = X0
| ~ aNaturalNumber0(X0)
| sz00 = xp
| ~ aNaturalNumber0(xp) )
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f1611,f562]) ).
fof(f1644,plain,
( ! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(xp,X0)
| sdtasdt0(xq,xq) = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) )
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f1624,f141]) ).
fof(f1664,plain,
( ! [X0] :
( sdtasdt0(xm,xm) != sdtasdt0(xp,X0)
| sdtasdt0(xq,xq) = X0
| ~ aNaturalNumber0(X0) )
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f1644,f144]) ).
fof(f1939,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(X0,sdtasdt0(xq,xq)),sdtasdt0(xm,xm))
| sz00 = sdtasdt0(xq,xq)
| xp = X0
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) ),
inference(superposition,[],[f216,f168]) ).
fof(f1948,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,sdtasdt0(xq,xq)),sdtasdt0(xm,xm))
| xp = X0
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) )
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f1939,f566]) ).
fof(f1981,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,sdtasdt0(xq,xq)),sdtasdt0(xm,xm))
| xp = X0
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(xp) )
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f1948,f562]) ).
fof(f2014,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,sdtasdt0(xq,xq)),sdtasdt0(xm,xm))
| xp = X0
| ~ sdtlseqdt0(X0,xp)
| ~ aNaturalNumber0(X0) )
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f1981,f144]) ).
fof(f2166,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xp,X0))
| sz00 = xp
| sdtasdt0(xq,xq) = X0
| ~ sdtlseqdt0(sdtasdt0(xq,xq),X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(X0) ),
inference(superposition,[],[f218,f168]) ).
fof(f2223,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xp,X0))
| sdtasdt0(xq,xq) = X0
| ~ sdtlseqdt0(sdtasdt0(xq,xq),X0)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f2166,f141]) ).
fof(f2265,plain,
! [X0] :
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xp,X0))
| sdtasdt0(xq,xq) = X0
| ~ sdtlseqdt0(sdtasdt0(xq,xq),X0)
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f2223,f144]) ).
fof(f2307,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xp,X0))
| sdtasdt0(xq,xq) = X0
| ~ sdtlseqdt0(sdtasdt0(xq,xq),X0)
| ~ aNaturalNumber0(X0) )
| ~ spl9_18 ),
inference(forward_subsumption_resolution,[],[f2265,f562]) ).
fof(f2452,plain,
( ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sz00 = xp
| sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(superposition,[],[f247,f154]) ).
fof(f2453,plain,
( ~ doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xq,xq))
| sz00 = xp
| sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(superposition,[],[f247,f168]) ).
fof(f2454,plain,
( ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| sz00 = xp
| sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_4 ),
inference(superposition,[],[f247,f1300]) ).
fof(f2456,plain,
( ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sK2)
| sz00 = xp
| sK2 = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(superposition,[],[f247,f163]) ).
fof(f2468,plain,
( ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| sz00 = xp
| sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ spl9_4 ),
inference(duplicate_literal_removal,[],[f2454]) ).
fof(f2484,plain,
( ~ aNaturalNumber0(sK2)
| sz00 = xp
| sK2 = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_subsumption_resolution,[],[f2456,f162]) ).
fof(f2485,plain,
( ~ aNaturalNumber0(sdtasdt0(xn,xn))
| sz00 = xp
| sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f2468,f162]) ).
fof(f2486,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| sz00 = xp
| sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2453,f1099]) ).
fof(f2487,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sz00 = xp
| sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_subsumption_resolution,[],[f2452,f162]) ).
fof(f2503,plain,
( sz00 = xp
| sK2 = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_subsumption_resolution,[],[f2484,f164]) ).
fof(f2504,plain,
( sz00 = xp
| sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f2485,f388]) ).
fof(f2505,plain,
( sz00 = xp
| sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2486,f562]) ).
fof(f2506,plain,
( sz00 = xp
| sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f2487,f1089]) ).
fof(f2521,plain,
( sK2 = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_subsumption_resolution,[],[f2503,f141]) ).
fof(f2522,plain,
( sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f2504,f141]) ).
fof(f2523,plain,
( sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2505,f141]) ).
fof(f2524,plain,
( sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f2506,f141]) ).
fof(f2539,plain,
( sK2 = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(forward_subsumption_resolution,[],[f2521,f144]) ).
fof(f2540,plain,
( sdtasdt0(xn,xn) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ spl9_4 ),
inference(forward_subsumption_resolution,[],[f2522,f144]) ).
fof(f2541,plain,
( sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2523,f144]) ).
fof(f2542,plain,
( sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f2524,f144]) ).
fof(f2553,plain,
sK2 = sdtsldt0(sdtasdt0(xn,xn),xp),
inference(forward_subsumption_resolution,[],[f2539,f388]) ).
fof(f2554,plain,
( sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xm,xm),xp)
| ~ spl9_18
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2541,f1089]) ).
fof(f2555,plain,
( sdtasdt0(xm,xm) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f2542,f388]) ).
fof(f2557,plain,
( sdtasdt0(xq,xq) = sdtsldt0(sdtasdt0(xn,xn),xp)
| ~ spl9_4
| ~ spl9_18
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_demodulation,[],[f2554,f272]) ).
fof(f2559,plain,
( sdtasdt0(xn,xn) = sdtasdt0(xq,xq)
| ~ spl9_4
| ~ spl9_18
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_demodulation,[],[f2557,f2540]) ).
fof(f2911,plain,
( sdtasdt0(xn,xn) != sdtasdt0(xq,xq)
| sz10 = xp
| ~ aNaturalNumber0(sz10)
| ~ spl9_4
| ~ spl9_18
| spl9_19 ),
inference(superposition,[],[f1574,f1142]) ).
fof(f2912,plain,
( sz10 = xp
| ~ aNaturalNumber0(sz10)
| ~ spl9_4
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2911,f2559]) ).
fof(f2913,plain,
( ~ aNaturalNumber0(sz10)
| ~ spl9_4
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2912,f158]) ).
fof(f2914,plain,
( $false
| ~ spl9_4
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_43 ),
inference(forward_subsumption_resolution,[],[f2913,f198]) ).
fof(f2915,plain,
( ~ spl9_4
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_43 ),
inference(avatar_contradiction_clause,[],[f2914]) ).
fof(f2942,plain,
( sdtasdt0(xm,xm) = sK2
| ~ spl9_41 ),
inference(forward_demodulation,[],[f2555,f2553]) ).
fof(f3370,plain,
( ~ sdtlseqdt0(sK2,sdtasdt0(xn,xn))
| ~ spl9_41
| spl9_52 ),
inference(forward_demodulation,[],[f1291,f2942]) ).
fof(f3376,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xq,xq)
| sz10 = xp
| ~ aNaturalNumber0(sz10)
| ~ spl9_18
| spl9_19 ),
inference(superposition,[],[f1557,f1142]) ).
fof(f3377,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xq,xq)
| ~ aNaturalNumber0(sz10)
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f3376,f158]) ).
fof(f3378,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xq,xq)
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f3377,f198]) ).
fof(f3379,plain,
( sdtasdt0(xq,xq) != sK2
| ~ spl9_18
| spl9_19
| ~ spl9_41 ),
inference(forward_demodulation,[],[f3378,f2942]) ).
fof(f3383,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xn,xn)
| sdtasdt0(xq,xq) = sK2
| ~ aNaturalNumber0(sK2)
| ~ spl9_18 ),
inference(superposition,[],[f1664,f163]) ).
fof(f3386,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xn,xn)
| ~ aNaturalNumber0(sK2)
| ~ spl9_18
| spl9_19
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f3383,f3379]) ).
fof(f3390,plain,
( sdtasdt0(xm,xm) != sdtasdt0(xn,xn)
| ~ spl9_18
| spl9_19
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f3386,f164]) ).
fof(f3394,plain,
( sdtasdt0(xn,xn) != sK2
| ~ spl9_18
| spl9_19
| ~ spl9_41 ),
inference(forward_demodulation,[],[f3390,f2942]) ).
fof(f3472,plain,
( sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| sz10 = xp
| ~ sdtlseqdt0(sz10,xp)
| ~ aNaturalNumber0(sz10)
| ~ spl9_18
| spl9_19 ),
inference(superposition,[],[f2014,f1142]) ).
fof(f3473,plain,
( sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(sz10,xp)
| ~ aNaturalNumber0(sz10)
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f3472,f158]) ).
fof(f3479,plain,
( sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sz10)
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f3473,f590]) ).
fof(f3485,plain,
( sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| spl9_19 ),
inference(forward_subsumption_resolution,[],[f3479,f198]) ).
fof(f3491,plain,
( sdtlseqdt0(sdtasdt0(xq,xq),sK2)
| ~ spl9_18
| spl9_19
| ~ spl9_41 ),
inference(forward_demodulation,[],[f3485,f2942]) ).
fof(f3620,plain,
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xq,xq)
| ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ spl9_18 ),
inference(superposition,[],[f2307,f154]) ).
fof(f3627,plain,
( sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xq,xq)
| ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_41 ),
inference(forward_subsumption_resolution,[],[f3620,f1089]) ).
fof(f3636,plain,
( sdtlseqdt0(sK2,sdtasdt0(xn,xn))
| sdtasdt0(xm,xm) = sdtasdt0(xq,xq)
| ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_41 ),
inference(forward_demodulation,[],[f3627,f2942]) ).
fof(f3670,plain,
( sdtasdt0(xn,xn) = sK2
| ~ spl9_41
| ~ spl9_51 ),
inference(forward_demodulation,[],[f1286,f2942]) ).
fof(f3702,plain,
( $false
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_51 ),
inference(forward_subsumption_resolution,[],[f3670,f3394]) ).
fof(f3703,plain,
( ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_51 ),
inference(avatar_contradiction_clause,[],[f3702]) ).
fof(f3781,plain,
( sdtasdt0(xm,xm) = sdtasdt0(xq,xq)
| ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_41
| spl9_52 ),
inference(forward_subsumption_resolution,[],[f3636,f3370]) ).
fof(f3795,plain,
( sdtasdt0(xq,xq) = sK2
| ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| ~ spl9_41
| spl9_52 ),
inference(forward_demodulation,[],[f3781,f2942]) ).
fof(f3799,plain,
( ~ sdtlseqdt0(sdtasdt0(xq,xq),sdtasdt0(xm,xm))
| ~ spl9_18
| spl9_19
| ~ spl9_41
| spl9_52 ),
inference(forward_subsumption_resolution,[],[f3795,f3379]) ).
fof(f3800,plain,
( ~ sdtlseqdt0(sdtasdt0(xq,xq),sK2)
| ~ spl9_18
| spl9_19
| ~ spl9_41
| spl9_52 ),
inference(forward_demodulation,[],[f3799,f2942]) ).
fof(f3801,plain,
( $false
| ~ spl9_18
| spl9_19
| ~ spl9_41
| spl9_52 ),
inference(forward_subsumption_resolution,[],[f3800,f3491]) ).
fof(f3802,plain,
( ~ spl9_18
| spl9_19
| ~ spl9_41
| spl9_52 ),
inference(avatar_contradiction_clause,[],[f3801]) ).
cnf(s3,plain,
( ~ spl9_3
| spl9_4 ),
inference(sat_conversion,[],[f273]) ).
cnf(s5,plain,
( ~ spl9_6
| spl9_7 ),
inference(sat_conversion,[],[f286]) ).
cnf(s28,plain,
~ spl9_17,
inference(sat_conversion,[],[f700]) ).
cnf(s44,plain,
( ~ spl9_18
| spl9_41 ),
inference(sat_conversion,[],[f1090]) ).
cnf(s46,plain,
( ~ spl9_18
| ~ spl9_41
| spl9_43 ),
inference(sat_conversion,[],[f1100]) ).
cnf(s48,plain,
spl9_18,
inference(sat_conversion,[],[f1112]) ).
cnf(s50,plain,
( spl9_17
| ~ spl9_19 ),
inference(sat_conversion,[],[f1205]) ).
cnf(s55,plain,
( spl9_3
| spl9_6 ),
inference(sat_conversion,[],[f1278]) ).
cnf(s57,plain,
( ~ spl9_7
| ~ spl9_41
| spl9_51
| ~ spl9_52 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s70,plain,
( ~ spl9_4
| ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_43 ),
inference(sat_conversion,[],[f2915]) ).
cnf(s93,plain,
( ~ spl9_18
| spl9_19
| ~ spl9_41
| ~ spl9_51 ),
inference(sat_conversion,[],[f3703]) ).
cnf(s108,plain,
( ~ spl9_18
| spl9_19
| ~ spl9_41
| spl9_52 ),
inference(sat_conversion,[],[f3802]) ).
cnf(s110,plain,
( ~ spl9_41
| spl9_43 ),
inference(rat,[],[s46,s48]) ).
cnf(s112,plain,
spl9_41,
inference(rat,[],[s44,s48]) ).
cnf(s113,plain,
spl9_43,
inference(rat,[],[s110,s112]) ).
cnf(s120,plain,
~ spl9_19,
inference(rat,[],[s50,s28]) ).
cnf(s121,plain,
spl9_52,
inference(rat,[],[s108,s112,s48,s120]) ).
cnf(s122,plain,
~ spl9_51,
inference(rat,[],[s93,s112,s48,s120]) ).
cnf(s123,plain,
~ spl9_4,
inference(rat,[],[s70,s113,s112,s48,s120]) ).
cnf(s126,plain,
~ spl9_7,
inference(rat,[],[s57,s121,s112,s122]) ).
cnf(s135,plain,
~ spl9_6,
inference(rat,[],[s5,s126]) ).
cnf(s136,plain,
spl9_3,
inference(rat,[],[s55,s135]) ).
cnf(s138,plain,
$false,
inference(rat,[],[s3,s123,s136]) ).
fof(f3803,plain,
$false,
inference(avatar_sat_refutation,[],[s138]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n009.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 20:21:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.73/1.34 % (2368633)Detected formulas, will run a generic FOF schedule.
% 2.73/1.34 % (2368643)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1120914596:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.73/1.34 % (2368640)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=1050384328:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.73/1.34 % (2368638)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=794702193:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.73/1.34 % (2368641)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2756240388:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.73/1.34 % (2368639)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=2559189787:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.73/1.34 % (2368644)dis-21_1_sil=8000:lcm=predicate:random_seed=2783541315:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.73/1.34 % (2368642)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2844466542:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.73/1.34 % (2368643)Instruction limit reached!
% 2.73/1.34 % (2368643)------------------------------
% 2.73/1.34 % (2368643)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.73/1.34 % (2368643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/1.34 % (2368643)CaDiCaL version: 2.1.3
% 2.73/1.34 % (2368643)Termination reason: Instruction limit
% 2.73/1.34 % (2368643)Termination phase: Saturation
% 2.73/1.34 % (2368643)Time elapsed: 0.049 s
% 2.73/1.34 % (2368643)Peak memory usage: 90 MB
% 2.73/1.34 % (2368643)Instructions burned: 140 (million)
% 2.73/1.34 % (2368641)Instruction limit reached!
% 2.73/1.34 % (2368641)------------------------------
% 2.73/1.34 % (2368641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.73/1.34 % (2368641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/1.34 % (2368641)CaDiCaL version: 2.1.3
% 2.73/1.34 % (2368641)Termination reason: Instruction limit
% 2.73/1.34 % (2368641)Termination phase: Saturation
% 2.73/1.34 % (2368641)Time elapsed: 0.059 s
% 2.73/1.34 % (2368641)Peak memory usage: 89 MB
% 2.73/1.34 % (2368641)Instructions burned: 109 (million)
% 2.73/1.34 % (2368642)Instruction limit reached!
% 2.73/1.34 % (2368642)------------------------------
% 2.73/1.34 % (2368642)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.73/1.34 % (2368642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/1.34 % (2368642)CaDiCaL version: 2.1.3
% 2.73/1.34 % (2368642)Termination reason: Instruction limit
% 2.73/1.34 % (2368642)Termination phase: Saturation
% 2.73/1.34 % (2368642)Time elapsed: 0.069 s
% 2.73/1.34 % (2368642)Peak memory usage: 88 MB
% 2.73/1.34 % (2368642)Instructions burned: 121 (million)
% 2.73/1.34 % (2368644)Instruction limit reached!
% 2.73/1.34 % (2368644)------------------------------
% 2.73/1.34 % (2368644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.73/1.34 % (2368644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/1.34 % (2368644)CaDiCaL version: 2.1.3
% 2.73/1.34 % (2368644)Termination reason: Instruction limit
% 2.73/1.34 % (2368644)Termination phase: Saturation
% 2.73/1.34 % (2368644)Time elapsed: 0.077 s
% 2.73/1.34 % (2368644)Peak memory usage: 91 MB
% 2.73/1.34 % (2368644)Instructions burned: 130 (million)
% 2.73/1.34 % (2368652)lrs+10_1_sil=8000:sp=occurrence:random_seed=1796996829:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 2.73/1.34 % (2368652)First to succeed.
% 2.73/1.34 % (2368652)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2368633"
% 2.73/1.34 % (2368653)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2541163440:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 2.73/1.34 % (2368654)lrs+1011_1_sil=32000:sp=occurrence:random_seed=856778974:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 2.73/1.34 % (2368655)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=4202111934:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 2.73/1.34 % (2368653)Instruction limit reached!
% 2.73/1.34 % (2368653)------------------------------
% 2.73/1.34 % (2368653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.73/1.34 % (2368653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.73/1.34 % (2368653)CaDiCaL version: 2.1.3
% 2.73/1.34 % (2368653)Termination reason: Instruction limit
% 2.73/1.34 % (2368653)Termination phase: Saturation
% 2.73/1.34 % (2368653)Time elapsed: 0.077 s
% 2.73/1.34 % (2368653)Peak memory usage: 91 MB
% 2.73/1.34 % (2368653)Instructions burned: 159 (million)
% 2.73/1.34 % (2368652)Refutation found. Thanks to Tanya!
% 2.73/1.34 % SZS status Theorem for theBenchmark
% 2.73/1.34 % SZS output start Proof for theBenchmark
% See solution above
% 4.04/1.47 % (2368652)------------------------------
% 4.04/1.47 % (2368652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.04/1.47 % (2368652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.04/1.47 % (2368652)CaDiCaL version: 2.1.3
% 4.04/1.47 % (2368652)Termination reason: Refutation
% 4.04/1.47 % (2368652)Time elapsed: 0.047 s
% 4.04/1.47 % (2368652)Peak memory usage: 91 MB
% 4.04/1.47 % (2368652)Instructions burned: 149 (million)
% 4.04/1.47 % (2368652)------------------------------
% 4.04/1.47 % (2368652)------------------------------
% 4.04/1.47 % (2368633)Success in time 0.499 s
% 4.04/1.47 % Vampire exiting
%------------------------------------------------------------------------------