%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM454+1 : 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:22 PM UTC 2026
% Result : Theorem 34.54s 5.37s
% Output : Refutation 34.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 18
% Syntax : Number of formulae : 125 ( 63 unt; 4 def)
% Number of atoms : 243 ( 142 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 205 ( 87 ~; 84 |; 23 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 79 ( 79 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
aInteger0(sz10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntOne) ).
fof(f4,axiom,
! [X0] :
( aInteger0(X0)
=> aInteger0(smndt0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mIntNeg) ).
fof(f7,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddAsso) ).
fof(f8,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddComm) ).
fof(f9,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddZero) ).
fof(f10,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddNeg) ).
fof(f13,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulOne) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aInteger0(X0)
& aInteger0(X1)
& aInteger0(X2) )
=> ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDistrib) ).
fof(f15,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulZero) ).
fof(f16,axiom,
! [X0] :
( aInteger0(X0)
=> ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMulMinOne) ).
fof(f17,axiom,
! [X0,X1] :
( ( aInteger0(X0)
& aInteger0(X1) )
=> ( sdtasdt0(X0,X1) = sz00
=> ( X0 = sz00
| X1 = sz00 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mZeroDiv) ).
fof(f46,axiom,
( aInteger0(xp)
& xp != sz00
& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2171) ).
fof(f48,axiom,
( sdtpldt0(sz10,xp) != sz10
& sdtpldt0(sz10,smndt0(xp)) != sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2258) ).
fof(f49,conjecture,
( sdtpldt0(sz10,xp) != smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(f50,negated_conjecture,
~ ( sdtpldt0(sz10,xp) != smndt0(sz10)
| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ),
inference(negated_conjecture,[status(cth)],[f49]) ).
fof(f57,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f4]) ).
fof(f62,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f7]) ).
fof(f63,plain,
! [X0,X1,X2] :
( sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f62]) ).
fof(f64,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f8]) ).
fof(f65,plain,
! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f64]) ).
fof(f66,plain,
! [X0] :
( ( sdtpldt0(X0,sz00) = X0
& X0 = sdtpldt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f67,plain,
! [X0] :
( ( sdtpldt0(X0,smndt0(X0)) = sz00
& sz00 = sdtpldt0(smndt0(X0),X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f72,plain,
! [X0] :
( ( sdtasdt0(X0,sz10) = X0
& X0 = sdtasdt0(sz10,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f74,plain,
! [X0,X1,X2] :
( ( sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2))
& sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)) )
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| ~ aInteger0(X2) ),
inference(flattening,[],[f73]) ).
fof(f75,plain,
! [X0] :
( ( sdtasdt0(X0,sz00) = sz00
& sz00 = sdtasdt0(sz00,X0) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f76,plain,
! [X0] :
( ( sdtasdt0(smndt0(sz10),X0) = smndt0(X0)
& smndt0(X0) = sdtasdt0(X0,smndt0(sz10)) )
| ~ aInteger0(X0) ),
inference(ennf_transformation,[],[f16]) ).
fof(f77,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f78,plain,
! [X0,X1] :
( X0 = sz00
| X1 = sz00
| sz00 != sdtasdt0(X0,X1)
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(flattening,[],[f77]) ).
fof(f113,plain,
( smndt0(sz10) = sdtpldt0(sz10,xp)
& smndt0(sz10) = sdtpldt0(sz10,smndt0(xp)) ),
inference(ennf_transformation,[],[f50]) ).
fof(f170,plain,
aInteger0(sz10),
inference(cnf_transformation,[],[f3]) ).
fof(f171,plain,
! [X0] :
( aInteger0(smndt0(X0))
| ~ aInteger0(X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f174,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2) ),
inference(cnf_transformation,[],[f63]) ).
fof(f175,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,X1) = sdtpldt0(X1,X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f176,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(sz00,X0) = X0 ),
inference(cnf_transformation,[],[f66]) ).
fof(f178,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(smndt0(X0),X0) ),
inference(cnf_transformation,[],[f67]) ).
fof(f179,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtpldt0(X0,smndt0(X0)) ),
inference(cnf_transformation,[],[f67]) ).
fof(f183,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sz10) = X0 ),
inference(cnf_transformation,[],[f72]) ).
fof(f185,plain,
! [X2,X0,X1] :
( ~ aInteger0(X2)
| ~ aInteger0(X0)
| ~ aInteger0(X1)
| sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf_transformation,[],[f74]) ).
fof(f187,plain,
! [X0] :
( ~ aInteger0(X0)
| sz00 = sdtasdt0(X0,sz00) ),
inference(cnf_transformation,[],[f75]) ).
fof(f189,plain,
! [X0] :
( ~ aInteger0(X0)
| smndt0(X0) = sdtasdt0(smndt0(sz10),X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f190,plain,
! [X0,X1] :
( sz00 != sdtasdt0(X0,X1)
| sz00 = X1
| sz00 = X0
| ~ aInteger0(X0)
| ~ aInteger0(X1) ),
inference(cnf_transformation,[],[f78]) ).
fof(f283,plain,
sz00 != xp,
inference(cnf_transformation,[],[f46]) ).
fof(f284,plain,
aInteger0(xp),
inference(cnf_transformation,[],[f46]) ).
fof(f288,plain,
sz10 != sdtpldt0(sz10,xp),
inference(cnf_transformation,[],[f48]) ).
fof(f289,plain,
smndt0(sz10) = sdtpldt0(sz10,smndt0(xp)),
inference(cnf_transformation,[],[f113]) ).
fof(f290,plain,
smndt0(sz10) = sdtpldt0(sz10,xp),
inference(cnf_transformation,[],[f113]) ).
fof(f311,definition,
sF21 = smndt0(sz10),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f312,plain,
smndt0(sz10) = sF21,
inference(reorient_equations,[],[f311]) ).
fof(f313,definition,
sF22 = sdtpldt0(sz10,xp),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f314,plain,
sdtpldt0(sz10,xp) = sF22,
inference(reorient_equations,[],[f313]) ).
fof(f315,plain,
sF21 = sF22,
inference(definition_folding,[],[f290,f314,f312]) ).
fof(f316,definition,
sF23 = smndt0(xp),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f317,plain,
smndt0(xp) = sF23,
inference(reorient_equations,[],[f316]) ).
fof(f318,definition,
sF24 = sdtpldt0(sz10,sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f319,plain,
sdtpldt0(sz10,sF23) = sF24,
inference(reorient_equations,[],[f318]) ).
fof(f320,plain,
sF21 = sF24,
inference(definition_folding,[],[f289,f319,f317,f312]) ).
fof(f321,plain,
sdtpldt0(sz10,xp) = sF21,
inference(forward_demodulation,[],[f314,f315]) ).
fof(f322,plain,
sF21 = sdtpldt0(sz10,sF23),
inference(forward_demodulation,[],[f319,f320]) ).
fof(f323,plain,
sz10 != sF21,
inference(superposition,[],[f288,f321]) ).
fof(f325,plain,
( aInteger0(sF21)
| ~ aInteger0(sz10) ),
inference(superposition,[],[f171,f312]) ).
fof(f326,plain,
( aInteger0(sF23)
| ~ aInteger0(xp) ),
inference(superposition,[],[f171,f317]) ).
fof(f327,plain,
aInteger0(sF23),
inference(forward_subsumption_resolution,[],[f326,f284]) ).
fof(f328,plain,
aInteger0(sF21),
inference(forward_subsumption_resolution,[],[f325,f170]) ).
fof(f335,plain,
sz10 = sdtpldt0(sz00,sz10),
inference(resolution,[],[f176,f170]) ).
fof(f337,plain,
xp = sdtpldt0(sz00,xp),
inference(resolution,[],[f176,f284]) ).
fof(f357,plain,
sF23 = sdtasdt0(sF23,sz10),
inference(resolution,[],[f183,f327]) ).
fof(f368,plain,
sz00 = sdtasdt0(sF21,sz00),
inference(resolution,[],[f187,f328]) ).
fof(f403,plain,
sz00 = sdtpldt0(smndt0(sz10),sz10),
inference(resolution,[],[f178,f170]) ).
fof(f411,plain,
sz00 = sdtpldt0(sF21,sz10),
inference(forward_demodulation,[],[f403,f312]) ).
fof(f414,plain,
sz00 = sdtpldt0(sz10,smndt0(sz10)),
inference(resolution,[],[f179,f170]) ).
fof(f418,plain,
sz00 = sdtpldt0(xp,smndt0(xp)),
inference(resolution,[],[f179,f284]) ).
fof(f421,plain,
sz00 = sdtpldt0(xp,sF23),
inference(forward_demodulation,[],[f418,f317]) ).
fof(f422,plain,
sz00 = sdtpldt0(sz10,sF21),
inference(forward_demodulation,[],[f414,f312]) ).
fof(f457,plain,
smndt0(xp) = sdtasdt0(smndt0(sz10),xp),
inference(resolution,[],[f189,f284]) ).
fof(f462,plain,
smndt0(xp) = sdtasdt0(sF21,xp),
inference(forward_demodulation,[],[f457,f312]) ).
fof(f468,plain,
sF23 = sdtasdt0(sF21,xp),
inference(forward_demodulation,[],[f462,f317]) ).
fof(f522,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sz10) = sdtpldt0(sz10,X0) ),
inference(resolution,[],[f175,f170]) ).
fof(f526,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,xp) = sdtpldt0(xp,X0) ),
inference(resolution,[],[f175,f284]) ).
fof(f674,plain,
sdtpldt0(sz10,xp) = sdtpldt0(xp,sz10),
inference(resolution,[],[f526,f170]) ).
fof(f681,plain,
sdtpldt0(sF21,xp) = sdtpldt0(xp,sF21),
inference(resolution,[],[f526,f328]) ).
fof(f684,plain,
sF21 = sdtpldt0(xp,sz10),
inference(forward_demodulation,[],[f674,f321]) ).
fof(f900,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(X1,sz10)) = sdtpldt0(sdtpldt0(X0,X1),sz10) ),
inference(resolution,[],[f174,f170]) ).
fof(f904,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtpldt0(sdtpldt0(X0,X1),xp) = sdtpldt0(X0,sdtpldt0(X1,xp)) ),
inference(resolution,[],[f174,f284]) ).
fof(f1038,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(X1,sz10)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz10)) ),
inference(resolution,[],[f185,f170]) ).
fof(f1042,plain,
! [X0,X1] :
( ~ aInteger0(X1)
| ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(X1,xp)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,xp)) ),
inference(resolution,[],[f185,f284]) ).
fof(f1465,plain,
sdtpldt0(sz10,sF23) = sdtpldt0(sF23,sz10),
inference(resolution,[],[f522,f327]) ).
fof(f1466,plain,
sF21 = sdtpldt0(sF23,sz10),
inference(forward_demodulation,[],[f1465,f322]) ).
fof(f3469,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(sdtpldt0(X0,sz10),xp) = sdtpldt0(X0,sdtpldt0(sz10,xp)) ),
inference(resolution,[],[f904,f170]) ).
fof(f3486,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sF21) = sdtpldt0(sdtpldt0(X0,sz10),xp) ),
inference(forward_demodulation,[],[f3469,f321]) ).
fof(f3489,plain,
sdtpldt0(sz10,sF21) = sdtpldt0(sdtpldt0(sz10,sz10),xp),
inference(resolution,[],[f3486,f170]) ).
fof(f3502,plain,
sdtpldt0(sF21,sF21) = sdtpldt0(sdtpldt0(sF21,sz10),xp),
inference(resolution,[],[f3486,f328]) ).
fof(f3505,plain,
sdtpldt0(sz00,xp) = sdtpldt0(sF21,sF21),
inference(forward_demodulation,[],[f3502,f411]) ).
fof(f3507,plain,
sz00 = sdtpldt0(sdtpldt0(sz10,sz10),xp),
inference(forward_demodulation,[],[f3489,f422]) ).
fof(f3510,plain,
xp = sdtpldt0(sF21,sF21),
inference(forward_demodulation,[],[f3505,f337]) ).
fof(f3860,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(xp,sz10)) = sdtpldt0(sdtpldt0(X0,xp),sz10) ),
inference(resolution,[],[f900,f284]) ).
fof(f3870,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sdtpldt0(sF23,sz10)) = sdtpldt0(sdtpldt0(X0,sF23),sz10) ),
inference(resolution,[],[f900,f327]) ).
fof(f3871,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sF21) = sdtpldt0(sdtpldt0(X0,sF23),sz10) ),
inference(forward_demodulation,[],[f3870,f1466]) ).
fof(f3873,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtpldt0(X0,sF21) = sdtpldt0(sdtpldt0(X0,xp),sz10) ),
inference(forward_demodulation,[],[f3860,f684]) ).
fof(f3975,plain,
sdtpldt0(xp,sF21) = sdtpldt0(sdtpldt0(xp,sF23),sz10),
inference(resolution,[],[f3871,f284]) ).
fof(f3988,plain,
sdtpldt0(sz00,sz10) = sdtpldt0(xp,sF21),
inference(forward_demodulation,[],[f3975,f421]) ).
fof(f3991,plain,
sz10 = sdtpldt0(xp,sF21),
inference(forward_demodulation,[],[f3988,f335]) ).
fof(f4220,plain,
sdtpldt0(sF21,sF21) = sdtpldt0(sdtpldt0(sF21,xp),sz10),
inference(resolution,[],[f3873,f328]) ).
fof(f4223,plain,
sdtpldt0(sF21,sF21) = sdtpldt0(sdtpldt0(xp,sF21),sz10),
inference(forward_demodulation,[],[f4220,f681]) ).
fof(f4229,plain,
sdtpldt0(sz10,sz10) = sdtpldt0(sF21,sF21),
inference(forward_demodulation,[],[f4223,f3991]) ).
fof(f4233,plain,
xp = sdtpldt0(sz10,sz10),
inference(forward_demodulation,[],[f4229,f3510]) ).
fof(f4305,plain,
sz00 = sdtpldt0(xp,xp),
inference(superposition,[],[f3507,f4233]) ).
fof(f4403,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(xp,xp)) = sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(X0,xp)) ),
inference(resolution,[],[f1042,f284]) ).
fof(f4419,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sz00) = sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(X0,xp)) ),
inference(forward_demodulation,[],[f4403,f4305]) ).
fof(f4972,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,sdtpldt0(sz10,sz10)) = sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)) ),
inference(resolution,[],[f1038,f170]) ).
fof(f4995,plain,
! [X0] :
( ~ aInteger0(X0)
| sdtasdt0(X0,xp) = sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)) ),
inference(forward_demodulation,[],[f4972,f4233]) ).
fof(f10773,plain,
sdtasdt0(sF21,sz00) = sdtpldt0(sdtasdt0(sF21,xp),sdtasdt0(sF21,xp)),
inference(resolution,[],[f4419,f328]) ).
fof(f10776,plain,
sdtasdt0(sF21,sz00) = sdtpldt0(sF23,sF23),
inference(forward_demodulation,[],[f10773,f468]) ).
fof(f10782,plain,
sz00 = sdtpldt0(sF23,sF23),
inference(forward_demodulation,[],[f10776,f368]) ).
fof(f11059,plain,
sdtasdt0(sF23,xp) = sdtpldt0(sdtasdt0(sF23,sz10),sdtasdt0(sF23,sz10)),
inference(resolution,[],[f4995,f327]) ).
fof(f11060,plain,
sdtasdt0(sF23,xp) = sdtpldt0(sF23,sF23),
inference(forward_demodulation,[],[f11059,f357]) ).
fof(f11066,plain,
sz00 = sdtasdt0(sF23,xp),
inference(forward_demodulation,[],[f11060,f10782]) ).
fof(f11111,plain,
( sz00 != sz00
| sz00 = xp
| sz00 = sF23
| ~ aInteger0(sF23)
| ~ aInteger0(xp) ),
inference(superposition,[],[f190,f11066]) ).
fof(f11119,plain,
( sz00 = xp
| sz00 = sF23
| ~ aInteger0(sF23)
| ~ aInteger0(xp) ),
inference(trivial_inequality_removal,[],[f11111]) ).
fof(f11126,plain,
( sz00 = sF23
| ~ aInteger0(sF23)
| ~ aInteger0(xp) ),
inference(forward_subsumption_resolution,[],[f11119,f283]) ).
fof(f11133,plain,
( sz00 = sF23
| ~ aInteger0(xp) ),
inference(forward_subsumption_resolution,[],[f11126,f327]) ).
fof(f11140,plain,
sz00 = sF23,
inference(forward_subsumption_resolution,[],[f11133,f284]) ).
fof(f11210,plain,
sF21 = sdtpldt0(sz00,sz10),
inference(superposition,[],[f1466,f11140]) ).
fof(f11243,plain,
sz10 = sF21,
inference(forward_demodulation,[],[f11210,f335]) ).
fof(f11263,plain,
$false,
inference(forward_subsumption_resolution,[],[f11243,f323]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM454+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 20:00:17 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 Running first-order model finding
% 0.11/0.41 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
% 15.43/2.67 % (1269565)Will run a generic schedule for satisfiability detection.
% 15.43/2.67 % (1269572)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=532739243:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.43/2.67 % (1269571)% WARNING: option uhcvi not known.
% 15.43/2.67 % (1269570)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3544078225_2999 on theBenchmark for (2999ds/0Mi)
% 15.43/2.67 % (1269571)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2667141164:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.43/2.67 % (1269575)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1221351869:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.43/2.67 % (1269573)dis+10_1_sil=32000:sp=arity:random_seed=4252038916:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.43/2.67 % (1269574)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3747397342:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.43/2.67 % (1269576)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3331441032:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.43/2.67 % TRYING [1]
% 15.43/2.67 % TRYING [2]
% 15.43/2.67 % TRYING [3]
% 15.43/2.67 % TRYING [4]
% 15.43/2.67 % (1269573)Instruction limit reached!
% 15.43/2.67 % (1269573)------------------------------
% 15.43/2.67 % (1269573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.67 % (1269573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.67 % (1269573)CaDiCaL version: 2.1.3
% 15.43/2.67 % (1269573)Termination reason: Instruction limit
% 15.43/2.67 % (1269573)Termination phase: Saturation
% 15.43/2.67 % (1269573)Time elapsed: 0.065 s
% 15.43/2.67 % (1269573)Peak memory usage: 12 MB
% 15.43/2.67 % (1269573)Instructions burned: 103 (million)
% 15.43/2.67 % (1269575)Instruction limit reached!
% 15.43/2.67 % (1269575)------------------------------
% 15.43/2.67 % (1269575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.67 % (1269575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.67 % (1269575)CaDiCaL version: 2.1.3
% 15.43/2.67 % (1269575)Termination reason: Instruction limit
% 15.43/2.67 % (1269575)Termination phase: Saturation
% 15.43/2.67 % (1269575)Time elapsed: 0.069 s
% 15.43/2.67 % (1269575)Peak memory usage: 13 MB
% 15.43/2.67 % (1269575)Instructions burned: 131 (million)
% 15.43/2.67 % TRYING [5]
% 15.43/2.67 % (1269574)Instruction limit reached!
% 15.43/2.67 % (1269574)------------------------------
% 15.43/2.67 % (1269574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.67 % (1269574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.67 % (1269574)CaDiCaL version: 2.1.3
% 15.43/2.67 % (1269574)Termination reason: Instruction limit
% 15.43/2.67 % (1269574)Termination phase: Saturation
% 15.43/2.67 % (1269574)Time elapsed: 0.071 s
% 15.43/2.67 % (1269574)Peak memory usage: 13 MB
% 15.43/2.67 % (1269574)Instructions burned: 117 (million)
% 15.43/2.67 % (1269584)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=787102182:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.43/2.67 % (1269585)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2336994633:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.43/2.67 % (1269586)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=3330307915:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.43/2.67 % TRYING [1]
% 15.43/2.67 % TRYING [2]
% 15.43/2.67 % (1269576)Instruction limit reached!
% 15.43/2.67 % (1269576)------------------------------
% 15.43/2.67 % (1269576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.67 % (1269576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.67 % (1269576)CaDiCaL version: 2.1.3
% 15.43/2.67 % (1269576)Termination reason: Instruction limit
% 15.43/2.67 % (1269576)Termination phase: Saturation
% 15.43/2.67 % (1269576)Time elapsed: 0.098 s
% 15.43/2.67 % (1269576)Peak memory usage: 14 MB
% 15.43/2.67 % (1269576)Instructions burned: 159 (million)
% 15.43/2.67 % TRYING [3]
% 15.43/2.67 % TRYING [4]
% 15.43/2.67 % (1269590)ott-21_1_sil=16000:fs=off:random_seed=387270891:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.43/2.67 % TRYING [5]
% 15.43/2.67 % (1269585)Instruction limit reached!
% 15.43/2.67 % (1269585)------------------------------
% 15.43/2.67 % (1269585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269585)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269585)Termination reason: Instruction limit
% 34.54/5.37 % (1269585)Termination phase: Saturation
% 34.54/5.37 % (1269585)Time elapsed: 0.068 s
% 34.54/5.37 % (1269585)Peak memory usage: 12 MB
% 34.54/5.37 % (1269585)Instructions burned: 133 (million)
% 34.54/5.37 % (1269592)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3852303508:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 34.54/5.37 % TRYING [6]
% 34.54/5.37 % (1269590)Instruction limit reached!
% 34.54/5.37 % (1269590)------------------------------
% 34.54/5.37 % (1269590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269590)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269590)Termination reason: Instruction limit
% 34.54/5.37 % (1269590)Termination phase: Saturation
% 34.54/5.37 % (1269590)Time elapsed: 0.093 s
% 34.54/5.37 % (1269590)Peak memory usage: 13 MB
% 34.54/5.37 % (1269590)Instructions burned: 182 (million)
% 34.54/5.37 % (1269594)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3573822422:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.54/5.37 % TRYING [1]
% 34.54/5.37 % TRYING [2]
% 34.54/5.37 % TRYING [3]
% 34.54/5.37 % TRYING [6]
% 34.54/5.37 % TRYING [4]
% 34.54/5.37 % (1269584)Instruction limit reached!
% 34.54/5.37 % (1269584)------------------------------
% 34.54/5.37 % (1269584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269584)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269584)Termination reason: Instruction limit
% 34.54/5.37 % (1269584)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269584)Time elapsed: 0.266 s
% 34.54/5.37 % (1269584)Peak memory usage: 30 MB
% 34.54/5.37 % (1269584)Instructions burned: 715 (million)
% 34.54/5.37 % (1269596)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4245023375:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 34.54/5.37 % (1269586)Instruction limit reached!
% 34.54/5.37 % (1269586)------------------------------
% 34.54/5.37 % (1269586)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269586)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269586)Termination reason: Instruction limit
% 34.54/5.37 % (1269586)Termination phase: Saturation
% 34.54/5.37 % (1269586)Time elapsed: 0.330 s
% 34.54/5.37 % (1269586)Peak memory usage: 17 MB
% 34.54/5.37 % (1269586)Instructions burned: 684 (million)
% 34.54/5.37 % TRYING [5]
% 34.54/5.37 % (1269598)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1881685901:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 34.54/5.37 % (1269592)Instruction limit reached!
% 34.54/5.37 % (1269592)------------------------------
% 34.54/5.37 % (1269592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269592)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269592)Termination reason: Instruction limit
% 34.54/5.37 % (1269592)Termination phase: Saturation
% 34.54/5.37 % (1269592)Time elapsed: 0.308 s
% 34.54/5.37 % (1269592)Peak memory usage: 14 MB
% 34.54/5.37 % (1269592)Instructions burned: 477 (million)
% 34.54/5.37 % (1269600)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=2258040236: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)
% 34.54/5.37 % TRYING [7]
% 34.54/5.37 % (1269594)Instruction limit reached!
% 34.54/5.37 % (1269594)------------------------------
% 34.54/5.37 % (1269594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269594)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269594)Termination reason: Instruction limit
% 34.54/5.37 % (1269594)Termination phase: Finite model building SAT solving
% 34.54/5.37 % (1269594)Time elapsed: 0.348 s
% 34.54/5.37 % (1269594)Peak memory usage: 24 MB
% 34.54/5.37 % (1269594)Instructions burned: 867 (million)
% 34.54/5.37 % (1269602)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1860897747:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 34.54/5.37 % TRYING [14]
% 34.54/5.37 % (1269598)Instruction limit reached!
% 34.54/5.37 % (1269598)------------------------------
% 34.54/5.37 % (1269598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269598)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269598)Termination reason: Instruction limit
% 34.54/5.37 % (1269598)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269598)Time elapsed: 0.361 s
% 34.54/5.37 % (1269598)Peak memory usage: 85 MB
% 34.54/5.37 % (1269598)Instructions burned: 892 (million)
% 34.54/5.37 % (1269604)fmb+10_1_sil=64000:random_seed=3712970178:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 34.54/5.37 % TRYING [1]
% 34.54/5.37 % TRYING [2]
% 34.54/5.37 % TRYING [3]
% 34.54/5.37 % (1269600)Instruction limit reached!
% 34.54/5.37 % (1269600)------------------------------
% 34.54/5.37 % (1269600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269600)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269600)Termination reason: Instruction limit
% 34.54/5.37 % (1269600)Termination phase: Saturation
% 34.54/5.37 % (1269600)Time elapsed: 0.347 s
% 34.54/5.37 % (1269600)Peak memory usage: 21 MB
% 34.54/5.37 % (1269600)Instructions burned: 693 (million)
% 34.54/5.37 % (1269606)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3823769231:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 34.54/5.37 % TRYING [20]
% 34.54/5.37 % TRYING [4]
% 34.54/5.37 % TRYING [5]
% 34.54/5.37 % (1269596)Instruction limit reached!
% 34.54/5.37 % (1269596)------------------------------
% 34.54/5.37 % (1269596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269596)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269596)Termination reason: Instruction limit
% 34.54/5.37 % (1269596)Termination phase: Saturation
% 34.54/5.37 % (1269596)Time elapsed: 0.674 s
% 34.54/5.37 % (1269596)Peak memory usage: 24 MB
% 34.54/5.37 % (1269596)Instructions burned: 1180 (million)
% 34.54/5.37 % (1269608)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3281655227:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 34.54/5.37 % TRYING [8]
% 34.54/5.37 % TRYING [8]
% 34.54/5.37 % (1269602)Instruction limit reached!
% 34.54/5.37 % (1269602)------------------------------
% 34.54/5.37 % (1269602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269602)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269602)Termination reason: Instruction limit
% 34.54/5.37 % (1269602)Termination phase: Saturation
% 34.54/5.37 % (1269602)Time elapsed: 0.510 s
% 34.54/5.37 % (1269602)Peak memory usage: 19 MB
% 34.54/5.37 % (1269602)Instructions burned: 879 (million)
% 34.54/5.37 % (1269610)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2361436774:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 34.54/5.37 % TRYING [6]
% 34.54/5.37 % (1269608)Instruction limit reached!
% 34.54/5.37 % (1269608)------------------------------
% 34.54/5.37 % (1269608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269608)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269608)Termination reason: Instruction limit
% 34.54/5.37 % (1269608)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269608)Time elapsed: 0.344 s
% 34.54/5.37 % (1269608)Peak memory usage: 72 MB
% 34.54/5.37 % (1269608)Instructions burned: 923 (million)
% 34.54/5.37 % (1269612)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=664817240:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 34.54/5.37 % TRYING [7]
% 34.54/5.37 % TRYING [9]
% 34.54/5.37 % (1269612)Instruction limit reached!
% 34.54/5.37 % (1269612)------------------------------
% 34.54/5.37 % (1269612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269612)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269612)Termination reason: Instruction limit
% 34.54/5.37 % (1269612)Termination phase: Saturation
% 34.54/5.37 % (1269612)Time elapsed: 0.751 s
% 34.54/5.37 % (1269612)Peak memory usage: 31 MB
% 34.54/5.37 % (1269612)Instructions burned: 1472 (million)
% 34.54/5.37 % (1269614)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1455625326:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 34.54/5.37 % TRYING [77]
% 34.54/5.37 % TRYING [8]
% 34.54/5.37 % (1269610)Instruction limit reached!
% 34.54/5.37 % (1269610)------------------------------
% 34.54/5.37 % (1269610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269610)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269610)Termination reason: Instruction limit
% 34.54/5.37 % (1269610)Termination phase: Saturation
% 34.54/5.37 % (1269610)Time elapsed: 2.454 s
% 34.54/5.37 % (1269610)Peak memory usage: 31 MB
% 34.54/5.37 % (1269610)Instructions burned: 5133 (million)
% 34.54/5.37 % (1269616)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3912000544:fmbsr=2.30978:i=2174_2963 on theBenchmark for (2963ds/2174Mi)
% 34.54/5.37 % TRYING [16]
% 34.54/5.37 % (1269606)Instruction limit reached!
% 34.54/5.37 % (1269606)------------------------------
% 34.54/5.37 % (1269606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269606)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269606)Termination reason: Instruction limit
% 34.54/5.37 % (1269606)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269606)Time elapsed: 3.341 s
% 34.54/5.37 % (1269606)Peak memory usage: 568 MB
% 34.54/5.37 % (1269606)Instructions burned: 9518 (million)
% 34.54/5.37 % (1269618)ott-2_1_sil=16000:newcnf=on:random_seed=3115045956:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2956 on theBenchmark for (2956ds/869Mi)
% 34.54/5.37 % (1269614)Instruction limit reached!
% 34.54/5.37 % (1269614)------------------------------
% 34.54/5.37 % (1269614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269614)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269614)Termination reason: Instruction limit
% 34.54/5.37 % (1269614)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269614)Time elapsed: 2.134 s
% 34.54/5.37 % (1269614)Peak memory usage: 344 MB
% 34.54/5.37 % (1269614)Instructions burned: 6324 (million)
% 34.54/5.37 % (1269616)Instruction limit reached!
% 34.54/5.37 % (1269616)------------------------------
% 34.54/5.37 % (1269616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269616)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269616)Termination reason: Instruction limit
% 34.54/5.37 % (1269616)Termination phase: Finite model building constraint generation
% 34.54/5.37 % (1269616)Time elapsed: 0.761 s
% 34.54/5.37 % (1269616)Peak memory usage: 134 MB
% 34.54/5.37 % (1269616)Instructions burned: 2177 (million)
% 34.54/5.37 % (1269620)ott+10_1_sil=32000:tgt=ground:random_seed=2009052475:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 34.54/5.37 % (1269621)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2390547723:i=54282_2955 on theBenchmark for (2955ds/54282Mi)
% 34.54/5.37 % TRYING [1]
% 34.54/5.37 % TRYING [2]
% 34.54/5.37 % TRYING [3]
% 34.54/5.37 % TRYING [4]
% 34.54/5.37 % TRYING [5]
% 34.54/5.37 % TRYING [6]
% 34.54/5.37 % TRYING [10]
% 34.54/5.37 % (1269618)Instruction limit reached!
% 34.54/5.37 % (1269618)------------------------------
% 34.54/5.37 % (1269618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.37 % (1269618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.37 % (1269618)CaDiCaL version: 2.1.3
% 34.54/5.37 % (1269618)Termination reason: Instruction limit
% 34.54/5.37 % (1269618)Termination phase: Saturation
% 34.54/5.37 % (1269618)Time elapsed: 0.475 s
% 34.54/5.37 % (1269618)Peak memory usage: 23 MB
% 34.54/5.37 % (1269618)Instructions burned: 869 (million)
% 34.54/5.37 % (1269624)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=340298786:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 34.54/5.37 % (1269620) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1269565-1269620"...
% 34.54/5.37 % (1269620)...printing done.
% 34.54/5.37 % (1269620)Refutation found. Thanks to Tanya!
% 34.54/5.37 % SZS status Theorem for theBenchmark
% 34.54/5.37 % SZS output start Proof for theBenchmark
% See solution above
% 34.54/5.37 % (1269620)------------------------------
% 34.54/5.37 % (1269620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.54/5.38 % (1269620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.54/5.38 % (1269620)CaDiCaL version: 2.1.3
% 34.54/5.38 % (1269620)Termination reason: Refutation
% 34.54/5.38 % (1269620)Time elapsed: 0.465 s
% 34.54/5.38 % (1269620)Peak memory usage: 20 MB
% 34.54/5.38 % (1269620)Instructions burned: 826 (million)
% 34.54/5.38 % (1269565)Success in time 4.957 s
% 34.54/5.38 % Vampire exiting
%------------------------------------------------------------------------------