%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM502+1 : 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 : n011.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:34 PM UTC 2026
% Result : Theorem 208.81s 41.45s
% Output : Refutation 208.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 36
% Syntax : Number of formulae : 284 ( 45 unt; 16 def)
% Number of atoms : 1099 ( 235 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1197 ( 382 ~; 718 |; 53 &)
% ( 25 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 17 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 232 ( 0 sgn 226 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
fof(f4,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f8,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_AddZero) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
fof(f15,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( X0 != sz00
=> ! [X1,X2] :
( ( aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtasdt0(X0,X1) = sdtasdt0(X0,X2)
| sdtasdt0(X1,X0) = sdtasdt0(X2,X0) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulCanc) ).
fof(f18,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefLE) ).
fof(f21,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X0) )
=> X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEAsym) ).
fof(f22,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtlseqdt0(X0,X1)
& sdtlseqdt0(X1,X2) )
=> sdtlseqdt0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETran) ).
fof(f23,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) ) ) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',mMonMul) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
fof(f39,axiom,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(f41,axiom,
( isPrime0(xp)
& doDivides0(xp,sdtasdt0(xn,xm)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1860) ).
fof(f42,axiom,
~ sdtlseqdt0(xp,xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1870) ).
fof(f44,axiom,
( xn != xp
& sdtlseqdt0(xn,xp)
& xm != xp
& sdtlseqdt0(xm,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2287) ).
fof(f45,axiom,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2306) ).
fof(f46,axiom,
~ ( xk = sz00
| xk = sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2315) ).
fof(f50,conjecture,
( xk != xp
& sdtlseqdt0(xk,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f51,negated_conjecture,
~ ( xk != xp
& sdtlseqdt0(xk,xp) ),
inference(negated_conjecture,[status(cth)],[f50]) ).
fof(f53,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f54,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f53]) ).
fof(f55,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f56,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f55]) ).
fof(f61,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f67,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f72,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(f73,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,[],[f72]) ).
fof(f78,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f79,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f78]) ).
fof(f83,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f84,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f83]) ).
fof(f85,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f22]) ).
fof(f86,plain,
! [X0,X1,X2] :
( sdtlseqdt0(X0,X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f85]) ).
fof(f87,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f23]) ).
fof(f88,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ( X1 != X0
& sdtlseqdt0(X1,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f87]) ).
fof(f91,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(f92,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,[],[f91]) ).
fof(f101,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f102,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f101]) ).
fof(f103,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(f104,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,[],[f103]) ).
fof(f121,plain,
( sz00 != xk
& sz10 != xk ),
inference(ennf_transformation,[],[f46]) ).
fof(f122,plain,
( xp = xk
| ~ sdtlseqdt0(xk,xp) ),
inference(ennf_transformation,[],[f51]) ).
fof(f123,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f126,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f127,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sdtasdt0(X0,X1)) ),
inference(cnf_transformation,[],[f56]) ).
fof(f130,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f61]) ).
fof(f137,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f67]) ).
fof(f142,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| X1 = X2 ),
inference(cnf_transformation,[],[f73]) ).
fof(f143,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f73]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f154,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f84]) ).
fof(f155,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| ~ sdtlseqdt0(X0,X1)
| sdtlseqdt0(X0,X2) ),
inference(cnf_transformation,[],[f86]) ).
fof(f156,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
fof(f162,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)) ),
inference(cnf_transformation,[],[f92]) ).
fof(f164,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f92]) ).
fof(f169,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sK1(X0,X1)) = X1
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f170,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| aNaturalNumber0(sK1(X0,X1))
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f171,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
fof(f172,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,X2) = X1
| sdtsldt0(X1,X0) != X2 ),
inference(cnf_transformation,[],[f104]) ).
fof(f173,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| aNaturalNumber0(X2)
| sdtsldt0(X1,X0) != X2 ),
inference(cnf_transformation,[],[f104]) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtsldt0(X1,X0) = X2 ),
inference(cnf_transformation,[],[f104]) ).
fof(f190,plain,
aNaturalNumber0(xp),
inference(cnf_transformation,[],[f39]) ).
fof(f191,plain,
aNaturalNumber0(xm),
inference(cnf_transformation,[],[f39]) ).
fof(f192,plain,
aNaturalNumber0(xn),
inference(cnf_transformation,[],[f39]) ).
fof(f194,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(cnf_transformation,[],[f41]) ).
fof(f196,plain,
~ sdtlseqdt0(xp,xn),
inference(cnf_transformation,[],[f42]) ).
fof(f198,plain,
sdtlseqdt0(xm,xp),
inference(cnf_transformation,[],[f44]) ).
fof(f199,plain,
xm != xp,
inference(cnf_transformation,[],[f44]) ).
fof(f200,plain,
sdtlseqdt0(xn,xp),
inference(cnf_transformation,[],[f44]) ).
fof(f201,plain,
xn != xp,
inference(cnf_transformation,[],[f44]) ).
fof(f202,plain,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
inference(cnf_transformation,[],[f45]) ).
fof(f204,plain,
sz00 != xk,
inference(cnf_transformation,[],[f121]) ).
fof(f212,plain,
( ~ sdtlseqdt0(xk,xp)
| xp = xk ),
inference(cnf_transformation,[],[f122]) ).
fof(f213,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(equality_resolution,[],[f149]) ).
fof(f218,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f171]) ).
fof(f219,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X0,X2))
| sz00 = X0
| ~ aNaturalNumber0(X2)
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(equality_resolution,[],[f174]) ).
fof(f220,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| aNaturalNumber0(sdtsldt0(X1,X0)) ),
inference(equality_resolution,[],[f173]) ).
fof(f221,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 ),
inference(equality_resolution,[],[f172]) ).
fof(f224,plain,
~ aNaturalNumber0(sz00),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f226,plain,
! [X0,X1] :
( ~ aNaturalNumber0(sdtpldt0(X0,X1))
| aNaturalNumber0(X0)
| aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f227,plain,
! [X0,X1] :
( ~ aNaturalNumber0(sdtasdt0(X0,X1))
| aNaturalNumber0(X0)
| aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f231,plain,
! [X0] :
( aNaturalNumber0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f236,plain,
! [X0] :
( aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f242,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) != sdtasdt0(X0,X2)
| sz00 = X0
| aNaturalNumber0(X2)
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f243,plain,
! [X2,X0,X1] :
( sdtasdt0(X1,X0) != sdtasdt0(X2,X0)
| sz00 = X0
| aNaturalNumber0(X2)
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| X1 = X2 ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f247,plain,
! [X2,X0] :
( aNaturalNumber0(sdtpldt0(X0,X2))
| aNaturalNumber0(X0)
| aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f213]) ).
fof(f254,plain,
! [X0,X1] :
( sdtlseqdt0(X1,X0)
| sdtlseqdt0(X0,X1)
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| X0 = X1 ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f255,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(X0,X2)
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| sdtlseqdt0(X1,X2)
| sdtlseqdt0(X0,X1)
| aNaturalNumber0(X2) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f257,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X0,X1)
| aNaturalNumber0(X0)
| ~ sdtlseqdt0(X1,X0)
| aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f263,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| aNaturalNumber0(X2) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f265,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0))
| aNaturalNumber0(X1)
| aNaturalNumber0(X0)
| sdtlseqdt0(X1,X2)
| X1 = X2
| sz00 = X0
| aNaturalNumber0(X2) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f269,plain,
! [X2,X0] :
( aNaturalNumber0(sdtasdt0(X0,X2))
| aNaturalNumber0(X0)
| aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(consistent_polarity_flipping,[],[f218]) ).
fof(f270,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK1(X0,X1))
| aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f271,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| aNaturalNumber0(X0)
| sdtasdt0(X0,sK1(X0,X1)) = X1
| aNaturalNumber0(X1) ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f272,plain,
! [X2,X0] :
( aNaturalNumber0(sdtasdt0(X0,X2))
| aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X0,X2))
| sz00 = X0
| aNaturalNumber0(X2)
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(consistent_polarity_flipping,[],[f219]) ).
fof(f273,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sz00 = X0
| ~ aNaturalNumber0(sdtsldt0(X1,X0)) ),
inference(consistent_polarity_flipping,[],[f220]) ).
fof(f274,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sz00 = X0
| sdtasdt0(X0,sdtsldt0(X1,X0)) = X1 ),
inference(consistent_polarity_flipping,[],[f221]) ).
fof(f290,plain,
~ aNaturalNumber0(xn),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f291,plain,
~ aNaturalNumber0(xm),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f292,plain,
~ aNaturalNumber0(xp),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f294,plain,
sdtlseqdt0(xp,xn),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f296,plain,
~ sdtlseqdt0(xn,xp),
inference(consistent_polarity_flipping,[],[f200]) ).
fof(f297,plain,
~ sdtlseqdt0(xm,xp),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f300,plain,
( sdtlseqdt0(xk,xp)
| xp = xk ),
inference(consistent_polarity_flipping,[],[f212]) ).
fof(f303,definition,
( spl4_1
<=> xp = xk ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
fof(f305,plain,
( xp = xk
| ~ spl4_1 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl4_2
<=> sdtlseqdt0(xk,xp) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
fof(f309,plain,
( sdtlseqdt0(xk,xp)
| ~ spl4_2 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f310,plain,
( spl4_1
| spl4_2 ),
inference(avatar_split_clause,[],[f300,f307,f303]) ).
fof(f325,definition,
( spl4_6
<=> aNaturalNumber0(sz00) ),
introduced(definition,[new_symbols(definition,[spl4_6])],[avatar_definition]) ).
fof(f326,plain,
( ~ aNaturalNumber0(sz00)
| spl4_6 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f330,plain,
~ spl4_6,
inference(avatar_split_clause,[],[f224,f325]) ).
fof(f339,plain,
xn = sdtpldt0(sz00,xn),
inference(resolution,[],[f231,f290]) ).
fof(f357,plain,
sz00 = sdtasdt0(xn,sz00),
inference(resolution,[],[f236,f290]) ).
fof(f359,plain,
sz00 = sdtasdt0(xp,sz00),
inference(resolution,[],[f236,f292]) ).
fof(f395,definition,
( spl4_8
<=> aNaturalNumber0(xk) ),
introduced(definition,[new_symbols(definition,[spl4_8])],[avatar_definition]) ).
fof(f396,plain,
( ~ aNaturalNumber0(xk)
| spl4_8 ),
inference(avatar_component_clause,[],[f395]) ).
fof(f458,plain,
( aNaturalNumber0(xp)
| ~ aNaturalNumber0(sK1(xp,sdtasdt0(xn,xm)))
| aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolution,[],[f270,f194]) ).
fof(f459,plain,
( ~ aNaturalNumber0(sK1(xp,sdtasdt0(xn,xm)))
| aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f458,f292]) ).
fof(f463,definition,
( spl4_9
<=> aNaturalNumber0(sdtasdt0(xn,xm)) ),
introduced(definition,[new_symbols(definition,[spl4_9])],[avatar_definition]) ).
fof(f465,plain,
( aNaturalNumber0(sdtasdt0(xn,xm))
| ~ spl4_9 ),
inference(avatar_component_clause,[],[f463]) ).
fof(f467,definition,
( spl4_10
<=> aNaturalNumber0(sK1(xp,sdtasdt0(xn,xm))) ),
introduced(definition,[new_symbols(definition,[spl4_10])],[avatar_definition]) ).
fof(f469,plain,
( ~ aNaturalNumber0(sK1(xp,sdtasdt0(xn,xm)))
| spl4_10 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f470,plain,
( spl4_9
| ~ spl4_10 ),
inference(avatar_split_clause,[],[f459,f467,f463]) ).
fof(f512,plain,
! [X2,X0] :
( ~ sdtlseqdt0(X0,sdtpldt0(X0,X2))
| aNaturalNumber0(X2)
| aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f247,f226]) ).
fof(f518,plain,
( ~ sdtlseqdt0(sz00,xn)
| aNaturalNumber0(xn)
| aNaturalNumber0(sz00) ),
inference(superposition,[],[f512,f339]) ).
fof(f526,plain,
( ~ sdtlseqdt0(sz00,xn)
| aNaturalNumber0(sz00) ),
inference(forward_subsumption_resolution,[],[f518,f290]) ).
fof(f530,plain,
( ~ sdtlseqdt0(sz00,xn)
| spl4_6 ),
inference(forward_subsumption_resolution,[],[f526,f326]) ).
fof(f561,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| aNaturalNumber0(X2)
| aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f269,f227]) ).
fof(f655,plain,
( aNaturalNumber0(xp)
| sdtasdt0(xn,xm) = sdtasdt0(xp,sK1(xp,sdtasdt0(xn,xm)))
| aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolution,[],[f271,f194]) ).
fof(f663,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,sK1(xp,sdtasdt0(xn,xm)))
| aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(forward_subsumption_resolution,[],[f655,f292]) ).
fof(f671,definition,
( spl4_19
<=> sdtasdt0(xn,xm) = sdtasdt0(xp,sK1(xp,sdtasdt0(xn,xm))) ),
introduced(definition,[new_symbols(definition,[spl4_19])],[avatar_definition]) ).
fof(f673,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,sK1(xp,sdtasdt0(xn,xm)))
| ~ spl4_19 ),
inference(avatar_component_clause,[],[f671]) ).
fof(f674,plain,
( spl4_9
| spl4_19 ),
inference(avatar_split_clause,[],[f663,f671,f463]) ).
fof(f676,plain,
( aNaturalNumber0(xp)
| aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp
| ~ aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp)) ),
inference(resolution,[],[f273,f194]) ).
fof(f684,plain,
( aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp
| ~ aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp)) ),
inference(forward_subsumption_resolution,[],[f676,f292]) ).
fof(f695,plain,
( ~ aNaturalNumber0(xk)
| aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp ),
inference(forward_demodulation,[],[f684,f202]) ).
fof(f698,definition,
( spl4_22
<=> sz00 = xp ),
introduced(definition,[new_symbols(definition,[spl4_22])],[avatar_definition]) ).
fof(f699,plain,
( sz00 != xp
| spl4_22 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f700,plain,
( sz00 = xp
| ~ spl4_22 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f720,plain,
( ! [X0] :
( aNaturalNumber0(X0)
| aNaturalNumber0(xk)
| sdtlseqdt0(X0,xp)
| sdtlseqdt0(xk,X0)
| aNaturalNumber0(xp) )
| ~ spl4_2 ),
inference(resolution,[],[f255,f309]) ).
fof(f962,plain,
( aNaturalNumber0(xp)
| aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp
| sdtasdt0(xn,xm) = sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xm),xp)) ),
inference(resolution,[],[f274,f194]) ).
fof(f973,plain,
( aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp
| sdtasdt0(xn,xm) = sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xm),xp)) ),
inference(forward_subsumption_resolution,[],[f962,f292]) ).
fof(f980,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| aNaturalNumber0(sdtasdt0(xn,xm))
| sz00 = xp ),
inference(forward_demodulation,[],[f973,f202]) ).
fof(f982,definition,
( spl4_26
<=> sdtasdt0(xn,xm) = sdtasdt0(xp,xk) ),
introduced(definition,[new_symbols(definition,[spl4_26])],[avatar_definition]) ).
fof(f984,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ spl4_26 ),
inference(avatar_component_clause,[],[f982]) ).
fof(f985,plain,
( spl4_22
| spl4_9
| spl4_26 ),
inference(avatar_split_clause,[],[f980,f982,f463,f698]) ).
fof(f1030,plain,
( aNaturalNumber0(xn)
| aNaturalNumber0(xm)
| ~ spl4_9 ),
inference(resolution,[],[f465,f227]) ).
fof(f1031,plain,
( aNaturalNumber0(xm)
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f1030,f290]) ).
fof(f1032,plain,
( $false
| ~ spl4_9 ),
inference(forward_subsumption_resolution,[],[f1031,f291]) ).
fof(f1033,plain,
~ spl4_9,
inference(avatar_contradiction_clause,[],[f1032]) ).
fof(f1124,plain,
( sdtlseqdt0(sz00,xn)
| ~ spl4_22 ),
inference(superposition,[],[f294,f700]) ).
fof(f1135,plain,
( $false
| spl4_6
| ~ spl4_22 ),
inference(forward_subsumption_resolution,[],[f1124,f530]) ).
fof(f1136,plain,
( spl4_6
| ~ spl4_22 ),
inference(avatar_contradiction_clause,[],[f1135]) ).
fof(f1145,plain,
( spl4_22
| spl4_9
| ~ spl4_8 ),
inference(avatar_split_clause,[],[f695,f395,f463,f698]) ).
fof(f1146,plain,
( ! [X0] :
( aNaturalNumber0(X0)
| aNaturalNumber0(xk)
| sdtlseqdt0(X0,xp)
| sdtlseqdt0(xk,X0) )
| ~ spl4_2 ),
inference(forward_subsumption_resolution,[],[f720,f292]) ).
fof(f1182,definition,
( spl4_37
<=> ! [X0] :
( aNaturalNumber0(X0)
| sdtlseqdt0(xk,X0)
| sdtlseqdt0(X0,xp) ) ),
introduced(definition,[new_symbols(definition,[spl4_37])],[avatar_definition]) ).
fof(f1183,plain,
( ! [X0] :
( sdtlseqdt0(xk,X0)
| sdtlseqdt0(X0,xp)
| aNaturalNumber0(X0) )
| ~ spl4_37 ),
inference(avatar_component_clause,[],[f1182]) ).
fof(f1469,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X0))
| aNaturalNumber0(sdtasdt0(X1,X0))
| aNaturalNumber0(sdtasdt0(X1,X2))
| sdtasdt0(X1,X0) = sdtasdt0(X1,X2) ),
inference(resolution,[],[f263,f254]) ).
fof(f1474,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X0))
| aNaturalNumber0(sdtasdt0(X1,X0))
| aNaturalNumber0(sdtasdt0(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f1469,f242]) ).
fof(f1480,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X0))
| aNaturalNumber0(sdtasdt0(X1,X2)) ),
inference(forward_subsumption_resolution,[],[f1474,f227]) ).
fof(f1486,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X1,X2),sdtasdt0(X1,X0))
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1480,f227]) ).
fof(f1515,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X0,X1))
| aNaturalNumber0(sdtasdt0(X0,X1))
| aNaturalNumber0(sdtasdt0(X2,X1))
| sdtasdt0(X0,X1) = sdtasdt0(X2,X1) ),
inference(resolution,[],[f265,f254]) ).
fof(f1520,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X0,X1))
| aNaturalNumber0(sdtasdt0(X0,X1))
| aNaturalNumber0(sdtasdt0(X2,X1)) ),
inference(forward_subsumption_resolution,[],[f1515,f243]) ).
fof(f1526,plain,
! [X2,X0,X1] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X0,X1))
| aNaturalNumber0(sdtasdt0(X2,X1)) ),
inference(forward_subsumption_resolution,[],[f1520,f227]) ).
fof(f1532,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtasdt0(X2,X1),sdtasdt0(X0,X1))
| aNaturalNumber0(X1)
| sdtlseqdt0(X0,X2)
| X0 = X2
| sz00 = X1
| aNaturalNumber0(X2)
| aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1526,f227]) ).
fof(f1534,plain,
! [X2,X0] :
( aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X0,X2))
| sz00 = X0
| aNaturalNumber0(X2)
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(forward_subsumption_resolution,[],[f272,f227]) ).
fof(f1535,plain,
! [X2,X0] :
( aNaturalNumber0(X0)
| aNaturalNumber0(X2)
| sz00 = X0
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(forward_subsumption_resolution,[],[f1534,f561]) ).
fof(f1543,plain,
! [X0] :
( aNaturalNumber0(X0)
| sz00 = xp
| sdtsldt0(sdtasdt0(xp,X0),xp) = X0 ),
inference(resolution,[],[f1535,f292]) ).
fof(f1550,plain,
( ! [X0] :
( aNaturalNumber0(X0)
| sz00 = X0
| sz00 = sdtsldt0(sdtasdt0(X0,sz00),X0) )
| spl4_6 ),
inference(resolution,[],[f1535,f326]) ).
fof(f1578,plain,
( ! [X0] :
( aNaturalNumber0(X0)
| sdtsldt0(sdtasdt0(xp,X0),xp) = X0 )
| spl4_22 ),
inference(forward_subsumption_resolution,[],[f1543,f699]) ).
fof(f1580,definition,
( spl4_45
<=> sz00 = xm ),
introduced(definition,[new_symbols(definition,[spl4_45])],[avatar_definition]) ).
fof(f1581,plain,
( sz00 != xm
| spl4_45 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1582,plain,
( sz00 = xm
| ~ spl4_45 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1674,plain,
( sdtlseqdt0(xk,xm)
| aNaturalNumber0(xm)
| ~ spl4_37 ),
inference(resolution,[],[f1183,f297]) ).
fof(f1684,plain,
( sdtlseqdt0(xk,xm)
| ~ spl4_37 ),
inference(forward_subsumption_resolution,[],[f1674,f291]) ).
fof(f1696,plain,
( xk = sdtsldt0(sdtasdt0(xp,xk),xp)
| spl4_8
| spl4_22 ),
inference(resolution,[],[f1578,f396]) ).
fof(f1704,plain,
( aNaturalNumber0(xk)
| ~ sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| ~ spl4_37 ),
inference(resolution,[],[f1684,f257]) ).
fof(f1705,plain,
( ~ sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| ~ spl4_37 ),
inference(forward_subsumption_resolution,[],[f1704,f396]) ).
fof(f1707,plain,
( ~ sdtlseqdt0(xm,xk)
| spl4_8
| ~ spl4_37 ),
inference(forward_subsumption_resolution,[],[f1705,f291]) ).
fof(f3095,plain,
( sK1(xp,sdtasdt0(xn,xm)) = sdtsldt0(sdtasdt0(xp,sK1(xp,sdtasdt0(xn,xm))),xp)
| spl4_10
| spl4_22 ),
inference(resolution,[],[f469,f1578]) ).
fof(f3340,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xp)
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_demodulation,[],[f984,f305]) ).
fof(f3356,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| aNaturalNumber0(xn)
| aNaturalNumber0(xm)
| sdtlseqdt0(xn,X0)
| xn = X0
| sz00 = xm
| aNaturalNumber0(X0) )
| ~ spl4_1
| ~ spl4_26 ),
inference(superposition,[],[f265,f3340]) ).
fof(f3363,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| aNaturalNumber0(xm)
| sdtlseqdt0(xn,X0)
| xn = X0
| sz00 = xm
| aNaturalNumber0(X0) )
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f3356,f290]) ).
fof(f3378,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| sdtlseqdt0(xn,X0)
| xn = X0
| sz00 = xm
| aNaturalNumber0(X0) )
| ~ spl4_1
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f3363,f291]) ).
fof(f3390,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| sdtlseqdt0(xn,X0)
| xn = X0
| aNaturalNumber0(X0) )
| ~ spl4_1
| ~ spl4_26
| spl4_45 ),
inference(forward_subsumption_resolution,[],[f3378,f1581]) ).
fof(f4332,definition,
( spl4_177
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| aNaturalNumber0(X0)
| xn = X0
| sdtlseqdt0(xn,X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_177])],[avatar_definition]) ).
fof(f4333,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,xp),sdtasdt0(X0,xm))
| aNaturalNumber0(X0)
| xn = X0
| sdtlseqdt0(xn,X0) )
| ~ spl4_177 ),
inference(avatar_component_clause,[],[f4332]) ).
fof(f4414,plain,
( xk = sdtsldt0(sdtasdt0(xn,sz00),xp)
| ~ spl4_45 ),
inference(superposition,[],[f202,f1582]) ).
fof(f4438,plain,
( xk = sdtsldt0(sz00,xp)
| ~ spl4_45 ),
inference(forward_demodulation,[],[f4414,f357]) ).
fof(f6067,definition,
( spl4_207
<=> sz00 = sdtsldt0(sz00,xp) ),
introduced(definition,[new_symbols(definition,[spl4_207])],[avatar_definition]) ).
fof(f6069,plain,
( sz00 = sdtsldt0(sz00,xp)
| ~ spl4_207 ),
inference(avatar_component_clause,[],[f6067]) ).
fof(f7850,plain,
( spl4_177
| ~ spl4_1
| ~ spl4_26
| spl4_45 ),
inference(avatar_split_clause,[],[f3390,f1580,f982,f303,f4332]) ).
fof(f9302,plain,
( sz00 = xp
| sz00 = sdtsldt0(sdtasdt0(xp,sz00),xp)
| spl4_6 ),
inference(resolution,[],[f1550,f292]) ).
fof(f9354,plain,
( sz00 = sdtsldt0(sdtasdt0(xp,sz00),xp)
| spl4_6
| spl4_22 ),
inference(forward_subsumption_resolution,[],[f9302,f699]) ).
fof(f9397,plain,
( sz00 = sdtsldt0(sz00,xp)
| spl4_6
| spl4_22 ),
inference(forward_demodulation,[],[f9354,f359]) ).
fof(f9412,plain,
( spl4_207
| spl4_6
| spl4_22 ),
inference(avatar_split_clause,[],[f9397,f698,f325,f6067]) ).
fof(f135992,plain,
( aNaturalNumber0(xp)
| xn = xp
| sdtlseqdt0(xn,xp)
| aNaturalNumber0(xp)
| sdtlseqdt0(xm,xp)
| xm = xp
| sz00 = xp
| aNaturalNumber0(xp)
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(resolution,[],[f4333,f1486]) ).
fof(f136062,plain,
( aNaturalNumber0(xp)
| xn = xp
| sdtlseqdt0(xn,xp)
| sdtlseqdt0(xm,xp)
| xm = xp
| sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(duplicate_literal_removal,[],[f135992]) ).
fof(f136132,plain,
( xn = xp
| sdtlseqdt0(xn,xp)
| sdtlseqdt0(xm,xp)
| xm = xp
| sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136062,f292]) ).
fof(f136154,plain,
( sdtlseqdt0(xn,xp)
| sdtlseqdt0(xm,xp)
| xm = xp
| sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136132,f201]) ).
fof(f136156,plain,
( sdtlseqdt0(xm,xp)
| xm = xp
| sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136154,f296]) ).
fof(f136158,plain,
( xm = xp
| sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136156,f297]) ).
fof(f136159,plain,
( sz00 = xp
| aNaturalNumber0(xm)
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136158,f199]) ).
fof(f136160,plain,
( aNaturalNumber0(xm)
| spl4_22
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136159,f699]) ).
fof(f136161,plain,
( $false
| spl4_22
| ~ spl4_177 ),
inference(forward_subsumption_resolution,[],[f136160,f291]) ).
fof(f136162,plain,
( spl4_22
| ~ spl4_177 ),
inference(avatar_contradiction_clause,[],[f136161]) ).
fof(f136169,plain,
( ! [X0] :
( aNaturalNumber0(X0)
| sdtlseqdt0(X0,xp)
| sdtlseqdt0(xk,X0) )
| ~ spl4_2
| spl4_8 ),
inference(forward_subsumption_resolution,[],[f1146,f396]) ).
fof(f137780,plain,
( spl4_37
| ~ spl4_2
| spl4_8 ),
inference(avatar_split_clause,[],[f136169,f395,f307,f1182]) ).
fof(f141119,definition,
( spl4_4516
<=> xm = xk ),
introduced(definition,[new_symbols(definition,[spl4_4516])],[avatar_definition]) ).
fof(f141120,plain,
( xm != xk
| spl4_4516 ),
inference(avatar_component_clause,[],[f141119]) ).
fof(f141121,plain,
( xm = xk
| ~ spl4_4516 ),
inference(avatar_component_clause,[],[f141119]) ).
fof(f143514,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,xm),sdtasdt0(xp,xk))
| aNaturalNumber0(xm)
| sdtlseqdt0(xn,X0)
| xn = X0
| sz00 = xm
| aNaturalNumber0(X0)
| aNaturalNumber0(xn) )
| ~ spl4_26 ),
inference(superposition,[],[f1532,f984]) ).
fof(f143517,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,xm),sdtasdt0(xp,xk))
| sdtlseqdt0(xn,X0)
| xn = X0
| sz00 = xm
| aNaturalNumber0(X0)
| aNaturalNumber0(xn) )
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f143514,f291]) ).
fof(f143538,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,xm),sdtasdt0(xp,xk))
| sdtlseqdt0(xn,X0)
| xn = X0
| aNaturalNumber0(X0)
| aNaturalNumber0(xn) )
| ~ spl4_26
| spl4_45 ),
inference(forward_subsumption_resolution,[],[f143517,f1581]) ).
fof(f143559,plain,
( ! [X0] :
( sdtlseqdt0(sdtasdt0(X0,xm),sdtasdt0(xp,xk))
| sdtlseqdt0(xn,X0)
| xn = X0
| aNaturalNumber0(X0) )
| ~ spl4_26
| spl4_45 ),
inference(forward_subsumption_resolution,[],[f143538,f290]) ).
fof(f146053,plain,
( ~ sdtlseqdt0(xk,xp)
| ~ spl4_4516 ),
inference(superposition,[],[f297,f141121]) ).
fof(f146103,plain,
( $false
| ~ spl4_2
| ~ spl4_4516 ),
inference(forward_subsumption_resolution,[],[f146053,f309]) ).
fof(f146104,plain,
( ~ spl4_2
| ~ spl4_4516 ),
inference(avatar_contradiction_clause,[],[f146103]) ).
fof(f146108,plain,
( sdtasdt0(xp,xk) = sdtasdt0(xp,sK1(xp,sdtasdt0(xp,xk)))
| ~ spl4_19
| ~ spl4_26 ),
inference(forward_demodulation,[],[f673,f984]) ).
fof(f146246,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| aNaturalNumber0(X0)
| aNaturalNumber0(xp)
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| sK1(xp,sdtasdt0(xp,xk)) = X0
| sz00 = xp
| aNaturalNumber0(sK1(xp,sdtasdt0(xp,xk))) )
| ~ spl4_19
| ~ spl4_26 ),
inference(superposition,[],[f263,f146108]) ).
fof(f146271,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| aNaturalNumber0(X0)
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| sK1(xp,sdtasdt0(xp,xk)) = X0
| sz00 = xp
| aNaturalNumber0(sK1(xp,sdtasdt0(xp,xk))) )
| ~ spl4_19
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f146246,f292]) ).
fof(f146280,definition,
( spl4_4793
<=> aNaturalNumber0(sK1(xp,sdtasdt0(xp,xk))) ),
introduced(definition,[new_symbols(definition,[spl4_4793])],[avatar_definition]) ).
fof(f146282,plain,
( aNaturalNumber0(sK1(xp,sdtasdt0(xp,xk)))
| ~ spl4_4793 ),
inference(avatar_component_clause,[],[f146280]) ).
fof(f146366,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| aNaturalNumber0(X0)
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| sK1(xp,sdtasdt0(xp,xk)) = X0
| aNaturalNumber0(sK1(xp,sdtasdt0(xp,xk))) )
| ~ spl4_19
| spl4_22
| ~ spl4_26 ),
inference(forward_subsumption_resolution,[],[f146271,f699]) ).
fof(f146391,definition,
( spl4_4815
<=> ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| sK1(xp,sdtasdt0(xp,xk)) = X0
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| aNaturalNumber0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl4_4815])],[avatar_definition]) ).
fof(f146392,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| sK1(xp,sdtasdt0(xp,xk)) = X0
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| aNaturalNumber0(X0) )
| ~ spl4_4815 ),
inference(avatar_component_clause,[],[f146391]) ).
fof(f146393,plain,
( spl4_4793
| spl4_4815
| ~ spl4_19
| spl4_22
| ~ spl4_26 ),
inference(avatar_split_clause,[],[f146366,f982,f698,f671,f146391,f146280]) ).
fof(f205078,plain,
( sK1(xp,sdtasdt0(xp,xk)) = sdtsldt0(sdtasdt0(xp,sK1(xp,sdtasdt0(xp,xk))),xp)
| spl4_10
| spl4_22
| ~ spl4_26 ),
inference(forward_demodulation,[],[f3095,f984]) ).
fof(f205079,plain,
( sdtsldt0(sdtasdt0(xp,xk),xp) = sK1(xp,sdtasdt0(xp,xk))
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26 ),
inference(forward_demodulation,[],[f205078,f146108]) ).
fof(f205080,plain,
( xk = sK1(xp,sdtasdt0(xp,xk))
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26 ),
inference(forward_demodulation,[],[f205079,f1696]) ).
fof(f317984,plain,
( aNaturalNumber0(xk)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4793 ),
inference(forward_demodulation,[],[f146282,f205080]) ).
fof(f317985,plain,
( $false
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4793 ),
inference(forward_subsumption_resolution,[],[f317984,f396]) ).
fof(f317986,plain,
( spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4793 ),
inference(avatar_contradiction_clause,[],[f317985]) ).
fof(f317991,plain,
( ! [X0] :
( xk = X0
| ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| sdtlseqdt0(X0,sK1(xp,sdtasdt0(xp,xk)))
| aNaturalNumber0(X0) )
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4815 ),
inference(forward_demodulation,[],[f146392,f205080]) ).
fof(f317996,plain,
( ! [X0] :
( ~ sdtlseqdt0(sdtasdt0(xp,X0),sdtasdt0(xp,xk))
| xk = X0
| sdtlseqdt0(X0,xk)
| aNaturalNumber0(X0) )
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4815 ),
inference(forward_demodulation,[],[f317991,f205080]) ).
fof(f1286104,plain,
( sdtlseqdt0(xn,xp)
| xn = xp
| aNaturalNumber0(xp)
| xm = xk
| sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_45
| ~ spl4_4815 ),
inference(resolution,[],[f143559,f317996]) ).
fof(f1286130,plain,
( xn = xp
| aNaturalNumber0(xp)
| xm = xk
| sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_45
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286104,f296]) ).
fof(f1286134,plain,
( aNaturalNumber0(xp)
| xm = xk
| sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_45
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286130,f201]) ).
fof(f1286138,plain,
( xm = xk
| sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_45
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286134,f292]) ).
fof(f1286141,plain,
( sdtlseqdt0(xm,xk)
| aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_45
| spl4_4516
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286138,f141120]) ).
fof(f1286144,plain,
( aNaturalNumber0(xm)
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_37
| spl4_45
| spl4_4516
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286141,f1707]) ).
fof(f1286147,plain,
( $false
| spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_37
| spl4_45
| spl4_4516
| ~ spl4_4815 ),
inference(forward_subsumption_resolution,[],[f1286144,f291]) ).
fof(f1286148,plain,
( spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_37
| spl4_45
| spl4_4516
| ~ spl4_4815 ),
inference(avatar_contradiction_clause,[],[f1286147]) ).
fof(f1286168,plain,
( sz00 = xk
| ~ spl4_45
| ~ spl4_207 ),
inference(forward_demodulation,[],[f4438,f6069]) ).
fof(f1286615,plain,
( $false
| ~ spl4_45
| ~ spl4_207 ),
inference(forward_subsumption_resolution,[],[f1286168,f204]) ).
fof(f1286616,plain,
( ~ spl4_45
| ~ spl4_207 ),
inference(avatar_contradiction_clause,[],[f1286615]) ).
cnf(s1,plain,
( spl4_1
| spl4_2 ),
inference(sat_conversion,[],[f310]) ).
cnf(s5,plain,
~ spl4_6,
inference(sat_conversion,[],[f330]) ).
cnf(s7,plain,
( spl4_9
| ~ spl4_10 ),
inference(sat_conversion,[],[f470]) ).
cnf(s15,plain,
( spl4_9
| spl4_19 ),
inference(sat_conversion,[],[f674]) ).
cnf(s21,plain,
( spl4_9
| spl4_22
| spl4_26 ),
inference(sat_conversion,[],[f985]) ).
cnf(s26,plain,
~ spl4_9,
inference(sat_conversion,[],[f1033]) ).
cnf(s28,plain,
( spl4_6
| ~ spl4_22 ),
inference(sat_conversion,[],[f1136]) ).
cnf(s30,plain,
( ~ spl4_8
| spl4_9
| spl4_22 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s339,plain,
( ~ spl4_1
| ~ spl4_26
| spl4_45
| spl4_177 ),
inference(sat_conversion,[],[f7850]) ).
cnf(s452,plain,
( spl4_6
| spl4_22
| spl4_207 ),
inference(sat_conversion,[],[f9412]) ).
cnf(s4989,plain,
( spl4_22
| ~ spl4_177 ),
inference(sat_conversion,[],[f136162]) ).
cnf(s5314,plain,
( ~ spl4_2
| spl4_8
| spl4_37 ),
inference(sat_conversion,[],[f137780]) ).
cnf(s6510,plain,
( ~ spl4_2
| ~ spl4_4516 ),
inference(sat_conversion,[],[f146104]) ).
cnf(s6554,plain,
( ~ spl4_19
| spl4_22
| ~ spl4_26
| spl4_4793
| spl4_4815 ),
inference(sat_conversion,[],[f146393]) ).
cnf(s16418,plain,
( spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_4793 ),
inference(sat_conversion,[],[f317986]) ).
cnf(s53572,plain,
( spl4_8
| spl4_10
| ~ spl4_19
| spl4_22
| ~ spl4_26
| ~ spl4_37
| spl4_45
| spl4_4516
| ~ spl4_4815 ),
inference(sat_conversion,[],[f1286148]) ).
cnf(s53613,plain,
( ~ spl4_45
| ~ spl4_207 ),
inference(sat_conversion,[],[f1286616]) ).
cnf(s55655,plain,
( spl4_22
| spl4_26 ),
inference(rat,[],[s21,s26]) ).
cnf(s55661,plain,
spl4_19,
inference(rat,[],[s15,s26]) ).
cnf(s55666,plain,
~ spl4_10,
inference(rat,[],[s7,s26]) ).
cnf(s55689,plain,
~ spl4_22,
inference(rat,[],[s28,s5]) ).
cnf(s55771,plain,
~ spl4_177,
inference(rat,[],[s4989,s55689]) ).
cnf(s55779,plain,
spl4_207,
inference(rat,[],[s452,s5,s55689]) ).
cnf(s55782,plain,
~ spl4_8,
inference(rat,[],[s30,s26,s55689]) ).
cnf(s55783,plain,
spl4_26,
inference(rat,[],[s55655,s55689]) ).
cnf(s55971,plain,
~ spl4_45,
inference(rat,[],[s53613,s55779]) ).
cnf(s56049,plain,
~ spl4_4793,
inference(rat,[],[s16418,s55689,s55783,s55666,s55661,s55782]) ).
cnf(s56126,plain,
~ spl4_1,
inference(rat,[],[s339,s55771,s55971,s55783]) ).
cnf(s56297,plain,
spl4_4815,
inference(rat,[],[s6554,s55783,s55689,s55661,s56049]) ).
cnf(s60612,plain,
spl4_2,
inference(rat,[],[s1,s56126]) ).
cnf(s60618,plain,
~ spl4_4516,
inference(rat,[],[s6510,s60612]) ).
cnf(s60621,plain,
spl4_37,
inference(rat,[],[s5314,s55782,s60612]) ).
cnf(s60624,plain,
$false,
inference(rat,[],[s53572,s56297,s55782,s55971,s55689,s55783,s55666,s55661,s60618,s60621]) ).
fof(f1287317,plain,
$false,
inference(avatar_sat_refutation,[],[s60624]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM502+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40 % Computer : n011.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 20:14:16 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.44 Running first-order model finding
% 0.13/0.44 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
% 14.54/2.53 % (2731449)Will run a generic schedule for satisfiability detection.
% 14.54/2.53 % (2731454)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2576041892_2999 on theBenchmark for (2999ds/0Mi)
% 14.54/2.53 % Detected minimum model sizes of [3]
% 14.54/2.53 % Detected maximum model sizes of [max]
% 14.54/2.53 % TRYING [3]
% 14.54/2.53 % (2731455)% WARNING: option uhcvi not known.
% 14.54/2.53 % (2731455)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=209730367:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.54/2.53 % (2731456)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3690444408:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.54/2.53 % (2731457)dis+10_1_sil=32000:sp=arity:random_seed=568523141:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.54/2.53 % (2731458)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2487192313:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.54/2.53 % (2731459)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2321943529:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.54/2.54 % TRYING [4]
% 14.54/2.54 % (2731460)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4137272740:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.54/2.54 % TRYING [5]
% 14.54/2.54 % TRYING [6]
% 14.54/2.54 % (2731457)Instruction limit reached!
% 14.54/2.54 % (2731457)------------------------------
% 14.54/2.54 % (2731457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.54/2.54 % (2731457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.54/2.54 % (2731457)CaDiCaL version: 2.1.3
% 14.54/2.54 % (2731457)Termination reason: Instruction limit
% 14.54/2.54 % (2731457)Termination phase: Saturation
% 14.54/2.54 % (2731457)Time elapsed: 0.061 s
% 14.54/2.54 % (2731457)Peak memory usage: 12 MB
% 14.54/2.54 % (2731457)Instructions burned: 104 (million)
% 14.54/2.54 % (2731458)Instruction limit reached!
% 14.54/2.54 % (2731458)------------------------------
% 14.54/2.54 % (2731458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.54/2.54 % (2731458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.54/2.54 % (2731458)CaDiCaL version: 2.1.3
% 14.54/2.54 % (2731458)Termination reason: Instruction limit
% 14.54/2.54 % (2731458)Termination phase: Saturation
% 14.54/2.54 % (2731458)Time elapsed: 0.066 s
% 14.54/2.54 % (2731458)Peak memory usage: 13 MB
% 14.54/2.54 % (2731458)Instructions burned: 116 (million)
% 14.54/2.54 % (2731459)Instruction limit reached!
% 14.54/2.54 % (2731459)------------------------------
% 14.54/2.54 % (2731459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.54/2.54 % (2731459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.54/2.54 % (2731459)CaDiCaL version: 2.1.3
% 14.54/2.54 % (2731459)Termination reason: Instruction limit
% 14.54/2.54 % (2731459)Termination phase: Saturation
% 14.54/2.54 % (2731459)Time elapsed: 0.078 s
% 14.54/2.54 % (2731459)Peak memory usage: 14 MB
% 14.54/2.54 % (2731459)Instructions burned: 131 (million)
% 14.54/2.54 % (2731468)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1336009790:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.54/2.54 % Detected minimum model sizes of [3]
% 14.54/2.54 % Detected maximum model sizes of [max]
% 14.54/2.54 % (2731469)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3611725219:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.54/2.54 % TRYING [3]
% 14.54/2.54 % TRYING [4]
% 14.54/2.54 % (2731470)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=2372193127:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.54/2.54 % (2731460)Instruction limit reached!
% 14.54/2.54 % (2731460)------------------------------
% 14.54/2.54 % (2731460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.54/2.54 % (2731460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.54/2.54 % (2731460)CaDiCaL version: 2.1.3
% 14.54/2.54 % (2731460)Termination reason: Instruction limit
% 14.54/2.54 % (2731460)Termination phase: Saturation
% 14.54/2.54 % (2731460)Time elapsed: 0.099 s
% 14.54/2.54 % (2731460)Peak memory usage: 14 MB
% 14.54/2.54 % (2731460)Instructions burned: 159 (million)
% 14.54/2.54 % (2731474)ott-21_1_sil=16000:fs=off:random_seed=3434142278:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.54/2.54 % TRYING [5]
% 14.54/2.54 % (2731469)Instruction limit reached!
% 33.67/5.21 % (2731469)------------------------------
% 33.67/5.21 % (2731469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731469)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731469)Termination reason: Instruction limit
% 33.67/5.21 % (2731469)Termination phase: Saturation
% 33.67/5.21 % (2731469)Time elapsed: 0.068 s
% 33.67/5.21 % (2731469)Peak memory usage: 12 MB
% 33.67/5.21 % (2731469)Instructions burned: 131 (million)
% 33.67/5.21 % TRYING [7]
% 33.67/5.21 % (2731476)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=916414299:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 33.67/5.21 % TRYING [6]
% 33.67/5.21 % (2731474)Instruction limit reached!
% 33.67/5.21 % (2731474)------------------------------
% 33.67/5.21 % (2731474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731474)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731474)Termination reason: Instruction limit
% 33.67/5.21 % (2731474)Termination phase: Saturation
% 33.67/5.21 % (2731474)Time elapsed: 0.092 s
% 33.67/5.21 % (2731474)Peak memory usage: 13 MB
% 33.67/5.21 % (2731474)Instructions burned: 181 (million)
% 33.67/5.21 % (2731478)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2474781111:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 33.67/5.21 % Detected minimum model sizes of [3]
% 33.67/5.21 % Detected maximum model sizes of [max]
% 33.67/5.21 % TRYING [3]
% 33.67/5.21 % TRYING [4]
% 33.67/5.21 % (2731468)Instruction limit reached!
% 33.67/5.21 % (2731468)------------------------------
% 33.67/5.21 % (2731468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731468)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731468)Termination reason: Instruction limit
% 33.67/5.21 % (2731468)Termination phase: Finite model building constraint generation
% 33.67/5.21 % (2731468)Time elapsed: 0.258 s
% 33.67/5.21 % (2731468)Peak memory usage: 34 MB
% 33.67/5.21 % (2731468)Instructions burned: 714 (million)
% 33.67/5.21 % TRYING [5]
% 33.67/5.21 % (2731480)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1791741186:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 33.67/5.21 % TRYING [8]
% 33.67/5.21 % (2731470)Instruction limit reached!
% 33.67/5.21 % (2731470)------------------------------
% 33.67/5.21 % (2731470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731470)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731470)Termination reason: Instruction limit
% 33.67/5.21 % (2731470)Termination phase: Saturation
% 33.67/5.21 % (2731470)Time elapsed: 0.372 s
% 33.67/5.21 % (2731470)Peak memory usage: 21 MB
% 33.67/5.21 % (2731470)Instructions burned: 685 (million)
% 33.67/5.21 % (2731482)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2455686886:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 33.67/5.21 % (2731476)Instruction limit reached!
% 33.67/5.21 % (2731476)------------------------------
% 33.67/5.21 % (2731476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731476)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731476)Termination reason: Instruction limit
% 33.67/5.21 % (2731476)Termination phase: Saturation
% 33.67/5.21 % (2731476)Time elapsed: 0.316 s
% 33.67/5.21 % (2731476)Peak memory usage: 14 MB
% 33.67/5.21 % (2731476)Instructions burned: 477 (million)
% 33.67/5.21 % (2731484)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=1727184785:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 33.67/5.21 % TRYING [6]
% 33.67/5.21 % (2731478)Instruction limit reached!
% 33.67/5.21 % (2731478)------------------------------
% 33.67/5.21 % (2731478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 33.67/5.21 % (2731478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.67/5.21 % (2731478)CaDiCaL version: 2.1.3
% 33.67/5.21 % (2731478)Termination reason: Instruction limit
% 33.67/5.21 % (2731478)Termination phase: Finite model building constraint generation
% 33.67/5.21 % (2731478)Time elapsed: 0.356 s
% 33.67/5.21 % (2731478)Peak memory usage: 22 MB
% 33.67/5.21 % (2731478)Instructions burned: 867 (million)
% 76.94/11.34 % (2731486)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2384146504:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 76.94/11.34 % TRYING [14]
% 76.94/11.34 % (2731482)Instruction limit reached!
% 76.94/11.34 % (2731482)------------------------------
% 76.94/11.34 % (2731482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.94/11.34 % (2731482)CaDiCaL version: 2.1.3
% 76.94/11.34 % (2731482)Termination reason: Instruction limit
% 76.94/11.34 % (2731482)Termination phase: Finite model building constraint generation
% 76.94/11.34 % (2731482)Time elapsed: 0.350 s
% 76.94/11.34 % (2731482)Peak memory usage: 80 MB
% 76.94/11.34 % (2731482)Instructions burned: 892 (million)
% 76.94/11.34 % (2731484)Instruction limit reached!
% 76.94/11.34 % (2731484)------------------------------
% 76.94/11.34 % (2731484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.94/11.34 % (2731484)CaDiCaL version: 2.1.3
% 76.94/11.34 % (2731484)Termination reason: Instruction limit
% 76.94/11.34 % (2731484)Termination phase: Saturation
% 76.94/11.34 % (2731484)Time elapsed: 0.339 s
% 76.94/11.34 % (2731484)Peak memory usage: 23 MB
% 76.94/11.34 % (2731484)Instructions burned: 692 (million)
% 76.94/11.34 % (2731488)fmb+10_1_sil=64000:random_seed=2670978651:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 76.94/11.34 % (2731489)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1929646896:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 76.94/11.34 % Detected minimum model sizes of [3]
% 76.94/11.34 % Detected maximum model sizes of [max]
% 76.94/11.34 % TRYING [3]
% 76.94/11.34 % Detected minimum model sizes of [3]
% 76.94/11.34 % Detected maximum model sizes of [max]
% 76.94/11.34 % TRYING [20]
% 76.94/11.34 % TRYING [4]
% 76.94/11.34 % TRYING [9]
% 76.94/11.34 % TRYING [5]
% 76.94/11.34 % (2731480)Instruction limit reached!
% 76.94/11.34 % (2731480)------------------------------
% 76.94/11.34 % (2731480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.94/11.34 % (2731480)CaDiCaL version: 2.1.3
% 76.94/11.34 % (2731480)Termination reason: Instruction limit
% 76.94/11.34 % (2731480)Termination phase: Saturation
% 76.94/11.34 % (2731480)Time elapsed: 0.627 s
% 76.94/11.34 % (2731480)Peak memory usage: 23 MB
% 76.94/11.34 % (2731480)Instructions burned: 1180 (million)
% 76.94/11.34 % (2731492)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2161701622:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 76.94/11.34 % Detected minimum model sizes of [3]
% 76.94/11.34 % Detected maximum model sizes of [max]
% 76.94/11.34 % TRYING [8]
% 76.94/11.34 % (2731486)Instruction limit reached!
% 76.94/11.34 % (2731486)------------------------------
% 76.94/11.34 % (2731486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.94/11.34 % (2731486)CaDiCaL version: 2.1.3
% 76.94/11.34 % (2731486)Termination reason: Instruction limit
% 76.94/11.34 % (2731486)Termination phase: Saturation
% 76.94/11.34 % (2731486)Time elapsed: 0.498 s
% 76.94/11.34 % (2731486)Peak memory usage: 20 MB
% 76.94/11.34 % (2731486)Instructions burned: 879 (million)
% 76.94/11.34 % (2731494)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=459077467:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 76.94/11.34 % TRYING [6]
% 76.94/11.34 % (2731492)Instruction limit reached!
% 76.94/11.34 % (2731492)------------------------------
% 76.94/11.34 % (2731492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 76.94/11.34 % (2731492)CaDiCaL version: 2.1.3
% 76.94/11.34 % (2731492)Termination reason: Instruction limit
% 76.94/11.34 % (2731492)Termination phase: Finite model building constraint generation
% 76.94/11.34 % (2731492)Time elapsed: 0.339 s
% 76.94/11.34 % (2731492)Peak memory usage: 66 MB
% 76.94/11.34 % (2731492)Instructions burned: 920 (million)
% 76.94/11.34 % (2731496)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1397894070:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 76.94/11.34 % TRYING [7]
% 76.94/11.34 % TRYING [10]
% 76.94/11.34 % (2731496)Instruction limit reached!
% 76.94/11.34 % (2731496)------------------------------
% 76.94/11.34 % (2731496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 76.94/11.34 % (2731496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731496)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731496)Termination reason: Instruction limit
% 255.01/36.49 % (2731496)Termination phase: Saturation
% 255.01/36.49 % (2731496)Time elapsed: 0.676 s
% 255.01/36.49 % (2731496)Peak memory usage: 25 MB
% 255.01/36.49 % (2731496)Instructions burned: 1474 (million)
% 255.01/36.49 % (2731498)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=981633067:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 255.01/36.49 % Detected minimum model sizes of [3]
% 255.01/36.49 % Detected maximum model sizes of [max]
% 255.01/36.49 % TRYING [77]
% 255.01/36.49 % TRYING [8]
% 255.01/36.49 % (2731494)Instruction limit reached!
% 255.01/36.49 % (2731494)------------------------------
% 255.01/36.49 % (2731494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 255.01/36.49 % (2731494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731494)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731494)Termination reason: Instruction limit
% 255.01/36.49 % (2731494)Termination phase: Saturation
% 255.01/36.49 % (2731494)Time elapsed: 2.733 s
% 255.01/36.49 % (2731494)Peak memory usage: 50 MB
% 255.01/36.49 % (2731494)Instructions burned: 5131 (million)
% 255.01/36.49 % (2731502)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1393069022:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 255.01/36.49 % Detected minimum model sizes of [3]
% 255.01/36.49 % Detected maximum model sizes of [max]
% 255.01/36.49 % TRYING [16]
% 255.01/36.49 % (2731489)Instruction limit reached!
% 255.01/36.49 % (2731489)------------------------------
% 255.01/36.49 % (2731489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 255.01/36.49 % (2731489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731489)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731489)Termination reason: Instruction limit
% 255.01/36.49 % (2731489)Termination phase: Finite model building constraint generation
% 255.01/36.49 % (2731489)Time elapsed: 3.296 s
% 255.01/36.49 % (2731489)Peak memory usage: 567 MB
% 255.01/36.49 % (2731489)Instructions burned: 9517 (million)
% 255.01/36.49 % TRYING [11]
% 255.01/36.49 % (2731504)ott-2_1_sil=16000:newcnf=on:random_seed=1638747669:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 255.01/36.49 % (2731498)Instruction limit reached!
% 255.01/36.49 % (2731498)------------------------------
% 255.01/36.49 % (2731498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 255.01/36.49 % (2731498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731498)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731498)Termination reason: Instruction limit
% 255.01/36.49 % (2731498)Termination phase: Finite model building constraint generation
% 255.01/36.49 % (2731498)Time elapsed: 2.356 s
% 255.01/36.49 % (2731498)Peak memory usage: 523 MB
% 255.01/36.49 % (2731498)Instructions burned: 6324 (million)
% 255.01/36.49 % (2731506)ott+10_1_sil=32000:tgt=ground:random_seed=1083158121:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 255.01/36.49 % (2731502)Instruction limit reached!
% 255.01/36.49 % (2731502)------------------------------
% 255.01/36.49 % (2731502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 255.01/36.49 % (2731502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731502)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731502)Termination reason: Instruction limit
% 255.01/36.49 % (2731502)Termination phase: Finite model building constraint generation
% 255.01/36.49 % (2731502)Time elapsed: 0.763 s
% 255.01/36.49 % (2731502)Peak memory usage: 146 MB
% 255.01/36.49 % (2731502)Instructions burned: 2177 (million)
% 255.01/36.49 % (2731508)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2985132629:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 255.01/36.49 % Detected minimum model sizes of [3]
% 255.01/36.49 % Detected maximum model sizes of [max]
% 255.01/36.49 % TRYING [3]
% 255.01/36.49 % (2731504)Instruction limit reached!
% 255.01/36.49 % (2731504)------------------------------
% 255.01/36.49 % (2731504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 255.01/36.49 % (2731504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 255.01/36.49 % (2731504)CaDiCaL version: 2.1.3
% 255.01/36.49 % (2731504)Termination reason: Instruction limit
% 255.01/36.49 % (2731504)Termination phase: Saturation
% 255.01/36.49 % (2731504)Time elapsed: 0.444 s
% 255.01/36.49 % (2731504)Peak memory usage: 23 MB
% 255.01/36.49 % (2731504)Instructions burned: 870 (million)
% 255.01/36.49 % TRYING [4]
% 255.01/36.49 % (2731510)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3404902584:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 208.81/41.45 % TRYING [5]
% 208.81/41.45 % TRYING [6]
% 208.81/41.45 % TRYING [7]
% 208.81/41.45 % TRYING [8]
% 208.81/41.45 % TRYING [9]
% 208.81/41.45 % TRYING [9]
% 208.81/41.45 % (2731510)Instruction limit reached!
% 208.81/41.45 % (2731510)------------------------------
% 208.81/41.45 % (2731510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731510)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731510)Termination reason: Instruction limit
% 208.81/41.45 % (2731510)Termination phase: Saturation
% 208.81/41.45 % (2731510)Time elapsed: 1.827 s
% 208.81/41.45 % (2731510)Peak memory usage: 42 MB
% 208.81/41.45 % (2731510)Instructions burned: 3513 (million)
% 208.81/41.45 % (2731512)dis+21_1_sil=32000:sas=cadical:random_seed=4279036664:i=3773:amm=off_2934 on theBenchmark for (2934ds/3773Mi)
% 208.81/41.45 % (2731506)Instruction limit reached!
% 208.81/41.45 % (2731506)------------------------------
% 208.81/41.45 % (2731506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731506)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731506)Termination reason: Instruction limit
% 208.81/41.45 % (2731506)Termination phase: Saturation
% 208.81/41.45 % (2731506)Time elapsed: 2.872 s
% 208.81/41.45 % (2731506)Peak memory usage: 35 MB
% 208.81/41.45 % (2731506)Instructions burned: 5115 (million)
% 208.81/41.45 % (2731514)ott+11_1_sil=16000:gs=on:random_seed=2678159041:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2925 on theBenchmark for (2925ds/2251Mi)
% 208.81/41.45 % TRYING [12]
% 208.81/41.45 % TRYING [10]
% 208.81/41.45 % (2731514)Instruction limit reached!
% 208.81/41.45 % (2731514)------------------------------
% 208.81/41.45 % (2731514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731514)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731514)Termination reason: Instruction limit
% 208.81/41.45 % (2731514)Termination phase: Saturation
% 208.81/41.45 % (2731514)Time elapsed: 0.993 s
% 208.81/41.45 % (2731514)Peak memory usage: 19 MB
% 208.81/41.45 % (2731514)Instructions burned: 2254 (million)
% 208.81/41.45 % (2731516)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1946966895:fmbsr=1.6:i=67534_2915 on theBenchmark for (2915ds/67534Mi)
% 208.81/41.45 % Detected minimum model sizes of [3]
% 208.81/41.45 % Detected maximum model sizes of [max]
% 208.81/41.45 % TRYING [7]
% 208.81/41.45 % (2731512)Instruction limit reached!
% 208.81/41.45 % (2731512)------------------------------
% 208.81/41.45 % (2731512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731512)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731512)Termination reason: Instruction limit
% 208.81/41.45 % (2731512)Termination phase: Saturation
% 208.81/41.45 % (2731512)Time elapsed: 2.043 s
% 208.81/41.45 % (2731512)Peak memory usage: 45 MB
% 208.81/41.45 % (2731512)Instructions burned: 3774 (million)
% 208.81/41.45 % (2731518)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1112745996:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2913 on theBenchmark for (2913ds/4591Mi)
% 208.81/41.45 % (2731488)Instruction limit reached!
% 208.81/41.45 % (2731488)------------------------------
% 208.81/41.45 % (2731488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731488)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731488)Termination reason: Instruction limit
% 208.81/41.45 % (2731488)Termination phase: Finite model building SAT solving
% 208.81/41.45 % (2731488)Time elapsed: 8.483 s
% 208.81/41.45 % (2731488)Peak memory usage: 158 MB
% 208.81/41.45 % (2731488)Instructions burned: 22063 (million)
% 208.81/41.45 % (2731520)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=367626306:i=29340_2905 on theBenchmark for (2905ds/29340Mi)
% 208.81/41.45 % TRYING [8]
% 208.81/41.45 % (2731518)Instruction limit reached!
% 208.81/41.45 % (2731518)------------------------------
% 208.81/41.45 % (2731518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731518)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731518)Termination reason: Instruction limit
% 208.81/41.45 % (2731518)Termination phase: Saturation
% 208.81/41.45 % (2731518)Time elapsed: 2.209 s
% 208.81/41.45 % (2731518)Peak memory usage: 60 MB
% 208.81/41.45 % (2731518)Instructions burned: 4592 (million)
% 208.81/41.45 % (2731522)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2774388594:i=5211_2891 on theBenchmark for (2891ds/5211Mi)
% 208.81/41.45 % TRYING [11]
% 208.81/41.45 % TRYING [9]
% 208.81/41.45 % (2731522)Instruction limit reached!
% 208.81/41.45 % (2731522)------------------------------
% 208.81/41.45 % (2731522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731522)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731522)Termination reason: Instruction limit
% 208.81/41.45 % (2731522)Termination phase: Saturation
% 208.81/41.45 % (2731522)Time elapsed: 2.796 s
% 208.81/41.45 % (2731522)Peak memory usage: 52 MB
% 208.81/41.45 % (2731522)Instructions burned: 5212 (million)
% 208.81/41.45 % (2731524)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2970757499:i=5497:nm=2_2862 on theBenchmark for (2862ds/5497Mi)
% 208.81/41.45 % Detected minimum model sizes of [3]
% 208.81/41.45 % Detected maximum model sizes of [max]
% 208.81/41.45 % TRYING [17]
% 208.81/41.45 % (2731524)Instruction limit reached!
% 208.81/41.45 % (2731524)------------------------------
% 208.81/41.45 % (2731524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731524)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731524)Termination reason: Instruction limit
% 208.81/41.45 % (2731524)Termination phase: Finite model building constraint generation
% 208.81/41.45 % (2731524)Time elapsed: 1.906 s
% 208.81/41.45 % (2731524)Peak memory usage: 328 MB
% 208.81/41.45 % (2731524)Instructions burned: 5499 (million)
% 208.81/41.45 % (2731526)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1895876257:fmbsr=2:i=46332_2843 on theBenchmark for (2843ds/46332Mi)
% 208.81/41.45 % Detected minimum model sizes of [3]
% 208.81/41.45 % Detected maximum model sizes of [max]
% 208.81/41.45 % TRYING [15]
% 208.81/41.45 % TRYING [12]
% 208.81/41.45 % TRYING [10]
% 208.81/41.45 % (2731520)Instruction limit reached!
% 208.81/41.45 % (2731520)------------------------------
% 208.81/41.45 % (2731520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731520)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731520)Termination reason: Instruction limit
% 208.81/41.45 % (2731520)Termination phase: Saturation
% 208.81/41.45 % (2731520)Time elapsed: 12.764 s
% 208.81/41.45 % (2731520)Peak memory usage: 320 MB
% 208.81/41.45 % (2731520)Instructions burned: 29340 (million)
% 208.81/41.45 % (2731648)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2896890490:i=14071_2777 on theBenchmark for (2777ds/14071Mi)
% 208.81/41.45 % Detected minimum model sizes of [3]
% 208.81/41.45 % Detected maximum model sizes of [max]
% 208.81/41.45 % TRYING [12]
% 208.81/41.45 % (2731648)Instruction limit reached!
% 208.81/41.45 % (2731648)------------------------------
% 208.81/41.45 % (2731648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731648)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731648)Termination reason: Instruction limit
% 208.81/41.45 % (2731648)Termination phase: Finite model building SAT solving
% 208.81/41.45 % (2731648)Time elapsed: 6.628 s
% 208.81/41.45 % (2731648)Peak memory usage: 726 MB
% 208.81/41.45 % (2731648)Instructions burned: 14071 (million)
% 208.81/41.45 % (2731772)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3947908652:i=22565:add=on:rawr=on_2710 on theBenchmark for (2710ds/22565Mi)
% 208.81/41.45 % TRYING [11]
% 208.81/41.45 % (2731508)Instruction limit reached!
% 208.81/41.45 % (2731508)------------------------------
% 208.81/41.45 % (2731508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731508)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731508)Termination reason: Instruction limit
% 208.81/41.45 % (2731508)Termination phase: Finite model building SAT solving
% 208.81/41.45 % (2731508)Time elapsed: 29.545 s
% 208.81/41.45 % (2731508)Peak memory usage: 1067 MB
% 208.81/41.45 % (2731508)Instructions burned: 54282 (million)
% 208.81/41.45 % (2731931)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=664556243:i=8173:av=off_2656 on theBenchmark for (2656ds/8173Mi)
% 208.81/41.45 % (2731516)Instruction limit reached!
% 208.81/41.45 % (2731516)------------------------------
% 208.81/41.45 % (2731516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731516)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731516)Termination reason: Instruction limit
% 208.81/41.45 % (2731516)Termination phase: Finite model building SAT solving
% 208.81/41.45 % (2731516)Time elapsed: 27.578 s
% 208.81/41.45 % (2731516)Peak memory usage: 311 MB
% 208.81/41.45 % (2731516)Instructions burned: 67537 (million)
% 208.81/41.45 % (2731933)dis+10_16:1_sil=16000:random_seed=1550550720:i=9155:fsr=off_2639 on theBenchmark for (2639ds/9155Mi)
% 208.81/41.45 % TRYING [13]
% 208.81/41.45 % (2731931)Instruction limit reached!
% 208.81/41.45 % (2731931)------------------------------
% 208.81/41.45 % (2731931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731931)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731931)Termination reason: Instruction limit
% 208.81/41.45 % (2731931)Termination phase: Saturation
% 208.81/41.45 % (2731931)Time elapsed: 4.416 s
% 208.81/41.45 % (2731931)Peak memory usage: 88 MB
% 208.81/41.45 % (2731931)Instructions burned: 8174 (million)
% 208.81/41.45 % (2732048)ott-3_8_sil=64000:random_seed=3155122636:i=20139:bs=on_2611 on theBenchmark for (2611ds/20139Mi)
% 208.81/41.45 % (2731456)Instruction limit reached!
% 208.81/41.45 % (2731456)------------------------------
% 208.81/41.45 % (2731456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.45 % (2731456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.45 % (2731456)CaDiCaL version: 2.1.3
% 208.81/41.45 % (2731456)Termination reason: Instruction limit
% 208.81/41.45 % (2731456)Termination phase: Saturation
% 208.81/41.45 % (2731456)Time elapsed: 39.224 s
% 208.81/41.45 % (2731456)Peak memory usage: 254 MB
% 208.81/41.45 % (2731456)Instructions burned: 88025 (million)
% 208.81/41.45 % (2732050)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2788755215:fmbsr=2:i=32576_2607 on theBenchmark for (2607ds/32576Mi)
% 208.81/41.45 % Detected minimum model sizes of [3]
% 208.81/41.45 % Detected maximum model sizes of [max]
% 208.81/41.45 % TRYING [9]
% 208.81/41.45 % (2731455) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2731449-2731455"...
% 208.81/41.45 % (2731455)...printing done.
% 208.81/41.45 % (2731455)Refutation found. Thanks to Tanya!
% 208.81/41.45 % SZS status Theorem for theBenchmark
% 208.81/41.45 % SZS output start Proof for theBenchmark
% See solution above
% 208.81/41.46 % (2731455)------------------------------
% 208.81/41.46 % (2731455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.81/41.46 % (2731455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.81/41.46 % (2731455)CaDiCaL version: 2.1.3
% 208.81/41.46 % (2731455)Termination reason: Refutation
% 208.81/41.46 % (2731455)Time elapsed: 40.500 s
% 208.81/41.46 % (2731455)Peak memory usage: 525 MB
% 208.81/41.46 % (2731455)Instructions burned: 75702 (million)
% 208.81/41.46 % (2731449)Success in time 41.005 s
% 208.81/41.46 % Vampire exiting
%------------------------------------------------------------------------------