%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : RNG078+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:35:25 PM UTC 2026
% Result : Theorem 63.88s 18.65s
% Output : Refutation 126.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 64
% Syntax : Number of formulae : 284 ( 115 unt; 47 def)
% Number of atoms : 651 ( 123 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 683 ( 316 ~; 307 |; 24 &)
% ( 33 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 34 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 29 con; 0-2 aty)
% Number of variables : 68 ( 0 sgn 68 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f10,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtpldt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
fof(f11,axiom,
! [X0,X1] :
( ( aScalar0(X0)
& aScalar0(X1) )
=> aScalar0(sdtasdt0(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
fof(f14,axiom,
! [X0,X1,X2] :
( ( aScalar0(X0)
& aScalar0(X1)
& aScalar0(X2) )
=> ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mArith) ).
fof(f44,axiom,
( aScalar0(xA)
& xA = sdtlbdtrb0(xs,aDimensionOf0(xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1746) ).
fof(f45,axiom,
( aScalar0(xB)
& xB = sdtlbdtrb0(xt,aDimensionOf0(xt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1766) ).
fof(f46,axiom,
( aScalar0(xC)
& xC = sdtasasdt0(xp,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1783) ).
fof(f47,axiom,
( aScalar0(xD)
& xD = sdtasasdt0(xq,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1800) ).
fof(f48,axiom,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1820) ).
fof(f49,axiom,
( aScalar0(xF)
& xF = sdtasdt0(xA,xA) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1837) ).
fof(f50,axiom,
( aScalar0(xG)
& xG = sdtasdt0(xB,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1854) ).
fof(f51,axiom,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1873) ).
fof(f52,axiom,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
fof(f53,axiom,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
fof(f54,axiom,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
fof(f58,axiom,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2796) ).
fof(f59,axiom,
sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2835) ).
fof(f60,conjecture,
sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(f61,negated_conjecture,
~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(negated_conjecture,[status(cth)],[f60]) ).
fof(f62,plain,
~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(flattening,[],[f61]) ).
fof(f81,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f82,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f81]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(ennf_transformation,[],[f14]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
& sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
& sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
& sdtasdt0(X0,X1) = sdtasdt0(X1,X0) )
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(flattening,[],[f102]) ).
fof(f104,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(ennf_transformation,[],[f10]) ).
fof(f105,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(flattening,[],[f104]) ).
fof(f131,plain,
aScalar0(xA),
inference(cnf_transformation,[],[f44]) ).
fof(f133,plain,
aScalar0(xB),
inference(cnf_transformation,[],[f45]) ).
fof(f135,plain,
aScalar0(xC),
inference(cnf_transformation,[],[f46]) ).
fof(f137,plain,
aScalar0(xD),
inference(cnf_transformation,[],[f47]) ).
fof(f139,plain,
aScalar0(xE),
inference(cnf_transformation,[],[f48]) ).
fof(f140,plain,
xF = sdtasdt0(xA,xA),
inference(cnf_transformation,[],[f49]) ).
fof(f141,plain,
aScalar0(xF),
inference(cnf_transformation,[],[f49]) ).
fof(f142,plain,
xG = sdtasdt0(xB,xB),
inference(cnf_transformation,[],[f50]) ).
fof(f143,plain,
aScalar0(xG),
inference(cnf_transformation,[],[f50]) ).
fof(f144,plain,
xH = sdtasdt0(xA,xB),
inference(cnf_transformation,[],[f51]) ).
fof(f145,plain,
aScalar0(xH),
inference(cnf_transformation,[],[f51]) ).
fof(f146,plain,
xR = sdtasdt0(xC,xG),
inference(cnf_transformation,[],[f52]) ).
fof(f147,plain,
aScalar0(xR),
inference(cnf_transformation,[],[f52]) ).
fof(f148,plain,
xP = sdtasdt0(xE,xH),
inference(cnf_transformation,[],[f53]) ).
fof(f150,plain,
xS = sdtasdt0(xF,xD),
inference(cnf_transformation,[],[f54]) ).
fof(f151,plain,
aScalar0(xS),
inference(cnf_transformation,[],[f54]) ).
fof(f156,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH))),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sdtasdt0(xH,xH)))),
inference(cnf_transformation,[],[f58]) ).
fof(f157,plain,
sdtpldt0(sdtpldt0(xP,xP),sdtasdt0(xH,xH)) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),
inference(cnf_transformation,[],[f59]) ).
fof(f158,plain,
~ sdtlseqdt0(sdtpldt0(sdtpldt0(sdtasdt0(xE,xE),sdtasdt0(xE,xH)),sdtpldt0(sdtasdt0(xH,xE),sdtasdt0(xH,xH))),sdtpldt0(sdtpldt0(sdtasdt0(xC,xD),sdtasdt0(xC,xG)),sdtpldt0(sdtasdt0(xF,xD),sdtasdt0(xF,xG)))),
inference(cnf_transformation,[],[f62]) ).
fof(f166,plain,
! [X0,X1] :
( aScalar0(sdtasdt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f82]) ).
fof(f184,plain,
! [X2,X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f185,plain,
! [X2,X0,X1] :
( sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f186,plain,
! [X2,X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f187,plain,
! [X2,X0,X1] :
( sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))
| ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2) ),
inference(cnf_transformation,[],[f103]) ).
fof(f188,plain,
! [X0,X1] :
( aScalar0(sdtpldt0(X0,X1))
| ~ aScalar0(X0)
| ~ aScalar0(X1) ),
inference(cnf_transformation,[],[f105]) ).
fof(f198,definition,
sF2 = sdtasdt0(xE,xE),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f199,plain,
sdtasdt0(xE,xE) = sF2,
inference(reorient_equations,[],[f198]) ).
fof(f200,definition,
sF3 = sdtasdt0(xE,xH),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f201,plain,
sdtasdt0(xE,xH) = sF3,
inference(reorient_equations,[],[f200]) ).
fof(f202,definition,
sF4 = sdtpldt0(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f203,plain,
sdtpldt0(sF2,sF3) = sF4,
inference(reorient_equations,[],[f202]) ).
fof(f204,definition,
sF5 = sdtasdt0(xH,xE),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f205,plain,
sdtasdt0(xH,xE) = sF5,
inference(reorient_equations,[],[f204]) ).
fof(f206,definition,
sF6 = sdtasdt0(xH,xH),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f207,plain,
sdtasdt0(xH,xH) = sF6,
inference(reorient_equations,[],[f206]) ).
fof(f208,definition,
sF7 = sdtpldt0(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f209,plain,
sdtpldt0(sF5,sF6) = sF7,
inference(reorient_equations,[],[f208]) ).
fof(f210,definition,
sF8 = sdtpldt0(sF4,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f211,plain,
sdtpldt0(sF4,sF7) = sF8,
inference(reorient_equations,[],[f210]) ).
fof(f212,definition,
sF9 = sdtasdt0(xC,xD),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f213,plain,
sdtasdt0(xC,xD) = sF9,
inference(reorient_equations,[],[f212]) ).
fof(f214,definition,
sF10 = sdtasdt0(xC,xG),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f215,plain,
sdtasdt0(xC,xG) = sF10,
inference(reorient_equations,[],[f214]) ).
fof(f216,definition,
sF11 = sdtpldt0(sF9,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f217,plain,
sdtpldt0(sF9,sF10) = sF11,
inference(reorient_equations,[],[f216]) ).
fof(f218,definition,
sF12 = sdtasdt0(xF,xD),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f219,plain,
sdtasdt0(xF,xD) = sF12,
inference(reorient_equations,[],[f218]) ).
fof(f220,definition,
sF13 = sdtasdt0(xF,xG),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f221,plain,
sdtasdt0(xF,xG) = sF13,
inference(reorient_equations,[],[f220]) ).
fof(f222,definition,
sF14 = sdtpldt0(sF12,sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f223,plain,
sdtpldt0(sF12,sF13) = sF14,
inference(reorient_equations,[],[f222]) ).
fof(f224,definition,
sF15 = sdtpldt0(sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f225,plain,
sdtpldt0(sF11,sF14) = sF15,
inference(reorient_equations,[],[f224]) ).
fof(f226,plain,
~ sdtlseqdt0(sF8,sF15),
inference(definition_folding,[],[f158,f225,f223,f221,f219,f217,f215,f213,f211,f209,f207,f205,f203,f201,f199]) ).
fof(f228,definition,
( spl16_1
<=> ! [X2] : ~ aScalar0(X2) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
fof(f229,plain,
( ! [X2] : ~ aScalar0(X2)
| ~ spl16_1 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f231,definition,
( spl16_2
<=> ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
fof(f232,plain,
( ! [X0,X1] :
( sdtasdt0(X0,X1) = sdtasdt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( spl16_1
| spl16_2 ),
inference(avatar_split_clause,[],[f184,f231,f228]) ).
fof(f235,definition,
( spl16_3
<=> ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
fof(f236,plain,
( ! [X0,X1] :
( sdtpldt0(X0,X1) = sdtpldt0(X1,X0)
| ~ aScalar0(X1)
| ~ aScalar0(X0) )
| ~ spl16_3 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f237,plain,
( spl16_1
| spl16_3 ),
inference(avatar_split_clause,[],[f186,f235,f228]) ).
fof(f248,definition,
( spl16_4
<=> aScalar0(sF13) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
fof(f256,definition,
( spl16_6
<=> aScalar0(sF14) ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
fof(f258,plain,
( aScalar0(sF14)
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f256]) ).
fof(f274,definition,
( spl16_10
<=> aScalar0(sF9) ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
fof(f279,definition,
( spl16_11
<=> aScalar0(sF6) ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
fof(f283,definition,
( spl16_12
<=> aScalar0(sF5) ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
fof(f287,definition,
( spl16_13
<=> aScalar0(sF7) ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
fof(f289,plain,
( aScalar0(sF7)
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f287]) ).
fof(f305,definition,
( spl16_17
<=> aScalar0(sF2) ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
fof(f354,definition,
( spl16_24
<=> aScalar0(xH) ),
introduced(definition,[new_symbols(definition,[spl16_24])],[avatar_definition]) ).
fof(f355,plain,
( aScalar0(xH)
| ~ spl16_24 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f359,definition,
( spl16_25
<=> aScalar0(xE) ),
introduced(definition,[new_symbols(definition,[spl16_25])],[avatar_definition]) ).
fof(f364,definition,
( spl16_26
<=> aScalar0(xG) ),
introduced(definition,[new_symbols(definition,[spl16_26])],[avatar_definition]) ).
fof(f365,plain,
( aScalar0(xG)
| ~ spl16_26 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f368,definition,
( spl16_27
<=> aScalar0(xC) ),
introduced(definition,[new_symbols(definition,[spl16_27])],[avatar_definition]) ).
fof(f373,definition,
( spl16_28
<=> aScalar0(xF) ),
introduced(definition,[new_symbols(definition,[spl16_28])],[avatar_definition]) ).
fof(f380,definition,
( spl16_29
<=> aScalar0(xD) ),
introduced(definition,[new_symbols(definition,[spl16_29])],[avatar_definition]) ).
fof(f401,plain,
spl16_29,
inference(avatar_split_clause,[],[f137,f380]) ).
fof(f402,plain,
spl16_27,
inference(avatar_split_clause,[],[f135,f368]) ).
fof(f616,plain,
xP = sF3,
inference(superposition,[],[f201,f148]) ).
fof(f623,definition,
( spl16_61
<=> aScalar0(xP) ),
introduced(definition,[new_symbols(definition,[spl16_61])],[avatar_definition]) ).
fof(f647,plain,
sF4 = sdtpldt0(sF2,xP),
inference(superposition,[],[f203,f616]) ).
fof(f654,plain,
! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(xP,X0))
| ~ aScalar0(sF2)
| ~ aScalar0(xP)
| ~ aScalar0(X0) ),
inference(superposition,[],[f187,f647]) ).
fof(f658,definition,
( spl16_65
<=> ! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(xP,X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_65])],[avatar_definition]) ).
fof(f659,plain,
( ! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(xP,X0))
| ~ aScalar0(X0) )
| ~ spl16_65 ),
inference(avatar_component_clause,[],[f658]) ).
fof(f660,plain,
( ~ spl16_61
| ~ spl16_17
| spl16_65 ),
inference(avatar_split_clause,[],[f654,f658,f305,f623]) ).
fof(f680,plain,
xS = sF12,
inference(superposition,[],[f219,f150]) ).
fof(f687,definition,
( spl16_69
<=> aScalar0(xS) ),
introduced(definition,[new_symbols(definition,[spl16_69])],[avatar_definition]) ).
fof(f707,plain,
sF14 = sdtpldt0(xS,sF13),
inference(superposition,[],[f223,f680]) ).
fof(f841,plain,
sdtpldt0(sdtpldt0(xP,xP),sF6) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sdtasdt0(xH,xE),sF6)),
inference(forward_demodulation,[],[f157,f207]) ).
fof(f842,plain,
sdtpldt0(sdtpldt0(xP,xP),sF6) = sdtpldt0(sdtasdt0(xE,xH),sdtpldt0(sF5,sF6)),
inference(forward_demodulation,[],[f841,f205]) ).
fof(f843,plain,
sdtpldt0(sdtpldt0(xP,xP),sF6) = sdtpldt0(sdtasdt0(xE,xH),sF7),
inference(forward_demodulation,[],[f842,f209]) ).
fof(f844,plain,
sdtpldt0(sdtpldt0(xP,xP),sF6) = sdtpldt0(sF3,sF7),
inference(forward_demodulation,[],[f843,f201]) ).
fof(f845,plain,
sdtpldt0(sdtpldt0(xP,xP),sF6) = sdtpldt0(xP,sF7),
inference(forward_demodulation,[],[f844,f616]) ).
fof(f1246,plain,
xR = sF10,
inference(superposition,[],[f215,f146]) ).
fof(f1299,definition,
( spl16_161
<=> aScalar0(xR) ),
introduced(definition,[new_symbols(definition,[spl16_161])],[avatar_definition]) ).
fof(f1303,plain,
sF11 = sdtpldt0(sF9,xR),
inference(superposition,[],[f217,f1246]) ).
fof(f1310,plain,
! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(xR,X0))
| ~ aScalar0(sF9)
| ~ aScalar0(xR)
| ~ aScalar0(X0) ),
inference(superposition,[],[f187,f1303]) ).
fof(f1314,definition,
( spl16_162
<=> ! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(xR,X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_162])],[avatar_definition]) ).
fof(f1315,plain,
( ! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(xR,X0))
| ~ aScalar0(X0) )
| ~ spl16_162 ),
inference(avatar_component_clause,[],[f1314]) ).
fof(f1316,plain,
( ~ spl16_161
| ~ spl16_10
| spl16_162 ),
inference(avatar_split_clause,[],[f1310,f1314,f274,f1299]) ).
fof(f1333,plain,
spl16_161,
inference(avatar_split_clause,[],[f147,f1299]) ).
fof(f1358,plain,
( $false
| ~ spl16_1 ),
inference(backward_subsumption_resolution,[],[f145,f229]) ).
fof(f1367,plain,
~ spl16_1,
inference(avatar_contradiction_clause,[],[f1358]) ).
fof(f1378,plain,
spl16_24,
inference(avatar_split_clause,[],[f145,f354]) ).
fof(f1379,plain,
spl16_26,
inference(avatar_split_clause,[],[f143,f364]) ).
fof(f1380,plain,
spl16_28,
inference(avatar_split_clause,[],[f141,f373]) ).
fof(f1381,plain,
spl16_25,
inference(avatar_split_clause,[],[f139,f359]) ).
fof(f1445,plain,
( aScalar0(sF7)
| ~ aScalar0(sF5)
| ~ aScalar0(sF6) ),
inference(superposition,[],[f188,f209]) ).
fof(f1449,plain,
( aScalar0(sF14)
| ~ aScalar0(sF12)
| ~ aScalar0(sF13) ),
inference(superposition,[],[f188,f223]) ).
fof(f1451,plain,
( ~ aScalar0(xS)
| aScalar0(sF14)
| ~ aScalar0(sF13) ),
inference(forward_demodulation,[],[f1449,f680]) ).
fof(f1455,plain,
( ~ spl16_11
| ~ spl16_12
| spl16_13 ),
inference(avatar_split_clause,[],[f1445,f287,f283,f279]) ).
fof(f1461,plain,
( ~ spl16_4
| spl16_6
| ~ spl16_69 ),
inference(avatar_split_clause,[],[f1451,f687,f256,f248]) ).
fof(f1468,plain,
( aScalar0(sF9)
| ~ aScalar0(xC)
| ~ aScalar0(xD) ),
inference(superposition,[],[f166,f213]) ).
fof(f1469,plain,
( aScalar0(sF2)
| ~ aScalar0(xE)
| ~ aScalar0(xE) ),
inference(superposition,[],[f166,f199]) ).
fof(f1470,plain,
( aScalar0(sF5)
| ~ aScalar0(xH)
| ~ aScalar0(xE) ),
inference(superposition,[],[f166,f205]) ).
fof(f1471,plain,
( aScalar0(sF13)
| ~ aScalar0(xF)
| ~ aScalar0(xG) ),
inference(superposition,[],[f166,f221]) ).
fof(f1475,plain,
( aScalar0(sF3)
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(superposition,[],[f166,f201]) ).
fof(f1476,plain,
( aScalar0(sF6)
| ~ aScalar0(xH)
| ~ aScalar0(xH) ),
inference(superposition,[],[f166,f207]) ).
fof(f1477,plain,
( aScalar0(sF6)
| ~ aScalar0(xH) ),
inference(duplicate_literal_removal,[],[f1476]) ).
fof(f1478,plain,
( aScalar0(sF2)
| ~ aScalar0(xE) ),
inference(duplicate_literal_removal,[],[f1469]) ).
fof(f1481,plain,
( ~ spl16_24
| spl16_11 ),
inference(avatar_split_clause,[],[f1477,f279,f354]) ).
fof(f1482,plain,
( aScalar0(xP)
| ~ aScalar0(xE)
| ~ aScalar0(xH) ),
inference(forward_demodulation,[],[f1475,f616]) ).
fof(f1486,plain,
( ~ spl16_26
| ~ spl16_28
| spl16_4 ),
inference(avatar_split_clause,[],[f1471,f248,f373,f364]) ).
fof(f1487,plain,
( ~ spl16_25
| ~ spl16_24
| spl16_12 ),
inference(avatar_split_clause,[],[f1470,f283,f354,f359]) ).
fof(f1488,plain,
( ~ spl16_25
| spl16_17 ),
inference(avatar_split_clause,[],[f1478,f305,f359]) ).
fof(f1489,plain,
( ~ spl16_29
| ~ spl16_27
| spl16_10 ),
inference(avatar_split_clause,[],[f1468,f274,f368,f380]) ).
fof(f1492,plain,
( ~ spl16_24
| ~ spl16_25
| spl16_61 ),
inference(avatar_split_clause,[],[f1482,f623,f359,f354]) ).
fof(f1589,definition,
( spl16_171
<=> sdtlseqdt0(sF8,sF15) ),
introduced(definition,[new_symbols(definition,[spl16_171])],[avatar_definition]) ).
fof(f1869,plain,
spl16_69,
inference(avatar_split_clause,[],[f151,f687]) ).
fof(f2266,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sF6)),sdtpldt0(sdtasdt0(xC,xD),sdtpldt0(sdtpldt0(xR,xS),sF6))),
inference(forward_demodulation,[],[f156,f207]) ).
fof(f2267,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(sdtpldt0(xP,xP),sF6)),sdtpldt0(sF9,sdtpldt0(sdtpldt0(xR,xS),sF6))),
inference(forward_demodulation,[],[f2266,f213]) ).
fof(f2268,plain,
sdtlseqdt0(sdtpldt0(sdtasdt0(xE,xE),sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(sdtpldt0(xR,xS),sF6))),
inference(forward_demodulation,[],[f2267,f845]) ).
fof(f2269,plain,
sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(sdtpldt0(xR,xS),sF6))),
inference(forward_demodulation,[],[f2268,f199]) ).
fof(f2272,plain,
( sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(xR,sdtpldt0(xS,sF6))))
| ~ aScalar0(xR)
| ~ aScalar0(xS)
| ~ aScalar0(sF6) ),
inference(superposition,[],[f2269,f187]) ).
fof(f2296,definition,
( spl16_263
<=> sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(xR,sdtpldt0(xS,sF6)))) ),
introduced(definition,[new_symbols(definition,[spl16_263])],[avatar_definition]) ).
fof(f2298,plain,
( sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(xR,sdtpldt0(xS,sF6))))
| ~ spl16_263 ),
inference(avatar_component_clause,[],[f2296]) ).
fof(f2299,plain,
( ~ spl16_11
| ~ spl16_69
| ~ spl16_161
| spl16_263 ),
inference(avatar_split_clause,[],[f2272,f2296,f1299,f687,f279]) ).
fof(f3004,definition,
( spl16_368
<=> aScalar0(xB) ),
introduced(definition,[new_symbols(definition,[spl16_368])],[avatar_definition]) ).
fof(f3005,plain,
( aScalar0(xB)
| ~ spl16_368 ),
inference(avatar_component_clause,[],[f3004]) ).
fof(f3070,plain,
! [X0] :
( sdtasdt0(xF,X0) = sdtasdt0(xA,sdtasdt0(xA,X0))
| ~ aScalar0(xA)
| ~ aScalar0(xA)
| ~ aScalar0(X0) ),
inference(superposition,[],[f185,f140]) ).
fof(f3078,plain,
! [X0] :
( sdtasdt0(xF,X0) = sdtasdt0(xA,sdtasdt0(xA,X0))
| ~ aScalar0(xA)
| ~ aScalar0(X0) ),
inference(duplicate_literal_removal,[],[f3070]) ).
fof(f3089,definition,
( spl16_382
<=> aScalar0(xA) ),
introduced(definition,[new_symbols(definition,[spl16_382])],[avatar_definition]) ).
fof(f3111,definition,
( spl16_387
<=> ! [X0] :
( sdtasdt0(xF,X0) = sdtasdt0(xA,sdtasdt0(xA,X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_387])],[avatar_definition]) ).
fof(f3112,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtasdt0(xF,X0) = sdtasdt0(xA,sdtasdt0(xA,X0)) )
| ~ spl16_387 ),
inference(avatar_component_clause,[],[f3111]) ).
fof(f3113,plain,
( ~ spl16_382
| spl16_387 ),
inference(avatar_split_clause,[],[f3078,f3111,f3089]) ).
fof(f3242,plain,
( ! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(X0,xP))
| ~ aScalar0(X0)
| ~ aScalar0(xP)
| ~ aScalar0(X0) )
| ~ spl16_3
| ~ spl16_65 ),
inference(superposition,[],[f659,f236]) ).
fof(f3269,plain,
( ! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(X0,xP))
| ~ aScalar0(X0)
| ~ aScalar0(xP) )
| ~ spl16_3
| ~ spl16_65 ),
inference(duplicate_literal_removal,[],[f3242]) ).
fof(f3335,definition,
( spl16_428
<=> ! [X0] :
( sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(X0,xP))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_428])],[avatar_definition]) ).
fof(f3336,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(sF4,X0) = sdtpldt0(sF2,sdtpldt0(X0,xP)) )
| ~ spl16_428 ),
inference(avatar_component_clause,[],[f3335]) ).
fof(f3338,plain,
( ~ spl16_61
| spl16_428
| ~ spl16_3
| ~ spl16_65 ),
inference(avatar_split_clause,[],[f3269,f658,f235,f3335,f623]) ).
fof(f3963,plain,
! [X0] :
( sdtasdt0(xH,X0) = sdtasdt0(xA,sdtasdt0(xB,X0))
| ~ aScalar0(xA)
| ~ aScalar0(xB)
| ~ aScalar0(X0) ),
inference(superposition,[],[f185,f144]) ).
fof(f3975,definition,
( spl16_516
<=> ! [X0] :
( sdtasdt0(xH,X0) = sdtasdt0(xA,sdtasdt0(xB,X0))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_516])],[avatar_definition]) ).
fof(f3976,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtasdt0(xH,X0) = sdtasdt0(xA,sdtasdt0(xB,X0)) )
| ~ spl16_516 ),
inference(avatar_component_clause,[],[f3975]) ).
fof(f3977,plain,
( ~ spl16_368
| ~ spl16_382
| spl16_516 ),
inference(avatar_split_clause,[],[f3963,f3975,f3089,f3004]) ).
fof(f4404,plain,
( ! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(X0,xR))
| ~ aScalar0(X0)
| ~ aScalar0(xR)
| ~ aScalar0(X0) )
| ~ spl16_3
| ~ spl16_162 ),
inference(superposition,[],[f1315,f236]) ).
fof(f4436,plain,
( ! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(X0,xR))
| ~ aScalar0(X0)
| ~ aScalar0(xR) )
| ~ spl16_3
| ~ spl16_162 ),
inference(duplicate_literal_removal,[],[f4404]) ).
fof(f4518,definition,
( spl16_608
<=> ! [X0] :
( sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(X0,xR))
| ~ aScalar0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl16_608])],[avatar_definition]) ).
fof(f4519,plain,
( ! [X0] :
( ~ aScalar0(X0)
| sdtpldt0(sF11,X0) = sdtpldt0(sF9,sdtpldt0(X0,xR)) )
| ~ spl16_608 ),
inference(avatar_component_clause,[],[f4518]) ).
fof(f4521,plain,
( ~ spl16_161
| spl16_608
| ~ spl16_3
| ~ spl16_162 ),
inference(avatar_split_clause,[],[f4436,f1314,f235,f4518,f1299]) ).
fof(f7851,definition,
( spl16_1112
<=> sF6 = sF13 ),
introduced(definition,[new_symbols(definition,[spl16_1112])],[avatar_definition]) ).
fof(f7853,plain,
( sF6 = sF13
| ~ spl16_1112 ),
inference(avatar_component_clause,[],[f7851]) ).
fof(f20187,plain,
~ spl16_171,
inference(avatar_split_clause,[],[f226,f1589]) ).
fof(f26018,plain,
( sdtpldt0(sF4,sF7) = sdtpldt0(sF2,sdtpldt0(sF7,xP))
| ~ spl16_13
| ~ spl16_428 ),
inference(resolution,[],[f3336,f289]) ).
fof(f26025,plain,
( sF8 = sdtpldt0(sF2,sdtpldt0(sF7,xP))
| ~ spl16_13
| ~ spl16_428 ),
inference(forward_demodulation,[],[f26018,f211]) ).
fof(f26030,plain,
( sF8 = sdtpldt0(sF2,sdtpldt0(xP,sF7))
| ~ aScalar0(sF7)
| ~ aScalar0(xP)
| ~ spl16_3
| ~ spl16_13
| ~ spl16_428 ),
inference(superposition,[],[f26025,f236]) ).
fof(f26196,definition,
( spl16_3568
<=> sF8 = sdtpldt0(sF2,sdtpldt0(xP,sF7)) ),
introduced(definition,[new_symbols(definition,[spl16_3568])],[avatar_definition]) ).
fof(f26198,plain,
( sF8 = sdtpldt0(sF2,sdtpldt0(xP,sF7))
| ~ spl16_3568 ),
inference(avatar_component_clause,[],[f26196]) ).
fof(f26200,plain,
( ~ spl16_61
| ~ spl16_13
| spl16_3568
| ~ spl16_3
| ~ spl16_13
| ~ spl16_428 ),
inference(avatar_split_clause,[],[f26030,f3335,f287,f235,f26196,f287,f623]) ).
fof(f33582,plain,
( sdtpldt0(sF11,sF14) = sdtpldt0(sF9,sdtpldt0(sF14,xR))
| ~ spl16_6
| ~ spl16_608 ),
inference(resolution,[],[f4519,f258]) ).
fof(f33584,plain,
( sF15 = sdtpldt0(sF9,sdtpldt0(sF14,xR))
| ~ spl16_6
| ~ spl16_608 ),
inference(forward_demodulation,[],[f33582,f225]) ).
fof(f33589,plain,
( sF15 = sdtpldt0(sF9,sdtpldt0(xR,sF14))
| ~ aScalar0(sF14)
| ~ aScalar0(xR)
| ~ spl16_3
| ~ spl16_6
| ~ spl16_608 ),
inference(superposition,[],[f33584,f236]) ).
fof(f33767,definition,
( spl16_4425
<=> sF15 = sdtpldt0(sF9,sdtpldt0(xR,sF14)) ),
introduced(definition,[new_symbols(definition,[spl16_4425])],[avatar_definition]) ).
fof(f33769,plain,
( sF15 = sdtpldt0(sF9,sdtpldt0(xR,sF14))
| ~ spl16_4425 ),
inference(avatar_component_clause,[],[f33767]) ).
fof(f33771,plain,
( ~ spl16_161
| ~ spl16_6
| spl16_4425
| ~ spl16_3
| ~ spl16_6
| ~ spl16_608 ),
inference(avatar_split_clause,[],[f33589,f4518,f256,f235,f33767,f256,f1299]) ).
fof(f43340,plain,
spl16_382,
inference(avatar_split_clause,[],[f131,f3089]) ).
fof(f44024,plain,
( sdtasdt0(xF,xG) = sdtasdt0(xA,sdtasdt0(xA,xG))
| ~ spl16_26
| ~ spl16_387 ),
inference(resolution,[],[f3112,f365]) ).
fof(f44041,plain,
( sF13 = sdtasdt0(xA,sdtasdt0(xA,xG))
| ~ spl16_26
| ~ spl16_387 ),
inference(forward_demodulation,[],[f44024,f221]) ).
fof(f47980,plain,
spl16_368,
inference(avatar_split_clause,[],[f133,f3004]) ).
fof(f49275,plain,
( sdtasdt0(xH,xB) = sdtasdt0(xA,sdtasdt0(xB,xB))
| ~ spl16_368
| ~ spl16_516 ),
inference(resolution,[],[f3976,f3005]) ).
fof(f49281,plain,
( sdtasdt0(xH,xH) = sdtasdt0(xA,sdtasdt0(xB,xH))
| ~ spl16_24
| ~ spl16_516 ),
inference(resolution,[],[f3976,f355]) ).
fof(f49297,plain,
( sF6 = sdtasdt0(xA,sdtasdt0(xB,xH))
| ~ spl16_24
| ~ spl16_516 ),
inference(forward_demodulation,[],[f49281,f207]) ).
fof(f49301,plain,
( sdtasdt0(xH,xB) = sdtasdt0(xA,xG)
| ~ spl16_368
| ~ spl16_516 ),
inference(forward_demodulation,[],[f49275,f142]) ).
fof(f49308,plain,
( sF6 = sdtasdt0(xA,sdtasdt0(xH,xB))
| ~ aScalar0(xB)
| ~ aScalar0(xH)
| ~ spl16_2
| ~ spl16_24
| ~ spl16_516 ),
inference(superposition,[],[f49297,f232]) ).
fof(f49422,definition,
( spl16_5928
<=> sF6 = sdtasdt0(xA,sdtasdt0(xH,xB)) ),
introduced(definition,[new_symbols(definition,[spl16_5928])],[avatar_definition]) ).
fof(f49424,plain,
( sF6 = sdtasdt0(xA,sdtasdt0(xH,xB))
| ~ spl16_5928 ),
inference(avatar_component_clause,[],[f49422]) ).
fof(f49426,plain,
( ~ spl16_24
| ~ spl16_368
| spl16_5928
| ~ spl16_2
| ~ spl16_24
| ~ spl16_516 ),
inference(avatar_split_clause,[],[f49308,f3975,f354,f231,f49422,f3004,f354]) ).
fof(f50541,plain,
( sF13 = sdtasdt0(xA,sdtasdt0(xH,xB))
| ~ spl16_26
| ~ spl16_368
| ~ spl16_387
| ~ spl16_516 ),
inference(superposition,[],[f44041,f49301]) ).
fof(f50664,plain,
( sF6 = sF13
| ~ spl16_26
| ~ spl16_368
| ~ spl16_387
| ~ spl16_516
| ~ spl16_5928 ),
inference(forward_demodulation,[],[f50541,f49424]) ).
fof(f50806,plain,
( spl16_1112
| ~ spl16_26
| ~ spl16_368
| ~ spl16_387
| ~ spl16_516
| ~ spl16_5928 ),
inference(avatar_split_clause,[],[f50664,f49422,f3975,f3111,f3004,f364,f7851]) ).
fof(f50811,plain,
( sF14 = sdtpldt0(xS,sF6)
| ~ spl16_1112 ),
inference(superposition,[],[f707,f7853]) ).
fof(f51202,plain,
( sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sdtpldt0(sF9,sdtpldt0(xR,sF14)))
| ~ spl16_263
| ~ spl16_1112 ),
inference(superposition,[],[f2298,f50811]) ).
fof(f51302,plain,
( sdtlseqdt0(sdtpldt0(sF2,sdtpldt0(xP,sF7)),sF15)
| ~ spl16_263
| ~ spl16_1112
| ~ spl16_4425 ),
inference(forward_demodulation,[],[f51202,f33769]) ).
fof(f51304,plain,
( sdtlseqdt0(sF8,sF15)
| ~ spl16_263
| ~ spl16_1112
| ~ spl16_3568
| ~ spl16_4425 ),
inference(forward_demodulation,[],[f51302,f26198]) ).
fof(f52244,plain,
( spl16_171
| ~ spl16_263
| ~ spl16_1112
| ~ spl16_3568
| ~ spl16_4425 ),
inference(avatar_split_clause,[],[f51304,f33767,f26196,f7851,f2296,f1589]) ).
cnf(s1,plain,
( spl16_1
| spl16_2 ),
inference(sat_conversion,[],[f233]) ).
cnf(s2,plain,
( spl16_1
| spl16_3 ),
inference(sat_conversion,[],[f237]) ).
cnf(s23,plain,
spl16_29,
inference(sat_conversion,[],[f401]) ).
cnf(s24,plain,
spl16_27,
inference(sat_conversion,[],[f402]) ).
cnf(s70,plain,
( ~ spl16_17
| ~ spl16_61
| spl16_65 ),
inference(sat_conversion,[],[f660]) ).
cnf(s191,plain,
( ~ spl16_10
| ~ spl16_161
| spl16_162 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s198,plain,
spl16_161,
inference(sat_conversion,[],[f1333]) ).
cnf(s208,plain,
~ spl16_1,
inference(sat_conversion,[],[f1367]) ).
cnf(s219,plain,
spl16_24,
inference(sat_conversion,[],[f1378]) ).
cnf(s220,plain,
spl16_26,
inference(sat_conversion,[],[f1379]) ).
cnf(s221,plain,
spl16_28,
inference(sat_conversion,[],[f1380]) ).
cnf(s222,plain,
spl16_25,
inference(sat_conversion,[],[f1381]) ).
cnf(s252,plain,
( ~ spl16_11
| ~ spl16_12
| spl16_13 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s257,plain,
( ~ spl16_4
| spl16_6
| ~ spl16_69 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s260,plain,
( spl16_11
| ~ spl16_24 ),
inference(sat_conversion,[],[f1481]) ).
cnf(s263,plain,
( spl16_4
| ~ spl16_26
| ~ spl16_28 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s264,plain,
( spl16_12
| ~ spl16_24
| ~ spl16_25 ),
inference(sat_conversion,[],[f1487]) ).
cnf(s265,plain,
( spl16_17
| ~ spl16_25 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s266,plain,
( spl16_10
| ~ spl16_27
| ~ spl16_29 ),
inference(sat_conversion,[],[f1489]) ).
cnf(s268,plain,
( ~ spl16_24
| ~ spl16_25
| spl16_61 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s319,plain,
spl16_69,
inference(sat_conversion,[],[f1869]) ).
cnf(s376,plain,
( ~ spl16_11
| ~ spl16_69
| ~ spl16_161
| spl16_263 ),
inference(sat_conversion,[],[f2299]) ).
cnf(s501,plain,
( ~ spl16_382
| spl16_387 ),
inference(sat_conversion,[],[f3113]) ).
cnf(s544,plain,
( ~ spl16_3
| ~ spl16_61
| ~ spl16_65
| spl16_428 ),
inference(sat_conversion,[],[f3338]) ).
cnf(s643,plain,
( ~ spl16_368
| ~ spl16_382
| spl16_516 ),
inference(sat_conversion,[],[f3977]) ).
cnf(s744,plain,
( ~ spl16_3
| ~ spl16_161
| ~ spl16_162
| spl16_608 ),
inference(sat_conversion,[],[f4521]) ).
cnf(s3667,plain,
~ spl16_171,
inference(sat_conversion,[],[f20187]) ).
cnf(s4819,plain,
( ~ spl16_13
| ~ spl16_3
| ~ spl16_13
| ~ spl16_61
| ~ spl16_428
| spl16_3568 ),
inference(sat_conversion,[],[f26200]) ).
cnf(s4820,plain,
( ~ spl16_3
| ~ spl16_13
| ~ spl16_61
| ~ spl16_428
| spl16_3568 ),
inference(rat,[],[s4819]) ).
cnf(s6333,plain,
( ~ spl16_6
| ~ spl16_3
| ~ spl16_6
| ~ spl16_161
| ~ spl16_608
| spl16_4425 ),
inference(sat_conversion,[],[f33771]) ).
cnf(s6334,plain,
( ~ spl16_3
| ~ spl16_6
| ~ spl16_161
| ~ spl16_608
| spl16_4425 ),
inference(rat,[],[s6333]) ).
cnf(s8259,plain,
spl16_382,
inference(sat_conversion,[],[f43340]) ).
cnf(s9274,plain,
spl16_368,
inference(sat_conversion,[],[f47980]) ).
cnf(s9602,plain,
( ~ spl16_24
| ~ spl16_2
| ~ spl16_24
| ~ spl16_368
| ~ spl16_516
| spl16_5928 ),
inference(sat_conversion,[],[f49426]) ).
cnf(s9603,plain,
( ~ spl16_2
| ~ spl16_24
| ~ spl16_368
| ~ spl16_516
| spl16_5928 ),
inference(rat,[],[s9602]) ).
cnf(s9837,plain,
( ~ spl16_26
| ~ spl16_368
| ~ spl16_387
| ~ spl16_516
| spl16_1112
| ~ spl16_5928 ),
inference(sat_conversion,[],[f50806]) ).
cnf(s10383,plain,
( spl16_171
| ~ spl16_263
| ~ spl16_1112
| ~ spl16_3568
| ~ spl16_4425 ),
inference(sat_conversion,[],[f52244]) ).
cnf(s10537,plain,
spl16_516,
inference(rat,[],[s643,s8259,s9274]) ).
cnf(s10548,plain,
spl16_387,
inference(rat,[],[s501,s8259]) ).
cnf(s10591,plain,
( ~ spl16_4
| spl16_6 ),
inference(rat,[],[s257,s319]) ).
cnf(s10598,plain,
spl16_17,
inference(rat,[],[s265,s222]) ).
cnf(s10683,plain,
spl16_4,
inference(rat,[],[s263,s221,s220]) ).
cnf(s10716,plain,
spl16_6,
inference(rat,[],[s10591,s10683]) ).
cnf(s10729,plain,
spl16_61,
inference(rat,[],[s268,s222,s219]) ).
cnf(s10730,plain,
spl16_12,
inference(rat,[],[s264,s222,s219]) ).
cnf(s10731,plain,
spl16_11,
inference(rat,[],[s260,s219]) ).
cnf(s10803,plain,
spl16_13,
inference(rat,[],[s252,s10730,s10731]) ).
cnf(s10873,plain,
spl16_263,
inference(rat,[],[s376,s10731,s319,s198]) ).
cnf(s10880,plain,
( ~ spl16_10
| spl16_162 ),
inference(rat,[],[s191,s198]) ).
cnf(s11274,plain,
spl16_65,
inference(rat,[],[s70,s10729,s10598]) ).
cnf(s11528,plain,
spl16_10,
inference(rat,[],[s266,s24,s23]) ).
cnf(s11592,plain,
spl16_162,
inference(rat,[],[s10880,s11528]) ).
cnf(s11709,plain,
spl16_3,
inference(rat,[],[s2,s208]) ).
cnf(s11763,plain,
spl16_608,
inference(rat,[],[s744,s11592,s198,s11709]) ).
cnf(s11773,plain,
spl16_428,
inference(rat,[],[s544,s11274,s10729,s11709]) ).
cnf(s11835,plain,
spl16_4425,
inference(rat,[],[s6334,s11709,s198,s10716,s11763]) ).
cnf(s11854,plain,
spl16_3568,
inference(rat,[],[s4820,s11709,s10803,s10729,s11773]) ).
cnf(s11932,plain,
~ spl16_1112,
inference(rat,[],[s10383,s11835,s10873,s3667,s11854]) ).
cnf(s12031,plain,
~ spl16_5928,
inference(rat,[],[s9837,s220,s10548,s10537,s9274,s11932]) ).
cnf(s12069,plain,
~ spl16_2,
inference(rat,[],[s9603,s219,s10537,s9274,s12031]) ).
cnf(s12091,plain,
$false,
inference(rat,[],[s1,s12069,s208]) ).
fof(f52316,plain,
$false,
inference(avatar_sat_refutation,[],[s12091]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG078+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n004.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 23:09:23 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.60/2.89 % (3992145)Detected formulas, will run a generic FOF schedule.
% 13.60/2.89 % (3992151)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=4243537069:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.60/2.89 % (3992153)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2334783173:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.60/2.89 % (3992152)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3774742936:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.60/2.89 % (3992156)dis-21_1_sil=8000:lcm=predicate:random_seed=29762759:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.60/2.89 % (3992150)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1779349258:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.60/2.89 % (3992154)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=963020866:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.60/2.89 % (3992155)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3432453219:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.60/2.89 % (3992153)Instruction limit reached!
% 13.60/2.89 % (3992153)------------------------------
% 13.60/2.89 % (3992153)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.89 % (3992153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.89 % (3992153)CaDiCaL version: 2.1.3
% 13.60/2.89 % (3992153)Termination reason: Instruction limit
% 13.60/2.89 % (3992153)Termination phase: Saturation
% 13.60/2.89 % (3992153)Time elapsed: 0.052 s
% 13.60/2.89 % (3992153)Peak memory usage: 89 MB
% 13.60/2.89 % (3992153)Instructions burned: 110 (million)
% 13.60/2.89 % (3992156)Instruction limit reached!
% 13.60/2.89 % (3992156)------------------------------
% 13.60/2.89 % (3992156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.89 % (3992156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.89 % (3992156)CaDiCaL version: 2.1.3
% 13.60/2.89 % (3992156)Termination reason: Instruction limit
% 13.60/2.89 % (3992156)Termination phase: Saturation
% 13.60/2.89 % (3992156)Time elapsed: 0.057 s
% 13.60/2.89 % (3992156)Peak memory usage: 89 MB
% 13.60/2.89 % (3992156)Instructions burned: 130 (million)
% 13.60/2.89 % (3992154)Instruction limit reached!
% 13.60/2.89 % (3992154)------------------------------
% 13.60/2.89 % (3992154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.89 % (3992154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.89 % (3992154)CaDiCaL version: 2.1.3
% 13.60/2.89 % (3992154)Termination reason: Instruction limit
% 13.60/2.89 % (3992154)Termination phase: Saturation
% 13.60/2.89 % (3992154)Time elapsed: 0.065 s
% 13.60/2.89 % (3992154)Peak memory usage: 88 MB
% 13.60/2.89 % (3992154)Instructions burned: 120 (million)
% 13.60/2.89 % (3992155)Instruction limit reached!
% 13.60/2.89 % (3992155)------------------------------
% 13.60/2.89 % (3992155)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.89 % (3992155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.89 % (3992155)CaDiCaL version: 2.1.3
% 13.60/2.89 % (3992155)Termination reason: Instruction limit
% 13.60/2.89 % (3992155)Termination phase: Saturation
% 13.60/2.89 % (3992155)Time elapsed: 0.089 s
% 13.60/2.89 % (3992155)Peak memory usage: 90 MB
% 13.60/2.89 % (3992155)Instructions burned: 141 (million)
% 13.60/2.89 % (3992165)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3401777059:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.60/2.89 % (3992164)lrs+10_1_sil=8000:sp=occurrence:random_seed=2851699946:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.60/2.89 % (3992166)lrs+1011_1_sil=32000:sp=occurrence:random_seed=79657803:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.60/2.89 % (3992167)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1740095871:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.60/2.89 % (3992165)Instruction limit reached!
% 20.41/3.80 % (3992165)------------------------------
% 20.41/3.80 % (3992165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992165)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992165)Termination reason: Instruction limit
% 20.41/3.80 % (3992165)Termination phase: Saturation
% 20.41/3.80 % (3992165)Time elapsed: 0.073 s
% 20.41/3.80 % (3992165)Peak memory usage: 92 MB
% 20.41/3.80 % (3992165)Instructions burned: 158 (million)
% 20.41/3.80 % (3992167)Instruction limit reached!
% 20.41/3.80 % (3992167)------------------------------
% 20.41/3.80 % (3992167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992167)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992167)Termination reason: Instruction limit
% 20.41/3.80 % (3992167)Termination phase: Saturation
% 20.41/3.80 % (3992167)Time elapsed: 0.116 s
% 20.41/3.80 % (3992167)Peak memory usage: 96 MB
% 20.41/3.80 % (3992167)Instructions burned: 248 (million)
% 20.41/3.80 % (3992164)Instruction limit reached!
% 20.41/3.80 % (3992164)------------------------------
% 20.41/3.80 % (3992164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992164)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992164)Termination reason: Instruction limit
% 20.41/3.80 % (3992164)Termination phase: Saturation
% 20.41/3.80 % (3992164)Time elapsed: 0.170 s
% 20.41/3.80 % (3992164)Peak memory usage: 93 MB
% 20.41/3.80 % (3992164)Instructions burned: 286 (million)
% 20.41/3.80 % (3992166)Instruction limit reached!
% 20.41/3.80 % (3992166)------------------------------
% 20.41/3.80 % (3992166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992166)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992166)Termination reason: Instruction limit
% 20.41/3.80 % (3992166)Termination phase: Saturation
% 20.41/3.80 % (3992166)Time elapsed: 0.196 s
% 20.41/3.80 % (3992166)Peak memory usage: 93 MB
% 20.41/3.80 % (3992166)Instructions burned: 326 (million)
% 20.41/3.80 % (3992172)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2686309995:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 20.41/3.80 % (3992173)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=38516508:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 20.41/3.80 % (3992174)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1027841568:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 20.41/3.80 % (3992175)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1280480012:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 20.41/3.80 % (3992174)Instruction limit reached!
% 20.41/3.80 % (3992174)------------------------------
% 20.41/3.80 % (3992174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992174)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992174)Termination reason: Instruction limit
% 20.41/3.80 % (3992174)Termination phase: Saturation
% 20.41/3.80 % (3992174)Time elapsed: 0.072 s
% 20.41/3.80 % (3992174)Peak memory usage: 91 MB
% 20.41/3.80 % (3992174)Instructions burned: 114 (million)
% 20.41/3.80 % (3992172)Instruction limit reached!
% 20.41/3.80 % (3992172)------------------------------
% 20.41/3.80 % (3992172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992172)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992172)Termination reason: Instruction limit
% 20.41/3.80 % (3992172)Termination phase: Saturation
% 20.41/3.80 % (3992172)Time elapsed: 0.163 s
% 20.41/3.80 % (3992172)Peak memory usage: 90 MB
% 20.41/3.80 % (3992172)Instructions burned: 295 (million)
% 20.41/3.80 % (3992175)Instruction limit reached!
% 20.41/3.80 % (3992175)------------------------------
% 20.41/3.80 % (3992175)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.41/3.80 % (3992175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.41/3.80 % (3992175)CaDiCaL version: 2.1.3
% 20.41/3.80 % (3992175)Termination reason: Instruction limit
% 20.41/3.80 % (3992175)Termination phase: Saturation
% 58.41/9.09 % (3992175)Time elapsed: 0.064 s
% 58.41/9.09 % (3992175)Peak memory usage: 89 MB
% 58.41/9.09 % (3992175)Instructions burned: 127 (million)
% 58.41/9.09 % (3992180)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1320344440:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 58.41/9.09 % (3992181)lrs+10_1_sil=8000:sp=occurrence:random_seed=756166002:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 58.41/9.09 % (3992182)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=15624930:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 58.41/9.09 % (3992180)Instruction limit reached!
% 58.41/9.09 % (3992180)------------------------------
% 58.41/9.09 % (3992180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.41/9.09 % (3992180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.41/9.09 % (3992180)CaDiCaL version: 2.1.3
% 58.41/9.09 % (3992180)Termination reason: Instruction limit
% 58.41/9.09 % (3992180)Termination phase: Saturation
% 58.41/9.09 % (3992180)Time elapsed: 0.062 s
% 58.41/9.09 % (3992180)Peak memory usage: 89 MB
% 58.41/9.09 % (3992180)Instructions burned: 114 (million)
% 58.41/9.09 % (3992186)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4090756554:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 58.41/9.09 % (3992182)Instruction limit reached!
% 58.41/9.09 % (3992182)------------------------------
% 58.41/9.09 % (3992182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.41/9.09 % (3992182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.41/9.09 % (3992182)CaDiCaL version: 2.1.3
% 58.41/9.09 % (3992182)Termination reason: Instruction limit
% 58.41/9.09 % (3992182)Termination phase: Saturation
% 58.41/9.09 % (3992182)Time elapsed: 0.245 s
% 58.41/9.09 % (3992182)Peak memory usage: 94 MB
% 58.41/9.09 % (3992182)Instructions burned: 439 (million)
% 58.41/9.09 % (3992188)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=119413917:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 58.41/9.09 % (3992181)Instruction limit reached!
% 58.41/9.09 % (3992181)------------------------------
% 58.41/9.09 % (3992181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.41/9.09 % (3992181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.41/9.09 % (3992181)CaDiCaL version: 2.1.3
% 58.41/9.09 % (3992181)Termination reason: Instruction limit
% 58.41/9.09 % (3992181)Termination phase: Saturation
% 58.41/9.09 % (3992181)Time elapsed: 0.496 s
% 58.41/9.09 % (3992181)Peak memory usage: 104 MB
% 58.41/9.09 % (3992181)Instructions burned: 907 (million)
% 58.41/9.09 % (3992188)Instruction limit reached!
% 58.41/9.09 % (3992188)------------------------------
% 58.41/9.09 % (3992188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.41/9.09 % (3992188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.41/9.09 % (3992188)CaDiCaL version: 2.1.3
% 58.41/9.09 % (3992188)Termination reason: Instruction limit
% 58.41/9.09 % (3992188)Termination phase: Saturation
% 58.41/9.09 % (3992188)Time elapsed: 0.059 s
% 58.41/9.09 % (3992188)Peak memory usage: 91 MB
% 58.41/9.09 % (3992188)Instructions burned: 135 (million)
% 58.41/9.09 % (3992191)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=105647125:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 58.41/9.09 % (3992190)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=480237293:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 58.41/9.09 % (3992190)Instruction limit reached!
% 58.41/9.09 % (3992190)------------------------------
% 58.41/9.09 % (3992190)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.41/9.09 % (3992190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.41/9.09 % (3992190)CaDiCaL version: 2.1.3
% 58.41/9.09 % (3992190)Termination reason: Instruction limit
% 58.41/9.09 % (3992190)Termination phase: Saturation
% 58.41/9.09 % (3992190)Time elapsed: 0.296 s
% 58.41/9.09 % (3992190)Peak memory usage: 92 MB
% 58.41/9.09 % (3992190)Instructions burned: 593 (million)
% 58.41/9.09 % (3992194)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2627312639:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 77.62/11.94 % (3992173)Instruction limit reached!
% 77.62/11.94 % (3992173)------------------------------
% 77.62/11.94 % (3992173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992173)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992173)Termination reason: Instruction limit
% 77.62/11.94 % (3992173)Termination phase: Saturation
% 77.62/11.94 % (3992173)Time elapsed: 1.407 s
% 77.62/11.94 % (3992173)Peak memory usage: 143 MB
% 77.62/11.94 % (3992173)Instructions burned: 2350 (million)
% 77.62/11.94 % (3992194)Instruction limit reached!
% 77.62/11.94 % (3992194)------------------------------
% 77.62/11.94 % (3992194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992194)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992194)Termination reason: Instruction limit
% 77.62/11.94 % (3992194)Termination phase: Saturation
% 77.62/11.94 % (3992194)Time elapsed: 0.066 s
% 77.62/11.94 % (3992194)Peak memory usage: 91 MB
% 77.62/11.94 % (3992194)Instructions burned: 125 (million)
% 77.62/11.94 % (3992196)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=395428997:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 77.62/11.94 % (3992197)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4090672748:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 77.62/11.94 % (3992197)Instruction limit reached!
% 77.62/11.94 % (3992197)------------------------------
% 77.62/11.94 % (3992197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992197)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992197)Termination reason: Instruction limit
% 77.62/11.94 % (3992197)Termination phase: Saturation
% 77.62/11.94 % (3992197)Time elapsed: 0.071 s
% 77.62/11.94 % (3992197)Peak memory usage: 91 MB
% 77.62/11.94 % (3992197)Instructions burned: 141 (million)
% 77.62/11.94 % (3992196)Instruction limit reached!
% 77.62/11.94 % (3992196)------------------------------
% 77.62/11.94 % (3992196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992196)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992196)Termination reason: Instruction limit
% 77.62/11.94 % (3992196)Termination phase: Saturation
% 77.62/11.94 % (3992196)Time elapsed: 0.073 s
% 77.62/11.94 % (3992196)Peak memory usage: 91 MB
% 77.62/11.94 % (3992196)Instructions burned: 135 (million)
% 77.62/11.94 % (3992201)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1027594507:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 77.62/11.94 % (3992200)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=604231347:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 77.62/11.94 % (3992200)Instruction limit reached!
% 77.62/11.94 % (3992200)------------------------------
% 77.62/11.94 % (3992200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992200)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992200)Termination reason: Instruction limit
% 77.62/11.94 % (3992200)Termination phase: Saturation
% 77.62/11.94 % (3992200)Time elapsed: 0.229 s
% 77.62/11.94 % (3992200)Peak memory usage: 95 MB
% 77.62/11.94 % (3992200)Instructions burned: 432 (million)
% 77.62/11.94 % (3992204)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1426949824:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2972 on theBenchmark for (2972ds/150Mi)
% 77.62/11.94 % (3992204)Instruction limit reached!
% 77.62/11.94 % (3992204)------------------------------
% 77.62/11.94 % (3992204)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.62/11.94 % (3992204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.62/11.94 % (3992204)CaDiCaL version: 2.1.3
% 77.62/11.94 % (3992204)Termination reason: Instruction limit
% 77.62/11.94 % (3992204)Termination phase: Saturation
% 77.62/11.94 % (3992204)Time elapsed: 0.078 s
% 77.62/11.94 % (3992204)Peak memory usage: 92 MB
% 112.87/16.87 % (3992204)Instructions burned: 155 (million)
% 112.87/16.87 % (3992206)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2523465451:i=14155:bd=all_2970 on theBenchmark for (2970ds/14155Mi)
% 112.87/16.87 % (3992186)Instruction limit reached!
% 112.87/16.87 % (3992186)------------------------------
% 112.87/16.87 % (3992186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992186)CaDiCaL version: 2.1.3
% 112.87/16.87 % (3992186)Termination reason: Instruction limit
% 112.87/16.87 % (3992186)Termination phase: Saturation
% 112.87/16.87 % (3992186)Time elapsed: 3.337 s
% 112.87/16.87 % (3992186)Peak memory usage: 166 MB
% 112.87/16.87 % (3992186)Instructions burned: 5203 (million)
% 112.87/16.87 % (3992208)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1721613324:i=667:av=off:fsr=off_2955 on theBenchmark for (2955ds/667Mi)
% 112.87/16.87 % (3992208)Instruction limit reached!
% 112.87/16.87 % (3992208)------------------------------
% 112.87/16.87 % (3992208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992208)CaDiCaL version: 2.1.3
% 112.87/16.87 % (3992208)Termination reason: Instruction limit
% 112.87/16.87 % (3992208)Termination phase: Saturation
% 112.87/16.87 % (3992208)Time elapsed: 0.249 s
% 112.87/16.87 % (3992208)Peak memory usage: 92 MB
% 112.87/16.87 % (3992208)Instructions burned: 670 (million)
% 112.87/16.87 % (3992210)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4025875537:s2a=on:i=185:s2at=1.8:fdi=4_2950 on theBenchmark for (2950ds/185Mi)
% 112.87/16.87 % (3992210)Instruction limit reached!
% 112.87/16.87 % (3992210)------------------------------
% 112.87/16.87 % (3992210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992210)CaDiCaL version: 2.1.3
% 112.87/16.87 % (3992210)Termination reason: Instruction limit
% 112.87/16.87 % (3992210)Termination phase: Saturation
% 112.87/16.87 % (3992210)Time elapsed: 0.093 s
% 112.87/16.87 % (3992210)Peak memory usage: 92 MB
% 112.87/16.87 % (3992210)Instructions burned: 191 (million)
% 112.87/16.87 % (3992212)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2050630879:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2948 on theBenchmark for (2948ds/193Mi)
% 112.87/16.87 % (3992212)Instruction limit reached!
% 112.87/16.87 % (3992212)------------------------------
% 112.87/16.87 % (3992212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992212)CaDiCaL version: 2.1.3
% 112.87/16.87 % (3992212)Termination reason: Instruction limit
% 112.87/16.87 % (3992212)Termination phase: Saturation
% 112.87/16.87 % (3992212)Time elapsed: 0.106 s
% 112.87/16.87 % (3992212)Peak memory usage: 90 MB
% 112.87/16.87 % (3992212)Instructions burned: 194 (million)
% 112.87/16.87 % (3992214)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=1943029656:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2945 on theBenchmark for (2945ds/4850Mi)
% 112.87/16.87 % (3992201)Instruction limit reached!
% 112.87/16.87 % (3992201)------------------------------
% 112.87/16.87 % (3992201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992201)CaDiCaL version: 2.1.3
% 112.87/16.87 % (3992201)Termination reason: Instruction limit
% 112.87/16.87 % (3992201)Termination phase: Saturation
% 112.87/16.87 % (3992201)Time elapsed: 3.788 s
% 112.87/16.87 % (3992201)Peak memory usage: 169 MB
% 112.87/16.87 % (3992201)Instructions burned: 6061 (million)
% 112.87/16.87 % (3992216)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3565438226:i=12111:sd=1:ss=included_2937 on theBenchmark for (2937ds/12111Mi)
% 112.87/16.87 % (3992214)Instruction limit reached!
% 112.87/16.87 % (3992214)------------------------------
% 112.87/16.87 % (3992214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.87/16.87 % (3992214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.87/16.87 % (3992214)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992214)Termination reason: Instruction limit
% 63.88/18.65 % (3992214)Termination phase: Saturation
% 63.88/18.65 % (3992214)Time elapsed: 2.612 s
% 63.88/18.65 % (3992214)Peak memory usage: 105 MB
% 63.88/18.65 % (3992214)Instructions burned: 4851 (million)
% 63.88/18.65 % (3992218)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2424234971:i=319:kws=precedence:fsr=off_2917 on theBenchmark for (2917ds/319Mi)
% 63.88/18.65 % (3992218)Instruction limit reached!
% 63.88/18.65 % (3992218)------------------------------
% 63.88/18.65 % (3992218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992218)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992218)Termination reason: Instruction limit
% 63.88/18.65 % (3992218)Termination phase: Saturation
% 63.88/18.65 % (3992218)Time elapsed: 0.174 s
% 63.88/18.65 % (3992218)Peak memory usage: 94 MB
% 63.88/18.65 % (3992218)Instructions burned: 320 (million)
% 63.88/18.65 % (3992220)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=104548158:i=2064:ep=RST_2914 on theBenchmark for (2914ds/2064Mi)
% 63.88/18.65 % (3992191)Instruction limit reached!
% 63.88/18.65 % (3992191)------------------------------
% 63.88/18.65 % (3992191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992191)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992191)Termination reason: Instruction limit
% 63.88/18.65 % (3992191)Termination phase: Saturation
% 63.88/18.65 % (3992191)Time elapsed: 7.371 s
% 63.88/18.65 % (3992191)Peak memory usage: 256 MB
% 63.88/18.65 % (3992191)Instructions burned: 13193 (million)
% 63.88/18.65 % (3992222)dis-1011_128_sil=32000:random_seed=1324143914:i=3706:ep=RST:av=off_2910 on theBenchmark for (2910ds/3706Mi)
% 63.88/18.65 % (3992220)Instruction limit reached!
% 63.88/18.65 % (3992220)------------------------------
% 63.88/18.65 % (3992220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992220)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992220)Termination reason: Instruction limit
% 63.88/18.65 % (3992220)Termination phase: Saturation
% 63.88/18.65 % (3992220)Time elapsed: 0.996 s
% 63.88/18.65 % (3992220)Peak memory usage: 111 MB
% 63.88/18.65 % (3992220)Instructions burned: 2066 (million)
% 63.88/18.65 % (3992224)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1849426964:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2902 on theBenchmark for (2902ds/757Mi)
% 63.88/18.65 % (3992224)Instruction limit reached!
% 63.88/18.65 % (3992224)------------------------------
% 63.88/18.65 % (3992224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992224)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992224)Termination reason: Instruction limit
% 63.88/18.65 % (3992224)Termination phase: Saturation
% 63.88/18.65 % (3992224)Time elapsed: 0.544 s
% 63.88/18.65 % (3992224)Peak memory usage: 95 MB
% 63.88/18.65 % (3992224)Instructions burned: 758 (million)
% 63.88/18.65 % (3992206)Instruction limit reached!
% 63.88/18.65 % (3992206)------------------------------
% 63.88/18.65 % (3992206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992206)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992206)Termination reason: Instruction limit
% 63.88/18.65 % (3992206)Termination phase: Saturation
% 63.88/18.65 % (3992206)Time elapsed: 7.374 s
% 63.88/18.65 % (3992206)Peak memory usage: 271 MB
% 63.88/18.65 % (3992206)Instructions burned: 14156 (million)
% 63.88/18.65 % (3992226)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3826442821:i=13913:ss=axioms:sgt=8_2895 on theBenchmark for (2895ds/13913Mi)
% 63.88/18.65 % (3992227)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=825012020:i=9925:aac=none_2894 on theBenchmark for (2894ds/9925Mi)
% 63.88/18.65 % (3992222)Instruction limit reached!
% 63.88/18.65 % (3992222)------------------------------
% 63.88/18.65 % (3992222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992222)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992222)Termination reason: Instruction limit
% 63.88/18.65 % (3992222)Termination phase: Saturation
% 63.88/18.65 % (3992222)Time elapsed: 1.951 s
% 63.88/18.65 % (3992222)Peak memory usage: 98 MB
% 63.88/18.65 % (3992222)Instructions burned: 3707 (million)
% 63.88/18.65 % (3992230)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=866605919:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2889 on theBenchmark for (2889ds/2479Mi)
% 63.88/18.65 % (3992230)Instruction limit reached!
% 63.88/18.65 % (3992230)------------------------------
% 63.88/18.65 % (3992230)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992230)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992230)Termination reason: Instruction limit
% 63.88/18.65 % (3992230)Termination phase: Saturation
% 63.88/18.65 % (3992230)Time elapsed: 1.443 s
% 63.88/18.65 % (3992230)Peak memory usage: 108 MB
% 63.88/18.65 % (3992230)Instructions burned: 2479 (million)
% 63.88/18.65 % (3992232)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3000226899:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2872 on theBenchmark for (2872ds/440Mi)
% 63.88/18.65 % (3992216)Instruction limit reached!
% 63.88/18.65 % (3992216)------------------------------
% 63.88/18.65 % (3992216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992216)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992216)Termination reason: Instruction limit
% 63.88/18.65 % (3992216)Termination phase: Saturation
% 63.88/18.65 % (3992216)Time elapsed: 6.436 s
% 63.88/18.65 % (3992216)Peak memory usage: 312 MB
% 63.88/18.65 % (3992216)Instructions burned: 12113 (million)
% 63.88/18.65 % (3992234)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=803605493:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2870 on theBenchmark for (2870ds/11145Mi)
% 63.88/18.65 % (3992232)Instruction limit reached!
% 63.88/18.65 % (3992232)------------------------------
% 63.88/18.65 % (3992232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992232)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992232)Termination reason: Instruction limit
% 63.88/18.65 % (3992232)Termination phase: Saturation
% 63.88/18.65 % (3992232)Time elapsed: 0.238 s
% 63.88/18.65 % (3992232)Peak memory usage: 92 MB
% 63.88/18.65 % (3992232)Instructions burned: 442 (million)
% 63.88/18.65 % (3992236)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=3442294045:cts=off:i=3034:av=off:er=known:fsd=on_2868 on theBenchmark for (2868ds/3034Mi)
% 63.88/18.65 % (3992236)Instruction limit reached!
% 63.88/18.65 % (3992236)------------------------------
% 63.88/18.65 % (3992236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992236)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992236)Termination reason: Instruction limit
% 63.88/18.65 % (3992236)Termination phase: Saturation
% 63.88/18.65 % (3992236)Time elapsed: 1.616 s
% 63.88/18.65 % (3992236)Peak memory usage: 152 MB
% 63.88/18.65 % (3992236)Instructions burned: 3035 (million)
% 63.88/18.65 % (3992238)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=616979193:st=2:s2a=on:i=524:s2at=2:ss=axioms_2851 on theBenchmark for (2851ds/524Mi)
% 63.88/18.65 % (3992238)Instruction limit reached!
% 63.88/18.65 % (3992238)------------------------------
% 63.88/18.65 % (3992238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992238)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992238)Termination reason: Instruction limit
% 63.88/18.65 % (3992238)Termination phase: Saturation
% 63.88/18.65 % (3992238)Time elapsed: 0.236 s
% 63.88/18.65 % (3992238)Peak memory usage: 100 MB
% 63.88/18.65 % (3992238)Instructions burned: 526 (million)
% 63.88/18.65 % (3992240)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=1752212089:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2847 on theBenchmark for (2847ds/1016Mi)
% 63.88/18.65 % (3992240)Instruction limit reached!
% 63.88/18.65 % (3992240)------------------------------
% 63.88/18.65 % (3992240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992240)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992240)Termination reason: Instruction limit
% 63.88/18.65 % (3992240)Termination phase: Saturation
% 63.88/18.65 % (3992240)Time elapsed: 0.560 s
% 63.88/18.65 % (3992240)Peak memory usage: 133 MB
% 63.88/18.65 % (3992240)Instructions burned: 1018 (million)
% 63.88/18.65 % (3992242)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=3936751866:i=14123:bd=preordered:ins=4_2839 on theBenchmark for (2839ds/14123Mi)
% 63.88/18.65 % (3992227)Instruction limit reached!
% 63.88/18.65 % (3992227)------------------------------
% 63.88/18.65 % (3992227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.88/18.65 % (3992227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.88/18.65 % (3992227)CaDiCaL version: 2.1.3
% 63.88/18.65 % (3992227)Termination reason: Instruction limit
% 63.88/18.65 % (3992227)Termination phase: Saturation
% 63.88/18.65 % (3992227)Time elapsed: 5.868 s
% 63.88/18.65 % (3992227)Peak memory usage: 208 MB
% 63.88/18.65 % (3992227)Instructions burned: 9926 (million)
% 63.88/18.65 % (3992244)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1917486879:i=5781:kws=precedence:bd=all:rawr=on_2834 on theBenchmark for (2834ds/5781Mi)
% 63.88/18.65 % (3992234)First to succeed.
% 63.88/18.65 % (3992234)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3992145"
% 63.88/18.65 % (3992234)Refutation found. Thanks to Tanya!
% 63.88/18.65 % SZS status Theorem for theBenchmark
% 63.88/18.65 % SZS output start Proof for theBenchmark
% See solution above
% 126.60/18.84 % (3992234)------------------------------
% 126.60/18.84 % (3992234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 126.60/18.84 % (3992234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.60/18.84 % (3992234)CaDiCaL version: 2.1.3
% 126.60/18.84 % (3992234)Termination reason: Refutation
% 126.60/18.84 % (3992234)Time elapsed: 4.380 s
% 126.60/18.84 % (3992234)Peak memory usage: 189 MB
% 126.60/18.84 % (3992234)Instructions burned: 7353 (million)
% 126.60/18.84 % (3992234)------------------------------
% 126.60/18.84 % (3992234)------------------------------
% 126.60/18.84 % (3992145)Success in time 17.794 s
% 126.60/18.84 % Vampire exiting
%------------------------------------------------------------------------------