%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM483+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:30 PM UTC 2026
% Result : Theorem 4.36s 1.81s
% Output : Refutation 4.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 20
% Syntax : Number of formulae : 164 ( 18 unt; 8 def)
% Number of atoms : 808 ( 193 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 1041 ( 397 ~; 520 |; 94 &)
% ( 11 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 125 ( 0 sgn 99 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSortsB_02) ).
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(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(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(f38,axiom,
aNaturalNumber0(xk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1716) ).
fof(f39,axiom,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( iLess0(X0,xk)
=> ? [X1] :
( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0)
& X1 != sz00
& X1 != sz10
& ! [X2] :
( ( aNaturalNumber0(X2)
& ( ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
| doDivides0(X2,X1) ) )
=> ( X2 = sz10
| X2 = X1 ) )
& isPrime0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1700) ).
fof(f40,axiom,
( xk != sz00
& xk != sz10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1716_04) ).
fof(f42,conjecture,
? [X0] :
( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xk = sdtasdt0(X0,X1) )
| doDivides0(X0,xk) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0) )
=> ( X1 = sz10
| X1 = X0 ) ) )
| isPrime0(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f43,negated_conjecture,
~ ? [X0] :
( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xk = sdtasdt0(X0,X1) )
| doDivides0(X0,xk) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X1] :
( ( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0) )
=> ( X1 = sz10
| X1 = X0 ) ) )
| isPrime0(X0) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f44,plain,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( iLess0(X0,xk)
=> ? [X1] :
( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0)
& X1 != sz00
& X1 != sz10
& ! [X3] :
( ( aNaturalNumber0(X3)
& ( ? [X4] :
( aNaturalNumber0(X4)
& sdtasdt0(X3,X4) = X1 )
| doDivides0(X3,X1) ) )
=> ( sz10 = X3
| X1 = X3 ) )
& isPrime0(X1) ) ) ),
inference(rectify,[],[f39]) ).
fof(f45,plain,
~ ? [X0] :
( aNaturalNumber0(X0)
& ( ? [X1] :
( aNaturalNumber0(X1)
& xk = sdtasdt0(X0,X1) )
| doDivides0(X0,xk) )
& ( ( X0 != sz00
& X0 != sz10
& ! [X2] :
( ( aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X2,X3) = X0 )
& doDivides0(X2,X0) )
=> ( sz10 = X2
| X0 = X2 ) ) )
| isPrime0(X0) ) ),
inference(rectify,[],[f43]) ).
fof(f49,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f50,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f49]) ).
fof(f60,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f11]) ).
fof(f61,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aNaturalNumber0(X0) ),
inference(ennf_transformation,[],[f12]) ).
fof(f93,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f29]) ).
fof(f94,plain,
! [X0,X1] :
( iLess0(X0,X1)
| X0 = X1
| ~ sdtlseqdt0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f30]) ).
fof(f96,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aNaturalNumber0(X2)
& X1 = sdtasdt0(X0,X2) ) )
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f95]) ).
fof(f99,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(ennf_transformation,[],[f32]) ).
fof(f100,plain,
! [X0,X1,X2] :
( doDivides0(X0,X2)
| ~ doDivides0(X0,X1)
| ~ doDivides0(X1,X2)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2) ),
inference(flattening,[],[f99]) ).
fof(f105,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f106,plain,
! [X0,X1] :
( sdtlseqdt0(X0,X1)
| ~ doDivides0(X0,X1)
| sz00 = X1
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f105]) ).
fof(f111,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0)
& X1 != sz00
& X1 != sz10
& ! [X3] :
( sz10 = X3
| X1 = X3
| ~ aNaturalNumber0(X3)
| ( ! [X4] :
( ~ aNaturalNumber0(X4)
| sdtasdt0(X3,X4) != X1 )
& ~ doDivides0(X3,X1) ) )
& isPrime0(X1) )
| ~ iLess0(X0,xk)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(ennf_transformation,[],[f44]) ).
fof(f112,plain,
! [X0] :
( ? [X1] :
( aNaturalNumber0(X1)
& ? [X2] :
( aNaturalNumber0(X2)
& X0 = sdtasdt0(X1,X2) )
& doDivides0(X1,X0)
& X1 != sz00
& X1 != sz10
& ! [X3] :
( sz10 = X3
| X1 = X3
| ~ aNaturalNumber0(X3)
| ( ! [X4] :
( ~ aNaturalNumber0(X4)
| sdtasdt0(X3,X4) != X1 )
& ~ doDivides0(X3,X1) ) )
& isPrime0(X1) )
| ~ iLess0(X0,xk)
| ~ aNaturalNumber0(X0)
| sz00 = X0
| sz10 = X0 ),
inference(flattening,[],[f111]) ).
fof(f115,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xk )
& ~ doDivides0(X0,xk) )
| ( ( sz00 = X0
| sz10 = X0
| ? [X2] :
( sz10 != X2
& X0 != X2
& aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X2,X3) = X0 )
& doDivides0(X2,X0) ) )
& ~ isPrime0(X0) ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f116,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| ( ! [X1] :
( ~ aNaturalNumber0(X1)
| sdtasdt0(X0,X1) != xk )
& ~ doDivides0(X0,xk) )
| ( ( sz00 = X0
| sz10 = X0
| ? [X2] :
( sz10 != X2
& X0 != X2
& aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& sdtasdt0(X2,X3) = X0 )
& doDivides0(X2,X0) ) )
& ~ isPrime0(X0) ) ),
inference(flattening,[],[f115]) ).
fof(f119,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f121,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f50]) ).
fof(f129,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f60]) ).
fof(f130,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f61]) ).
fof(f162,plain,
! [X0,X1] :
( iLess0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f94]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
fof(f169,plain,
! [X2,X0,X1] :
( doDivides0(X0,X2)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ doDivides0(X1,X2)
| ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X2) ),
inference(cnf_transformation,[],[f100]) ).
fof(f172,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| ~ aNaturalNumber0(X0)
| sz00 = X1
| ~ aNaturalNumber0(X1)
| sdtlseqdt0(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
fof(f181,plain,
aNaturalNumber0(xk),
inference(cnf_transformation,[],[f38]) ).
fof(f186,plain,
! [X0] :
( isPrime0(sK3(X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ iLess0(X0,xk)
| sz10 = X0 ),
inference(cnf_transformation,[],[f112]) ).
fof(f189,plain,
! [X0] :
( doDivides0(sK3(X0),X0)
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ iLess0(X0,xk)
| sz10 = X0 ),
inference(cnf_transformation,[],[f112]) ).
fof(f190,plain,
! [X0] :
( aNaturalNumber0(sK3(X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ iLess0(X0,xk)
| sz10 = X0 ),
inference(cnf_transformation,[],[f112]) ).
fof(f191,plain,
sz10 != xk,
inference(cnf_transformation,[],[f40]) ).
fof(f192,plain,
sz00 != xk,
inference(cnf_transformation,[],[f40]) ).
fof(f200,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) != xk
| sz10 = X0
| sz00 = X0
| sdtasdt0(sK7(X0),sK8(X0)) = X0
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f203,plain,
! [X0] :
( aNaturalNumber0(sK8(X0))
| sz10 = X0
| sz00 = X0
| ~ doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f204,plain,
! [X0] :
( doDivides0(sK7(X0),X0)
| sz10 = X0
| sz00 = X0
| ~ doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f205,plain,
! [X0] :
( aNaturalNumber0(sK7(X0))
| sz10 = X0
| sz00 = X0
| ~ doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f207,plain,
! [X0] :
( sz10 != sK7(X0)
| sz10 = X0
| sz00 = X0
| ~ doDivides0(X0,xk)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f208,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) != xk
| sz10 = X0
| sz00 = X0
| doDivides0(sK7(X0),X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f210,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) != xk
| sz10 = X0
| sz00 = X0
| sK7(X0) != X0
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f213,plain,
! [X0] :
( ~ doDivides0(X0,xk)
| ~ isPrime0(X0)
| ~ aNaturalNumber0(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f219,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f165]) ).
fof(f235,definition,
( spl9_2
<=> aNaturalNumber0(xk) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f236,plain,
( aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f239,definition,
( spl9_3
<=> doDivides0(xk,xk) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f240,plain,
( doDivides0(xk,xk)
| ~ spl9_3 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( ~ doDivides0(xk,xk)
| spl9_3 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl9_4
<=> sz00 = xk ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f244,plain,
( sz00 != xk
| spl9_4 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl9_5
<=> sz10 = xk ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
fof(f248,plain,
( sz10 != xk
| spl9_5 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f254,plain,
spl9_2,
inference(avatar_split_clause,[],[f181,f235]) ).
fof(f255,plain,
~ spl9_5,
inference(avatar_split_clause,[],[f191,f247]) ).
fof(f256,plain,
~ spl9_4,
inference(avatar_split_clause,[],[f192,f243]) ).
fof(f306,definition,
( spl9_11
<=> sz00 = sK7(xk) ),
introduced(definition,[new_symbols(definition,[spl9_11])],[avatar_definition]) ).
fof(f307,plain,
( sz00 != sK7(xk)
| spl9_11 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f308,plain,
( sz00 = sK7(xk)
| ~ spl9_11 ),
inference(avatar_component_clause,[],[f306]) ).
fof(f343,plain,
( xk = sdtasdt0(xk,sz10)
| ~ spl9_2 ),
inference(resolution,[],[f129,f236]) ).
fof(f360,plain,
! [X0] :
( ~ doDivides0(X0,xk)
| sz10 = X0
| sz00 = X0
| sz00 = sdtasdt0(sz00,sK8(X0))
| ~ aNaturalNumber0(X0) ),
inference(resolution,[],[f130,f203]) ).
fof(f399,plain,
( xk != xk
| sz10 = xk
| sz00 = xk
| xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(superposition,[],[f200,f343]) ).
fof(f400,plain,
( xk != xk
| sz10 = xk
| sz00 = xk
| xk != sK7(xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(superposition,[],[f210,f343]) ).
fof(f401,plain,
( xk != xk
| sz10 = xk
| sz00 = xk
| doDivides0(sK7(xk),xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(superposition,[],[f208,f343]) ).
fof(f404,plain,
( sz10 = xk
| sz00 = xk
| doDivides0(sK7(xk),xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(trivial_inequality_removal,[],[f401]) ).
fof(f405,plain,
( sz10 = xk
| sz00 = xk
| xk != sK7(xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(trivial_inequality_removal,[],[f400]) ).
fof(f406,plain,
( sz10 = xk
| sz00 = xk
| xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(trivial_inequality_removal,[],[f399]) ).
fof(f407,plain,
( sz00 = xk
| doDivides0(sK7(xk),xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f404,f248]) ).
fof(f408,plain,
( sz00 = xk
| xk != sK7(xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f405,f248]) ).
fof(f409,plain,
( sz00 = xk
| xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f406,f248]) ).
fof(f410,plain,
( doDivides0(sK7(xk),xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f407,f244]) ).
fof(f411,plain,
( xk != sK7(xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f408,f244]) ).
fof(f412,plain,
( xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f409,f244]) ).
fof(f413,plain,
( doDivides0(sK7(xk),xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f410,f119]) ).
fof(f414,plain,
( xk != sK7(xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f411,f119]) ).
fof(f415,plain,
( xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f412,f119]) ).
fof(f416,plain,
( doDivides0(sK7(xk),xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f413,f236]) ).
fof(f417,plain,
( xk != sK7(xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f414,f236]) ).
fof(f418,plain,
( xk = sdtasdt0(sK7(xk),sK8(xk))
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f415,f236]) ).
fof(f596,plain,
( ~ aNaturalNumber0(sK7(xk))
| sz00 = xk
| ~ aNaturalNumber0(xk)
| sdtlseqdt0(sK7(xk),xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(resolution,[],[f172,f416]) ).
fof(f600,plain,
( ~ aNaturalNumber0(sK7(xk))
| ~ aNaturalNumber0(xk)
| sdtlseqdt0(sK7(xk),xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f596,f244]) ).
fof(f603,plain,
( ~ aNaturalNumber0(sK7(xk))
| sdtlseqdt0(sK7(xk),xk)
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f600,f236]) ).
fof(f630,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f219,f121]) ).
fof(f634,plain,
( doDivides0(xk,xk)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2 ),
inference(superposition,[],[f630,f343]) ).
fof(f641,plain,
( ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f634,f241]) ).
fof(f646,plain,
( ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f641,f119]) ).
fof(f649,plain,
( $false
| ~ spl9_2
| spl9_3 ),
inference(forward_subsumption_resolution,[],[f646,f236]) ).
fof(f650,plain,
( ~ spl9_2
| spl9_3 ),
inference(avatar_contradiction_clause,[],[f649]) ).
fof(f876,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,xk)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(xk)
| ~ isPrime0(X1)
| ~ aNaturalNumber0(X1) ),
inference(resolution,[],[f169,f213]) ).
fof(f881,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,xk)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(xk)
| ~ isPrime0(X1) ),
inference(duplicate_literal_removal,[],[f876]) ).
fof(f884,plain,
( ! [X0,X1] :
( ~ doDivides0(X0,xk)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X1) )
| ~ spl9_2 ),
inference(forward_subsumption_resolution,[],[f881,f236]) ).
fof(f2125,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK7(xk))
| ~ isPrime0(X0)
| sz10 = xk
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk) )
| ~ spl9_2 ),
inference(resolution,[],[f884,f204]) ).
fof(f2150,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz10 = xk
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk) )
| ~ spl9_2 ),
inference(forward_subsumption_resolution,[],[f2125,f205]) ).
fof(f2159,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk) )
| ~ spl9_2
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2150,f248]) ).
fof(f2162,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk) )
| ~ spl9_2
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2159,f244]) ).
fof(f2164,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| ~ aNaturalNumber0(xk) )
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2162,f240]) ).
fof(f2165,plain,
( ! [X0] :
( ~ doDivides0(X0,sK7(xk))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0) )
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2164,f236]) ).
fof(f2230,plain,
( sz10 = xk
| sz00 = xk
| sz00 = sdtasdt0(sz00,sK8(xk))
| ~ aNaturalNumber0(xk)
| ~ spl9_3 ),
inference(resolution,[],[f360,f240]) ).
fof(f2240,plain,
( sz00 = xk
| sz00 = sdtasdt0(sz00,sK8(xk))
| ~ aNaturalNumber0(xk)
| ~ spl9_3
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2230,f248]) ).
fof(f2244,plain,
( sz00 = sdtasdt0(sz00,sK8(xk))
| ~ aNaturalNumber0(xk)
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2240,f244]) ).
fof(f2247,plain,
( sz00 = sdtasdt0(sz00,sK8(xk))
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f2244,f236]) ).
fof(f3748,definition,
( spl9_20
<=> aNaturalNumber0(sK7(xk)) ),
introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition]) ).
fof(f3749,plain,
( aNaturalNumber0(sK7(xk))
| ~ spl9_20 ),
inference(avatar_component_clause,[],[f3748]) ).
fof(f3750,plain,
( ~ aNaturalNumber0(sK7(xk))
| spl9_20 ),
inference(avatar_component_clause,[],[f3748]) ).
fof(f3781,plain,
( sz10 = xk
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| spl9_20 ),
inference(resolution,[],[f3750,f205]) ).
fof(f3782,plain,
( sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| spl9_5
| spl9_20 ),
inference(forward_subsumption_resolution,[],[f3781,f248]) ).
fof(f3784,plain,
( ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| spl9_4
| spl9_5
| spl9_20 ),
inference(forward_subsumption_resolution,[],[f3782,f244]) ).
fof(f3786,plain,
( ~ aNaturalNumber0(xk)
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_20 ),
inference(forward_subsumption_resolution,[],[f3784,f240]) ).
fof(f3788,plain,
( $false
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_20 ),
inference(forward_subsumption_resolution,[],[f3786,f236]) ).
fof(f3789,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_20 ),
inference(avatar_contradiction_clause,[],[f3788]) ).
fof(f3829,plain,
( xk = sdtasdt0(sz00,sK8(xk))
| ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_11 ),
inference(superposition,[],[f418,f308]) ).
fof(f3844,plain,
( sz00 = xk
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_11 ),
inference(forward_demodulation,[],[f3829,f2247]) ).
fof(f3845,plain,
( $false
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_11 ),
inference(forward_subsumption_resolution,[],[f3844,f244]) ).
fof(f3846,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_11 ),
inference(avatar_contradiction_clause,[],[f3845]) ).
fof(f5447,plain,
( sdtlseqdt0(sK7(xk),xk)
| ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f603,f3749]) ).
fof(f6677,plain,
( ~ aNaturalNumber0(sK3(sK7(xk)))
| ~ isPrime0(sK3(sK7(xk)))
| sz00 = sK7(xk)
| ~ aNaturalNumber0(sK7(xk))
| ~ iLess0(sK7(xk),xk)
| sz10 = sK7(xk)
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(resolution,[],[f2165,f189]) ).
fof(f6683,plain,
( ~ isPrime0(sK3(sK7(xk)))
| sz00 = sK7(xk)
| ~ aNaturalNumber0(sK7(xk))
| ~ iLess0(sK7(xk),xk)
| sz10 = sK7(xk)
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f6677,f190]) ).
fof(f6686,plain,
( sz00 = sK7(xk)
| ~ aNaturalNumber0(sK7(xk))
| ~ iLess0(sK7(xk),xk)
| sz10 = sK7(xk)
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5 ),
inference(forward_subsumption_resolution,[],[f6683,f186]) ).
fof(f6688,plain,
( ~ aNaturalNumber0(sK7(xk))
| ~ iLess0(sK7(xk),xk)
| sz10 = sK7(xk)
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_11 ),
inference(forward_subsumption_resolution,[],[f6686,f307]) ).
fof(f6690,plain,
( ~ iLess0(sK7(xk),xk)
| sz10 = sK7(xk)
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_11
| ~ spl9_20 ),
inference(forward_subsumption_resolution,[],[f6688,f3749]) ).
fof(f7088,definition,
( spl9_27
<=> sz10 = sK7(xk) ),
introduced(definition,[new_symbols(definition,[spl9_27])],[avatar_definition]) ).
fof(f7090,plain,
( sz10 = sK7(xk)
| ~ spl9_27 ),
inference(avatar_component_clause,[],[f7088]) ).
fof(f7189,definition,
( spl9_29
<=> iLess0(sK7(xk),xk) ),
introduced(definition,[new_symbols(definition,[spl9_29])],[avatar_definition]) ).
fof(f7191,plain,
( ~ iLess0(sK7(xk),xk)
| spl9_29 ),
inference(avatar_component_clause,[],[f7189]) ).
fof(f7192,plain,
( spl9_27
| ~ spl9_29
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_11
| ~ spl9_20 ),
inference(avatar_split_clause,[],[f6690,f3748,f306,f247,f243,f239,f235,f7189,f7088]) ).
fof(f7238,plain,
( ~ aNaturalNumber0(sK7(xk))
| ~ sdtlseqdt0(sK7(xk),xk)
| xk = sK7(xk)
| ~ aNaturalNumber0(xk)
| spl9_29 ),
inference(resolution,[],[f7191,f162]) ).
fof(f7239,plain,
( ~ sdtlseqdt0(sK7(xk),xk)
| xk = sK7(xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_20
| spl9_29 ),
inference(forward_subsumption_resolution,[],[f7238,f3749]) ).
fof(f7240,plain,
( xk = sK7(xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20
| spl9_29 ),
inference(forward_subsumption_resolution,[],[f7239,f5447]) ).
fof(f7241,plain,
( ~ aNaturalNumber0(xk)
| ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20
| spl9_29 ),
inference(forward_subsumption_resolution,[],[f7240,f417]) ).
fof(f7242,plain,
( $false
| ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20
| spl9_29 ),
inference(forward_subsumption_resolution,[],[f7241,f236]) ).
fof(f7243,plain,
( ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20
| spl9_29 ),
inference(avatar_contradiction_clause,[],[f7242]) ).
fof(f7314,plain,
( sz10 != sz10
| sz10 = xk
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_27 ),
inference(superposition,[],[f207,f7090]) ).
fof(f7320,plain,
( sz10 = xk
| sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| ~ spl9_27 ),
inference(trivial_inequality_removal,[],[f7314]) ).
fof(f7322,plain,
( sz00 = xk
| ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| spl9_5
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f7320,f248]) ).
fof(f7324,plain,
( ~ doDivides0(xk,xk)
| ~ aNaturalNumber0(xk)
| spl9_4
| spl9_5
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f7322,f244]) ).
fof(f7326,plain,
( ~ aNaturalNumber0(xk)
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f7324,f240]) ).
fof(f7327,plain,
( $false
| ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_27 ),
inference(forward_subsumption_resolution,[],[f7326,f236]) ).
fof(f7328,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_27 ),
inference(avatar_contradiction_clause,[],[f7327]) ).
cnf(s2,plain,
spl9_2,
inference(sat_conversion,[],[f254]) ).
cnf(s3,plain,
~ spl9_5,
inference(sat_conversion,[],[f255]) ).
cnf(s4,plain,
~ spl9_4,
inference(sat_conversion,[],[f256]) ).
cnf(s11,plain,
( ~ spl9_2
| spl9_3 ),
inference(sat_conversion,[],[f650]) ).
cnf(s19,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_20 ),
inference(sat_conversion,[],[f3789]) ).
cnf(s21,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_11 ),
inference(sat_conversion,[],[f3846]) ).
cnf(s27,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| spl9_11
| ~ spl9_20
| spl9_27
| ~ spl9_29 ),
inference(sat_conversion,[],[f7192]) ).
cnf(s28,plain,
( ~ spl9_2
| spl9_4
| spl9_5
| ~ spl9_20
| spl9_29 ),
inference(sat_conversion,[],[f7243]) ).
cnf(s29,plain,
( ~ spl9_2
| ~ spl9_3
| spl9_4
| spl9_5
| ~ spl9_27 ),
inference(sat_conversion,[],[f7328]) ).
cnf(s32,plain,
spl9_3,
inference(rat,[],[s11,s2]) ).
cnf(s35,plain,
~ spl9_27,
inference(rat,[],[s29,s2,s3,s4,s32]) ).
cnf(s37,plain,
~ spl9_11,
inference(rat,[],[s21,s2,s3,s4,s32]) ).
cnf(s38,plain,
spl9_20,
inference(rat,[],[s19,s2,s3,s4,s32]) ).
cnf(s42,plain,
spl9_29,
inference(rat,[],[s28,s2,s3,s4,s38]) ).
cnf(s44,plain,
$false,
inference(rat,[],[s27,s37,s35,s32,s2,s3,s4,s42,s38]) ).
fof(f7329,plain,
$false,
inference(avatar_sat_refutation,[],[s44]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM483+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n007.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 20:05:11 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/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
% 4.36/1.81 % (1748311)Will run a generic schedule for satisfiability detection.
% 4.36/1.81 % (1748319)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3453017943_2999 on theBenchmark for (2999ds/0Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [3]
% 4.36/1.81 % (1748320)% WARNING: option uhcvi not known.
% 4.36/1.81 % TRYING [4]
% 4.36/1.81 % (1748322)dis+10_1_sil=32000:sp=arity:random_seed=1548684795:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.36/1.81 % (1748321)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=29571176:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.36/1.81 % (1748324)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3657715665:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.36/1.81 % (1748325)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3942454685:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.36/1.81 % (1748323)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=536832807:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.36/1.81 % (1748320)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3915018447:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.36/1.81 % TRYING [5]
% 4.36/1.81 % TRYING [6]
% 4.36/1.81 % (1748322)Instruction limit reached!
% 4.36/1.81 % (1748322)------------------------------
% 4.36/1.81 % (1748322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748322)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748322)Termination reason: Instruction limit
% 4.36/1.81 % (1748322)Termination phase: Saturation
% 4.36/1.81 % (1748322)Time elapsed: 0.062 s
% 4.36/1.81 % (1748322)Peak memory usage: 12 MB
% 4.36/1.81 % (1748322)Instructions burned: 104 (million)
% 4.36/1.81 % (1748323)Instruction limit reached!
% 4.36/1.81 % (1748323)------------------------------
% 4.36/1.81 % (1748323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748323)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748323)Termination reason: Instruction limit
% 4.36/1.81 % (1748323)Termination phase: Saturation
% 4.36/1.81 % (1748323)Time elapsed: 0.066 s
% 4.36/1.81 % (1748323)Peak memory usage: 13 MB
% 4.36/1.81 % (1748323)Instructions burned: 116 (million)
% 4.36/1.81 % (1748324)Instruction limit reached!
% 4.36/1.81 % (1748324)------------------------------
% 4.36/1.81 % (1748324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748324)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748324)Termination reason: Instruction limit
% 4.36/1.81 % (1748324)Termination phase: Saturation
% 4.36/1.81 % (1748324)Time elapsed: 0.077 s
% 4.36/1.81 % (1748324)Peak memory usage: 13 MB
% 4.36/1.81 % (1748324)Instructions burned: 132 (million)
% 4.36/1.81 % (1748333)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=80279283:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.36/1.81 % (1748334)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=635307112:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [3]
% 4.36/1.81 % TRYING [4]
% 4.36/1.81 % (1748335)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=85319657:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.36/1.81 % (1748325)Instruction limit reached!
% 4.36/1.81 % (1748325)------------------------------
% 4.36/1.81 % (1748325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748325)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748325)Termination reason: Instruction limit
% 4.36/1.81 % (1748325)Termination phase: Saturation
% 4.36/1.81 % (1748325)Time elapsed: 0.099 s
% 4.36/1.81 % (1748325)Peak memory usage: 13 MB
% 4.36/1.81 % (1748325)Instructions burned: 160 (million)
% 4.36/1.81 % TRYING [5]
% 4.36/1.81 % (1748339)ott-21_1_sil=16000:fs=off:random_seed=3035438720:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.36/1.81 % TRYING [7]
% 4.36/1.81 % (1748334)Instruction limit reached!
% 4.36/1.81 % (1748334)------------------------------
% 4.36/1.81 % (1748334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748334)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748334)Termination reason: Instruction limit
% 4.36/1.81 % (1748334)Termination phase: Saturation
% 4.36/1.81 % (1748334)Time elapsed: 0.070 s
% 4.36/1.81 % (1748334)Peak memory usage: 12 MB
% 4.36/1.81 % (1748334)Instructions burned: 131 (million)
% 4.36/1.81 % (1748341)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3528800987:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.36/1.81 % TRYING [6]
% 4.36/1.81 % (1748339)Instruction limit reached!
% 4.36/1.81 % (1748339)------------------------------
% 4.36/1.81 % (1748339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748339)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748339)Termination reason: Instruction limit
% 4.36/1.81 % (1748339)Termination phase: Saturation
% 4.36/1.81 % (1748339)Time elapsed: 0.094 s
% 4.36/1.81 % (1748339)Peak memory usage: 13 MB
% 4.36/1.81 % (1748339)Instructions burned: 181 (million)
% 4.36/1.81 % (1748343)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1959325993:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [3]
% 4.36/1.81 % TRYING [4]
% 4.36/1.81 % TRYING [5]
% 4.36/1.81 % (1748333)Instruction limit reached!
% 4.36/1.81 % (1748333)------------------------------
% 4.36/1.81 % (1748333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748333)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748333)Termination reason: Instruction limit
% 4.36/1.81 % (1748333)Termination phase: Finite model building constraint generation
% 4.36/1.81 % (1748333)Time elapsed: 0.249 s
% 4.36/1.81 % (1748333)Peak memory usage: 32 MB
% 4.36/1.81 % (1748333)Instructions burned: 717 (million)
% 4.36/1.81 % TRYING [8]
% 4.36/1.81 % (1748345)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1557151967:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 4.36/1.81 % (1748335)Instruction limit reached!
% 4.36/1.81 % (1748335)------------------------------
% 4.36/1.81 % (1748335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748335)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748335)Termination reason: Instruction limit
% 4.36/1.81 % (1748335)Termination phase: Saturation
% 4.36/1.81 % (1748335)Time elapsed: 0.362 s
% 4.36/1.81 % (1748335)Peak memory usage: 16 MB
% 4.36/1.81 % (1748335)Instructions burned: 685 (million)
% 4.36/1.81 % (1748347)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=496021784:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 4.36/1.81 % (1748341)Instruction limit reached!
% 4.36/1.81 % (1748341)------------------------------
% 4.36/1.81 % (1748341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748341)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748341)Termination reason: Instruction limit
% 4.36/1.81 % (1748341)Termination phase: Saturation
% 4.36/1.81 % (1748341)Time elapsed: 0.327 s
% 4.36/1.81 % (1748341)Peak memory usage: 15 MB
% 4.36/1.81 % (1748341)Instructions burned: 478 (million)
% 4.36/1.81 % (1748349)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=1383081462: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)
% 4.36/1.81 % TRYING [6]
% 4.36/1.81 % (1748343)Instruction limit reached!
% 4.36/1.81 % (1748343)------------------------------
% 4.36/1.81 % (1748343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748343)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748343)Termination reason: Instruction limit
% 4.36/1.81 % (1748343)Termination phase: Finite model building constraint generation
% 4.36/1.81 % (1748343)Time elapsed: 0.346 s
% 4.36/1.81 % (1748343)Peak memory usage: 23 MB
% 4.36/1.81 % (1748343)Instructions burned: 865 (million)
% 4.36/1.81 % (1748351)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=885807290:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 4.36/1.81 % TRYING [14]
% 4.36/1.81 % TRYING [9]
% 4.36/1.81 % (1748347)Instruction limit reached!
% 4.36/1.81 % (1748347)------------------------------
% 4.36/1.81 % (1748347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748347)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748347)Termination reason: Instruction limit
% 4.36/1.81 % (1748347)Termination phase: Finite model building constraint generation
% 4.36/1.81 % (1748347)Time elapsed: 0.341 s
% 4.36/1.81 % (1748347)Peak memory usage: 79 MB
% 4.36/1.81 % (1748347)Instructions burned: 889 (million)
% 4.36/1.81 % (1748353)fmb+10_1_sil=64000:random_seed=548062887:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [3]
% 4.36/1.81 % TRYING [4]
% 4.36/1.81 % (1748349)Instruction limit reached!
% 4.36/1.81 % (1748349)------------------------------
% 4.36/1.81 % (1748349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748349)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748349)Termination reason: Instruction limit
% 4.36/1.81 % (1748349)Termination phase: Saturation
% 4.36/1.81 % (1748349)Time elapsed: 0.358 s
% 4.36/1.81 % (1748349)Peak memory usage: 19 MB
% 4.36/1.81 % (1748349)Instructions burned: 693 (million)
% 4.36/1.81 % (1748355)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1720905059:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [20]
% 4.36/1.81 % TRYING [5]
% 4.36/1.81 % (1748345)Instruction limit reached!
% 4.36/1.81 % (1748345)------------------------------
% 4.36/1.81 % (1748345)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748345)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748345)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748345)Termination reason: Instruction limit
% 4.36/1.81 % (1748345)Termination phase: Saturation
% 4.36/1.81 % (1748345)Time elapsed: 0.658 s
% 4.36/1.81 % (1748345)Peak memory usage: 24 MB
% 4.36/1.81 % (1748345)Instructions burned: 1180 (million)
% 4.36/1.81 % (1748357)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3363118788:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 4.36/1.81 % Detected minimum model sizes of [3]
% 4.36/1.81 % Detected maximum model sizes of [max]
% 4.36/1.81 % TRYING [8]
% 4.36/1.81 % (1748351)Instruction limit reached!
% 4.36/1.81 % (1748351)------------------------------
% 4.36/1.81 % (1748351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748351)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748351)Termination reason: Instruction limit
% 4.36/1.81 % (1748351)Termination phase: Saturation
% 4.36/1.81 % (1748351)Time elapsed: 0.488 s
% 4.36/1.81 % (1748351)Peak memory usage: 19 MB
% 4.36/1.81 % (1748351)Instructions burned: 880 (million)
% 4.36/1.81 % (1748359)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2617227294:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 4.36/1.81 % TRYING [6]
% 4.36/1.81 % (1748359) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1748311-1748359"...
% 4.36/1.81 % (1748359)...printing done.
% 4.36/1.81 % (1748359)Refutation found. Thanks to Tanya!
% 4.36/1.81 % SZS status Theorem for theBenchmark
% 4.36/1.81 % SZS output start Proof for theBenchmark
% See solution above
% 4.36/1.81 % (1748359)------------------------------
% 4.36/1.81 % (1748359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.36/1.81 % (1748359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.81 % (1748359)CaDiCaL version: 2.1.3
% 4.36/1.81 % (1748359)Termination reason: Refutation
% 4.36/1.81 % (1748359)Time elapsed: 0.237 s
% 4.36/1.81 % (1748359)Peak memory usage: 15 MB
% 4.36/1.81 % (1748359)Instructions burned: 459 (million)
% 4.36/1.81 % (1748311)Success in time 1.389 s
% 4.36/1.81 % Vampire exiting
%------------------------------------------------------------------------------