%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM481+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:29 PM UTC 2026
% Result : Theorem 23.93s 3.88s
% Output : Refutation 23.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 28
% Syntax : Number of formulae : 252 ( 36 unt; 9 def)
% Number of atoms : 920 ( 223 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1161 ( 493 ~; 520 |; 90 &)
% ( 21 <=>; 37 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 10 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 227 ( 0 sgn 211 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
aNaturalNumber0(sz00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC) ).
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f4,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f6,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddComm) ).
fof(f8,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_AddZero) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_MulZero) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( sdtpldt0(X0,X1) = sdtpldt0(X0,X2)
| sdtpldt0(X1,X0) = sdtpldt0(X2,X0) )
=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAddCanc) ).
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(f24,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != X1
& sdtlseqdt0(X0,X1) )
=> ! [X2] :
( aNaturalNumber0(X2)
=> ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMonAdd) ).
fof(f29,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != X1
& sdtlseqdt0(X0,X1) )
=> iLess0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mIH_03) ).
fof(f30,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
fof(f31,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != sz00
& doDivides0(X0,X1) )
=> ! [X2] :
( X2 = sdtsldt0(X1,X0)
<=> ( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
fof(f32,axiom,
! [X0,X1,X2] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1)
& aNaturalNumber0(X2) )
=> ( ( doDivides0(X0,X1)
& doDivides0(X1,X2) )
=> doDivides0(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDivTrans) ).
fof(f35,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( doDivides0(X0,X1)
& X1 != sz00 )
=> sdtlseqdt0(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDivLE) ).
fof(f37,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& doDivides0(X1,X0) )
=> ( X1 = sz10
| X1 = X0 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefPrime) ).
fof(f38,conjecture,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( ! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00
& X1 != sz10 )
=> ( iLess0(X1,X0)
=> ? [X2] :
( aNaturalNumber0(X2)
& doDivides0(X2,X1)
& isPrime0(X2) ) ) )
=> ? [X1] :
( aNaturalNumber0(X1)
& doDivides0(X1,X0)
& isPrime0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f39,negated_conjecture,
~ ! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( ! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00
& X1 != sz10 )
=> ( iLess0(X1,X0)
=> ? [X2] :
( aNaturalNumber0(X2)
& doDivides0(X2,X1)
& isPrime0(X2) ) ) )
=> ? [X1] :
( aNaturalNumber0(X1)
& doDivides0(X1,X0)
& isPrime0(X1) ) ) ),
inference(negated_conjecture,[status(cth)],[f38]) ).
fof(f40,plain,
~ ! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( ! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00
& X1 != sz10 )
=> ( iLess0(X1,X0)
=> ? [X2] :
( aNaturalNumber0(X2)
& doDivides0(X2,X1)
& isPrime0(X2) ) ) )
=> ? [X3] :
( aNaturalNumber0(X3)
& doDivides0(X3,X0)
& isPrime0(X3) ) ) ),
inference(rectify,[],[f39]) ).
fof(f42,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f43,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f45,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f44]) ).
fof(f46,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f47,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f46]) ).
fof(f50,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f55,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f56,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f59,plain,
! [X0,X1,X2] :
( X1 = X2
| ( sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
& sdtpldt0(X1,X0) != sdtpldt0(X2,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f60,plain,
! [X0,X1,X2] :
( X1 = X2
| ( sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
& sdtpldt0(X1,X0) != sdtpldt0(X2,X0) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f59]) ).
fof(f67,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f18]) ).
fof(f68,plain,
! [X0,X1] :
( ( sdtlseqdt0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& sdtpldt0(X0,X2) = X1 ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f67]) ).
fof(f72,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f21]) ).
fof(f73,plain,
! [X0,X1] :
( X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f72]) ).
fof(f78,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2) )
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f24]) ).
fof(f79,plain,
! [X0,X1] :
( ! [X2] :
( ( sdtpldt0(X2,X0) != sdtpldt0(X2,X1)
& sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1))
& sdtpldt0(X0,X2) != sdtpldt0(X1,X2)
& sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2)) )
| ~ aNaturalNumber0(X2) )
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f78]) ).
fof(f88,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f89,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f91,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f90]) ).
fof(f92,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(f93,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,[],[f92]) ).
fof(f94,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f95,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f94]) ).
fof(f100,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f101,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f100]) ).
fof(f104,plain,
! [X0] :
( ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) ) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f105,plain,
! [X0] :
( ( isPrime0(X0)
<=> ( X0 != sz00
& X0 != sz10
& ! [X1] :
( X1 = sz10
| X1 = X0
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X1,X0) ) ) )
| ~ aNaturalNumber0(X0) ),
inference(flattening,[],[f104]) ).
fof(f106,plain,
? [X0] :
( ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ doDivides0(X3,X0)
| ~ isPrime0(X3) )
& ! [X1] :
( ? [X2] :
( aNaturalNumber0(X2)
& doDivides0(X2,X1)
& isPrime0(X2) )
| ~ iLess0(X1,X0)
| ~ aNaturalNumber0(X1)
| sz00 = X1
| sz10 = X1 )
& aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 ),
inference(ennf_transformation,[],[f40]) ).
fof(f107,plain,
? [X0] :
( ! [X3] :
( ~ aNaturalNumber0(X3)
| ~ doDivides0(X3,X0)
| ~ isPrime0(X3) )
& ! [X1] :
( ? [X2] :
( aNaturalNumber0(X2)
& doDivides0(X2,X1)
& isPrime0(X2) )
| ~ iLess0(X1,X0)
| ~ aNaturalNumber0(X1)
| sz00 = X1
| sz10 = X1 )
& aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
aNaturalNumber0(sz00),
inference(cnf_transformation,[],[f2]) ).
fof(f109,plain,
sz00 != sz10,
inference(cnf_transformation,[],[f3]) ).
fof(f110,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f111,plain,
! [X0,X1] :
( aNaturalNumber0(sdtpldt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f43]) ).
fof(f112,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f45]) ).
fof(f113,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f47]) ).
fof(f115,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f50]) ).
fof(f120,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f122,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f56]) ).
fof(f125,plain,
! [X2,X0,X1] :
( sdtpldt0(X1,X0) != sdtpldt0(X2,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| X1 = X2 ),
inference(cnf_transformation,[],[f60]) ).
fof(f134,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f68]) ).
fof(f139,plain,
! [X0,X1] :
( ~ sdtlseqdt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f73]) ).
fof(f143,plain,
! [X2,X0,X1] :
( sdtlseqdt0(sdtpldt0(X0,X2),sdtpldt0(X1,X2))
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f79]) ).
fof(f153,plain,
! [X0,X1] :
( iLess0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f154,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sK1(X0,X1)) = X1
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f155,plain,
! [X0,X1] :
( aNaturalNumber0(sK1(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f156,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
fof(f159,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,[],[f93]) ).
fof(f160,plain,
! [X2,X0,X1] :
( doDivides0(X0,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f95]) ).
fof(f163,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| sz00 = X1
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
fof(f165,plain,
! [X0] :
( isPrime0(X0)
| doDivides0(sK2(X0),X0)
| sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f166,plain,
! [X0] :
( aNaturalNumber0(sK2(X0))
| ~ aNaturalNumber0(X0)
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f167,plain,
! [X0] :
( isPrime0(X0)
| sK2(X0) != X0
| sz10 = X0
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f168,plain,
! [X0] :
( sz10 != sK2(X0)
| ~ aNaturalNumber0(X0)
| sz10 = X0
| sz00 = X0
| isPrime0(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f172,plain,
! [X1] :
( isPrime0(sK4(X1))
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f173,plain,
! [X1] :
( doDivides0(sK4(X1),X1)
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f174,plain,
! [X1] :
( aNaturalNumber0(sK4(X1))
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f175,plain,
! [X3] :
( ~ doDivides0(X3,sK3)
| ~ isPrime0(X3)
| ~ aNaturalNumber0(X3) ),
inference(cnf_transformation,[],[f107]) ).
fof(f176,plain,
sz10 != sK3,
inference(cnf_transformation,[],[f107]) ).
fof(f177,plain,
sz00 != sK3,
inference(cnf_transformation,[],[f107]) ).
fof(f178,plain,
aNaturalNumber0(sK3),
inference(cnf_transformation,[],[f107]) ).
fof(f179,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X0,sdtpldt0(X0,X2)) ),
inference(equality_resolution,[],[f134]) ).
fof(f184,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f156]) ).
fof(f185,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,[],[f159]) ).
fof(f200,plain,
sz10 = sdtpldt0(sz00,sz10),
inference(resolution,[],[f115,f110]) ).
fof(f201,plain,
sK3 = sdtpldt0(sz00,sK3),
inference(resolution,[],[f115,f178]) ).
fof(f213,plain,
sK3 = sdtasdt0(sK3,sz10),
inference(resolution,[],[f120,f178]) ).
fof(f223,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sdtpldt0(X0,X1),sz00) ),
inference(resolution,[],[f111,f122]) ).
fof(f245,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(X0,sK3) = sdtpldt0(sK3,X0) ),
inference(resolution,[],[f113,f178]) ).
fof(f255,plain,
sdtpldt0(sz10,sK3) = sdtpldt0(sK3,sz10),
inference(resolution,[],[f245,f110]) ).
fof(f256,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(X0,X1),sK3) = sdtpldt0(sK3,sdtpldt0(X0,X1)) ),
inference(resolution,[],[f245,f111]) ).
fof(f297,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sK1(X0,X1) = sdtpldt0(sz00,sK1(X0,X1)) ),
inference(resolution,[],[f155,f115]) ).
fof(f320,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtpldt0(sdtpldt0(X0,sz10),sK3) = sdtpldt0(sK3,sdtpldt0(X0,sz10)) ),
inference(resolution,[],[f256,f110]) ).
fof(f392,plain,
sdtpldt0(sdtpldt0(sz00,sz10),sK3) = sdtpldt0(sK3,sdtpldt0(sz00,sz10)),
inference(resolution,[],[f320,f108]) ).
fof(f421,plain,
! [X2,X0] :
( sdtlseqdt0(X0,sdtpldt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f179,f111]) ).
fof(f440,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f184,f112]) ).
fof(f443,plain,
( doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(superposition,[],[f440,f213]) ).
fof(f449,plain,
( doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f443,f110]) ).
fof(f454,plain,
doDivides0(sK3,sK3),
inference(forward_subsumption_resolution,[],[f449,f178]) ).
fof(f492,plain,
( ~ isPrime0(sK3)
| ~ aNaturalNumber0(sK3) ),
inference(resolution,[],[f454,f175]) ).
fof(f493,plain,
( ~ aNaturalNumber0(sK3)
| sK3 = sdtasdt0(sK3,sK1(sK3,sK3))
| ~ aNaturalNumber0(sK3) ),
inference(resolution,[],[f454,f154]) ).
fof(f496,plain,
( ~ aNaturalNumber0(sK3)
| sK3 = sdtasdt0(sK3,sK1(sK3,sK3)) ),
inference(duplicate_literal_removal,[],[f493]) ).
fof(f497,plain,
sK3 = sdtasdt0(sK3,sK1(sK3,sK3)),
inference(forward_subsumption_resolution,[],[f496,f178]) ).
fof(f498,plain,
~ isPrime0(sK3),
inference(forward_subsumption_resolution,[],[f492,f178]) ).
fof(f501,plain,
( doDivides0(sK2(sK3),sK3)
| sz10 = sK3
| sz00 = sK3
| ~ aNaturalNumber0(sK3) ),
inference(resolution,[],[f498,f165]) ).
fof(f502,plain,
( doDivides0(sK2(sK3),sK3)
| sz00 = sK3
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f501,f176]) ).
fof(f503,plain,
( doDivides0(sK2(sK3),sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f502,f177]) ).
fof(f504,plain,
doDivides0(sK2(sK3),sK3),
inference(forward_subsumption_resolution,[],[f503,f178]) ).
fof(f507,plain,
( sK3 != sK2(sK3)
| sz10 = sK3
| sz00 = sK3
| ~ aNaturalNumber0(sK3) ),
inference(resolution,[],[f167,f498]) ).
fof(f508,plain,
( sK3 != sK2(sK3)
| sz00 = sK3
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f507,f176]) ).
fof(f509,plain,
( sK3 != sK2(sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f508,f177]) ).
fof(f510,plain,
sK3 != sK2(sK3),
inference(forward_subsumption_resolution,[],[f509,f178]) ).
fof(f518,plain,
( ~ aNaturalNumber0(sK2(sK3))
| sz00 = sK3
| ~ aNaturalNumber0(sK3)
| sdtlseqdt0(sK2(sK3),sK3) ),
inference(resolution,[],[f504,f163]) ).
fof(f519,plain,
( ~ aNaturalNumber0(sK2(sK3))
| ~ aNaturalNumber0(sK3)
| sdtlseqdt0(sK2(sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f518,f177]) ).
fof(f521,plain,
( ~ aNaturalNumber0(sK2(sK3))
| sdtlseqdt0(sK2(sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f519,f178]) ).
fof(f560,definition,
( spl5_1
<=> aNaturalNumber0(sK2(sK3)) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
fof(f561,plain,
( aNaturalNumber0(sK2(sK3))
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f562,plain,
( ~ aNaturalNumber0(sK2(sK3))
| spl5_1 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f570,plain,
( ~ aNaturalNumber0(sK3)
| sz10 = sK3
| sz00 = sK3
| isPrime0(sK3)
| spl5_1 ),
inference(resolution,[],[f562,f166]) ).
fof(f571,plain,
( sz10 = sK3
| sz00 = sK3
| isPrime0(sK3)
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f570,f178]) ).
fof(f572,plain,
( sz00 = sK3
| isPrime0(sK3)
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f571,f176]) ).
fof(f573,plain,
( isPrime0(sK3)
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f572,f177]) ).
fof(f574,plain,
( $false
| spl5_1 ),
inference(forward_subsumption_resolution,[],[f573,f498]) ).
fof(f575,plain,
spl5_1,
inference(avatar_contradiction_clause,[],[f574]) ).
fof(f600,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(sK3)
| ~ isPrime0(X1)
| ~ aNaturalNumber0(X1) ),
inference(resolution,[],[f160,f175]) ).
fof(f602,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| sz00 = X2
| ~ aNaturalNumber0(X2)
| sdtlseqdt0(X1,X2) ),
inference(resolution,[],[f160,f163]) ).
fof(f603,plain,
! [X2,X0,X1] :
( sdtlseqdt0(X1,X2)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,X2)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X2)
| sz00 = X2
| ~ aNaturalNumber0(X0) ),
inference(duplicate_literal_removal,[],[f602]) ).
fof(f605,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(sK3)
| ~ isPrime0(X1) ),
inference(duplicate_literal_removal,[],[f600]) ).
fof(f606,plain,
! [X0,X1] :
( ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X1) ),
inference(forward_subsumption_resolution,[],[f605,f178]) ).
fof(f1111,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2))
| sdtpldt0(X1,X2) = sdtpldt0(X0,X2) ),
inference(resolution,[],[f143,f139]) ).
fof(f1156,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X1,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2)) ),
inference(forward_subsumption_resolution,[],[f1111,f125]) ).
fof(f1166,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ aNaturalNumber0(sdtpldt0(X0,X2)) ),
inference(forward_subsumption_resolution,[],[f1156,f111]) ).
fof(f1170,plain,
! [X2,X0,X1] :
( ~ sdtlseqdt0(sdtpldt0(X1,X2),sdtpldt0(X0,X2))
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f1166,f111]) ).
fof(f1266,plain,
( sdtlseqdt0(sK2(sK3),sK3)
| ~ spl5_1 ),
inference(forward_subsumption_resolution,[],[f521,f561]) ).
fof(f1621,plain,
! [X2,X0] :
( ~ aNaturalNumber0(X0)
| ~ doDivides0(X0,sdtasdt0(X0,X2))
| sz00 = X0
| ~ aNaturalNumber0(X2)
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(forward_subsumption_resolution,[],[f185,f112]) ).
fof(f1622,plain,
! [X2,X0] :
( ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sdtsldt0(sdtasdt0(X0,X2),X0) = X2 ),
inference(forward_subsumption_resolution,[],[f1621,f440]) ).
fof(f1679,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sK3
| sdtsldt0(sdtasdt0(sK3,X0),sK3) = X0 ),
inference(resolution,[],[f1622,f178]) ).
fof(f1682,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtsldt0(sdtasdt0(sK3,X0),sK3) = X0 ),
inference(forward_subsumption_resolution,[],[f1679,f177]) ).
fof(f1729,plain,
sz10 = sdtsldt0(sdtasdt0(sK3,sz10),sK3),
inference(resolution,[],[f1682,f110]) ).
fof(f1740,plain,
sz10 = sdtsldt0(sK3,sK3),
inference(forward_demodulation,[],[f1729,f213]) ).
fof(f1757,plain,
! [X0] :
( ~ doDivides0(X0,sK3)
| ~ aNaturalNumber0(sK4(X0))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(sK4(X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ iLess0(X0,sK3)
| sz10 = X0 ),
inference(resolution,[],[f606,f173]) ).
fof(f1760,plain,
! [X0] :
( ~ doDivides0(X0,sK3)
| ~ aNaturalNumber0(sK4(X0))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(sK4(X0))
| sz00 = X0
| ~ iLess0(X0,sK3)
| sz10 = X0 ),
inference(duplicate_literal_removal,[],[f1757]) ).
fof(f1766,plain,
! [X0] :
( ~ doDivides0(X0,sK3)
| ~ aNaturalNumber0(X0)
| ~ isPrime0(sK4(X0))
| sz00 = X0
| ~ iLess0(X0,sK3)
| sz10 = X0 ),
inference(forward_subsumption_resolution,[],[f1760,f174]) ).
fof(f1773,plain,
! [X0] :
( ~ iLess0(X0,sK3)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ doDivides0(X0,sK3)
| sz10 = X0 ),
inference(forward_subsumption_resolution,[],[f1766,f172]) ).
fof(f2088,definition,
( spl5_3
<=> sz00 = sK2(sK3) ),
introduced(definition,[new_symbols(definition,[spl5_3])],[avatar_definition]) ).
fof(f2089,plain,
( sz00 != sK2(sK3)
| spl5_3 ),
inference(avatar_component_clause,[],[f2088]) ).
fof(f2090,plain,
( sz00 = sK2(sK3)
| ~ spl5_3 ),
inference(avatar_component_clause,[],[f2088]) ).
fof(f3763,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sdtpldt0(X0,sK3),sz00) ),
inference(resolution,[],[f223,f178]) ).
fof(f3888,plain,
sz00 = sdtasdt0(sdtpldt0(sz10,sK3),sz00),
inference(resolution,[],[f3763,f110]) ).
fof(f3909,plain,
( doDivides0(sdtpldt0(sz10,sK3),sz00)
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,sK3)) ),
inference(superposition,[],[f440,f3888]) ).
fof(f3910,plain,
( doDivides0(sdtpldt0(sz10,sK3),sz00)
| ~ aNaturalNumber0(sdtpldt0(sz10,sK3)) ),
inference(forward_subsumption_resolution,[],[f3909,f108]) ).
fof(f6160,plain,
( ~ aNaturalNumber0(sK3)
| ~ aNaturalNumber0(sK3)
| sK1(sK3,sK3) = sdtpldt0(sz00,sK1(sK3,sK3)) ),
inference(resolution,[],[f297,f454]) ).
fof(f6165,plain,
( ~ aNaturalNumber0(sK3)
| sK1(sK3,sK3) = sdtpldt0(sz00,sK1(sK3,sK3)) ),
inference(duplicate_literal_removal,[],[f6160]) ).
fof(f6173,plain,
sK1(sK3,sK3) = sdtpldt0(sz00,sK1(sK3,sK3)),
inference(forward_subsumption_resolution,[],[f6165,f178]) ).
fof(f6765,plain,
( sdtlseqdt0(sz00,sK1(sK3,sK3))
| ~ aNaturalNumber0(sK1(sK3,sK3))
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[],[f421,f6173]) ).
fof(f6767,plain,
( sdtlseqdt0(sz00,sK1(sK3,sK3))
| ~ aNaturalNumber0(sK1(sK3,sK3)) ),
inference(forward_subsumption_resolution,[],[f6765,f108]) ).
fof(f7309,definition,
( spl5_7
<=> aNaturalNumber0(sdtpldt0(sz10,sK3)) ),
introduced(definition,[new_symbols(definition,[spl5_7])],[avatar_definition]) ).
fof(f7310,plain,
( aNaturalNumber0(sdtpldt0(sz10,sK3))
| ~ spl5_7 ),
inference(avatar_component_clause,[],[f7309]) ).
fof(f7311,plain,
( ~ aNaturalNumber0(sdtpldt0(sz10,sK3))
| spl5_7 ),
inference(avatar_component_clause,[],[f7309]) ).
fof(f7313,definition,
( spl5_8
<=> doDivides0(sdtpldt0(sz10,sK3),sz00) ),
introduced(definition,[new_symbols(definition,[spl5_8])],[avatar_definition]) ).
fof(f7315,plain,
( doDivides0(sdtpldt0(sz10,sK3),sz00)
| ~ spl5_8 ),
inference(avatar_component_clause,[],[f7313]) ).
fof(f7316,plain,
( ~ spl5_7
| spl5_8 ),
inference(avatar_split_clause,[],[f3910,f7313,f7309]) ).
fof(f7324,plain,
( ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3)
| spl5_7 ),
inference(resolution,[],[f7311,f111]) ).
fof(f7325,plain,
( ~ aNaturalNumber0(sK3)
| spl5_7 ),
inference(forward_subsumption_resolution,[],[f7324,f110]) ).
fof(f7326,plain,
( $false
| spl5_7 ),
inference(forward_subsumption_resolution,[],[f7325,f178]) ).
fof(f7327,plain,
spl5_7,
inference(avatar_contradiction_clause,[],[f7326]) ).
fof(f7779,definition,
( spl5_10
<=> doDivides0(sz00,sK3) ),
introduced(definition,[new_symbols(definition,[spl5_10])],[avatar_definition]) ).
fof(f7780,plain,
( doDivides0(sz00,sK3)
| ~ spl5_10 ),
inference(avatar_component_clause,[],[f7779]) ).
fof(f7781,plain,
( ~ doDivides0(sz00,sK3)
| spl5_10 ),
inference(avatar_component_clause,[],[f7779]) ).
fof(f10728,definition,
( spl5_18
<=> aNaturalNumber0(sK1(sK3,sK3)) ),
introduced(definition,[new_symbols(definition,[spl5_18])],[avatar_definition]) ).
fof(f10729,plain,
( aNaturalNumber0(sK1(sK3,sK3))
| ~ spl5_18 ),
inference(avatar_component_clause,[],[f10728]) ).
fof(f10730,plain,
( ~ aNaturalNumber0(sK1(sK3,sK3))
| spl5_18 ),
inference(avatar_component_clause,[],[f10728]) ).
fof(f10879,plain,
( ~ aNaturalNumber0(sK3)
| ~ aNaturalNumber0(sK3)
| ~ doDivides0(sK3,sK3)
| spl5_18 ),
inference(resolution,[],[f10730,f155]) ).
fof(f10880,plain,
( ~ aNaturalNumber0(sK3)
| ~ doDivides0(sK3,sK3)
| spl5_18 ),
inference(duplicate_literal_removal,[],[f10879]) ).
fof(f10881,plain,
( ~ doDivides0(sK3,sK3)
| spl5_18 ),
inference(forward_subsumption_resolution,[],[f10880,f178]) ).
fof(f10882,plain,
( $false
| spl5_18 ),
inference(forward_subsumption_resolution,[],[f10881,f454]) ).
fof(f10883,plain,
spl5_18,
inference(avatar_contradiction_clause,[],[f10882]) ).
fof(f11266,plain,
( sK1(sK3,sK3) = sdtsldt0(sdtasdt0(sK3,sK1(sK3,sK3)),sK3)
| ~ spl5_18 ),
inference(resolution,[],[f10729,f1682]) ).
fof(f11279,plain,
( sK1(sK3,sK3) = sdtsldt0(sK3,sK3)
| ~ spl5_18 ),
inference(forward_demodulation,[],[f11266,f497]) ).
fof(f11327,plain,
( sz10 = sK1(sK3,sK3)
| ~ spl5_18 ),
inference(forward_demodulation,[],[f11279,f1740]) ).
fof(f11553,plain,
! [X0] :
( ~ sdtlseqdt0(sdtpldt0(X0,sK3),sK3)
| ~ sdtlseqdt0(sz00,X0)
| sz00 = X0
| ~ aNaturalNumber0(sK3)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz00) ),
inference(superposition,[],[f1170,f201]) ).
fof(f11604,plain,
! [X0] :
( ~ sdtlseqdt0(sdtpldt0(X0,sK3),sK3)
| ~ sdtlseqdt0(sz00,X0)
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sz00) ),
inference(forward_subsumption_resolution,[],[f11553,f178]) ).
fof(f11672,plain,
! [X0] :
( ~ sdtlseqdt0(sdtpldt0(X0,sK3),sK3)
| ~ sdtlseqdt0(sz00,X0)
| sz00 = X0
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f11604,f108]) ).
fof(f13033,plain,
( sdtlseqdt0(sz00,sK1(sK3,sK3))
| ~ spl5_18 ),
inference(forward_subsumption_resolution,[],[f6767,f10729]) ).
fof(f13034,plain,
( sdtlseqdt0(sz00,sz10)
| ~ spl5_18 ),
inference(forward_demodulation,[],[f13033,f11327]) ).
fof(f36046,definition,
( spl5_26
<=> sdtlseqdt0(sdtpldt0(sz10,sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl5_26])],[avatar_definition]) ).
fof(f36047,plain,
( ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| spl5_26 ),
inference(avatar_component_clause,[],[f36046]) ).
fof(f45880,plain,
( ~ sdtlseqdt0(sdtpldt0(sK3,sdtpldt0(sz00,sz10)),sK3)
| ~ sdtlseqdt0(sz00,sdtpldt0(sz00,sz10))
| sz00 = sdtpldt0(sz00,sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10)) ),
inference(superposition,[],[f11672,f392]) ).
fof(f45887,plain,
( ~ sdtlseqdt0(sdtpldt0(sK3,sz10),sK3)
| ~ sdtlseqdt0(sz00,sdtpldt0(sz00,sz10))
| sz00 = sdtpldt0(sz00,sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10)) ),
inference(forward_demodulation,[],[f45880,f200]) ).
fof(f45895,plain,
( ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| ~ sdtlseqdt0(sz00,sdtpldt0(sz00,sz10))
| sz00 = sdtpldt0(sz00,sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10)) ),
inference(forward_demodulation,[],[f45887,f255]) ).
fof(f45899,plain,
( ~ sdtlseqdt0(sz00,sz10)
| ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| sz00 = sdtpldt0(sz00,sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10)) ),
inference(forward_demodulation,[],[f45895,f200]) ).
fof(f45901,plain,
( ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| sz00 = sdtpldt0(sz00,sz10)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10))
| ~ spl5_18 ),
inference(forward_subsumption_resolution,[],[f45899,f13034]) ).
fof(f45903,plain,
( sz00 = sz10
| ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10))
| ~ spl5_18 ),
inference(forward_demodulation,[],[f45901,f200]) ).
fof(f45905,plain,
( ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| ~ aNaturalNumber0(sdtpldt0(sz00,sz10))
| ~ spl5_18 ),
inference(forward_subsumption_resolution,[],[f45903,f109]) ).
fof(f45907,plain,
( ~ aNaturalNumber0(sz10)
| ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| ~ spl5_18 ),
inference(forward_demodulation,[],[f45905,f200]) ).
fof(f45909,plain,
( ~ sdtlseqdt0(sdtpldt0(sz10,sK3),sK3)
| ~ spl5_18 ),
inference(forward_subsumption_resolution,[],[f45907,f110]) ).
fof(f45911,plain,
( ~ spl5_26
| ~ spl5_18 ),
inference(avatar_split_clause,[],[f45909,f10728,f36046]) ).
fof(f45964,plain,
( ! [X0] :
( ~ aNaturalNumber0(sdtpldt0(sz10,sK3))
| ~ doDivides0(X0,sK3)
| ~ doDivides0(sdtpldt0(sz10,sK3),X0)
| ~ aNaturalNumber0(sK3)
| sz00 = sK3
| ~ aNaturalNumber0(X0) )
| spl5_26 ),
inference(resolution,[],[f36047,f603]) ).
fof(f45972,plain,
( ! [X0] :
( ~ doDivides0(X0,sK3)
| ~ doDivides0(sdtpldt0(sz10,sK3),X0)
| ~ aNaturalNumber0(sK3)
| sz00 = sK3
| ~ aNaturalNumber0(X0) )
| ~ spl5_7
| spl5_26 ),
inference(forward_subsumption_resolution,[],[f45964,f7310]) ).
fof(f45978,plain,
( ! [X0] :
( ~ doDivides0(X0,sK3)
| ~ doDivides0(sdtpldt0(sz10,sK3),X0)
| sz00 = sK3
| ~ aNaturalNumber0(X0) )
| ~ spl5_7
| spl5_26 ),
inference(forward_subsumption_resolution,[],[f45972,f178]) ).
fof(f45980,plain,
( ! [X0] :
( ~ doDivides0(sdtpldt0(sz10,sK3),X0)
| ~ doDivides0(X0,sK3)
| ~ aNaturalNumber0(X0) )
| ~ spl5_7
| spl5_26 ),
inference(forward_subsumption_resolution,[],[f45978,f177]) ).
fof(f52577,plain,
( ~ doDivides0(sz00,sK3)
| ~ aNaturalNumber0(sz00)
| ~ spl5_7
| ~ spl5_8
| spl5_26 ),
inference(resolution,[],[f45980,f7315]) ).
fof(f55059,definition,
( spl5_46
<=> sz10 = sK2(sK3) ),
introduced(definition,[new_symbols(definition,[spl5_46])],[avatar_definition]) ).
fof(f55060,plain,
( sz10 != sK2(sK3)
| spl5_46 ),
inference(avatar_component_clause,[],[f55059]) ).
fof(f55061,plain,
( sz10 = sK2(sK3)
| ~ spl5_46 ),
inference(avatar_component_clause,[],[f55059]) ).
fof(f56724,plain,
( doDivides0(sz00,sK3)
| ~ spl5_3 ),
inference(superposition,[],[f504,f2090]) ).
fof(f56827,plain,
( $false
| ~ spl5_3
| spl5_10 ),
inference(forward_subsumption_resolution,[],[f56724,f7781]) ).
fof(f56828,plain,
( ~ spl5_3
| spl5_10 ),
inference(avatar_contradiction_clause,[],[f56827]) ).
fof(f57557,plain,
( sz10 != sz10
| ~ aNaturalNumber0(sK3)
| sz10 = sK3
| sz00 = sK3
| isPrime0(sK3)
| ~ spl5_46 ),
inference(superposition,[],[f168,f55061]) ).
fof(f57559,plain,
( ~ aNaturalNumber0(sK3)
| sz10 = sK3
| sz00 = sK3
| isPrime0(sK3)
| ~ spl5_46 ),
inference(trivial_inequality_removal,[],[f57557]) ).
fof(f57560,plain,
( sz10 = sK3
| sz00 = sK3
| isPrime0(sK3)
| ~ spl5_46 ),
inference(forward_subsumption_resolution,[],[f57559,f178]) ).
fof(f57577,plain,
( sz00 = sK3
| isPrime0(sK3)
| ~ spl5_46 ),
inference(forward_subsumption_resolution,[],[f57560,f176]) ).
fof(f57578,plain,
( isPrime0(sK3)
| ~ spl5_46 ),
inference(forward_subsumption_resolution,[],[f57577,f177]) ).
fof(f57579,plain,
( $false
| ~ spl5_46 ),
inference(forward_subsumption_resolution,[],[f57578,f498]) ).
fof(f57580,plain,
~ spl5_46,
inference(avatar_contradiction_clause,[],[f57579]) ).
fof(f71745,plain,
( ~ doDivides0(sz00,sK3)
| ~ spl5_7
| ~ spl5_8
| spl5_26 ),
inference(forward_subsumption_resolution,[],[f52577,f108]) ).
fof(f72257,plain,
( $false
| ~ spl5_7
| ~ spl5_8
| ~ spl5_10
| spl5_26 ),
inference(forward_subsumption_resolution,[],[f71745,f7780]) ).
fof(f72258,plain,
( ~ spl5_7
| ~ spl5_8
| ~ spl5_10
| spl5_26 ),
inference(avatar_contradiction_clause,[],[f72257]) ).
fof(f84629,definition,
( spl5_53
<=> iLess0(sK2(sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl5_53])],[avatar_definition]) ).
fof(f84630,plain,
( iLess0(sK2(sK3),sK3)
| ~ spl5_53 ),
inference(avatar_component_clause,[],[f84629]) ).
fof(f84631,plain,
( ~ iLess0(sK2(sK3),sK3)
| spl5_53 ),
inference(avatar_component_clause,[],[f84629]) ).
fof(f84658,plain,
( ~ aNaturalNumber0(sK2(sK3))
| ~ sdtlseqdt0(sK2(sK3),sK3)
| sK3 = sK2(sK3)
| ~ aNaturalNumber0(sK3)
| spl5_53 ),
inference(resolution,[],[f84631,f153]) ).
fof(f84659,plain,
( ~ sdtlseqdt0(sK2(sK3),sK3)
| sK3 = sK2(sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl5_1
| spl5_53 ),
inference(forward_subsumption_resolution,[],[f84658,f561]) ).
fof(f84660,plain,
( sK3 = sK2(sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl5_1
| spl5_53 ),
inference(forward_subsumption_resolution,[],[f84659,f1266]) ).
fof(f84661,plain,
( ~ aNaturalNumber0(sK3)
| ~ spl5_1
| spl5_53 ),
inference(forward_subsumption_resolution,[],[f84660,f510]) ).
fof(f84662,plain,
( $false
| ~ spl5_1
| spl5_53 ),
inference(forward_subsumption_resolution,[],[f84661,f178]) ).
fof(f84663,plain,
( ~ spl5_1
| spl5_53 ),
inference(avatar_contradiction_clause,[],[f84662]) ).
fof(f84719,plain,
( ~ aNaturalNumber0(sK2(sK3))
| sz00 = sK2(sK3)
| ~ doDivides0(sK2(sK3),sK3)
| sz10 = sK2(sK3)
| ~ spl5_53 ),
inference(resolution,[],[f84630,f1773]) ).
fof(f84842,plain,
( sz00 = sK2(sK3)
| ~ doDivides0(sK2(sK3),sK3)
| sz10 = sK2(sK3)
| ~ spl5_1
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f84719,f561]) ).
fof(f84931,plain,
( ~ doDivides0(sK2(sK3),sK3)
| sz10 = sK2(sK3)
| ~ spl5_1
| spl5_3
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f84842,f2089]) ).
fof(f85020,plain,
( sz10 = sK2(sK3)
| ~ spl5_1
| spl5_3
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f84931,f504]) ).
fof(f85059,plain,
( $false
| ~ spl5_1
| spl5_3
| spl5_46
| ~ spl5_53 ),
inference(forward_subsumption_resolution,[],[f85020,f55060]) ).
fof(f85060,plain,
( ~ spl5_1
| spl5_3
| spl5_46
| ~ spl5_53 ),
inference(avatar_contradiction_clause,[],[f85059]) ).
cnf(s2,plain,
spl5_1,
inference(sat_conversion,[],[f575]) ).
cnf(s6,plain,
( ~ spl5_7
| spl5_8 ),
inference(sat_conversion,[],[f7316]) ).
cnf(s7,plain,
spl5_7,
inference(sat_conversion,[],[f7327]) ).
cnf(s17,plain,
spl5_18,
inference(sat_conversion,[],[f10883]) ).
cnf(s30,plain,
( ~ spl5_18
| ~ spl5_26 ),
inference(sat_conversion,[],[f45911]) ).
cnf(s60,plain,
( ~ spl5_3
| spl5_10 ),
inference(sat_conversion,[],[f56828]) ).
cnf(s62,plain,
~ spl5_46,
inference(sat_conversion,[],[f57580]) ).
cnf(s66,plain,
( ~ spl5_7
| ~ spl5_8
| ~ spl5_10
| spl5_26 ),
inference(sat_conversion,[],[f72258]) ).
cnf(s70,plain,
( ~ spl5_1
| spl5_53 ),
inference(sat_conversion,[],[f84663]) ).
cnf(s71,plain,
( ~ spl5_1
| spl5_3
| spl5_46
| ~ spl5_53 ),
inference(sat_conversion,[],[f85060]) ).
cnf(s85,plain,
~ spl5_26,
inference(rat,[],[s30,s17]) ).
cnf(s94,plain,
spl5_8,
inference(rat,[],[s6,s7]) ).
cnf(s95,plain,
~ spl5_10,
inference(rat,[],[s66,s85,s7,s94]) ).
cnf(s96,plain,
~ spl5_3,
inference(rat,[],[s60,s95]) ).
cnf(s100,plain,
~ spl5_53,
inference(rat,[],[s71,s96,s62,s2]) ).
cnf(s101,plain,
$false,
inference(rat,[],[s70,s100,s2]) ).
fof(f85066,plain,
$false,
inference(avatar_sat_refutation,[],[s101]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM481+1 : 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 : n011.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:06:01 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
% 14.70/2.51 % (2724887)Will run a generic schedule for satisfiability detection.
% 14.70/2.51 % (2724896)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=536411677:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.70/2.51 % (2724893)% WARNING: option uhcvi not known.
% 14.70/2.51 % (2724892)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2150872400_2999 on theBenchmark for (2999ds/0Mi)
% 14.70/2.51 % (2724893)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=41614074:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.70/2.51 % (2724894)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1901298419:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.70/2.51 % (2724895)dis+10_1_sil=32000:sp=arity:random_seed=1776783081:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.70/2.51 % (2724897)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4259732440:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.70/2.51 % (2724898)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2560016810:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.70/2.51 % Detected minimum model sizes of [3]
% 14.70/2.51 % Detected maximum model sizes of [max]
% 14.70/2.51 % TRYING [3]
% 14.70/2.51 % TRYING [4]
% 14.70/2.51 % (2724896)Instruction limit reached!
% 14.70/2.51 % (2724896)------------------------------
% 14.70/2.51 % (2724896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.51 % (2724896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.51 % (2724896)CaDiCaL version: 2.1.3
% 14.70/2.51 % (2724896)Termination reason: Instruction limit
% 14.70/2.51 % (2724896)Termination phase: Saturation
% 14.70/2.51 % (2724896)Time elapsed: 0.038 s
% 14.70/2.51 % (2724896)Peak memory usage: 13 MB
% 14.70/2.51 % (2724896)Instructions burned: 117 (million)
% 14.70/2.51 % TRYING [5]
% 14.70/2.51 % (2724906)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2253057269:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.70/2.51 % Detected minimum model sizes of [3]
% 14.70/2.51 % Detected maximum model sizes of [max]
% 14.70/2.51 % TRYING [3]
% 14.70/2.51 % TRYING [4]
% 14.70/2.51 % TRYING [5]
% 14.70/2.51 % (2724895)Instruction limit reached!
% 14.70/2.51 % (2724895)------------------------------
% 14.70/2.51 % (2724895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.51 % (2724895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.51 % (2724895)CaDiCaL version: 2.1.3
% 14.70/2.51 % (2724895)Termination reason: Instruction limit
% 14.70/2.51 % (2724895)Termination phase: Saturation
% 14.70/2.51 % (2724895)Time elapsed: 0.063 s
% 14.70/2.51 % (2724895)Peak memory usage: 13 MB
% 14.70/2.51 % (2724895)Instructions burned: 104 (million)
% 14.70/2.51 % (2724897)Instruction limit reached!
% 14.70/2.51 % (2724897)------------------------------
% 14.70/2.51 % (2724897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.51 % (2724897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.51 % (2724897)CaDiCaL version: 2.1.3
% 14.70/2.51 % (2724897)Termination reason: Instruction limit
% 14.70/2.51 % (2724897)Termination phase: Saturation
% 14.70/2.51 % (2724897)Time elapsed: 0.071 s
% 14.70/2.51 % (2724897)Peak memory usage: 13 MB
% 14.70/2.51 % (2724897)Instructions burned: 131 (million)
% 14.70/2.51 % (2724908)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1379983764:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 14.70/2.51 % (2724909)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=1633267105:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.70/2.51 % (2724898)Instruction limit reached!
% 14.70/2.51 % (2724898)------------------------------
% 14.70/2.51 % (2724898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.70/2.51 % (2724898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.70/2.51 % (2724898)CaDiCaL version: 2.1.3
% 14.70/2.51 % (2724898)Termination reason: Instruction limit
% 14.70/2.51 % (2724898)Termination phase: Saturation
% 14.70/2.51 % (2724898)Time elapsed: 0.095 s
% 14.70/2.51 % (2724898)Peak memory usage: 14 MB
% 14.70/2.51 % (2724898)Instructions burned: 160 (million)
% 14.70/2.51 % TRYING [6]
% 14.70/2.51 % TRYING [6]
% 14.70/2.51 % (2724912)ott-21_1_sil=16000:fs=off:random_seed=1789578537:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.70/2.51 % (2724908)Instruction limit reached!
% 23.93/3.88 % (2724908)------------------------------
% 23.93/3.88 % (2724908)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724908)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724908)Termination reason: Instruction limit
% 23.93/3.88 % (2724908)Termination phase: Saturation
% 23.93/3.88 % (2724908)Time elapsed: 0.071 s
% 23.93/3.88 % (2724908)Peak memory usage: 12 MB
% 23.93/3.88 % (2724908)Instructions burned: 131 (million)
% 23.93/3.88 % (2724914)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=723695787:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 23.93/3.88 % (2724906)Instruction limit reached!
% 23.93/3.88 % (2724906)------------------------------
% 23.93/3.88 % (2724906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724906)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724906)Termination reason: Instruction limit
% 23.93/3.88 % (2724906)Termination phase: Finite model building constraint generation
% 23.93/3.88 % (2724906)Time elapsed: 0.136 s
% 23.93/3.88 % (2724906)Peak memory usage: 32 MB
% 23.93/3.88 % (2724906)Instructions burned: 715 (million)
% 23.93/3.88 % (2724916)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=547355468:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 23.93/3.88 % Detected minimum model sizes of [3]
% 23.93/3.88 % Detected maximum model sizes of [max]
% 23.93/3.88 % TRYING [3]
% 23.93/3.88 % TRYING [4]
% 23.93/3.88 % (2724912)Instruction limit reached!
% 23.93/3.88 % (2724912)------------------------------
% 23.93/3.88 % (2724912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724912)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724912)Termination reason: Instruction limit
% 23.93/3.88 % (2724912)Termination phase: Saturation
% 23.93/3.88 % (2724912)Time elapsed: 0.095 s
% 23.93/3.88 % (2724912)Peak memory usage: 13 MB
% 23.93/3.88 % (2724912)Instructions burned: 180 (million)
% 23.93/3.88 % (2724918)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3159919922:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 23.93/3.88 % TRYING [5]
% 23.93/3.88 % TRYING [7]
% 23.93/3.88 % TRYING [6]
% 23.93/3.88 % (2724916)Instruction limit reached!
% 23.93/3.88 % (2724916)------------------------------
% 23.93/3.88 % (2724916)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724916)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724916)Termination reason: Instruction limit
% 23.93/3.88 % (2724916)Termination phase: Finite model building constraint generation
% 23.93/3.88 % (2724916)Time elapsed: 0.183 s
% 23.93/3.88 % (2724916)Peak memory usage: 22 MB
% 23.93/3.88 % (2724916)Instructions burned: 868 (million)
% 23.93/3.88 % (2724920)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1246157521:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 23.93/3.88 % (2724909)Instruction limit reached!
% 23.93/3.88 % (2724909)------------------------------
% 23.93/3.88 % (2724909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724909)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724909)Termination reason: Instruction limit
% 23.93/3.88 % (2724909)Termination phase: Saturation
% 23.93/3.88 % (2724909)Time elapsed: 0.364 s
% 23.93/3.88 % (2724909)Peak memory usage: 17 MB
% 23.93/3.88 % (2724909)Instructions burned: 685 (million)
% 23.93/3.88 % (2724922)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=2138175706: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)
% 23.93/3.88 % TRYING [14]
% 23.93/3.88 % (2724914)Instruction limit reached!
% 23.93/3.88 % (2724914)------------------------------
% 23.93/3.88 % (2724914)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724914)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724914)Termination reason: Instruction limit
% 23.93/3.88 % (2724914)Termination phase: Saturation
% 23.93/3.88 % (2724914)Time elapsed: 0.326 s
% 23.93/3.88 % (2724914)Peak memory usage: 15 MB
% 23.93/3.88 % (2724914)Instructions burned: 478 (million)
% 23.93/3.88 % (2724924)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3921450189:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 23.93/3.88 % (2724920)Instruction limit reached!
% 23.93/3.88 % (2724920)------------------------------
% 23.93/3.88 % (2724920)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724920)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724920)Termination reason: Instruction limit
% 23.93/3.88 % (2724920)Termination phase: Finite model building constraint generation
% 23.93/3.88 % (2724920)Time elapsed: 0.191 s
% 23.93/3.88 % (2724920)Peak memory usage: 80 MB
% 23.93/3.88 % (2724920)Instructions burned: 892 (million)
% 23.93/3.88 % (2724926)fmb+10_1_sil=64000:random_seed=3209530621:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 23.93/3.88 % Detected minimum model sizes of [3]
% 23.93/3.88 % Detected maximum model sizes of [max]
% 23.93/3.88 % TRYING [3]
% 23.93/3.88 % TRYING [4]
% 23.93/3.88 % TRYING [5]
% 23.93/3.88 % TRYING [8]
% 23.93/3.88 % TRYING [6]
% 23.93/3.88 % (2724922)Instruction limit reached!
% 23.93/3.88 % (2724922)------------------------------
% 23.93/3.88 % (2724922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724922)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724922)Termination reason: Instruction limit
% 23.93/3.88 % (2724922)Termination phase: Saturation
% 23.93/3.88 % (2724922)Time elapsed: 0.389 s
% 23.93/3.88 % (2724922)Peak memory usage: 21 MB
% 23.93/3.88 % (2724922)Instructions burned: 692 (million)
% 23.93/3.88 % (2724928)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3709575755:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 23.93/3.88 % Detected minimum model sizes of [3]
% 23.93/3.88 % Detected maximum model sizes of [max]
% 23.93/3.88 % TRYING [20]
% 23.93/3.88 % (2724918)Instruction limit reached!
% 23.93/3.88 % (2724918)------------------------------
% 23.93/3.88 % (2724918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724918)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724918)Termination reason: Instruction limit
% 23.93/3.88 % (2724918)Termination phase: Saturation
% 23.93/3.88 % (2724918)Time elapsed: 0.672 s
% 23.93/3.88 % (2724918)Peak memory usage: 25 MB
% 23.93/3.88 % (2724918)Instructions burned: 1180 (million)
% 23.93/3.88 % (2724930)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3150599558:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 23.93/3.88 % Detected minimum model sizes of [3]
% 23.93/3.88 % Detected maximum model sizes of [max]
% 23.93/3.88 % TRYING [8]
% 23.93/3.88 % (2724924)Instruction limit reached!
% 23.93/3.88 % (2724924)------------------------------
% 23.93/3.88 % (2724924)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724924)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724924)Termination reason: Instruction limit
% 23.93/3.88 % (2724924)Termination phase: Saturation
% 23.93/3.88 % (2724924)Time elapsed: 0.507 s
% 23.93/3.88 % (2724924)Peak memory usage: 20 MB
% 23.93/3.88 % (2724924)Instructions burned: 881 (million)
% 23.93/3.88 % (2724932)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3878315032:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 23.93/3.88 % TRYING [7]
% 23.93/3.88 % (2724930)Instruction limit reached!
% 23.93/3.88 % (2724930)------------------------------
% 23.93/3.88 % (2724930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724930)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724930)Termination reason: Instruction limit
% 23.93/3.88 % (2724930)Termination phase: Finite model building constraint generation
% 23.93/3.88 % (2724930)Time elapsed: 0.339 s
% 23.93/3.88 % (2724930)Peak memory usage: 67 MB
% 23.93/3.88 % (2724930)Instructions burned: 921 (million)
% 23.93/3.88 % (2724934)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3565932374:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 23.93/3.88 % TRYING [9]
% 23.93/3.88 % TRYING [8]
% 23.93/3.88 % (2724934)Instruction limit reached!
% 23.93/3.88 % (2724934)------------------------------
% 23.93/3.88 % (2724934)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724934)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724934)Termination reason: Instruction limit
% 23.93/3.88 % (2724934)Termination phase: Saturation
% 23.93/3.88 % (2724934)Time elapsed: 0.763 s
% 23.93/3.88 % (2724934)Peak memory usage: 33 MB
% 23.93/3.88 % (2724934)Instructions burned: 1474 (million)
% 23.93/3.88 % (2724936)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=452875120:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 23.93/3.88 % Detected minimum model sizes of [3]
% 23.93/3.88 % Detected maximum model sizes of [max]
% 23.93/3.88 % TRYING [77]
% 23.93/3.88 % (2724932) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2724887-2724932"...
% 23.93/3.88 % (2724932)...printing done.
% 23.93/3.88 % (2724932)Refutation found. Thanks to Tanya!
% 23.93/3.88 % SZS status Theorem for theBenchmark
% 23.93/3.88 % SZS output start Proof for theBenchmark
% See solution above
% 23.93/3.88 % (2724932)------------------------------
% 23.93/3.88 % (2724932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.93/3.88 % (2724932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.93/3.88 % (2724932)CaDiCaL version: 2.1.3
% 23.93/3.88 % (2724932)Termination reason: Refutation
% 23.93/3.88 % (2724932)Time elapsed: 2.298 s
% 23.93/3.88 % (2724932)Peak memory usage: 40 MB
% 23.93/3.88 % (2724932)Instructions burned: 4315 (million)
% 23.93/3.88 % (2724887)Success in time 3.455 s
% 23.93/3.88 % Vampire exiting
%------------------------------------------------------------------------------