%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM481+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 7.97s 1.73s
% Output : Refutation 7.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 17
% Syntax : Number of formulae : 159 ( 19 unt; 8 def)
% Number of atoms : 683 ( 204 equ)
% Maximal formula atoms : 33 ( 4 avg)
% Number of connectives : 881 ( 357 ~; 368 |; 117 &)
% ( 11 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 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 : 139 ( 0 sgn 108 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
( aNaturalNumber0(sz10)
& sz10 != sz00 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsC_01) ).
fof(f5,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> aNaturalNumber0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f11,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulUnit) ).
fof(f12,axiom,
! [X0] :
( aNaturalNumber0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_MulZero) ).
fof(f27,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( X0 != sz00
=> sdtlseqdt0(X1,sdtasdt0(X1,X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonMul2) ).
fof(f29,axiom,
! [X0,X1] :
( ( aNaturalNumber0(X0)
& aNaturalNumber0(X1) )
=> ( ( X0 != X1
& sdtlseqdt0(X0,X1) )
=> iLess0(X0,X1) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',mDivTrans) ).
fof(f38,conjecture,
! [X0] :
( ( aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 )
=> ( ! [X1] :
( ( aNaturalNumber0(X1)
& X1 != sz00
& X1 != sz10 )
=> ( iLess0(X1,X0)
=> ? [X2] :
( aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1)
& X2 != sz00
& X2 != sz10
& ! [X3] :
( ( aNaturalNumber0(X3)
& ( ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
| doDivides0(X3,X2) ) )
=> ( X3 = sz10
| X3 = X2 ) )
& isPrime0(X2) ) ) )
=> ? [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/sandbox/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)
& ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1)
& X2 != sz00
& X2 != sz10
& ! [X3] :
( ( aNaturalNumber0(X3)
& ( ? [X4] :
( aNaturalNumber0(X4)
& X2 = sdtasdt0(X3,X4) )
| doDivides0(X3,X2) ) )
=> ( X3 = sz10
| X3 = X2 ) )
& isPrime0(X2) ) ) )
=> ? [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) ) ) ) ),
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)
& ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1)
& X2 != sz00
& X2 != sz10
& ! [X4] :
( ( aNaturalNumber0(X4)
& ( ? [X5] :
( aNaturalNumber0(X5)
& sdtasdt0(X4,X5) = X2 )
| doDivides0(X4,X2) ) )
=> ( sz10 = X4
| X2 = X4 ) )
& isPrime0(X2) ) ) )
=> ? [X6] :
( aNaturalNumber0(X6)
& ( ? [X7] :
( aNaturalNumber0(X7)
& sdtasdt0(X6,X7) = X0 )
| doDivides0(X6,X0) )
& ( ( sz00 != X6
& sz10 != X6
& ! [X8] :
( ( aNaturalNumber0(X8)
& ? [X9] :
( aNaturalNumber0(X9)
& sdtasdt0(X8,X9) = X6 )
& doDivides0(X8,X6) )
=> ( sz10 = X8
| X6 = X8 ) ) )
| isPrime0(X6) ) ) ) ),
inference(rectify,[],[f39]) ).
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(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(f84,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(ennf_transformation,[],[f27]) ).
fof(f85,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| sz00 = X0
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(flattening,[],[f84]) ).
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(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(f106,plain,
? [X0] :
( ! [X6] :
( ~ aNaturalNumber0(X6)
| ( ! [X7] :
( ~ aNaturalNumber0(X7)
| sdtasdt0(X6,X7) != X0 )
& ~ doDivides0(X6,X0) )
| ( ( sz00 = X6
| sz10 = X6
| ? [X8] :
( sz10 != X8
& X6 != X8
& aNaturalNumber0(X8)
& ? [X9] :
( aNaturalNumber0(X9)
& sdtasdt0(X8,X9) = X6 )
& doDivides0(X8,X6) ) )
& ~ isPrime0(X6) ) )
& ! [X1] :
( ? [X2] :
( aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1)
& X2 != sz00
& X2 != sz10
& ! [X4] :
( sz10 = X4
| X2 = X4
| ~ aNaturalNumber0(X4)
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| sdtasdt0(X4,X5) != X2 )
& ~ doDivides0(X4,X2) ) )
& 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] :
( ! [X6] :
( ~ aNaturalNumber0(X6)
| ( ! [X7] :
( ~ aNaturalNumber0(X7)
| sdtasdt0(X6,X7) != X0 )
& ~ doDivides0(X6,X0) )
| ( ( sz00 = X6
| sz10 = X6
| ? [X8] :
( sz10 != X8
& X6 != X8
& aNaturalNumber0(X8)
& ? [X9] :
( aNaturalNumber0(X9)
& sdtasdt0(X8,X9) = X6 )
& doDivides0(X8,X6) ) )
& ~ isPrime0(X6) ) )
& ! [X1] :
( ? [X2] :
( aNaturalNumber0(X2)
& ? [X3] :
( aNaturalNumber0(X3)
& X1 = sdtasdt0(X2,X3) )
& doDivides0(X2,X1)
& X2 != sz00
& X2 != sz10
& ! [X4] :
( sz10 = X4
| X2 = X4
| ~ aNaturalNumber0(X4)
| ( ! [X5] :
( ~ aNaturalNumber0(X5)
| sdtasdt0(X4,X5) != X2 )
& ~ doDivides0(X4,X2) ) )
& isPrime0(X2) )
| ~ iLess0(X1,X0)
| ~ aNaturalNumber0(X1)
| sz00 = X1
| sz10 = X1 )
& aNaturalNumber0(X0)
& X0 != sz00
& X0 != sz10 ),
inference(flattening,[],[f106]) ).
fof(f110,plain,
aNaturalNumber0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f112,plain,
! [X0,X1] :
( aNaturalNumber0(sdtasdt0(X0,X1))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f45]) ).
fof(f120,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f55]) ).
fof(f121,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(sz00,X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f122,plain,
! [X0] :
( ~ aNaturalNumber0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f56]) ).
fof(f152,plain,
! [X0,X1] :
( sdtlseqdt0(X1,sdtasdt0(X1,X0))
| ~ aNaturalNumber0(X0)
| sz00 = X0
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f85]) ).
fof(f153,plain,
! [X0,X1] :
( iLess0(X0,X1)
| ~ aNaturalNumber0(X0)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| ~ aNaturalNumber0(X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f156,plain,
! [X2,X0,X1] :
( ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| sdtasdt0(X0,X2) != X1
| ~ aNaturalNumber0(X2)
| doDivides0(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
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(f173,plain,
! [X6,X7] :
( sdtasdt0(X6,X7) != sK3
| sz10 = X6
| sz00 = X6
| sdtasdt0(sK6(X6),sK7(X6)) = X6
| ~ aNaturalNumber0(X7)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f176,plain,
! [X6] :
( aNaturalNumber0(sK7(X6))
| sz10 = X6
| sz00 = X6
| ~ doDivides0(X6,sK3)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f178,plain,
! [X6] :
( doDivides0(sK6(X6),X6)
| sz10 = X6
| sz00 = X6
| ~ doDivides0(X6,sK3)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f179,plain,
! [X6] :
( aNaturalNumber0(sK6(X6))
| sz10 = X6
| sz00 = X6
| ~ doDivides0(X6,sK3)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f181,plain,
! [X6] :
( sz10 != sK6(X6)
| sz10 = X6
| sz00 = X6
| ~ doDivides0(X6,sK3)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f183,plain,
! [X6,X7] :
( aNaturalNumber0(sK6(X6))
| sz10 = X6
| sz00 = X6
| sdtasdt0(X6,X7) != sK3
| ~ aNaturalNumber0(X7)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f184,plain,
! [X6,X7] :
( sdtasdt0(X6,X7) != sK3
| sz10 = X6
| sz00 = X6
| sK6(X6) != X6
| ~ aNaturalNumber0(X7)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f189,plain,
! [X1] :
( isPrime0(sK4(X1))
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f192,plain,
! [X1] :
( doDivides0(sK4(X1),X1)
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f193,plain,
! [X1] :
( aNaturalNumber0(sK4(X1))
| sz00 = X1
| ~ aNaturalNumber0(X1)
| ~ iLess0(X1,sK3)
| sz10 = X1 ),
inference(cnf_transformation,[],[f107]) ).
fof(f194,plain,
! [X6] :
( ~ doDivides0(X6,sK3)
| ~ isPrime0(X6)
| ~ aNaturalNumber0(X6) ),
inference(cnf_transformation,[],[f107]) ).
fof(f195,plain,
sz10 != sK3,
inference(cnf_transformation,[],[f107]) ).
fof(f196,plain,
sz00 != sK3,
inference(cnf_transformation,[],[f107]) ).
fof(f197,plain,
aNaturalNumber0(sK3),
inference(cnf_transformation,[],[f107]) ).
fof(f203,plain,
! [X2,X0] :
( ~ aNaturalNumber0(sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X2)
| doDivides0(X0,sdtasdt0(X0,X2)) ),
inference(equality_resolution,[],[f156]) ).
fof(f225,definition,
( spl8_2
<=> doDivides0(sK3,sK3) ),
introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition]) ).
fof(f226,plain,
( doDivides0(sK3,sK3)
| ~ spl8_2 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f227,plain,
( ~ doDivides0(sK3,sK3)
| spl8_2 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f257,definition,
( spl8_4
<=> sz00 = sK6(sK3) ),
introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition]) ).
fof(f258,plain,
( sz00 != sK6(sK3)
| spl8_4 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( sz00 = sK6(sK3)
| ~ spl8_4 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f261,definition,
( spl8_5
<=> sz10 = sK6(sK3) ),
introduced(definition,[new_symbols(definition,[spl8_5])],[avatar_definition]) ).
fof(f263,plain,
( sz10 = sK6(sK3)
| ~ spl8_5 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f306,plain,
sK3 = sdtasdt0(sK3,sz10),
inference(resolution,[],[f120,f197]) ).
fof(f325,plain,
( sK3 != sK3
| sz10 = sK3
| sz00 = sK3
| sK3 = sdtasdt0(sK6(sK3),sK7(sK3))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(superposition,[],[f173,f306]) ).
fof(f326,plain,
( sK3 != sK3
| sz10 = sK3
| sz00 = sK3
| sK3 != sK6(sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(superposition,[],[f184,f306]) ).
fof(f331,plain,
( sz10 = sK3
| sz00 = sK3
| sK3 != sK6(sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(trivial_inequality_removal,[],[f326]) ).
fof(f332,plain,
( sz10 = sK3
| sz00 = sK3
| sK3 = sdtasdt0(sK6(sK3),sK7(sK3))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(trivial_inequality_removal,[],[f325]) ).
fof(f335,plain,
( sz00 = sK3
| sK3 != sK6(sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f331,f195]) ).
fof(f336,plain,
( sz00 = sK3
| sK3 = sdtasdt0(sK6(sK3),sK7(sK3))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f332,f195]) ).
fof(f339,plain,
( sK3 != sK6(sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f335,f196]) ).
fof(f340,plain,
( sK3 = sdtasdt0(sK6(sK3),sK7(sK3))
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f336,f196]) ).
fof(f342,plain,
( sK3 != sK6(sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f339,f110]) ).
fof(f343,plain,
( sK3 = sdtasdt0(sK6(sK3),sK7(sK3))
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f340,f110]) ).
fof(f345,plain,
sK3 != sK6(sK3),
inference(forward_subsumption_resolution,[],[f342,f197]) ).
fof(f346,plain,
sK3 = sdtasdt0(sK6(sK3),sK7(sK3)),
inference(forward_subsumption_resolution,[],[f343,f197]) ).
fof(f512,plain,
( sdtlseqdt0(sK6(sK3),sK3)
| ~ aNaturalNumber0(sK7(sK3))
| sz00 = sK7(sK3)
| ~ aNaturalNumber0(sK6(sK3)) ),
inference(superposition,[],[f152,f346]) ).
fof(f529,definition,
( spl8_6
<=> aNaturalNumber0(sK6(sK3)) ),
introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition]) ).
fof(f530,plain,
( aNaturalNumber0(sK6(sK3))
| ~ spl8_6 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f531,plain,
( ~ aNaturalNumber0(sK6(sK3))
| spl8_6 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f533,definition,
( spl8_7
<=> sz00 = sK7(sK3) ),
introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition]) ).
fof(f535,plain,
( sz00 = sK7(sK3)
| ~ spl8_7 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f537,definition,
( spl8_8
<=> aNaturalNumber0(sK7(sK3)) ),
introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition]) ).
fof(f538,plain,
( aNaturalNumber0(sK7(sK3))
| ~ spl8_8 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f539,plain,
( ~ aNaturalNumber0(sK7(sK3))
| spl8_8 ),
inference(avatar_component_clause,[],[f537]) ).
fof(f541,definition,
( spl8_9
<=> sdtlseqdt0(sK6(sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl8_9])],[avatar_definition]) ).
fof(f543,plain,
( sdtlseqdt0(sK6(sK3),sK3)
| ~ spl8_9 ),
inference(avatar_component_clause,[],[f541]) ).
fof(f544,plain,
( ~ spl8_6
| spl8_7
| ~ spl8_8
| spl8_9 ),
inference(avatar_split_clause,[],[f512,f541,f537,f533,f529]) ).
fof(f553,plain,
( ! [X0] :
( sz10 = sK3
| sz00 = sK3
| sK3 != sdtasdt0(sK3,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3) )
| spl8_6 ),
inference(resolution,[],[f531,f183]) ).
fof(f555,plain,
( ! [X0] :
( sz00 = sK3
| sK3 != sdtasdt0(sK3,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3) )
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f553,f195]) ).
fof(f556,plain,
( ! [X0] :
( sK3 != sdtasdt0(sK3,X0)
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK3) )
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f555,f196]) ).
fof(f557,plain,
( ! [X0] :
( sK3 != sdtasdt0(sK3,X0)
| ~ aNaturalNumber0(X0) )
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f556,f197]) ).
fof(f565,plain,
( sK3 != sK3
| ~ aNaturalNumber0(sz10)
| spl8_6 ),
inference(superposition,[],[f557,f306]) ).
fof(f567,plain,
( ~ aNaturalNumber0(sz10)
| spl8_6 ),
inference(trivial_inequality_removal,[],[f565]) ).
fof(f568,plain,
( $false
| spl8_6 ),
inference(forward_subsumption_resolution,[],[f567,f110]) ).
fof(f569,plain,
spl8_6,
inference(avatar_contradiction_clause,[],[f568]) ).
fof(f593,plain,
( sz00 = sdtasdt0(sK6(sK3),sz00)
| ~ spl8_6 ),
inference(resolution,[],[f530,f122]) ).
fof(f598,plain,
( sz10 = sK3
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| spl8_8 ),
inference(resolution,[],[f539,f176]) ).
fof(f609,plain,
! [X2,X0] :
( doDivides0(X0,sdtasdt0(X0,X2))
| ~ aNaturalNumber0(X2)
| ~ aNaturalNumber0(X0) ),
inference(forward_subsumption_resolution,[],[f203,f112]) ).
fof(f613,plain,
( doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3) ),
inference(superposition,[],[f609,f306]) ).
fof(f618,plain,
( ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK3)
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f613,f227]) ).
fof(f623,plain,
( ~ aNaturalNumber0(sK3)
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f618,f110]) ).
fof(f626,plain,
( $false
| spl8_2 ),
inference(forward_subsumption_resolution,[],[f623,f197]) ).
fof(f627,plain,
spl8_2,
inference(avatar_contradiction_clause,[],[f626]) ).
fof(f628,plain,
( sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| spl8_8 ),
inference(forward_subsumption_resolution,[],[f598,f195]) ).
fof(f630,plain,
( ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| spl8_8 ),
inference(forward_subsumption_resolution,[],[f628,f196]) ).
fof(f632,plain,
( ~ doDivides0(sK3,sK3)
| spl8_8 ),
inference(forward_subsumption_resolution,[],[f630,f197]) ).
fof(f706,plain,
( $false
| ~ spl8_2
| spl8_8 ),
inference(forward_subsumption_resolution,[],[f632,f226]) ).
fof(f707,plain,
( ~ spl8_2
| spl8_8 ),
inference(avatar_contradiction_clause,[],[f706]) ).
fof(f737,plain,
( sz00 = sdtasdt0(sz00,sK7(sK3))
| ~ spl8_8 ),
inference(resolution,[],[f538,f121]) ).
fof(f754,plain,
( sK3 = sdtasdt0(sK6(sK3),sz00)
| ~ spl8_7 ),
inference(superposition,[],[f346,f535]) ).
fof(f778,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(sK3)
| ~ isPrime0(X1)
| ~ aNaturalNumber0(X1) ),
inference(resolution,[],[f160,f194]) ).
fof(f786,plain,
! [X0,X1] :
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(sK3)
| ~ isPrime0(X1) ),
inference(duplicate_literal_removal,[],[f778]) ).
fof(f791,plain,
! [X0,X1] :
( ~ doDivides0(X0,sK3)
| ~ doDivides0(X1,X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X1) ),
inference(forward_subsumption_resolution,[],[f786,f197]) ).
fof(f1036,plain,
( sz00 = sK3
| ~ spl8_6
| ~ spl8_7 ),
inference(forward_demodulation,[],[f754,f593]) ).
fof(f1037,plain,
( $false
| ~ spl8_6
| ~ spl8_7 ),
inference(forward_subsumption_resolution,[],[f1036,f196]) ).
fof(f1038,plain,
( ~ spl8_6
| ~ spl8_7 ),
inference(avatar_contradiction_clause,[],[f1037]) ).
fof(f1860,plain,
! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(sK6(sK3))
| ~ isPrime0(X0)
| sz10 = sK3
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3) ),
inference(resolution,[],[f791,f178]) ).
fof(f1889,plain,
! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz10 = sK3
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f1860,f179]) ).
fof(f1895,plain,
! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f1889,f195]) ).
fof(f1896,plain,
! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3) ),
inference(forward_subsumption_resolution,[],[f1895,f196]) ).
fof(f1897,plain,
( ! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0)
| ~ aNaturalNumber0(sK3) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1896,f226]) ).
fof(f1898,plain,
( ! [X0] :
( ~ doDivides0(X0,sK6(sK3))
| ~ aNaturalNumber0(X0)
| ~ isPrime0(X0) )
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f1897,f197]) ).
fof(f2251,plain,
( sK3 = sdtasdt0(sz00,sK7(sK3))
| ~ spl8_4 ),
inference(superposition,[],[f346,f259]) ).
fof(f2265,plain,
( sz00 = sK3
| ~ spl8_4
| ~ spl8_8 ),
inference(forward_demodulation,[],[f2251,f737]) ).
fof(f2267,plain,
( $false
| ~ spl8_4
| ~ spl8_8 ),
inference(forward_subsumption_resolution,[],[f2265,f196]) ).
fof(f2268,plain,
( ~ spl8_4
| ~ spl8_8 ),
inference(avatar_contradiction_clause,[],[f2267]) ).
fof(f3832,plain,
( ~ aNaturalNumber0(sK4(sK6(sK3)))
| ~ isPrime0(sK4(sK6(sK3)))
| sz00 = sK6(sK3)
| ~ aNaturalNumber0(sK6(sK3))
| ~ iLess0(sK6(sK3),sK3)
| sz10 = sK6(sK3)
| ~ spl8_2 ),
inference(resolution,[],[f1898,f192]) ).
fof(f3836,plain,
( ~ isPrime0(sK4(sK6(sK3)))
| sz00 = sK6(sK3)
| ~ aNaturalNumber0(sK6(sK3))
| ~ iLess0(sK6(sK3),sK3)
| sz10 = sK6(sK3)
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f3832,f193]) ).
fof(f3838,plain,
( sz00 = sK6(sK3)
| ~ aNaturalNumber0(sK6(sK3))
| ~ iLess0(sK6(sK3),sK3)
| sz10 = sK6(sK3)
| ~ spl8_2 ),
inference(forward_subsumption_resolution,[],[f3836,f189]) ).
fof(f3840,plain,
( ~ aNaturalNumber0(sK6(sK3))
| ~ iLess0(sK6(sK3),sK3)
| sz10 = sK6(sK3)
| ~ spl8_2
| spl8_4 ),
inference(forward_subsumption_resolution,[],[f3838,f258]) ).
fof(f3842,plain,
( ~ iLess0(sK6(sK3),sK3)
| sz10 = sK6(sK3)
| ~ spl8_2
| spl8_4
| ~ spl8_6 ),
inference(forward_subsumption_resolution,[],[f3840,f530]) ).
fof(f3895,definition,
( spl8_15
<=> iLess0(sK6(sK3),sK3) ),
introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition]) ).
fof(f3897,plain,
( ~ iLess0(sK6(sK3),sK3)
| spl8_15 ),
inference(avatar_component_clause,[],[f3895]) ).
fof(f3898,plain,
( spl8_5
| ~ spl8_15
| ~ spl8_2
| spl8_4
| ~ spl8_6 ),
inference(avatar_split_clause,[],[f3842,f529,f257,f225,f3895,f261]) ).
fof(f3924,plain,
( ~ aNaturalNumber0(sK6(sK3))
| ~ sdtlseqdt0(sK6(sK3),sK3)
| sK3 = sK6(sK3)
| ~ aNaturalNumber0(sK3)
| spl8_15 ),
inference(resolution,[],[f3897,f153]) ).
fof(f3925,plain,
( ~ sdtlseqdt0(sK6(sK3),sK3)
| sK3 = sK6(sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_6
| spl8_15 ),
inference(forward_subsumption_resolution,[],[f3924,f530]) ).
fof(f3926,plain,
( sK3 = sK6(sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_6
| ~ spl8_9
| spl8_15 ),
inference(forward_subsumption_resolution,[],[f3925,f543]) ).
fof(f3927,plain,
( ~ aNaturalNumber0(sK3)
| ~ spl8_6
| ~ spl8_9
| spl8_15 ),
inference(forward_subsumption_resolution,[],[f3926,f345]) ).
fof(f3928,plain,
( $false
| ~ spl8_6
| ~ spl8_9
| spl8_15 ),
inference(forward_subsumption_resolution,[],[f3927,f197]) ).
fof(f3929,plain,
( ~ spl8_6
| ~ spl8_9
| spl8_15 ),
inference(avatar_contradiction_clause,[],[f3928]) ).
fof(f3958,plain,
( sz10 != sz10
| sz10 = sK3
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_5 ),
inference(superposition,[],[f181,f263]) ).
fof(f3964,plain,
( sz10 = sK3
| sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_5 ),
inference(trivial_inequality_removal,[],[f3958]) ).
fof(f3966,plain,
( sz00 = sK3
| ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f3964,f195]) ).
fof(f3968,plain,
( ~ doDivides0(sK3,sK3)
| ~ aNaturalNumber0(sK3)
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f3966,f196]) ).
fof(f3970,plain,
( ~ aNaturalNumber0(sK3)
| ~ spl8_2
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f3968,f226]) ).
fof(f3971,plain,
( $false
| ~ spl8_2
| ~ spl8_5 ),
inference(forward_subsumption_resolution,[],[f3970,f197]) ).
fof(f3972,plain,
( ~ spl8_2
| ~ spl8_5 ),
inference(avatar_contradiction_clause,[],[f3971]) ).
cnf(s3,plain,
( ~ spl8_6
| spl8_7
| ~ spl8_8
| spl8_9 ),
inference(sat_conversion,[],[f544]) ).
cnf(s4,plain,
spl8_6,
inference(sat_conversion,[],[f569]) ).
cnf(s5,plain,
spl8_2,
inference(sat_conversion,[],[f627]) ).
cnf(s6,plain,
( ~ spl8_2
| spl8_8 ),
inference(sat_conversion,[],[f707]) ).
cnf(s7,plain,
( ~ spl8_6
| ~ spl8_7 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s12,plain,
( ~ spl8_4
| ~ spl8_8 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s13,plain,
( ~ spl8_2
| spl8_4
| spl8_5
| ~ spl8_6
| ~ spl8_15 ),
inference(sat_conversion,[],[f3898]) ).
cnf(s14,plain,
( ~ spl8_6
| ~ spl8_9
| spl8_15 ),
inference(sat_conversion,[],[f3929]) ).
cnf(s15,plain,
( ~ spl8_2
| ~ spl8_5 ),
inference(sat_conversion,[],[f3972]) ).
cnf(s17,plain,
~ spl8_5,
inference(rat,[],[s15,s5]) ).
cnf(s18,plain,
spl8_8,
inference(rat,[],[s6,s5]) ).
cnf(s19,plain,
~ spl8_4,
inference(rat,[],[s12,s18]) ).
cnf(s21,plain,
~ spl8_7,
inference(rat,[],[s7,s4]) ).
cnf(s22,plain,
~ spl8_15,
inference(rat,[],[s13,s19,s5,s17,s4]) ).
cnf(s23,plain,
~ spl8_9,
inference(rat,[],[s14,s4,s22]) ).
cnf(s24,plain,
$false,
inference(rat,[],[s3,s23,s18,s21,s4]) ).
fof(f3973,plain,
$false,
inference(avatar_sat_refutation,[],[s24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM481+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.38 % Computer : n010.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 20:07:16 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.97/1.73 % (1275837)Will run a generic schedule for satisfiability detection.
% 7.97/1.73 % (1275842)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1541172438_2999 on theBenchmark for (2999ds/0Mi)
% 7.97/1.73 % (1275843)% WARNING: option uhcvi not known.
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [3]
% 7.97/1.73 % (1275843)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=95264785:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.97/1.73 % (1275844)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3404751880:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.97/1.73 % (1275845)dis+10_1_sil=32000:sp=arity:random_seed=835459913:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.97/1.73 % (1275846)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=205387008:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.97/1.73 % (1275847)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2256159807:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.97/1.73 % (1275848)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2264327372:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.97/1.73 % TRYING [4]
% 7.97/1.73 % TRYING [5]
% 7.97/1.73 % TRYING [6]
% 7.97/1.73 % (1275845)Instruction limit reached!
% 7.97/1.73 % (1275845)------------------------------
% 7.97/1.73 % (1275845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275845)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275845)Termination reason: Instruction limit
% 7.97/1.73 % (1275845)Termination phase: Saturation
% 7.97/1.73 % (1275845)Time elapsed: 0.062 s
% 7.97/1.73 % (1275845)Peak memory usage: 12 MB
% 7.97/1.73 % (1275845)Instructions burned: 104 (million)
% 7.97/1.73 % (1275846)Instruction limit reached!
% 7.97/1.73 % (1275846)------------------------------
% 7.97/1.73 % (1275846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275846)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275846)Termination reason: Instruction limit
% 7.97/1.73 % (1275846)Termination phase: Saturation
% 7.97/1.73 % (1275846)Time elapsed: 0.064 s
% 7.97/1.73 % (1275846)Peak memory usage: 13 MB
% 7.97/1.73 % (1275846)Instructions burned: 116 (million)
% 7.97/1.73 % (1275847)Instruction limit reached!
% 7.97/1.73 % (1275847)------------------------------
% 7.97/1.73 % (1275847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275847)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275847)Termination reason: Instruction limit
% 7.97/1.73 % (1275847)Termination phase: Saturation
% 7.97/1.73 % (1275847)Time elapsed: 0.071 s
% 7.97/1.73 % (1275847)Peak memory usage: 13 MB
% 7.97/1.73 % (1275847)Instructions burned: 133 (million)
% 7.97/1.73 % (1275856)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3181785448:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.97/1.73 % (1275857)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4202385171:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [3]
% 7.97/1.73 % (1275858)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=1640744433:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.97/1.73 % (1275848)Instruction limit reached!
% 7.97/1.73 % (1275848)------------------------------
% 7.97/1.73 % (1275848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275848)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275848)Termination reason: Instruction limit
% 7.97/1.73 % (1275848)Termination phase: Saturation
% 7.97/1.73 % (1275848)Time elapsed: 0.097 s
% 7.97/1.73 % (1275848)Peak memory usage: 14 MB
% 7.97/1.73 % (1275848)Instructions burned: 160 (million)
% 7.97/1.73 % TRYING [4]
% 7.97/1.73 % (1275862)ott-21_1_sil=16000:fs=off:random_seed=3736542556:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.97/1.73 % TRYING [5]
% 7.97/1.73 % TRYING [7]
% 7.97/1.73 % (1275857)Instruction limit reached!
% 7.97/1.73 % (1275857)------------------------------
% 7.97/1.73 % (1275857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275857)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275857)Termination reason: Instruction limit
% 7.97/1.73 % (1275857)Termination phase: Saturation
% 7.97/1.73 % (1275857)Time elapsed: 0.074 s
% 7.97/1.73 % (1275857)Peak memory usage: 12 MB
% 7.97/1.73 % (1275857)Instructions burned: 131 (million)
% 7.97/1.73 % (1275864)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1504229547:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.97/1.73 % TRYING [6]
% 7.97/1.73 % (1275862)Instruction limit reached!
% 7.97/1.73 % (1275862)------------------------------
% 7.97/1.73 % (1275862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275862)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275862)Termination reason: Instruction limit
% 7.97/1.73 % (1275862)Termination phase: Saturation
% 7.97/1.73 % (1275862)Time elapsed: 0.093 s
% 7.97/1.73 % (1275862)Peak memory usage: 13 MB
% 7.97/1.73 % (1275862)Instructions burned: 181 (million)
% 7.97/1.73 % (1275866)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=728361488:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [3]
% 7.97/1.73 % TRYING [4]
% 7.97/1.73 % TRYING [5]
% 7.97/1.73 % (1275856)Instruction limit reached!
% 7.97/1.73 % (1275856)------------------------------
% 7.97/1.73 % (1275856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275856)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275856)Termination reason: Instruction limit
% 7.97/1.73 % (1275856)Termination phase: Finite model building constraint generation
% 7.97/1.73 % (1275856)Time elapsed: 0.252 s
% 7.97/1.73 % (1275856)Peak memory usage: 32 MB
% 7.97/1.73 % (1275856)Instructions burned: 716 (million)
% 7.97/1.73 % TRYING [8]
% 7.97/1.73 % (1275868)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=913962022:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 7.97/1.73 % (1275858)Instruction limit reached!
% 7.97/1.73 % (1275858)------------------------------
% 7.97/1.73 % (1275858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275858)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275858)Termination reason: Instruction limit
% 7.97/1.73 % (1275858)Termination phase: Saturation
% 7.97/1.73 % (1275858)Time elapsed: 0.381 s
% 7.97/1.73 % (1275858)Peak memory usage: 17 MB
% 7.97/1.73 % (1275858)Instructions burned: 686 (million)
% 7.97/1.73 % (1275870)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4188903198:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 7.97/1.73 % (1275864)Instruction limit reached!
% 7.97/1.73 % (1275864)------------------------------
% 7.97/1.73 % (1275864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275864)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275864)Termination reason: Instruction limit
% 7.97/1.73 % (1275864)Termination phase: Saturation
% 7.97/1.73 % (1275864)Time elapsed: 0.334 s
% 7.97/1.73 % (1275864)Peak memory usage: 15 MB
% 7.97/1.73 % (1275864)Instructions burned: 477 (million)
% 7.97/1.73 % (1275872)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=2784290942: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)
% 7.97/1.73 % TRYING [6]
% 7.97/1.73 % (1275866)Instruction limit reached!
% 7.97/1.73 % (1275866)------------------------------
% 7.97/1.73 % (1275866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275866)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275866)Termination reason: Instruction limit
% 7.97/1.73 % (1275866)Termination phase: Finite model building constraint generation
% 7.97/1.73 % (1275866)Time elapsed: 0.342 s
% 7.97/1.73 % (1275866)Peak memory usage: 22 MB
% 7.97/1.73 % (1275866)Instructions burned: 866 (million)
% 7.97/1.73 % (1275874)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3603697145:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 7.97/1.73 % TRYING [14]
% 7.97/1.73 % (1275870)Instruction limit reached!
% 7.97/1.73 % (1275870)------------------------------
% 7.97/1.73 % (1275870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275870)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275870)Termination reason: Instruction limit
% 7.97/1.73 % (1275870)Termination phase: Finite model building constraint generation
% 7.97/1.73 % (1275870)Time elapsed: 0.343 s
% 7.97/1.73 % (1275870)Peak memory usage: 81 MB
% 7.97/1.73 % (1275870)Instructions burned: 890 (million)
% 7.97/1.73 % (1275876)fmb+10_1_sil=64000:random_seed=1609312453:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [3]
% 7.97/1.73 % TRYING [4]
% 7.97/1.73 % TRYING [9]
% 7.97/1.73 % (1275872)Instruction limit reached!
% 7.97/1.73 % (1275872)------------------------------
% 7.97/1.73 % (1275872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275872)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275872)Termination reason: Instruction limit
% 7.97/1.73 % (1275872)Termination phase: Saturation
% 7.97/1.73 % (1275872)Time elapsed: 0.365 s
% 7.97/1.73 % (1275872)Peak memory usage: 20 MB
% 7.97/1.73 % (1275872)Instructions burned: 692 (million)
% 7.97/1.73 % (1275878)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2385169687:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [20]
% 7.97/1.73 % TRYING [5]
% 7.97/1.73 % (1275868)Instruction limit reached!
% 7.97/1.73 % (1275868)------------------------------
% 7.97/1.73 % (1275868)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275868)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275868)Termination reason: Instruction limit
% 7.97/1.73 % (1275868)Termination phase: Saturation
% 7.97/1.73 % (1275868)Time elapsed: 0.676 s
% 7.97/1.73 % (1275868)Peak memory usage: 25 MB
% 7.97/1.73 % (1275868)Instructions burned: 1179 (million)
% 7.97/1.73 % (1275880)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=343492391:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 7.97/1.73 % Detected minimum model sizes of [3]
% 7.97/1.73 % Detected maximum model sizes of [max]
% 7.97/1.73 % TRYING [8]
% 7.97/1.73 % (1275874)Instruction limit reached!
% 7.97/1.73 % (1275874)------------------------------
% 7.97/1.73 % (1275874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275874)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275874)Termination reason: Instruction limit
% 7.97/1.73 % (1275874)Termination phase: Saturation
% 7.97/1.73 % (1275874)Time elapsed: 0.508 s
% 7.97/1.73 % (1275874)Peak memory usage: 19 MB
% 7.97/1.73 % (1275874)Instructions burned: 880 (million)
% 7.97/1.73 % (1275882)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1789714970:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 7.97/1.73 % TRYING [6]
% 7.97/1.73 % (1275882) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1275837-1275882"...
% 7.97/1.73 % (1275882)...printing done.
% 7.97/1.73 % (1275882)Refutation found. Thanks to Tanya!
% 7.97/1.73 % SZS status Theorem for theBenchmark
% 7.97/1.73 % SZS output start Proof for theBenchmark
% See solution above
% 7.97/1.73 % (1275882)------------------------------
% 7.97/1.73 % (1275882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.97/1.73 % (1275882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.97/1.73 % (1275882)CaDiCaL version: 2.1.3
% 7.97/1.73 % (1275882)Termination reason: Refutation
% 7.97/1.73 % (1275882)Time elapsed: 0.106 s
% 7.97/1.73 % (1275882)Peak memory usage: 14 MB
% 7.97/1.73 % (1275882)Instructions burned: 189 (million)
% 7.97/1.73 % (1275837)Success in time 1.294 s
% 7.97/1.73 % Vampire exiting
%------------------------------------------------------------------------------