%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM512+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:24:37 PM UTC 2026
% Result : Theorem 46.83s 7.12s
% Output : Refutation 46.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 17
% Syntax : Number of formulae : 122 ( 47 unt; 6 def)
% Number of atoms : 439 ( 205 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 471 ( 154 ~; 145 |; 155 &)
% ( 3 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 17 con; 0-2 aty)
% Number of variables : 95 ( 76 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
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(f10,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulAsso) ).
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(f39,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
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(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(f53,axiom,
( ~ ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
=> sdtsldt0(xn,xr) = xn )
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtsldt0(xn,xr),X0) = xn )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2504) ).
fof(f54,conjecture,
( ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
=> sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm) )
& ( ( aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) )
=> sdtasdt0(xn,xm) = sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f55,negated_conjecture,
~ ( ( ( aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
=> sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr) = sdtasdt0(xn,xm) )
& ( ( aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) )
=> sdtasdt0(xn,xm) = sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr) ) ),
inference(negated_conjecture,[status(cth)],[f54]) ).
fof(f59,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(f61,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(f62,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(f66,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f67,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f66]) ).
fof(f73,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f9]) ).
fof(f74,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f10]) ).
fof(f76,plain,
! [X0,X1,X2] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f75]) ).
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(ennf_transformation,[],[f31]) ).
fof(f113,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,[],[f112]) ).
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(ennf_transformation,[],[f59]) ).
fof(f131,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,[],[f130]) ).
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(ennf_transformation,[],[f61]) ).
fof(f136,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,[],[f135]) ).
fof(f137,plain,
( xn != sdtsldt0(xn,xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtsldt0(xn,xr),X0) = xn )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(ennf_transformation,[],[f53]) ).
fof(f138,plain,
( xn != sdtsldt0(xn,xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& ? [X0] :
( aNaturalNumber0(X0)
& sdtpldt0(sdtsldt0(xn,xr),X0) = xn )
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(flattening,[],[f137]) ).
fof(f139,plain,
( ( sdtasdt0(xn,xm) != sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
| ( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)
& aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) ) ),
inference(ennf_transformation,[],[f55]) ).
fof(f140,plain,
( ( sdtasdt0(xn,xm) != sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
| ( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)
& aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) ) ),
inference(flattening,[],[f139]) ).
fof(f146,definition,
( ( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)
& aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) )
| ~ sP3 ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f147,plain,
( ( sdtasdt0(xn,xm) != sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr)) )
| sP3 ),
inference(definition_folding,[],[f140,f146]) ).
fof(f156,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,[],[f113]) ).
fof(f157,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,[],[f156]) ).
fof(f171,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(sK12)
& sdtasdt0(xn,xm) = sdtasdt0(xp,sK12)
& doDivides0(xp,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12)],[f131]) ).
fof(f173,plain,
( aNaturalNumber0(xr)
& aNaturalNumber0(sK15)
& xk = sdtasdt0(xr,sK15)
& 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,[sK15]),skolemize(X0,sK15)],[f136]) ).
fof(f174,plain,
( aNaturalNumber0(sK16)
& xk = sdtpldt0(xr,sK16)
& aNaturalNumber0(sK17)
& sdtasdt0(xn,xm) = sdtasdt0(xr,sK17)
& doDivides0(xr,sdtasdt0(xn,xm)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16,sK17]),skolemize(X0,sK16),skolemize(X1,sK17)],[f62]) ).
fof(f181,plain,
( xn != sdtsldt0(xn,xr)
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sdtsldt0(xn,xr))
& xn = sdtasdt0(xr,sdtsldt0(xn,xr))
& aNaturalNumber0(sK22)
& xn = sdtpldt0(sdtsldt0(xn,xr),sK22)
& sdtlseqdt0(sdtsldt0(xn,xr),xn) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X0,sK22)],[f138]) ).
fof(f182,plain,
( ( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)
& aNaturalNumber0(sdtsldt0(sdtasdt0(xp,xk),xr))
& sdtasdt0(xp,xk) = sdtasdt0(xr,sdtsldt0(sdtasdt0(xp,xk),xr)) )
| ~ sP3 ),
inference(nnf_transformation,[],[f146]) ).
fof(f187,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f67]) ).
fof(f192,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f193,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) ),
inference(cnf_transformation,[],[f76]) ).
fof(f233,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X2) = X1
| sdtsldt0(X1,X0) != X2
| sz00 = X0
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f157]) ).
fof(f235,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,[],[f157]) ).
fof(f251,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f39]) ).
fof(f252,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f39]) ).
fof(f253,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f39]) ).
fof(f270,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(cnf_transformation,[],[f171]) ).
fof(f277,plain,
sz00 != xp,
inference(cnf_transformation,[],[f171]) ).
fof(f290,plain,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
inference(cnf_transformation,[],[f45]) ).
fof(f301,plain,
sz00 != xr,
inference(cnf_transformation,[],[f173]) ).
fof(f305,plain,
aNaturalNumber0(xr),
inference(cnf_transformation,[],[f173]) ).
fof(f306,plain,
doDivides0(xr,sdtasdt0(xn,xm)),
inference(cnf_transformation,[],[f174]) ).
fof(f307,plain,
sdtasdt0(xn,xm) = sdtasdt0(xr,sK17),
inference(cnf_transformation,[],[f174]) ).
fof(f308,plain,
aNaturalNumber0(sK17),
inference(cnf_transformation,[],[f174]) ).
fof(f327,plain,
xn = sdtasdt0(xr,sdtsldt0(xn,xr)),
inference(cnf_transformation,[],[f181]) ).
fof(f328,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(cnf_transformation,[],[f181]) ).
fof(f334,plain,
( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sdtasdt0(xp,xk),xr),xr)
| ~ sP3 ),
inference(cnf_transformation,[],[f182]) ).
fof(f336,plain,
( aNaturalNumber0(sdtsldt0(xn,xr))
| sP3 ),
inference(cnf_transformation,[],[f147]) ).
fof(f337,plain,
( sdtasdt0(xn,xm) != sdtasdt0(sdtasdt0(sdtsldt0(xn,xr),xm),xr)
| sP3 ),
inference(cnf_transformation,[],[f147]) ).
fof(f345,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,[],[f235]) ).
fof(f347,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(equality_resolution,[],[f233]) ).
fof(f350,definition,
sF23 = sdtasdt0(xn,xm),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f351,plain,
sdtasdt0(xn,xm) = sF23,
inference(reorient_equations,[],[f350]) ).
fof(f352,definition,
sF24 = sdtsldt0(xn,xr),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f353,plain,
sdtsldt0(xn,xr) = sF24,
inference(reorient_equations,[],[f352]) ).
fof(f354,definition,
sF25 = sdtasdt0(sF24,xm),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f355,plain,
sdtasdt0(sF24,xm) = sF25,
inference(reorient_equations,[],[f354]) ).
fof(f356,definition,
sF26 = sdtasdt0(sF25,xr),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f357,plain,
sdtasdt0(sF25,xr) = sF26,
inference(reorient_equations,[],[f356]) ).
fof(f358,plain,
( sF23 != sF26
| sP3 ),
inference(definition_folding,[],[f337,f357,f355,f353,f351]) ).
fof(f359,plain,
( aNaturalNumber0(sF24)
| sP3 ),
inference(definition_folding,[],[f336,f353]) ).
fof(f360,definition,
sF27 = sdtasdt0(xr,sF24),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f361,plain,
sdtasdt0(xr,sF24) = sF27,
inference(reorient_equations,[],[f360]) ).
fof(f365,plain,
doDivides0(xp,sF23),
inference(superposition,[],[f270,f351]) ).
fof(f368,plain,
aNaturalNumber0(sF24),
inference(superposition,[],[f328,f353]) ).
fof(f370,plain,
xk = sdtsldt0(sF23,xp),
inference(superposition,[],[f290,f351]) ).
fof(f372,plain,
xn = sdtasdt0(xr,sF24),
inference(superposition,[],[f327,f353]) ).
fof(f512,plain,
xn = sF27,
inference(superposition,[],[f361,f372]) ).
fof(f552,plain,
( aNaturalNumber0(sF23)
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm) ),
inference(superposition,[],[f187,f351]) ).
fof(f569,plain,
( aNaturalNumber0(sF23)
| ~ aNaturalNumber0(xm) ),
inference(forward_subsumption_resolution,[],[f552,f253]) ).
fof(f575,plain,
aNaturalNumber0(sF23),
inference(forward_subsumption_resolution,[],[f569,f252]) ).
fof(f672,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xn) = sdtasdt0(xn,X0) ),
inference(resolution,[],[f192,f253]) ).
fof(f673,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xm) = sdtasdt0(xm,X0) ),
inference(resolution,[],[f192,f252]) ).
fof(f676,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(xr,X0) = sdtasdt0(X0,xr) ),
inference(resolution,[],[f192,f305]) ).
fof(f1610,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,X1),xr) = sdtasdt0(X0,sdtasdt0(X1,xr)) ),
inference(resolution,[],[f193,f305]) ).
fof(f1718,plain,
( sz00 = xp
| sF23 = sdtasdt0(xp,sdtsldt0(sF23,xp))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sF23) ),
inference(resolution,[],[f347,f365]) ).
fof(f1738,plain,
( sF23 = sdtasdt0(xp,sdtsldt0(sF23,xp))
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sF23) ),
inference(forward_subsumption_resolution,[],[f1718,f277]) ).
fof(f1746,plain,
( sF23 = sdtasdt0(xp,sdtsldt0(sF23,xp))
| ~ aNaturalNumber0(sF23) ),
inference(forward_subsumption_resolution,[],[f1738,f251]) ).
fof(f1752,plain,
sF23 = sdtasdt0(xp,sdtsldt0(sF23,xp)),
inference(forward_subsumption_resolution,[],[f1746,f575]) ).
fof(f1754,plain,
sdtasdt0(xp,xk) = sF23,
inference(forward_demodulation,[],[f1752,f370]) ).
fof(f3125,plain,
( ~ doDivides0(xr,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(sK17)
| sz00 = xr
| sK17 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(superposition,[],[f345,f307]) ).
fof(f3136,plain,
( ~ aNaturalNumber0(sK17)
| sz00 = xr
| sK17 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f3125,f306]) ).
fof(f3145,plain,
( sz00 = xr
| sK17 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f3136,f308]) ).
fof(f3153,plain,
( sK17 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f3145,f301]) ).
fof(f3161,plain,
( sK17 = sdtsldt0(sdtasdt0(xn,xm),xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f3153,f305]) ).
fof(f3167,plain,
( sK17 = sdtsldt0(sF23,xr)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_demodulation,[],[f3161,f351]) ).
fof(f3172,plain,
( ~ aNaturalNumber0(sF23)
| sK17 = sdtsldt0(sF23,xr) ),
inference(forward_demodulation,[],[f3167,f351]) ).
fof(f3174,plain,
sK17 = sdtsldt0(sF23,xr),
inference(forward_subsumption_resolution,[],[f3172,f575]) ).
fof(f13634,plain,
sdtasdt0(xn,xm) = sdtasdt0(xm,xn),
inference(resolution,[],[f672,f252]) ).
fof(f13663,plain,
sF23 = sdtasdt0(xm,xn),
inference(forward_demodulation,[],[f13634,f351]) ).
fof(f13714,plain,
sdtasdt0(sF24,xm) = sdtasdt0(xm,sF24),
inference(resolution,[],[f673,f368]) ).
fof(f13719,plain,
sF25 = sdtasdt0(xm,sF24),
inference(forward_demodulation,[],[f13714,f355]) ).
fof(f13965,plain,
sdtasdt0(xr,sK17) = sdtasdt0(sK17,xr),
inference(resolution,[],[f676,f308]) ).
fof(f13972,plain,
sdtasdt0(xr,sF24) = sdtasdt0(sF24,xr),
inference(resolution,[],[f676,f368]) ).
fof(f13978,plain,
sF27 = sdtasdt0(sF24,xr),
inference(forward_demodulation,[],[f13972,f361]) ).
fof(f13980,plain,
sdtasdt0(xn,xm) = sdtasdt0(sK17,xr),
inference(forward_demodulation,[],[f13965,f307]) ).
fof(f13989,plain,
xn = sdtasdt0(sF24,xr),
inference(forward_demodulation,[],[f13978,f512]) ).
fof(f13991,plain,
sF23 = sdtasdt0(sK17,xr),
inference(forward_demodulation,[],[f13980,f351]) ).
fof(f24353,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(sdtasdt0(X0,sF24),xr) = sdtasdt0(X0,sdtasdt0(sF24,xr))
| sP3 ),
inference(resolution,[],[f1610,f359]) ).
fof(f24358,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,xn) = sdtasdt0(sdtasdt0(X0,sF24),xr)
| sP3 ),
inference(forward_demodulation,[],[f24353,f13989]) ).
fof(f36770,plain,
( sdtasdt0(xm,xn) = sdtasdt0(sdtasdt0(xm,sF24),xr)
| sP3 ),
inference(resolution,[],[f24358,f252]) ).
fof(f36815,plain,
( sdtasdt0(sF25,xr) = sdtasdt0(xm,xn)
| sP3 ),
inference(forward_demodulation,[],[f36770,f13719]) ).
fof(f36832,plain,
( sF23 = sdtasdt0(sF25,xr)
| sP3 ),
inference(forward_demodulation,[],[f36815,f13663]) ).
fof(f36837,plain,
( sF23 = sF26
| sP3 ),
inference(forward_demodulation,[],[f36832,f357]) ).
fof(f36838,plain,
sP3,
inference(forward_subsumption_resolution,[],[f36837,f358]) ).
fof(f87775,plain,
( sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sF23,xr),xr)
| ~ sP3 ),
inference(superposition,[],[f334,f1754]) ).
fof(f87888,plain,
sdtasdt0(xn,xm) != sdtasdt0(sdtsldt0(sF23,xr),xr),
inference(forward_subsumption_resolution,[],[f87775,f36838]) ).
fof(f87901,plain,
sdtasdt0(xn,xm) != sdtasdt0(sK17,xr),
inference(forward_demodulation,[],[f87888,f3174]) ).
fof(f87914,plain,
sdtasdt0(xn,xm) != sF23,
inference(forward_demodulation,[],[f87901,f13991]) ).
fof(f87924,plain,
$false,
inference(forward_subsumption_resolution,[],[f87914,f351]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM512+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 20:19:22 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.26/2.38 % (3849466)Will run a generic schedule for satisfiability detection.
% 13.26/2.38 % (3849474)dis+10_1_sil=32000:sp=arity:random_seed=680651671:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.26/2.38 % (3849472)% WARNING: option uhcvi not known.
% 13.26/2.38 % (3849471)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2774171940_2999 on theBenchmark for (2999ds/0Mi)
% 13.26/2.38 % (3849472)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3526313320:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.26/2.38 % (3849473)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1445939735:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.26/2.38 % (3849475)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3794105122:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.26/2.38 % (3849477)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1386431042:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.26/2.38 % (3849476)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3030378474:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.38 % Detected minimum model sizes of [4]
% 13.26/2.38 % Detected maximum model sizes of [max]
% 13.26/2.38 % TRYING [4]
% 13.26/2.38 % (3849474)Instruction limit reached!
% 13.26/2.38 % (3849474)------------------------------
% 13.26/2.38 % (3849474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.38 % (3849474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.38 % (3849474)CaDiCaL version: 2.1.3
% 13.26/2.38 % (3849474)Termination reason: Instruction limit
% 13.26/2.38 % (3849474)Termination phase: Saturation
% 13.26/2.38 % (3849474)Time elapsed: 0.031 s
% 13.26/2.38 % (3849474)Peak memory usage: 13 MB
% 13.26/2.38 % (3849474)Instructions burned: 103 (million)
% 13.26/2.38 % (3849485)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1441291706:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.26/2.38 % Detected minimum model sizes of [4]
% 13.26/2.38 % Detected maximum model sizes of [max]
% 13.26/2.38 % TRYING [4]
% 13.26/2.38 % TRYING [5]
% 13.26/2.38 % TRYING [5]
% 13.26/2.38 % (3849475)Instruction limit reached!
% 13.26/2.38 % (3849475)------------------------------
% 13.26/2.38 % (3849475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.38 % (3849475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.38 % (3849475)CaDiCaL version: 2.1.3
% 13.26/2.38 % (3849475)Termination reason: Instruction limit
% 13.26/2.38 % (3849475)Termination phase: Saturation
% 13.26/2.38 % (3849475)Time elapsed: 0.062 s
% 13.26/2.38 % (3849475)Peak memory usage: 13 MB
% 13.26/2.38 % (3849475)Instructions burned: 117 (million)
% 13.26/2.38 % (3849476)Instruction limit reached!
% 13.26/2.38 % (3849476)------------------------------
% 13.26/2.38 % (3849476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.38 % (3849476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.38 % (3849476)CaDiCaL version: 2.1.3
% 13.26/2.38 % (3849476)Termination reason: Instruction limit
% 13.26/2.38 % (3849476)Termination phase: Saturation
% 13.26/2.38 % (3849476)Time elapsed: 0.065 s
% 13.26/2.38 % (3849476)Peak memory usage: 13 MB
% 13.26/2.38 % (3849476)Instructions burned: 131 (million)
% 13.26/2.38 % (3849487)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2836524855:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 13.26/2.38 % (3849488)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3030446650:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.26/2.38 % (3849477)Instruction limit reached!
% 13.26/2.38 % (3849477)------------------------------
% 13.26/2.38 % (3849477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.26/2.38 % (3849477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.26/2.38 % (3849477)CaDiCaL version: 2.1.3
% 13.26/2.38 % (3849477)Termination reason: Instruction limit
% 13.26/2.38 % (3849477)Termination phase: Saturation
% 13.26/2.38 % (3849477)Time elapsed: 0.095 s
% 13.26/2.38 % (3849477)Peak memory usage: 15 MB
% 13.26/2.38 % (3849477)Instructions burned: 160 (million)
% 13.26/2.38 % TRYING [6]
% 13.26/2.38 % (3849491)ott-21_1_sil=16000:fs=off:random_seed=3924825235:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.26/2.38 % TRYING [6]
% 13.26/2.38 % (3849487)Instruction limit reached!
% 13.26/2.38 % (3849487)------------------------------
% 34.47/5.30 % (3849487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849487)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849487)Termination reason: Instruction limit
% 34.47/5.30 % (3849487)Termination phase: Saturation
% 34.47/5.30 % (3849487)Time elapsed: 0.062 s
% 34.47/5.30 % (3849487)Peak memory usage: 12 MB
% 34.47/5.30 % (3849487)Instructions burned: 131 (million)
% 34.47/5.30 % (3849493)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3991516592:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 34.47/5.30 % (3849485)Instruction limit reached!
% 34.47/5.30 % (3849485)------------------------------
% 34.47/5.30 % (3849485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849485)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849485)Termination reason: Instruction limit
% 34.47/5.30 % (3849485)Termination phase: Finite model building constraint generation
% 34.47/5.30 % (3849485)Time elapsed: 0.138 s
% 34.47/5.30 % (3849485)Peak memory usage: 32 MB
% 34.47/5.30 % (3849485)Instructions burned: 718 (million)
% 34.47/5.30 % (3849495)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3655589567:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.47/5.30 % Detected minimum model sizes of [4]
% 34.47/5.30 % Detected maximum model sizes of [max]
% 34.47/5.30 % TRYING [4]
% 34.47/5.30 % (3849491)Instruction limit reached!
% 34.47/5.30 % (3849491)------------------------------
% 34.47/5.30 % (3849491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849491)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849491)Termination reason: Instruction limit
% 34.47/5.30 % (3849491)Termination phase: Saturation
% 34.47/5.30 % (3849491)Time elapsed: 0.092 s
% 34.47/5.30 % (3849491)Peak memory usage: 13 MB
% 34.47/5.30 % (3849491)Instructions burned: 182 (million)
% 34.47/5.30 % (3849497)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1950617639:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 34.47/5.30 % TRYING [5]
% 34.47/5.30 % TRYING [7]
% 34.47/5.30 % (3849495)Instruction limit reached!
% 34.47/5.30 % (3849495)------------------------------
% 34.47/5.30 % (3849495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849495)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849495)Termination reason: Instruction limit
% 34.47/5.30 % (3849495)Termination phase: Finite model building SAT solving
% 34.47/5.30 % (3849495)Time elapsed: 0.187 s
% 34.47/5.30 % (3849495)Peak memory usage: 24 MB
% 34.47/5.30 % (3849495)Instructions burned: 868 (million)
% 34.47/5.30 % (3849499)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3442866941:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 34.47/5.30 % (3849493)Instruction limit reached!
% 34.47/5.30 % (3849493)------------------------------
% 34.47/5.30 % (3849493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849493)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849493)Termination reason: Instruction limit
% 34.47/5.30 % (3849493)Termination phase: Saturation
% 34.47/5.30 % (3849493)Time elapsed: 0.292 s
% 34.47/5.30 % (3849493)Peak memory usage: 15 MB
% 34.47/5.30 % (3849493)Instructions burned: 477 (million)
% 34.47/5.30 % (3849488)Instruction limit reached!
% 34.47/5.30 % (3849488)------------------------------
% 34.47/5.30 % (3849488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.47/5.30 % (3849488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.47/5.30 % (3849488)CaDiCaL version: 2.1.3
% 34.47/5.30 % (3849488)Termination reason: Instruction limit
% 34.47/5.30 % (3849488)Termination phase: Saturation
% 34.47/5.30 % (3849488)Time elapsed: 0.376 s
% 34.47/5.30 % (3849488)Peak memory usage: 19 MB
% 34.47/5.30 % (3849488)Instructions burned: 684 (million)
% 34.47/5.30 % (3849501)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2648322000:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 34.47/5.30 % (3849502)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3056903365:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 46.83/7.12 % TRYING [14]
% 46.83/7.12 % (3849499)Instruction limit reached!
% 46.83/7.12 % (3849499)------------------------------
% 46.83/7.12 % (3849499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849499)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849499)Termination reason: Instruction limit
% 46.83/7.12 % (3849499)Termination phase: Finite model building constraint generation
% 46.83/7.12 % (3849499)Time elapsed: 0.189 s
% 46.83/7.12 % (3849499)Peak memory usage: 77 MB
% 46.83/7.12 % (3849499)Instructions burned: 892 (million)
% 46.83/7.12 % (3849505)fmb+10_1_sil=64000:random_seed=892121194:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [4]
% 46.83/7.12 % TRYING [5]
% 46.83/7.12 % TRYING [8]
% 46.83/7.12 % TRYING [6]
% 46.83/7.12 % (3849501)Instruction limit reached!
% 46.83/7.12 % (3849501)------------------------------
% 46.83/7.12 % (3849501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849501)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849501)Termination reason: Instruction limit
% 46.83/7.12 % (3849501)Termination phase: Saturation
% 46.83/7.12 % (3849501)Time elapsed: 0.387 s
% 46.83/7.12 % (3849501)Peak memory usage: 23 MB
% 46.83/7.12 % (3849501)Instructions burned: 693 (million)
% 46.83/7.12 % (3849507)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=156249074:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [20]
% 46.83/7.12 % (3849497)Instruction limit reached!
% 46.83/7.12 % (3849497)------------------------------
% 46.83/7.12 % (3849497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849497)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849497)Termination reason: Instruction limit
% 46.83/7.12 % (3849497)Termination phase: Saturation
% 46.83/7.12 % (3849497)Time elapsed: 0.676 s
% 46.83/7.12 % (3849497)Peak memory usage: 23 MB
% 46.83/7.12 % (3849497)Instructions burned: 1180 (million)
% 46.83/7.12 % (3849509)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2530984609:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [8]
% 46.83/7.12 % (3849502)Instruction limit reached!
% 46.83/7.12 % (3849502)------------------------------
% 46.83/7.12 % (3849502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849502)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849502)Termination reason: Instruction limit
% 46.83/7.12 % (3849502)Termination phase: Saturation
% 46.83/7.12 % (3849502)Time elapsed: 0.499 s
% 46.83/7.12 % (3849502)Peak memory usage: 20 MB
% 46.83/7.12 % (3849502)Instructions burned: 879 (million)
% 46.83/7.12 % (3849511)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3582387759:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 46.83/7.12 % TRYING [7]
% 46.83/7.12 % (3849509)Instruction limit reached!
% 46.83/7.12 % (3849509)------------------------------
% 46.83/7.12 % (3849509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849509)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849509)Termination reason: Instruction limit
% 46.83/7.12 % (3849509)Termination phase: Finite model building constraint generation
% 46.83/7.12 % (3849509)Time elapsed: 0.339 s
% 46.83/7.12 % (3849509)Peak memory usage: 70 MB
% 46.83/7.12 % (3849509)Instructions burned: 921 (million)
% 46.83/7.12 % (3849513)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1106390643:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 46.83/7.12 % TRYING [9]
% 46.83/7.12 % (3849513)Instruction limit reached!
% 46.83/7.12 % (3849513)------------------------------
% 46.83/7.12 % (3849513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849513)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849513)Termination reason: Instruction limit
% 46.83/7.12 % (3849513)Termination phase: Saturation
% 46.83/7.12 % (3849513)Time elapsed: 0.636 s
% 46.83/7.12 % (3849513)Peak memory usage: 16 MB
% 46.83/7.12 % (3849513)Instructions burned: 1472 (million)
% 46.83/7.12 % (3849515)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3559588595:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [77]
% 46.83/7.12 % TRYING [8]
% 46.83/7.12 % TRYING [10]
% 46.83/7.12 % (3849511)Instruction limit reached!
% 46.83/7.12 % (3849511)------------------------------
% 46.83/7.12 % (3849511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849511)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849511)Termination reason: Instruction limit
% 46.83/7.12 % (3849511)Termination phase: Saturation
% 46.83/7.12 % (3849511)Time elapsed: 2.672 s
% 46.83/7.12 % (3849511)Peak memory usage: 38 MB
% 46.83/7.12 % (3849511)Instructions burned: 5132 (million)
% 46.83/7.12 % (3849517)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3718989856:fmbsr=2.30978:i=2174_2962 on theBenchmark for (2962ds/2174Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [16]
% 46.83/7.12 % TRYING [9]
% 46.83/7.12 % (3849507)Instruction limit reached!
% 46.83/7.12 % (3849507)------------------------------
% 46.83/7.12 % (3849507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849507)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849507)Termination reason: Instruction limit
% 46.83/7.12 % (3849507)Termination phase: Finite model building constraint generation
% 46.83/7.12 % (3849507)Time elapsed: 3.285 s
% 46.83/7.12 % (3849507)Peak memory usage: 577 MB
% 46.83/7.12 % (3849507)Instructions burned: 9517 (million)
% 46.83/7.12 % (3849515)Instruction limit reached!
% 46.83/7.12 % (3849515)------------------------------
% 46.83/7.12 % (3849515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849515)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849515)Termination reason: Instruction limit
% 46.83/7.12 % (3849515)Termination phase: Finite model building constraint generation
% 46.83/7.12 % (3849515)Time elapsed: 2.265 s
% 46.83/7.12 % (3849515)Peak memory usage: 457 MB
% 46.83/7.12 % (3849515)Instructions burned: 6325 (million)
% 46.83/7.12 % (3849519)ott-2_1_sil=16000:newcnf=on:random_seed=2365704466:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 46.83/7.12 % (3849521)ott+10_1_sil=32000:tgt=ground:random_seed=503909812:i=5114:av=off_2956 on theBenchmark for (2956ds/5114Mi)
% 46.83/7.12 % (3849517)Instruction limit reached!
% 46.83/7.12 % (3849517)------------------------------
% 46.83/7.12 % (3849517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849517)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849517)Termination reason: Instruction limit
% 46.83/7.12 % (3849517)Termination phase: Finite model building constraint generation
% 46.83/7.12 % (3849517)Time elapsed: 0.760 s
% 46.83/7.12 % (3849517)Peak memory usage: 146 MB
% 46.83/7.12 % (3849517)Instructions burned: 2176 (million)
% 46.83/7.12 % (3849523)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2376445963:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 46.83/7.12 % Detected minimum model sizes of [4]
% 46.83/7.12 % Detected maximum model sizes of [max]
% 46.83/7.12 % TRYING [4]
% 46.83/7.12 % TRYING [5]
% 46.83/7.12 % TRYING [6]
% 46.83/7.12 % (3849519)Instruction limit reached!
% 46.83/7.12 % (3849519)------------------------------
% 46.83/7.12 % (3849519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849519)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849519)Termination reason: Instruction limit
% 46.83/7.12 % (3849519)Termination phase: Saturation
% 46.83/7.12 % (3849519)Time elapsed: 0.476 s
% 46.83/7.12 % (3849519)Peak memory usage: 22 MB
% 46.83/7.12 % (3849519)Instructions burned: 870 (million)
% 46.83/7.12 % (3849525)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3528916529:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 46.83/7.12 % TRYING [7]
% 46.83/7.12 % TRYING [8]
% 46.83/7.12 % (3849505)Instruction limit reached!
% 46.83/7.12 % (3849505)------------------------------
% 46.83/7.12 % (3849505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849505)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849505)Termination reason: Instruction limit
% 46.83/7.12 % (3849505)Termination phase: Finite model building SAT solving
% 46.83/7.12 % (3849505)Time elapsed: 4.744 s
% 46.83/7.12 % (3849505)Peak memory usage: 163 MB
% 46.83/7.12 % (3849505)Instructions burned: 22067 (million)
% 46.83/7.12 % (3849527)dis+21_1_sil=32000:sas=cadical:random_seed=1936729760:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi)
% 46.83/7.12 % TRYING [9]
% 46.83/7.12 % TRYING [11]
% 46.83/7.12 % (3849527)Instruction limit reached!
% 46.83/7.12 % (3849527)------------------------------
% 46.83/7.12 % (3849527)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849527)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849527)Termination reason: Instruction limit
% 46.83/7.12 % (3849527)Termination phase: Saturation
% 46.83/7.12 % (3849527)Time elapsed: 1.071 s
% 46.83/7.12 % (3849527)Peak memory usage: 47 MB
% 46.83/7.12 % (3849527)Instructions burned: 3773 (million)
% 46.83/7.12 % (3849529)ott+11_1_sil=16000:gs=on:random_seed=3593720248:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 46.83/7.12 % (3849525)Instruction limit reached!
% 46.83/7.12 % (3849525)------------------------------
% 46.83/7.12 % (3849525)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.12 % (3849525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.12 % (3849525)CaDiCaL version: 2.1.3
% 46.83/7.12 % (3849525)Termination reason: Instruction limit
% 46.83/7.12 % (3849525)Termination phase: Saturation
% 46.83/7.12 % (3849525)Time elapsed: 1.843 s
% 46.83/7.12 % (3849525)Peak memory usage: 39 MB
% 46.83/7.12 % (3849525)Instructions burned: 3513 (million)
% 46.83/7.12 % (3849521) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3849466-3849521"...
% 46.83/7.12 % (3849521)...printing done.
% 46.83/7.12 % (3849521)Refutation found. Thanks to Tanya!
% 46.83/7.12 % SZS status Theorem for theBenchmark
% 46.83/7.12 % SZS output start Proof for theBenchmark
% See solution above
% 46.83/7.13 % (3849521)------------------------------
% 46.83/7.13 % (3849521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.83/7.13 % (3849521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.83/7.13 % (3849521)CaDiCaL version: 2.1.3
% 46.83/7.13 % (3849521)Termination reason: Refutation
% 46.83/7.13 % (3849521)Time elapsed: 2.321 s
% 46.83/7.13 % (3849521)Peak memory usage: 39 MB
% 46.83/7.13 % (3849521)Instructions burned: 4353 (million)
% 46.83/7.13 % (3849466)Success in time 6.705 s
% 46.83/7.13 % Vampire exiting
%------------------------------------------------------------------------------