%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : RNG126+4 : 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 : n019.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 8.42s 1.97s
% Output : Refutation 8.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 89 ( 23 unt; 5 def)
% Number of atoms : 302 ( 58 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 314 ( 101 ~; 84 |; 88 &)
% ( 24 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 6 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-2 aty)
% Number of variables : 112 ( 0 sgn 71 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> aElement0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
fof(f6,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> aElement0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
fof(f11,axiom,
! [X0,X1] :
( ( aElement0(X0)
& aElement0(X1) )
=> sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulComm) ).
fof(f39,axiom,
( aElement0(xa)
& aElement0(xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2091) ).
fof(f42,axiom,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X1] :
( aElement0(X1)
=> aElementOf0(sdtasdt0(X1,X0),xI) ) ) )
& aIdeal0(xI)
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xb))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xb,X1) = X0 ) )
& ! [X0] :
( aElementOf0(X0,xI)
<=> ? [X1,X2] :
( aElementOf0(X1,slsdtgt0(xa))
& aElementOf0(X2,slsdtgt0(xb))
& sdtpldt0(X1,X2) = X0 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2174) ).
fof(f45,axiom,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X0] :
( ( ( ? [X1,X2] :
( aElementOf0(X1,slsdtgt0(xa))
& aElementOf0(X2,slsdtgt0(xb))
& sdtpldt0(X1,X2) = X0 )
| aElementOf0(X0,xI) )
& X0 != sz00 )
=> ~ iLess0(sbrdtbr0(X0),sbrdtbr0(xu)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2273) ).
fof(f47,axiom,
? [X0] :
( aElement0(X0)
& sdtasdt0(xu,X0) = xc ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2744) ).
fof(f48,conjecture,
( ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) )
=> ( ! [X0] :
( aElementOf0(X0,slsdtgt0(xb))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xb,X1) = X0 ) )
=> ( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xc )
| aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f49,negated_conjecture,
~ ( ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) )
=> ( ! [X0] :
( aElementOf0(X0,slsdtgt0(xb))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xb,X1) = X0 ) )
=> ( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xc )
| aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f54,plain,
( aSet0(xI)
& ! [X0] :
( aElementOf0(X0,xI)
=> ( ! [X1] :
( aElementOf0(X1,xI)
=> aElementOf0(sdtpldt0(X0,X1),xI) )
& ! [X2] :
( aElement0(X2)
=> aElementOf0(sdtasdt0(X2,X0),xI) ) ) )
& aIdeal0(xI)
& ! [X3] :
( aElementOf0(X3,slsdtgt0(xa))
<=> ? [X4] :
( aElement0(X4)
& sdtasdt0(xa,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,slsdtgt0(xb))
<=> ? [X6] :
( aElement0(X6)
& sdtasdt0(xb,X6) = X5 ) )
& ! [X7] :
( aElementOf0(X7,xI)
<=> ? [X8,X9] :
( aElementOf0(X8,slsdtgt0(xa))
& aElementOf0(X9,slsdtgt0(xb))
& sdtpldt0(X8,X9) = X7 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(rectify,[],[f42]) ).
fof(f57,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ( ( ? [X3,X4] :
( aElementOf0(X3,slsdtgt0(xa))
& aElementOf0(X4,slsdtgt0(xb))
& sdtpldt0(X3,X4) = X2 )
| aElementOf0(X2,xI) )
& sz00 != X2 )
=> ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu)) ) ),
inference(rectify,[],[f45]) ).
fof(f59,plain,
~ ( ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) )
=> ( ! [X2] :
( aElementOf0(X2,slsdtgt0(xb))
<=> ? [X3] :
( aElement0(X3)
& sdtasdt0(xb,X3) = X2 ) )
=> ( ? [X4,X5] :
( aElementOf0(X4,slsdtgt0(xa))
& aElementOf0(X5,slsdtgt0(xb))
& sdtpldt0(X4,X5) = xc )
| aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) ) ) ),
inference(rectify,[],[f49]) ).
fof(f62,plain,
! [X0,X1] :
( aElement0(sdtpldt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f5]) ).
fof(f63,plain,
! [X0,X1] :
( aElement0(sdtpldt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f6]) ).
fof(f65,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f64]) ).
fof(f72,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f73,plain,
! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(flattening,[],[f72]) ).
fof(f118,plain,
( aSet0(xI)
& ! [X0] :
( ( ! [X1] :
( aElementOf0(sdtpldt0(X0,X1),xI)
| ~ aElementOf0(X1,xI) )
& ! [X2] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2) ) )
| ~ aElementOf0(X0,xI) )
& aIdeal0(xI)
& ! [X3] :
( aElementOf0(X3,slsdtgt0(xa))
<=> ? [X4] :
( aElement0(X4)
& sdtasdt0(xa,X4) = X3 ) )
& ! [X5] :
( aElementOf0(X5,slsdtgt0(xb))
<=> ? [X6] :
( aElement0(X6)
& sdtasdt0(xb,X6) = X5 ) )
& ! [X7] :
( aElementOf0(X7,xI)
<=> ? [X8,X9] :
( aElementOf0(X8,slsdtgt0(xa))
& aElementOf0(X9,slsdtgt0(xb))
& sdtpldt0(X8,X9) = X7 ) )
& xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)) ),
inference(ennf_transformation,[],[f54]) ).
fof(f119,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu))
| ( ! [X3,X4] :
( ~ aElementOf0(X3,slsdtgt0(xa))
| ~ aElementOf0(X4,slsdtgt0(xb))
| sdtpldt0(X3,X4) != X2 )
& ~ aElementOf0(X2,xI) )
| sz00 = X2 ) ),
inference(ennf_transformation,[],[f57]) ).
fof(f120,plain,
( ? [X0,X1] :
( aElementOf0(X0,slsdtgt0(xa))
& aElementOf0(X1,slsdtgt0(xb))
& sdtpldt0(X0,X1) = xu )
& aElementOf0(xu,xI)
& xu != sz00
& ! [X2] :
( ~ iLess0(sbrdtbr0(X2),sbrdtbr0(xu))
| ( ! [X3,X4] :
( ~ aElementOf0(X3,slsdtgt0(xa))
| ~ aElementOf0(X4,slsdtgt0(xb))
| sdtpldt0(X3,X4) != X2 )
& ~ aElementOf0(X2,xI) )
| sz00 = X2 ) ),
inference(flattening,[],[f119]) ).
fof(f121,plain,
( ! [X4,X5] :
( ~ aElementOf0(X4,slsdtgt0(xa))
| ~ aElementOf0(X5,slsdtgt0(xb))
| sdtpldt0(X4,X5) != xc )
& ~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ! [X2] :
( aElementOf0(X2,slsdtgt0(xb))
<=> ? [X3] :
( aElement0(X3)
& sdtasdt0(xb,X3) = X2 ) )
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) ) ),
inference(ennf_transformation,[],[f59]) ).
fof(f122,plain,
( ! [X4,X5] :
( ~ aElementOf0(X4,slsdtgt0(xa))
| ~ aElementOf0(X5,slsdtgt0(xb))
| sdtpldt0(X4,X5) != xc )
& ~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)))
& ! [X2] :
( aElementOf0(X2,slsdtgt0(xb))
<=> ? [X3] :
( aElement0(X3)
& sdtasdt0(xb,X3) = X2 ) )
& ! [X0] :
( aElementOf0(X0,slsdtgt0(xa))
<=> ? [X1] :
( aElement0(X1)
& sdtasdt0(xa,X1) = X0 ) ) ),
inference(flattening,[],[f121]) ).
fof(f126,plain,
! [X0,X1] :
( aElement0(sdtpldt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f63]) ).
fof(f127,plain,
! [X0,X1] :
( aElement0(sdtasdt0(X0,X1))
| ~ aElement0(X0)
| ~ aElement0(X1) ),
inference(cnf_transformation,[],[f65]) ).
fof(f134,plain,
! [X0,X1] :
( ~ aElement0(X1)
| ~ aElement0(X0)
| sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ),
inference(cnf_transformation,[],[f73]) ).
fof(f212,plain,
aElement0(xb),
inference(cnf_transformation,[],[f39]) ).
fof(f213,plain,
aElement0(xa),
inference(cnf_transformation,[],[f39]) ).
fof(f247,plain,
! [X2,X0] :
( aElementOf0(sdtasdt0(X2,X0),xI)
| ~ aElement0(X2)
| ~ aElementOf0(X0,xI) ),
inference(cnf_transformation,[],[f118]) ).
fof(f258,plain,
xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)),
inference(cnf_transformation,[],[f118]) ).
fof(f286,plain,
xu = sdtpldt0(sK37,sK38),
inference(cnf_transformation,[],[f120]) ).
fof(f287,plain,
aElementOf0(sK38,slsdtgt0(xb)),
inference(cnf_transformation,[],[f120]) ).
fof(f288,plain,
aElementOf0(sK37,slsdtgt0(xa)),
inference(cnf_transformation,[],[f120]) ).
fof(f290,plain,
aElementOf0(xu,xI),
inference(cnf_transformation,[],[f120]) ).
fof(f299,plain,
xc = sdtasdt0(xu,sK41),
inference(cnf_transformation,[],[f47]) ).
fof(f300,plain,
aElement0(sK41),
inference(cnf_transformation,[],[f47]) ).
fof(f301,plain,
! [X2] :
( ~ aElementOf0(X2,slsdtgt0(xb))
| sdtasdt0(xb,sK43(X2)) = X2 ),
inference(cnf_transformation,[],[f122]) ).
fof(f302,plain,
! [X2] :
( aElement0(sK43(X2))
| ~ aElementOf0(X2,slsdtgt0(xb)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f304,plain,
! [X0] :
( ~ aElementOf0(X0,slsdtgt0(xa))
| sdtasdt0(xa,sK42(X0)) = X0 ),
inference(cnf_transformation,[],[f122]) ).
fof(f305,plain,
! [X0] :
( aElement0(sK42(X0))
| ~ aElementOf0(X0,slsdtgt0(xa)) ),
inference(cnf_transformation,[],[f122]) ).
fof(f308,plain,
~ aElementOf0(xc,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))),
inference(cnf_transformation,[],[f122]) ).
fof(f426,plain,
sK38 = sdtasdt0(xb,sK43(sK38)),
inference(resolution,[],[f287,f301]) ).
fof(f428,plain,
sK37 = sdtasdt0(xa,sK42(sK37)),
inference(resolution,[],[f288,f304]) ).
fof(f510,plain,
~ aElementOf0(xc,xI),
inference(superposition,[],[f308,f258]) ).
fof(f733,plain,
( aElement0(xu)
| ~ aElement0(sK37)
| ~ aElement0(sK38) ),
inference(superposition,[],[f126,f286]) ).
fof(f758,plain,
( aElement0(sK37)
| ~ aElement0(xa)
| ~ aElement0(sK42(sK37)) ),
inference(superposition,[],[f127,f428]) ).
fof(f776,plain,
( aElement0(sK38)
| ~ aElement0(xb)
| ~ aElement0(sK43(sK38)) ),
inference(superposition,[],[f127,f426]) ).
fof(f784,plain,
( aElement0(sK38)
| ~ aElement0(sK43(sK38)) ),
inference(forward_subsumption_resolution,[],[f776,f212]) ).
fof(f800,plain,
( aElement0(sK37)
| ~ aElement0(sK42(sK37)) ),
inference(forward_subsumption_resolution,[],[f758,f213]) ).
fof(f949,definition,
( spl44_17
<=> aElement0(sK43(sK38)) ),
introduced(definition,[new_symbols(definition,[spl44_17])],[avatar_definition]) ).
fof(f951,plain,
( ~ aElement0(sK43(sK38))
| spl44_17 ),
inference(avatar_component_clause,[],[f949]) ).
fof(f953,definition,
( spl44_18
<=> aElement0(sK38) ),
introduced(definition,[new_symbols(definition,[spl44_18])],[avatar_definition]) ).
fof(f955,plain,
( aElement0(sK38)
| ~ spl44_18 ),
inference(avatar_component_clause,[],[f953]) ).
fof(f956,plain,
( ~ spl44_17
| spl44_18 ),
inference(avatar_split_clause,[],[f784,f953,f949]) ).
fof(f958,plain,
( ~ aElementOf0(sK38,slsdtgt0(xb))
| spl44_17 ),
inference(resolution,[],[f951,f302]) ).
fof(f962,plain,
( $false
| spl44_17 ),
inference(forward_subsumption_resolution,[],[f958,f287]) ).
fof(f963,plain,
spl44_17,
inference(avatar_contradiction_clause,[],[f962]) ).
fof(f1116,definition,
( spl44_21
<=> aElement0(sK42(sK37)) ),
introduced(definition,[new_symbols(definition,[spl44_21])],[avatar_definition]) ).
fof(f1118,plain,
( ~ aElement0(sK42(sK37))
| spl44_21 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1120,definition,
( spl44_22
<=> aElement0(sK37) ),
introduced(definition,[new_symbols(definition,[spl44_22])],[avatar_definition]) ).
fof(f1122,plain,
( aElement0(sK37)
| ~ spl44_22 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1123,plain,
( ~ spl44_21
| spl44_22 ),
inference(avatar_split_clause,[],[f800,f1120,f1116]) ).
fof(f1207,plain,
( ~ aElementOf0(sK37,slsdtgt0(xa))
| spl44_21 ),
inference(resolution,[],[f1118,f305]) ).
fof(f1211,plain,
( $false
| spl44_21 ),
inference(forward_subsumption_resolution,[],[f1207,f288]) ).
fof(f1212,plain,
spl44_21,
inference(avatar_contradiction_clause,[],[f1211]) ).
fof(f1262,definition,
( spl44_24
<=> aElement0(xu) ),
introduced(definition,[new_symbols(definition,[spl44_24])],[avatar_definition]) ).
fof(f1263,plain,
( aElement0(xu)
| ~ spl44_24 ),
inference(avatar_component_clause,[],[f1262]) ).
fof(f1577,plain,
! [X0] :
( ~ aElement0(X0)
| sdtasdt0(X0,sK41) = sdtasdt0(sK41,X0) ),
inference(resolution,[],[f134,f300]) ).
fof(f15337,plain,
( aElement0(xu)
| ~ aElement0(sK38)
| ~ spl44_22 ),
inference(forward_subsumption_resolution,[],[f733,f1122]) ).
fof(f15338,plain,
( aElement0(xu)
| ~ spl44_18
| ~ spl44_22 ),
inference(forward_subsumption_resolution,[],[f15337,f955]) ).
fof(f15339,plain,
( spl44_24
| ~ spl44_18
| ~ spl44_22 ),
inference(avatar_split_clause,[],[f15338,f1120,f953,f1262]) ).
fof(f22130,plain,
( sdtasdt0(xu,sK41) = sdtasdt0(sK41,xu)
| ~ spl44_24 ),
inference(resolution,[],[f1577,f1263]) ).
fof(f22183,plain,
( xc = sdtasdt0(sK41,xu)
| ~ spl44_24 ),
inference(forward_demodulation,[],[f22130,f299]) ).
fof(f22263,plain,
( aElementOf0(xc,xI)
| ~ aElement0(sK41)
| ~ aElementOf0(xu,xI)
| ~ spl44_24 ),
inference(superposition,[],[f247,f22183]) ).
fof(f22268,plain,
( ~ aElement0(sK41)
| ~ aElementOf0(xu,xI)
| ~ spl44_24 ),
inference(forward_subsumption_resolution,[],[f22263,f510]) ).
fof(f22272,plain,
( ~ aElementOf0(xu,xI)
| ~ spl44_24 ),
inference(forward_subsumption_resolution,[],[f22268,f300]) ).
fof(f22273,plain,
( $false
| ~ spl44_24 ),
inference(forward_subsumption_resolution,[],[f22272,f290]) ).
fof(f22274,plain,
~ spl44_24,
inference(avatar_contradiction_clause,[],[f22273]) ).
cnf(s23,plain,
( ~ spl44_17
| spl44_18 ),
inference(sat_conversion,[],[f956]) ).
cnf(s24,plain,
spl44_17,
inference(sat_conversion,[],[f963]) ).
cnf(s27,plain,
( ~ spl44_21
| spl44_22 ),
inference(sat_conversion,[],[f1123]) ).
cnf(s28,plain,
spl44_21,
inference(sat_conversion,[],[f1212]) ).
cnf(s56,plain,
( ~ spl44_18
| ~ spl44_22
| spl44_24 ),
inference(sat_conversion,[],[f15339]) ).
cnf(s83,plain,
~ spl44_24,
inference(sat_conversion,[],[f22274]) ).
cnf(s85,plain,
( ~ spl44_18
| ~ spl44_22 ),
inference(rat,[],[s56,s83]) ).
cnf(s93,plain,
spl44_22,
inference(rat,[],[s27,s28]) ).
cnf(s94,plain,
~ spl44_18,
inference(rat,[],[s85,s93]) ).
cnf(s96,plain,
$false,
inference(rat,[],[s23,s94,s24]) ).
fof(f22275,plain,
$false,
inference(avatar_sat_refutation,[],[s96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG126+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n019.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 23:23:34 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 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
% 8.42/1.97 % (3521152)Will run a generic schedule for satisfiability detection.
% 8.42/1.97 % (3521162)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=978932624:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.42/1.97 % (3521158)% WARNING: option uhcvi not known.
% 8.42/1.97 % (3521161)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3428128109:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.42/1.97 % (3521157)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3967139904_2999 on theBenchmark for (2999ds/0Mi)
% 8.42/1.97 % (3521158)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4254355585:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.42/1.97 % (3521159)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2601527747:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.42/1.97 % (3521160)dis+10_1_sil=32000:sp=arity:random_seed=183177543:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.42/1.97 % (3521163)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1777486829:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.42/1.97 % TRYING [1]
% 8.42/1.97 % TRYING [2]
% 8.42/1.97 % TRYING [3]
% 8.42/1.97 % (3521162)Instruction limit reached!
% 8.42/1.97 % (3521162)------------------------------
% 8.42/1.97 % (3521162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521162)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521162)Termination reason: Instruction limit
% 8.42/1.97 % (3521162)Termination phase: Saturation
% 8.42/1.97 % (3521162)Time elapsed: 0.039 s
% 8.42/1.97 % (3521162)Peak memory usage: 14 MB
% 8.42/1.97 % (3521162)Instructions burned: 133 (million)
% 8.42/1.97 % TRYING [4]
% 8.42/1.97 % (3521171)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1925688592:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 8.42/1.97 % TRYING [1]
% 8.42/1.97 % TRYING [2]
% 8.42/1.97 % TRYING [3]
% 8.42/1.97 % (3521160)Instruction limit reached!
% 8.42/1.97 % (3521160)------------------------------
% 8.42/1.97 % (3521160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521160)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521160)Termination reason: Instruction limit
% 8.42/1.97 % (3521160)Termination phase: Saturation
% 8.42/1.97 % (3521160)Time elapsed: 0.062 s
% 8.42/1.97 % (3521160)Peak memory usage: 13 MB
% 8.42/1.97 % (3521160)Instructions burned: 104 (million)
% 8.42/1.97 % TRYING [4]
% 8.42/1.97 % (3521161)Instruction limit reached!
% 8.42/1.97 % (3521161)------------------------------
% 8.42/1.97 % (3521161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521161)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521161)Termination reason: Instruction limit
% 8.42/1.97 % (3521161)Termination phase: Saturation
% 8.42/1.97 % (3521161)Time elapsed: 0.067 s
% 8.42/1.97 % (3521161)Peak memory usage: 14 MB
% 8.42/1.97 % (3521161)Instructions burned: 116 (million)
% 8.42/1.97 % (3521173)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4086293376:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 8.42/1.97 % (3521174)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=1198835158:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.42/1.97 % (3521163)Instruction limit reached!
% 8.42/1.97 % (3521163)------------------------------
% 8.42/1.97 % (3521163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521163)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521163)Termination reason: Instruction limit
% 8.42/1.97 % (3521163)Termination phase: Saturation
% 8.42/1.97 % (3521163)Time elapsed: 0.102 s
% 8.42/1.97 % (3521163)Peak memory usage: 14 MB
% 8.42/1.97 % (3521163)Instructions burned: 160 (million)
% 8.42/1.97 % TRYING [5]
% 8.42/1.97 % TRYING [5]
% 8.42/1.97 % (3521177)ott-21_1_sil=16000:fs=off:random_seed=2087952369:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.42/1.97 % (3521173)Instruction limit reached!
% 8.42/1.97 % (3521173)------------------------------
% 8.42/1.97 % (3521173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521173)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521173)Termination reason: Instruction limit
% 8.42/1.97 % (3521173)Termination phase: Saturation
% 8.42/1.97 % (3521173)Time elapsed: 0.074 s
% 8.42/1.97 % (3521173)Peak memory usage: 14 MB
% 8.42/1.97 % (3521173)Instructions burned: 131 (million)
% 8.42/1.97 % (3521179)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2567563759:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.42/1.97 % (3521171)Instruction limit reached!
% 8.42/1.97 % (3521171)------------------------------
% 8.42/1.97 % (3521171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521171)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521171)Termination reason: Instruction limit
% 8.42/1.97 % (3521171)Termination phase: Finite model building SAT solving
% 8.42/1.97 % (3521171)Time elapsed: 0.165 s
% 8.42/1.97 % (3521171)Peak memory usage: 33 MB
% 8.42/1.97 % (3521171)Instructions burned: 715 (million)
% 8.42/1.97 % (3521177)Instruction limit reached!
% 8.42/1.97 % (3521177)------------------------------
% 8.42/1.97 % (3521177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521177)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521177)Termination reason: Instruction limit
% 8.42/1.97 % (3521177)Termination phase: Saturation
% 8.42/1.97 % (3521177)Time elapsed: 0.093 s
% 8.42/1.97 % (3521177)Peak memory usage: 13 MB
% 8.42/1.97 % (3521177)Instructions burned: 181 (million)
% 8.42/1.97 % (3521181)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3898699824:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.42/1.97 % TRYING [1]
% 8.42/1.97 % TRYING [2]
% 8.42/1.97 % TRYING [3]
% 8.42/1.97 % (3521182)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3883353836:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.42/1.97 % TRYING [4]
% 8.42/1.97 % TRYING [6]
% 8.42/1.97 % TRYING [5]
% 8.42/1.97 % (3521181)Instruction limit reached!
% 8.42/1.97 % (3521181)------------------------------
% 8.42/1.97 % (3521181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521181)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521181)Termination reason: Instruction limit
% 8.42/1.97 % (3521181)Termination phase: Finite model building constraint generation
% 8.42/1.97 % (3521181)Time elapsed: 0.183 s
% 8.42/1.97 % (3521181)Peak memory usage: 22 MB
% 8.42/1.97 % (3521181)Instructions burned: 867 (million)
% 8.42/1.97 % (3521174)Instruction limit reached!
% 8.42/1.97 % (3521174)------------------------------
% 8.42/1.97 % (3521174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521174)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521174)Termination reason: Instruction limit
% 8.42/1.97 % (3521174)Termination phase: Saturation
% 8.42/1.97 % (3521174)Time elapsed: 0.321 s
% 8.42/1.97 % (3521174)Peak memory usage: 17 MB
% 8.42/1.97 % (3521174)Instructions burned: 685 (million)
% 8.42/1.97 % (3521185)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4032561971:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 8.42/1.97 % (3521186)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=1318833083:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 8.42/1.97 % (3521179)Instruction limit reached!
% 8.42/1.97 % (3521179)------------------------------
% 8.42/1.97 % (3521179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521179)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521179)Termination reason: Instruction limit
% 8.42/1.97 % (3521179)Termination phase: Saturation
% 8.42/1.97 % (3521179)Time elapsed: 0.302 s
% 8.42/1.97 % (3521179)Peak memory usage: 16 MB
% 8.42/1.97 % (3521179)Instructions burned: 477 (million)
% 8.42/1.97 % (3521189)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2212006956:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 8.42/1.97 % (3521185)Instruction limit reached!
% 8.42/1.97 % (3521185)------------------------------
% 8.42/1.97 % (3521185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521185)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521185)Termination reason: Instruction limit
% 8.42/1.97 % (3521185)Termination phase: Finite model building constraint generation
% 8.42/1.97 % (3521185)Time elapsed: 0.231 s
% 8.42/1.97 % (3521185)Peak memory usage: 107 MB
% 8.42/1.97 % (3521185)Instructions burned: 890 (million)
% 8.42/1.97 % (3521191)fmb+10_1_sil=64000:random_seed=2811442680:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 8.42/1.97 % TRYING [1]
% 8.42/1.97 % TRYING [2]
% 8.42/1.97 % TRYING [3]
% 8.42/1.97 % TRYING [4]
% 8.42/1.97 % TRYING [7]
% 8.42/1.97 % TRYING [5]
% 8.42/1.97 % (3521186)Instruction limit reached!
% 8.42/1.97 % (3521186)------------------------------
% 8.42/1.97 % (3521186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521186)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521186)Termination reason: Instruction limit
% 8.42/1.97 % (3521186)Termination phase: Saturation
% 8.42/1.97 % (3521186)Time elapsed: 0.371 s
% 8.42/1.97 % (3521186)Peak memory usage: 20 MB
% 8.42/1.97 % (3521186)Instructions burned: 693 (million)
% 8.42/1.97 % (3521193)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=544814800:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 8.42/1.97 % TRYING [20]
% 8.42/1.97 % (3521182)Instruction limit reached!
% 8.42/1.97 % (3521182)------------------------------
% 8.42/1.97 % (3521182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521182)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521182)Termination reason: Instruction limit
% 8.42/1.97 % (3521182)Termination phase: Saturation
% 8.42/1.97 % (3521182)Time elapsed: 0.672 s
% 8.42/1.97 % (3521182)Peak memory usage: 27 MB
% 8.42/1.97 % (3521182)Instructions burned: 1180 (million)
% 8.42/1.97 % (3521195)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=67481966:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 8.42/1.97 % TRYING [8]
% 8.42/1.97 % TRYING [6]
% 8.42/1.97 % (3521189)Instruction limit reached!
% 8.42/1.97 % (3521189)------------------------------
% 8.42/1.97 % (3521189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521189)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521189)Termination reason: Instruction limit
% 8.42/1.97 % (3521189)Termination phase: Saturation
% 8.42/1.97 % (3521189)Time elapsed: 0.487 s
% 8.42/1.97 % (3521189)Peak memory usage: 20 MB
% 8.42/1.97 % (3521189)Instructions burned: 879 (million)
% 8.42/1.97 % (3521197)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3041721407:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 8.42/1.97 % (3521195)Instruction limit reached!
% 8.42/1.97 % (3521195)------------------------------
% 8.42/1.97 % (3521195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521195)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521195)Termination reason: Instruction limit
% 8.42/1.97 % (3521195)Termination phase: Finite model building constraint generation
% 8.42/1.97 % (3521195)Time elapsed: 0.308 s
% 8.42/1.97 % (3521195)Peak memory usage: 57 MB
% 8.42/1.97 % (3521195)Instructions burned: 923 (million)
% 8.42/1.97 % (3521199)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3018775851:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 8.42/1.97 % (3521197) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3521152-3521197"...
% 8.42/1.97 % (3521197)...printing done.
% 8.42/1.97 % (3521197)Refutation found. Thanks to Tanya!
% 8.42/1.97 % SZS status Theorem for theBenchmark
% 8.42/1.97 % SZS output start Proof for theBenchmark
% See solution above
% 8.42/1.97 % (3521197)------------------------------
% 8.42/1.97 % (3521197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.42/1.97 % (3521197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.42/1.97 % (3521197)CaDiCaL version: 2.1.3
% 8.42/1.97 % (3521197)Termination reason: Refutation
% 8.42/1.97 % (3521197)Time elapsed: 0.492 s
% 8.42/1.97 % (3521197)Peak memory usage: 20 MB
% 8.42/1.97 % (3521197)Instructions burned: 920 (million)
% 8.42/1.97 % (3521152)Success in time 1.561 s
% 8.42/1.97 % Vampire exiting
%------------------------------------------------------------------------------