%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG126+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 : n016.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:36:08 PM UTC 2026
% Result : Theorem 51.22s 20.64s
% Output : Refutation 51.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of formulae : 85 ( 25 unt; 1 def)
% Number of atoms : 348 ( 28 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 428 ( 165 ~; 154 |; 85 &)
% ( 12 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 2 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 122 ( 0 sgn 105 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulComm) ).
fof(f24,axiom,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X1),X0) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefIdeal) ).
fof(f33,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> ( doDivides0(X0,X1)
<=> ? [X2] :
( aElement0(X2)
& sdtasdt0(X0,X2) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiv) ).
fof(f34,axiom,
! [X0] :
( aElement0(X0)
=> ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aElement0(X1)
& doDivides0(X1,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDvs) ).
fof(f35,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> ! [X2] :
( aGcdOfAnd0(X2,X0,X1)
<=> ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X3] :
( ( aDivisorOf0(X3,X0)
& aDivisorOf0(X3,X1) )
=> doDivides0(X3,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefGCD) ).
fof(f39,axiom,
( aElement0(xa)
& aElement0(xb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2091) ).
fof(f41,axiom,
aGcdOfAnd0(xc,xa,xb),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2129) ).
fof(f42,axiom,
( aIdeal0(xI)
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2174) ).
fof(f45,axiom,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X0] :
( ( aElementOf0(X0,xI)
& X0 != sz00 )
=> ~ iLess0(sbrdtbr0(X0),sbrdtbr0(xu)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2273) ).
fof(f46,axiom,
( aDivisorOf0(xu,xa)
& aDivisorOf0(xu,xb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2373) ).
fof(f47,axiom,
doDivides0(xu,xc),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2744) ).
fof(f48,conjecture,
aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f49,negated_conjecture,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f53,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( aElementOf0(X1,X0)
=> ( ! [X2] :
( aElementOf0(X2,X0)
=> aElementOf0(sdtpldt0(X1,X2),X0) )
& ! [X3] :
( aElement0(X3)
=> aElementOf0(sdtasdt0(X3,X1),X0) ) ) ) ) ),
inference(rectify,[],[f24]) ).
fof(f57,plain,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(flattening,[],[f49]) ).
fof(f70,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f71,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f70]) ).
fof(f88,plain,
! [X0] :
( aIdeal0(X0)
<=> ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) ) ),
inference(ennf_transformation,[],[f53]) ).
fof(f99,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aElement0(X2)
& sdtasdt0(X0,X2) = X1 ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f100,plain,
! [X0,X1] :
( ( doDivides0(X0,X1)
<=> ? [X2] :
( aElement0(X2)
& sdtasdt0(X0,X2) = X1 ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ! [X1] :
( aDivisorOf0(X1,X0)
<=> ( aElement0(X1)
& doDivides0(X1,X0) ) )
| ~ aElement0(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f102,plain,
! [X0,X1] :
( ! [X2] :
( aGcdOfAnd0(X2,X0,X1)
<=> ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X3] :
( doDivides0(X3,X2)
| ~ aDivisorOf0(X3,X0)
| ~ aDivisorOf0(X3,X1) ) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f35]) ).
fof(f103,plain,
! [X0,X1] :
( ! [X2] :
( aGcdOfAnd0(X2,X0,X1)
<=> ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X3] :
( doDivides0(X3,X2)
| ~ aDivisorOf0(X3,X0)
| ~ aDivisorOf0(X3,X1) ) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f102]) ).
fof(f108,plain,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X0] :
( ~ iLess0(sbrdtbr0(X0),sbrdtbr0(xu))
| ~ aElementOf0(X0,xI)
| sz00 = X0 ) ),
inference(ennf_transformation,[],[f45]) ).
fof(f109,plain,
( aElementOf0(xu,xI)
& xu != sz00
& ! [X0] :
( ~ iLess0(sbrdtbr0(X0),sbrdtbr0(xu))
| ~ aElementOf0(X0,xI)
| sz00 = X0 ) ),
inference(flattening,[],[f108]) ).
fof(f124,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f125,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X1] :
( ( ! [X2] :
( aElementOf0(sdtpldt0(X1,X2),X0)
| ~ aElementOf0(X2,X0) )
& ! [X3] :
( aElementOf0(sdtasdt0(X3,X1),X0)
| ~ aElement0(X3) ) )
| ~ aElementOf0(X1,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(flattening,[],[f124]) ).
fof(f126,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ? [X1] :
( ( ? [X2] :
( ~ aElementOf0(sdtpldt0(X1,X2),X0)
& aElementOf0(X2,X0) )
| ? [X3] :
( ~ aElementOf0(sdtasdt0(X3,X1),X0)
& aElement0(X3) ) )
& aElementOf0(X1,X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(rectify,[],[f125]) ).
fof(f127,plain,
! [X0] :
( ( aIdeal0(X0)
| ~ aSet0(X0)
| ( ( ( ~ aElementOf0(sdtpldt0(sK10(X0),sK11(X0)),X0)
& aElementOf0(sK11(X0),X0) )
| ( ~ aElementOf0(sdtasdt0(sK12(X0),sK10(X0)),X0)
& aElement0(sK12(X0)) ) )
& aElementOf0(sK10(X0),X0) ) )
& ( ( aSet0(X0)
& ! [X4] :
( ( ! [X5] :
( aElementOf0(sdtpldt0(X4,X5),X0)
| ~ aElementOf0(X5,X0) )
& ! [X6] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6) ) )
| ~ aElementOf0(X4,X0) ) )
| ~ aIdeal0(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12]),skolemize(X1,sK10(X0)),skolemize(X2,sK11(X0)),skolemize(X3,sK12(X0))],[f126]) ).
fof(f132,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aElement0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X2] :
( aElement0(X2)
& sdtasdt0(X0,X2) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(nnf_transformation,[],[f100]) ).
fof(f133,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aElement0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ? [X3] :
( aElement0(X3)
& sdtasdt0(X0,X3) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(rectify,[],[f132]) ).
fof(f134,plain,
! [X0,X1] :
( ( ( doDivides0(X0,X1)
| ! [X2] :
( ~ aElement0(X2)
| sdtasdt0(X0,X2) != X1 ) )
& ( ( aElement0(sK17(X0,X1))
& sdtasdt0(X0,sK17(X0,X1)) = X1 )
| ~ doDivides0(X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(X3,sK17(X0,X1))],[f133]) ).
fof(f135,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aElement0(X1)
| ~ doDivides0(X1,X0) )
& ( ( aElement0(X1)
& doDivides0(X1,X0) )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aElement0(X0) ),
inference(nnf_transformation,[],[f101]) ).
fof(f136,plain,
! [X0] :
( ! [X1] :
( ( aDivisorOf0(X1,X0)
| ~ aElement0(X1)
| ~ doDivides0(X1,X0) )
& ( ( aElement0(X1)
& doDivides0(X1,X0) )
| ~ aDivisorOf0(X1,X0) ) )
| ~ aElement0(X0) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( ! [X2] :
( ( aGcdOfAnd0(X2,X0,X1)
| ~ aDivisorOf0(X2,X0)
| ~ aDivisorOf0(X2,X1)
| ? [X3] :
( ~ doDivides0(X3,X2)
& aDivisorOf0(X3,X0)
& aDivisorOf0(X3,X1) ) )
& ( ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X3] :
( doDivides0(X3,X2)
| ~ aDivisorOf0(X3,X0)
| ~ aDivisorOf0(X3,X1) ) )
| ~ aGcdOfAnd0(X2,X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(nnf_transformation,[],[f103]) ).
fof(f138,plain,
! [X0,X1] :
( ! [X2] :
( ( aGcdOfAnd0(X2,X0,X1)
| ~ aDivisorOf0(X2,X0)
| ~ aDivisorOf0(X2,X1)
| ? [X3] :
( ~ doDivides0(X3,X2)
& aDivisorOf0(X3,X0)
& aDivisorOf0(X3,X1) ) )
& ( ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X3] :
( doDivides0(X3,X2)
| ~ aDivisorOf0(X3,X0)
| ~ aDivisorOf0(X3,X1) ) )
| ~ aGcdOfAnd0(X2,X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f137]) ).
fof(f139,plain,
! [X0,X1] :
( ! [X2] :
( ( aGcdOfAnd0(X2,X0,X1)
| ~ aDivisorOf0(X2,X0)
| ~ aDivisorOf0(X2,X1)
| ? [X3] :
( ~ doDivides0(X3,X2)
& aDivisorOf0(X3,X0)
& aDivisorOf0(X3,X1) ) )
& ( ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X4] :
( doDivides0(X4,X2)
| ~ aDivisorOf0(X4,X0)
| ~ aDivisorOf0(X4,X1) ) )
| ~ aGcdOfAnd0(X2,X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(rectify,[],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( ! [X2] :
( ( aGcdOfAnd0(X2,X0,X1)
| ~ aDivisorOf0(X2,X0)
| ~ aDivisorOf0(X2,X1)
| ( ~ doDivides0(sK18(X0,X1,X2),X2)
& aDivisorOf0(sK18(X0,X1,X2),X0)
& aDivisorOf0(sK18(X0,X1,X2),X1) ) )
& ( ( aDivisorOf0(X2,X0)
& aDivisorOf0(X2,X1)
& ! [X4] :
( doDivides0(X4,X2)
| ~ aDivisorOf0(X4,X0)
| ~ aDivisorOf0(X4,X1) ) )
| ~ aGcdOfAnd0(X2,X0,X1) ) )
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X3,sK18(X0,X1,X2))],[f139]) ).
fof(f158,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f194,plain,
! [X0,X6,X4] :
( aElementOf0(sdtasdt0(X6,X4),X0)
| ~ aElement0(X6)
| ~ aElementOf0(X4,X0)
| ~ aIdeal0(X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f216,plain,
! [X0,X1] :
( ~ doDivides0(X0,X1)
| sdtasdt0(X0,sK17(X0,X1)) = X1
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f217,plain,
! [X0,X1] :
( aElement0(sK17(X0,X1))
| ~ doDivides0(X0,X1)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f134]) ).
fof(f220,plain,
! [X0,X1] :
( ~ aDivisorOf0(X1,X0)
| aElement0(X1)
| ~ aElement0(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f223,plain,
! [X2,X0,X1] :
( ~ aGcdOfAnd0(X2,X0,X1)
| aDivisorOf0(X2,X1)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f140]) ).
fof(f238,plain,
aElement0(xb),
inference(cnf_transformation,[],[f39]) ).
fof(f239,plain,
aElement0(xa),
inference(cnf_transformation,[],[f39]) ).
fof(f241,plain,
aGcdOfAnd0(xc,xa,xb),
inference(cnf_transformation,[],[f41]) ).
fof(f242,plain,
xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)),
inference(cnf_transformation,[],[f42]) ).
fof(f243,plain,
aIdeal0(xI),
inference(cnf_transformation,[],[f42]) ).
fof(f252,plain,
aElementOf0(xu,xI),
inference(cnf_transformation,[],[f109]) ).
fof(f254,plain,
aDivisorOf0(xu,xa),
inference(cnf_transformation,[],[f46]) ).
fof(f255,plain,
doDivides0(xu,xc),
inference(cnf_transformation,[],[f47]) ).
fof(f256,plain,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(cnf_transformation,[],[f57]) ).
fof(f278,plain,
~ aElementOf0(xc,xI),
inference(superposition,[],[f256,f242]) ).
fof(f740,plain,
( aElement0(xu)
| ~ aElement0(xa) ),
inference(resolution,[],[f220,f254]) ).
fof(f922,plain,
aElement0(xu),
inference(forward_subsumption_resolution,[],[f740,f239]) ).
fof(f2536,plain,
! [X0] :
( ~ aElement0(X0)
| sdtasdt0(X0,xu) = sdtasdt0(xu,X0) ),
inference(resolution,[],[f158,f922]) ).
fof(f2851,plain,
( aDivisorOf0(xc,xb)
| ~ aElement0(xa)
| ~ aElement0(xb) ),
inference(resolution,[],[f223,f241]) ).
fof(f2852,plain,
( aDivisorOf0(xc,xb)
| ~ aElement0(xb) ),
inference(forward_subsumption_resolution,[],[f2851,f239]) ).
fof(f2853,plain,
aDivisorOf0(xc,xb),
inference(forward_subsumption_resolution,[],[f2852,f238]) ).
fof(f2854,plain,
( aElement0(xc)
| ~ aElement0(xb) ),
inference(resolution,[],[f2853,f220]) ).
fof(f2855,plain,
aElement0(xc),
inference(forward_subsumption_resolution,[],[f2854,f238]) ).
fof(f42315,plain,
( xc = sdtasdt0(xu,sK17(xu,xc))
| ~ aElement0(xu)
| ~ aElement0(xc) ),
inference(resolution,[],[f216,f255]) ).
fof(f42362,plain,
( xc = sdtasdt0(xu,sK17(xu,xc))
| ~ aElement0(xc) ),
inference(forward_subsumption_resolution,[],[f42315,f922]) ).
fof(f42423,plain,
xc = sdtasdt0(xu,sK17(xu,xc)),
inference(forward_subsumption_resolution,[],[f42362,f2855]) ).
fof(f77384,definition,
( spl23_338
<=> aElement0(sK17(xu,xc)) ),
introduced(definition,[new_symbols(definition,[spl23_338])],[avatar_definition]) ).
fof(f77385,plain,
( aElement0(sK17(xu,xc))
| ~ spl23_338 ),
inference(avatar_component_clause,[],[f77384]) ).
fof(f77386,plain,
( ~ aElement0(sK17(xu,xc))
| spl23_338 ),
inference(avatar_component_clause,[],[f77384]) ).
fof(f77392,plain,
( ~ doDivides0(xu,xc)
| ~ aElement0(xu)
| ~ aElement0(xc)
| spl23_338 ),
inference(resolution,[],[f77386,f217]) ).
fof(f77393,plain,
( ~ aElement0(xu)
| ~ aElement0(xc)
| spl23_338 ),
inference(forward_subsumption_resolution,[],[f77392,f255]) ).
fof(f77394,plain,
( ~ aElement0(xc)
| spl23_338 ),
inference(forward_subsumption_resolution,[],[f77393,f922]) ).
fof(f77395,plain,
( $false
| spl23_338 ),
inference(forward_subsumption_resolution,[],[f77394,f2855]) ).
fof(f77396,plain,
spl23_338,
inference(avatar_contradiction_clause,[],[f77395]) ).
fof(f77418,plain,
( sdtasdt0(xu,sK17(xu,xc)) = sdtasdt0(sK17(xu,xc),xu)
| ~ spl23_338 ),
inference(resolution,[],[f77385,f2536]) ).
fof(f77424,plain,
( xc = sdtasdt0(sK17(xu,xc),xu)
| ~ spl23_338 ),
inference(forward_demodulation,[],[f77418,f42423]) ).
fof(f77483,plain,
( ! [X0] :
( aElementOf0(xc,X0)
| ~ aElement0(sK17(xu,xc))
| ~ aElementOf0(xu,X0)
| ~ aIdeal0(X0) )
| ~ spl23_338 ),
inference(superposition,[],[f194,f77424]) ).
fof(f77495,plain,
( ! [X0] :
( ~ aElementOf0(xu,X0)
| aElementOf0(xc,X0)
| ~ aIdeal0(X0) )
| ~ spl23_338 ),
inference(forward_subsumption_resolution,[],[f77483,f77385]) ).
fof(f77867,plain,
( aElementOf0(xc,xI)
| ~ aIdeal0(xI)
| ~ spl23_338 ),
inference(resolution,[],[f77495,f252]) ).
fof(f77878,plain,
( ~ aIdeal0(xI)
| ~ spl23_338 ),
inference(forward_subsumption_resolution,[],[f77867,f278]) ).
fof(f77879,plain,
( $false
| ~ spl23_338 ),
inference(forward_subsumption_resolution,[],[f77878,f243]) ).
fof(f77880,plain,
~ spl23_338,
inference(avatar_contradiction_clause,[],[f77879]) ).
cnf(s28525,plain,
spl23_338,
inference(sat_conversion,[],[f77396]) ).
cnf(s28701,plain,
~ spl23_338,
inference(sat_conversion,[],[f77880]) ).
cnf(s28704,plain,
$false,
inference(rat,[],[s28525,s28701]) ).
fof(f77881,plain,
$false,
inference(avatar_sat_refutation,[],[s28704]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG126+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.11/0.39 % Computer : n016.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 23:28:03 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.87/2.48 % (3108411)Will run a generic schedule for satisfiability detection.
% 13.87/2.48 % (3108419)dis+10_1_sil=32000:sp=arity:random_seed=1663688354:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.87/2.48 % (3108417)% WARNING: option uhcvi not known.
% 13.87/2.48 % (3108416)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3839197651_2999 on theBenchmark for (2999ds/0Mi)
% 13.87/2.48 % (3108417)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1227630481:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.87/2.48 % (3108418)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1141358344:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.87/2.48 % (3108420)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3988176755:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.87/2.48 % (3108421)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=337838084:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.87/2.48 % (3108422)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1843103604:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.87/2.48 % TRYING [1]
% 13.87/2.48 % TRYING [2]
% 13.87/2.48 % TRYING [3]
% 13.87/2.48 % (3108419)Instruction limit reached!
% 13.87/2.48 % (3108419)------------------------------
% 13.87/2.48 % (3108419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.48 % (3108419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.48 % (3108419)CaDiCaL version: 2.1.3
% 13.87/2.48 % (3108419)Termination reason: Instruction limit
% 13.87/2.48 % (3108419)Termination phase: Saturation
% 13.87/2.48 % (3108419)Time elapsed: 0.036 s
% 13.87/2.48 % (3108419)Peak memory usage: 13 MB
% 13.87/2.48 % (3108419)Instructions burned: 105 (million)
% 13.87/2.48 % TRYING [4]
% 13.87/2.48 % (3108430)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=981137424:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 13.87/2.48 % TRYING [1]
% 13.87/2.48 % TRYING [2]
% 13.87/2.48 % TRYING [3]
% 13.87/2.48 % TRYING [4]
% 13.87/2.48 % (3108420)Instruction limit reached!
% 13.87/2.48 % (3108420)------------------------------
% 13.87/2.48 % (3108420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.48 % (3108420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.48 % (3108420)CaDiCaL version: 2.1.3
% 13.87/2.48 % (3108420)Termination reason: Instruction limit
% 13.87/2.48 % (3108420)Termination phase: Saturation
% 13.87/2.48 % (3108420)Time elapsed: 0.069 s
% 13.87/2.48 % (3108420)Peak memory usage: 13 MB
% 13.87/2.48 % (3108420)Instructions burned: 116 (million)
% 13.87/2.48 % (3108421)Instruction limit reached!
% 13.87/2.48 % (3108421)------------------------------
% 13.87/2.48 % (3108421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.48 % (3108421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.48 % (3108421)CaDiCaL version: 2.1.3
% 13.87/2.48 % (3108421)Termination reason: Instruction limit
% 13.87/2.48 % (3108421)Termination phase: Saturation
% 13.87/2.48 % (3108421)Time elapsed: 0.071 s
% 13.87/2.48 % (3108421)Peak memory usage: 13 MB
% 13.87/2.48 % (3108421)Instructions burned: 131 (million)
% 13.87/2.48 % (3108432)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2951668488:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 13.87/2.48 % (3108433)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=2307050640:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.87/2.48 % TRYING [5]
% 13.87/2.48 % TRYING [5]
% 13.87/2.48 % (3108422)Instruction limit reached!
% 13.87/2.48 % (3108422)------------------------------
% 13.87/2.48 % (3108422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.87/2.48 % (3108422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.48 % (3108422)CaDiCaL version: 2.1.3
% 13.87/2.48 % (3108422)Termination reason: Instruction limit
% 13.87/2.48 % (3108422)Termination phase: Saturation
% 13.87/2.48 % (3108422)Time elapsed: 0.104 s
% 13.87/2.48 % (3108422)Peak memory usage: 15 MB
% 13.87/2.48 % (3108422)Instructions burned: 160 (million)
% 13.87/2.48 % (3108436)ott-21_1_sil=16000:fs=off:random_seed=368006774:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.87/2.48 % (3108432)Instruction limit reached!
% 13.87/2.48 % (3108432)------------------------------
% 13.87/2.48 % (3108432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108432)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108432)Termination reason: Instruction limit
% 37.26/5.74 % (3108432)Termination phase: Saturation
% 37.26/5.74 % (3108432)Time elapsed: 0.069 s
% 37.26/5.74 % (3108432)Peak memory usage: 12 MB
% 37.26/5.74 % (3108432)Instructions burned: 132 (million)
% 37.26/5.74 % (3108438)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1337092837:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 37.26/5.74 % (3108430)Instruction limit reached!
% 37.26/5.74 % (3108430)------------------------------
% 37.26/5.74 % (3108430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108430)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108430)Termination reason: Instruction limit
% 37.26/5.74 % (3108430)Termination phase: Finite model building SAT solving
% 37.26/5.74 % (3108430)Time elapsed: 0.172 s
% 37.26/5.74 % (3108430)Peak memory usage: 32 MB
% 37.26/5.74 % (3108430)Instructions burned: 715 (million)
% 37.26/5.74 % (3108436)Instruction limit reached!
% 37.26/5.74 % (3108436)------------------------------
% 37.26/5.74 % (3108436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108436)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108436)Termination reason: Instruction limit
% 37.26/5.74 % (3108436)Termination phase: Saturation
% 37.26/5.74 % (3108436)Time elapsed: 0.094 s
% 37.26/5.74 % (3108436)Peak memory usage: 13 MB
% 37.26/5.74 % (3108436)Instructions burned: 180 (million)
% 37.26/5.74 % (3108441)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1336296544:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 37.26/5.74 % (3108440)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3589860998:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.26/5.74 % TRYING [1]
% 37.26/5.74 % TRYING [2]
% 37.26/5.74 % TRYING [3]
% 37.26/5.74 % TRYING [6]
% 37.26/5.74 % TRYING [4]
% 37.26/5.74 % (3108433)Instruction limit reached!
% 37.26/5.74 % (3108433)------------------------------
% 37.26/5.74 % (3108433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108433)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108433)Termination reason: Instruction limit
% 37.26/5.74 % (3108433)Termination phase: Saturation
% 37.26/5.74 % (3108433)Time elapsed: 0.336 s
% 37.26/5.74 % (3108433)Peak memory usage: 20 MB
% 37.26/5.74 % (3108433)Instructions burned: 684 (million)
% 37.26/5.74 % (3108444)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1149520492:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.26/5.74 % (3108438)Instruction limit reached!
% 37.26/5.74 % (3108438)------------------------------
% 37.26/5.74 % (3108438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108438)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108438)Termination reason: Instruction limit
% 37.26/5.74 % (3108438)Termination phase: Saturation
% 37.26/5.74 % (3108438)Time elapsed: 0.319 s
% 37.26/5.74 % (3108438)Peak memory usage: 15 MB
% 37.26/5.74 % (3108438)Instructions burned: 478 (million)
% 37.26/5.74 % (3108446)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=3984215310: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)
% 37.26/5.74 % TRYING [5]
% 37.26/5.74 % (3108441)Instruction limit reached!
% 37.26/5.74 % (3108441)------------------------------
% 37.26/5.74 % (3108441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.26/5.74 % (3108441)CaDiCaL version: 2.1.3
% 37.26/5.74 % (3108441)Termination reason: Instruction limit
% 37.26/5.74 % (3108441)Termination phase: Saturation
% 37.26/5.74 % (3108441)Time elapsed: 0.344 s
% 37.26/5.74 % (3108441)Peak memory usage: 27 MB
% 37.26/5.74 % (3108441)Instructions burned: 1182 (million)
% 37.26/5.74 % (3108440)Instruction limit reached!
% 37.26/5.74 % (3108440)------------------------------
% 37.26/5.74 % (3108440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.26/5.74 % (3108440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108440)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108440)Termination reason: Instruction limit
% 86.95/12.72 % (3108440)Termination phase: Finite model building constraint generation
% 86.95/12.72 % (3108440)Time elapsed: 0.343 s
% 86.95/12.72 % (3108440)Peak memory usage: 21 MB
% 86.95/12.72 % (3108440)Instructions burned: 867 (million)
% 86.95/12.72 % (3108448)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4193855318:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 86.95/12.72 % (3108449)fmb+10_1_sil=64000:random_seed=1583405198:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 86.95/12.72 % TRYING [1]
% 86.95/12.72 % TRYING [2]
% 86.95/12.72 % TRYING [3]
% 86.95/12.72 % TRYING [4]
% 86.95/12.72 % TRYING [7]
% 86.95/12.72 % TRYING [5]
% 86.95/12.72 % (3108444)Instruction limit reached!
% 86.95/12.72 % (3108444)------------------------------
% 86.95/12.72 % (3108444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.95/12.72 % (3108444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108444)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108444)Termination reason: Instruction limit
% 86.95/12.72 % (3108444)Termination phase: Finite model building constraint generation
% 86.95/12.72 % (3108444)Time elapsed: 0.402 s
% 86.95/12.72 % (3108444)Peak memory usage: 107 MB
% 86.95/12.72 % (3108444)Instructions burned: 891 (million)
% 86.95/12.72 % (3108448)Instruction limit reached!
% 86.95/12.72 % (3108448)------------------------------
% 86.95/12.72 % (3108448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.95/12.72 % (3108448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108448)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108448)Termination reason: Instruction limit
% 86.95/12.72 % (3108448)Termination phase: Saturation
% 86.95/12.72 % (3108448)Time elapsed: 0.272 s
% 86.95/12.72 % (3108448)Peak memory usage: 20 MB
% 86.95/12.72 % (3108448)Instructions burned: 881 (million)
% 86.95/12.72 % (3108452)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1406835154:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 86.95/12.72 % TRYING [20]
% 86.95/12.72 % (3108453)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=685454594:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 86.95/12.72 % TRYING [8]
% 86.95/12.72 % (3108446)Instruction limit reached!
% 86.95/12.72 % (3108446)------------------------------
% 86.95/12.72 % (3108446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.95/12.72 % (3108446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108446)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108446)Termination reason: Instruction limit
% 86.95/12.72 % (3108446)Termination phase: Saturation
% 86.95/12.72 % (3108446)Time elapsed: 0.418 s
% 86.95/12.72 % (3108446)Peak memory usage: 25 MB
% 86.95/12.72 % (3108446)Instructions burned: 693 (million)
% 86.95/12.72 % (3108456)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1095996419:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 86.95/12.72 % TRYING [6]
% 86.95/12.72 % (3108453)Instruction limit reached!
% 86.95/12.72 % (3108453)------------------------------
% 86.95/12.72 % (3108453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.95/12.72 % (3108453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108453)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108453)Termination reason: Instruction limit
% 86.95/12.72 % (3108453)Termination phase: Finite model building constraint generation
% 86.95/12.72 % (3108453)Time elapsed: 0.310 s
% 86.95/12.72 % (3108453)Peak memory usage: 57 MB
% 86.95/12.72 % (3108453)Instructions burned: 923 (million)
% 86.95/12.72 % (3108458)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=455478484:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 86.95/12.72 % TRYING [8]
% 86.95/12.72 % (3108458)Instruction limit reached!
% 86.95/12.72 % (3108458)------------------------------
% 86.95/12.72 % (3108458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.95/12.72 % (3108458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.95/12.72 % (3108458)CaDiCaL version: 2.1.3
% 86.95/12.72 % (3108458)Termination reason: Instruction limit
% 86.95/12.72 % (3108458)Termination phase: Saturation
% 86.95/12.72 % (3108458)Time elapsed: 0.766 s
% 86.95/12.72 % (3108458)Peak memory usage: 31 MB
% 86.95/12.72 % (3108458)Instructions burned: 1474 (million)
% 86.95/12.72 % (3108460)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3524251489:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 51.22/20.64 % (3108460)Cannot represent all propositional literals internally
% 51.22/20.64 % (3108460)Refutation not found, incomplete strategy
% 51.22/20.64 % (3108460)------------------------------
% 51.22/20.64 % (3108460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108460)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108460)Termination reason: Refutation not found, incomplete strategy
% 51.22/20.64 % (3108460)Time elapsed: 0.008 s
% 51.22/20.64 % (3108460)Peak memory usage: 11 MB
% 51.22/20.64 % (3108460)Instructions burned: 15 (million)
% 51.22/20.64 % (3108460)------------------------------
% 51.22/20.64 % (3108460)------------------------------
% 51.22/20.64 % (3108462)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1539144483:fmbsr=2.30978:i=2174_2979 on theBenchmark for (2979ds/2174Mi)
% 51.22/20.64 % TRYING [16]
% 51.22/20.64 % TRYING [7]
% 51.22/20.64 % (3108452)Instruction limit reached!
% 51.22/20.64 % (3108452)------------------------------
% 51.22/20.64 % (3108452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108452)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108452)Termination reason: Instruction limit
% 51.22/20.64 % (3108452)Termination phase: Finite model building constraint generation
% 51.22/20.64 % (3108452)Time elapsed: 1.825 s
% 51.22/20.64 % (3108452)Peak memory usage: 545 MB
% 51.22/20.64 % (3108452)Instructions burned: 9519 (million)
% 51.22/20.64 % (3108464)ott-2_1_sil=16000:newcnf=on:random_seed=4230489750:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 51.22/20.64 % (3108462)Instruction limit reached!
% 51.22/20.64 % (3108462)------------------------------
% 51.22/20.64 % (3108462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108462)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108462)Termination reason: Instruction limit
% 51.22/20.64 % (3108462)Termination phase: Finite model building constraint generation
% 51.22/20.64 % (3108462)Time elapsed: 0.750 s
% 51.22/20.64 % (3108462)Peak memory usage: 136 MB
% 51.22/20.64 % (3108462)Instructions burned: 2176 (million)
% 51.22/20.64 % (3108466)ott+10_1_sil=32000:tgt=ground:random_seed=1783293907:i=5114:av=off_2971 on theBenchmark for (2971ds/5114Mi)
% 51.22/20.64 % (3108464)Instruction limit reached!
% 51.22/20.64 % (3108464)------------------------------
% 51.22/20.64 % (3108464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108464)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108464)Termination reason: Instruction limit
% 51.22/20.64 % (3108464)Termination phase: Saturation
% 51.22/20.64 % (3108464)Time elapsed: 0.257 s
% 51.22/20.64 % (3108464)Peak memory usage: 24 MB
% 51.22/20.64 % (3108464)Instructions burned: 870 (million)
% 51.22/20.64 % (3108468)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3681598934:i=54282_2969 on theBenchmark for (2969ds/54282Mi)
% 51.22/20.64 % TRYING [1]
% 51.22/20.64 % TRYING [2]
% 51.22/20.64 % TRYING [3]
% 51.22/20.64 % TRYING [4]
% 51.22/20.64 % TRYING [5]
% 51.22/20.64 % TRYING [6]
% 51.22/20.64 % TRYING [7]
% 51.22/20.64 % (3108456)Instruction limit reached!
% 51.22/20.64 % (3108456)------------------------------
% 51.22/20.64 % (3108456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108456)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108456)Termination reason: Instruction limit
% 51.22/20.64 % (3108456)Termination phase: Saturation
% 51.22/20.64 % (3108456)Time elapsed: 2.570 s
% 51.22/20.64 % (3108456)Peak memory usage: 37 MB
% 51.22/20.64 % (3108456)Instructions burned: 5132 (million)
% 51.22/20.64 % (3108470)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=866420162:i=3512:aac=none_2964 on theBenchmark for (2964ds/3512Mi)
% 51.22/20.64 % TRYING [9]
% 51.22/20.64 % TRYING [8]
% 51.22/20.64 % TRYING [8]
% 51.22/20.64 % TRYING [9]
% 51.22/20.64 % (3108470)Instruction limit reached!
% 51.22/20.64 % (3108470)------------------------------
% 51.22/20.64 % (3108470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108470)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108470)Termination reason: Instruction limit
% 51.22/20.64 % (3108470)Termination phase: Saturation
% 51.22/20.64 % (3108470)Time elapsed: 1.713 s
% 51.22/20.64 % (3108470)Peak memory usage: 33 MB
% 51.22/20.64 % (3108470)Instructions burned: 3512 (million)
% 51.22/20.64 % (3108472)dis+21_1_sil=32000:sas=cadical:random_seed=1430310011:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi)
% 51.22/20.64 % (3108466)Instruction limit reached!
% 51.22/20.64 % (3108466)------------------------------
% 51.22/20.64 % (3108466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108466)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108466)Termination reason: Instruction limit
% 51.22/20.64 % (3108466)Termination phase: Saturation
% 51.22/20.64 % (3108466)Time elapsed: 2.873 s
% 51.22/20.64 % (3108466)Peak memory usage: 83 MB
% 51.22/20.64 % (3108466)Instructions burned: 5114 (million)
% 51.22/20.64 % (3108474)ott+11_1_sil=16000:gs=on:random_seed=1561572246:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 51.22/20.64 % (3108474)Instruction limit reached!
% 51.22/20.64 % (3108474)------------------------------
% 51.22/20.64 % (3108474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108474)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108474)Termination reason: Instruction limit
% 51.22/20.64 % (3108474)Termination phase: Saturation
% 51.22/20.64 % (3108474)Time elapsed: 0.892 s
% 51.22/20.64 % (3108474)Peak memory usage: 14 MB
% 51.22/20.64 % (3108474)Instructions burned: 2252 (million)
% 51.22/20.64 % (3108476)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2475427463:fmbsr=1.6:i=67534_2933 on theBenchmark for (2933ds/67534Mi)
% 51.22/20.64 % TRYING [7]
% 51.22/20.64 % (3108472)Instruction limit reached!
% 51.22/20.64 % (3108472)------------------------------
% 51.22/20.64 % (3108472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108472)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108472)Termination reason: Instruction limit
% 51.22/20.64 % (3108472)Termination phase: Saturation
% 51.22/20.64 % (3108472)Time elapsed: 1.958 s
% 51.22/20.64 % (3108472)Peak memory usage: 52 MB
% 51.22/20.64 % (3108472)Instructions burned: 3774 (million)
% 51.22/20.64 % (3108478)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3176299963:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 51.22/20.64 % TRYING [10]
% 51.22/20.64 % TRYING [10]
% 51.22/20.64 % (3108478)Instruction limit reached!
% 51.22/20.64 % (3108478)------------------------------
% 51.22/20.64 % (3108478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108478)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108478)Termination reason: Instruction limit
% 51.22/20.64 % (3108478)Termination phase: Saturation
% 51.22/20.64 % (3108478)Time elapsed: 2.040 s
% 51.22/20.64 % (3108478)Peak memory usage: 44 MB
% 51.22/20.64 % (3108478)Instructions burned: 4593 (million)
% 51.22/20.64 % (3108480)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4197847590:i=29340_2906 on theBenchmark for (2906ds/29340Mi)
% 51.22/20.64 % (3108449)Instruction limit reached!
% 51.22/20.64 % (3108449)------------------------------
% 51.22/20.64 % (3108449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108449)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108449)Termination reason: Instruction limit
% 51.22/20.64 % (3108449)Termination phase: Finite model building SAT solving
% 51.22/20.64 % (3108449)Time elapsed: 8.995 s
% 51.22/20.64 % (3108449)Peak memory usage: 175 MB
% 51.22/20.64 % (3108449)Instructions burned: 22061 (million)
% 51.22/20.64 % (3108482)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3192131132:i=5211_2903 on theBenchmark for (2903ds/5211Mi)
% 51.22/20.64 % TRYING [8]
% 51.22/20.64 % TRYING [11]
% 51.22/20.64 % (3108482)Instruction limit reached!
% 51.22/20.64 % (3108482)------------------------------
% 51.22/20.64 % (3108482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108482)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108482)Termination reason: Instruction limit
% 51.22/20.64 % (3108482)Termination phase: Saturation
% 51.22/20.64 % (3108482)Time elapsed: 2.620 s
% 51.22/20.64 % (3108482)Peak memory usage: 53 MB
% 51.22/20.64 % (3108482)Instructions burned: 5212 (million)
% 51.22/20.64 % (3108484)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4265500805:i=5497:nm=2_2877 on theBenchmark for (2877ds/5497Mi)
% 51.22/20.64 % TRYING [17]
% 51.22/20.64 % (3108484)Instruction limit reached!
% 51.22/20.64 % (3108484)------------------------------
% 51.22/20.64 % (3108484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108484)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108484)Termination reason: Instruction limit
% 51.22/20.64 % (3108484)Termination phase: Finite model building constraint generation
% 51.22/20.64 % (3108484)Time elapsed: 1.905 s
% 51.22/20.64 % (3108484)Peak memory usage: 343 MB
% 51.22/20.64 % (3108484)Instructions burned: 5498 (million)
% 51.22/20.64 % (3108486)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1201038344:fmbsr=2:i=46332_2857 on theBenchmark for (2857ds/46332Mi)
% 51.22/20.64 % TRYING [15]
% 51.22/20.64 % TRYING [11]
% 51.22/20.64 % (3108468)Instruction limit reached!
% 51.22/20.64 % (3108468)------------------------------
% 51.22/20.64 % (3108468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108468)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108468)Termination reason: Instruction limit
% 51.22/20.64 % (3108468)Termination phase: Finite model building constraint generation
% 51.22/20.64 % (3108468)Time elapsed: 12.507 s
% 51.22/20.64 % (3108468)Peak memory usage: 1018 MB
% 51.22/20.64 % (3108468)Instructions burned: 54287 (million)
% 51.22/20.64 % (3108488)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1242415369:i=14071_2843 on theBenchmark for (2843ds/14071Mi)
% 51.22/20.64 % TRYING [12]
% 51.22/20.64 % (3108488)Instruction limit reached!
% 51.22/20.64 % (3108488)------------------------------
% 51.22/20.64 % (3108488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108488)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108488)Termination reason: Instruction limit
% 51.22/20.64 % (3108488)Termination phase: Finite model building constraint generation
% 51.22/20.64 % (3108488)Time elapsed: 3.382 s
% 51.22/20.64 % (3108488)Peak memory usage: 915 MB
% 51.22/20.64 % (3108488)Instructions burned: 14073 (million)
% 51.22/20.64 % (3108490)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1088208428:i=22565:add=on:rawr=on_2809 on theBenchmark for (2809ds/22565Mi)
% 51.22/20.64 % (3108490) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3108411-3108490"...
% 51.22/20.64 % (3108490)...printing done.
% 51.22/20.64 % (3108490)Refutation found. Thanks to Tanya!
% 51.22/20.64 % SZS status Theorem for theBenchmark
% 51.22/20.64 % SZS output start Proof for theBenchmark
% See solution above
% 51.22/20.64 % (3108490)------------------------------
% 51.22/20.64 % (3108490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.22/20.64 % (3108490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.22/20.64 % (3108490)CaDiCaL version: 2.1.3
% 51.22/20.64 % (3108490)Termination reason: Refutation
% 51.22/20.64 % (3108490)Time elapsed: 0.956 s
% 51.22/20.64 % (3108490)Peak memory usage: 38 MB
% 51.22/20.64 % (3108490)Instructions burned: 2823 (million)
% 51.22/20.64 % (3108411)Success in time 20.213 s
% 51.22/20.64 % Vampire exiting
%------------------------------------------------------------------------------