%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX189-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 01:46:06 PM UTC 2026
% Result : Unsatisfiable 87.44s 26.23s
% Output : Refutation 181.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 49
% Syntax : Number of formulae : 160 ( 100 unt; 19 def)
% Number of atoms : 270 ( 138 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 238 ( 128 ~; 100 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 9 con; 0-3 aty)
% Number of variables : 164 ( 0 sgn 164 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X2,X0,X1] : aux(y(X0,X1),X2,bfalse) = x(opt(y(X0,X1)),opt(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_003) ).
fof(f6,axiom,
! [X0,X1] : fail2(X0,X1) = aux(X0,X1,eq2(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_005) ).
fof(f12,axiom,
! [X2,X0,X1] : fail1(y(X0,X1),X2) = fail2(y(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
fof(f17,axiom,
! [X2,X0,X1] : fail(X0,y(X1,X2)) = fail1(X0,y(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
fof(f19,axiom,
! [X0,X1] : fail4(X0,X1) = y(opt(X0),opt(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
fof(f26,axiom,
! [X0] : fail32(x2,X0) = fail4(x2,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_025) ).
fof(f28,axiom,
! [X0] : fail22(X0,n(s(z))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_027) ).
fof(f30,axiom,
! [X2,X0,X1] : fail22(X0,x(X1,X2)) = fail32(X0,x(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
fof(f34,axiom,
! [X0] : fail12(n(s(z)),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_033) ).
fof(f38,axiom,
! [X0] : fail12(x2,X0) = fail22(x2,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
fof(f39,axiom,
! [X0,X1] : fail3(X0,n(s(X1))) = fail12(X0,n(s(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_038) ).
fof(f42,axiom,
! [X2,X0,X1] : fail3(X0,x(X1,X2)) = fail12(X0,x(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_040) ).
fof(f43,axiom,
! [X2,X0,X1] : fail3(X0,y(X1,X2)) = fail12(X0,y(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
fof(f44,axiom,
! [X0] : fail3(X0,x2) = fail12(X0,x2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
fof(f45,axiom,
! [X0] : impl(btrue,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
fof(f51,axiom,
! [X0,X1] : d(y(X0,X1)) = x(y(d(X0),X1),y(X0,d(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
fof(f52,axiom,
d(x2) = n(s(z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
fof(f53,plain,
n(s(z)) = d(x2),
inference(reorient_equations,[],[f52]) ).
fof(f62,axiom,
! [X2,X0,X1] : opt(x(y(X0,X1),X2)) = fail(y(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
fof(f64,axiom,
! [X0,X1] : opt(y(n(s(X0)),X1)) = fail3(n(s(X0)),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_058) ).
fof(f69,axiom,
! [X0] : opt(y(x2,X0)) = fail3(x2,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_062) ).
fof(f72,axiom,
opt(x2) = x2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_064) ).
fof(f73,plain,
x2 = opt(x2),
inference(reorient_equations,[],[f72]) ).
fof(f74,axiom,
! [X0] : prop2(X0) = impl(eq2(opt(d(X0)),x(y(x2,x2),y(x2,x(x2,x2)))),eq3(btrue,bfalse)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
fof(f77,axiom,
eq3(btrue,bfalse) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_067) ).
fof(f78,plain,
bfalse = eq3(btrue,bfalse),
inference(reorient_equations,[],[f77]) ).
fof(f82,axiom,
! [X2,X3,X0,X1] :
( eq2(X0,X1) != btrue
| eq2(x(X0,X2),x(X1,X3)) = eq2(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_070) ).
fof(f83,plain,
! [X2,X3,X0,X1] :
( btrue != eq2(X0,X1)
| eq2(x(X0,X2),x(X1,X3)) = eq2(X2,X3) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,axiom,
! [X2,X3,X0,X1] :
( eq2(X0,X1) != bfalse
| eq2(y(X0,X2),y(X1,X3)) = bfalse ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
fof(f85,plain,
! [X2,X3,X0,X1] :
( bfalse != eq2(X0,X1)
| bfalse = eq2(y(X0,X2),y(X1,X3)) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,axiom,
! [X2,X3,X0,X1] :
( eq2(X0,X1) != btrue
| eq2(y(X0,X2),y(X1,X3)) = eq2(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_072) ).
fof(f87,plain,
! [X2,X3,X0,X1] :
( btrue != eq2(X0,X1)
| eq2(X2,X3) = eq2(y(X0,X2),y(X1,X3)) ),
inference(reorient_equations,[],[f86]) ).
fof(f92,axiom,
! [X0] : eq2(n(X0),x2) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_075) ).
fof(f93,plain,
! [X0] : bfalse = eq2(n(X0),x2),
inference(reorient_equations,[],[f92]) ).
fof(f120,axiom,
! [X0] : eq2(X0,X0) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_089) ).
fof(f121,plain,
! [X0] : btrue = eq2(X0,X0),
inference(reorient_equations,[],[f120]) ).
fof(f122,axiom,
! [X0] : eq3(X0,X0) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_090) ).
fof(f123,plain,
! [X0] : btrue = eq3(X0,X0),
inference(reorient_equations,[],[f122]) ).
fof(f124,negated_conjecture,
! [X0] : eq3(prop2(X0),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f125,plain,
! [X0] : btrue != eq3(prop2(X0),bfalse),
inference(reorient_equations,[],[f124]) ).
fof(f130,plain,
! [X2,X0,X1] : fail1(y(X0,X1),X2) = aux(y(X0,X1),X2,eq2(y(X0,X1),X2)),
inference(definition_unfolding,[],[f12,f6]) ).
fof(f136,plain,
! [X0] : fail32(x2,X0) = y(opt(x2),opt(X0)),
inference(definition_unfolding,[],[f26,f19]) ).
fof(f141,plain,
! [X0] : btrue != eq3(impl(eq2(opt(d(X0)),x(y(x2,x2),y(x2,x(x2,x2)))),eq3(btrue,bfalse)),bfalse),
inference(definition_unfolding,[],[f125,f74]) ).
fof(f142,definition,
! [X0] : sF0(X0) = opt(d(X0)),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f143,plain,
! [X0] : opt(d(X0)) = sF0(X0),
inference(reorient_equations,[],[f142]) ).
fof(f144,definition,
sF1 = y(x2,x2),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f145,plain,
y(x2,x2) = sF1,
inference(reorient_equations,[],[f144]) ).
fof(f146,definition,
sF2 = x(x2,x2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f147,plain,
x(x2,x2) = sF2,
inference(reorient_equations,[],[f146]) ).
fof(f148,definition,
sF3 = y(x2,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f149,plain,
y(x2,sF2) = sF3,
inference(reorient_equations,[],[f148]) ).
fof(f150,definition,
sF4 = x(sF1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f151,plain,
x(sF1,sF3) = sF4,
inference(reorient_equations,[],[f150]) ).
fof(f152,definition,
! [X0] : sF5(X0) = eq2(sF0(X0),sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f153,plain,
! [X0] : eq2(sF0(X0),sF4) = sF5(X0),
inference(reorient_equations,[],[f152]) ).
fof(f154,definition,
sF6 = eq3(btrue,bfalse),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f155,plain,
eq3(btrue,bfalse) = sF6,
inference(reorient_equations,[],[f154]) ).
fof(f156,definition,
! [X0] : sF7(X0) = impl(sF5(X0),sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f157,plain,
! [X0] : impl(sF5(X0),sF6) = sF7(X0),
inference(reorient_equations,[],[f156]) ).
fof(f158,definition,
! [X0] : sF8(X0) = eq3(sF7(X0),bfalse),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f159,plain,
! [X0] : eq3(sF7(X0),bfalse) = sF8(X0),
inference(reorient_equations,[],[f158]) ).
fof(f160,plain,
! [X0] : btrue != sF8(X0),
inference(definition_folding,[],[f141,f159,f157,f155,f153,f151,f149,f147,f145,f143]) ).
fof(f161,plain,
! [X0] : fail32(x2,X0) = y(x2,opt(X0)),
inference(forward_demodulation,[],[f136,f73]) ).
fof(f170,plain,
! [X0] : sF5(X0) = eq2(opt(d(X0)),sF4),
inference(forward_demodulation,[],[f153,f143]) ).
fof(f171,plain,
bfalse = sF6,
inference(forward_demodulation,[],[f155,f78]) ).
fof(f172,plain,
! [X0] : sF8(X0) = eq3(impl(sF5(X0),sF6),bfalse),
inference(forward_demodulation,[],[f159,f157]) ).
fof(f174,plain,
! [X0] : sF8(X0) = eq3(impl(sF5(X0),bfalse),bfalse),
inference(forward_demodulation,[],[f172,f171]) ).
fof(f175,plain,
! [X0] : sF8(X0) = eq3(impl(eq2(opt(d(X0)),sF4),bfalse),bfalse),
inference(forward_demodulation,[],[f174,f170]) ).
fof(f182,definition,
( spl9_2
<=> y(x2,x2) = sF1 ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
fof(f184,plain,
( y(x2,x2) = sF1
| ~ spl9_2 ),
inference(avatar_component_clause,[],[f182]) ).
fof(f185,plain,
spl9_2,
inference(avatar_split_clause,[],[f145,f182]) ).
fof(f189,definition,
( spl9_3
<=> x(x2,x2) = sF2 ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
fof(f191,plain,
( x(x2,x2) = sF2
| ~ spl9_3 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f192,plain,
spl9_3,
inference(avatar_split_clause,[],[f147,f189]) ).
fof(f196,definition,
( spl9_4
<=> y(x2,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
fof(f198,plain,
( y(x2,sF2) = sF3
| ~ spl9_4 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
spl9_4,
inference(avatar_split_clause,[],[f149,f196]) ).
fof(f203,definition,
( spl9_5
<=> x(sF1,sF3) = sF4 ),
introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition]) ).
fof(f205,plain,
( x(sF1,sF3) = sF4
| ~ spl9_5 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,plain,
spl9_5,
inference(avatar_split_clause,[],[f151,f203]) ).
fof(f237,plain,
! [X2,X0,X1] :
( btrue != btrue
| eq2(X1,X2) = eq2(y(X0,X1),y(X0,X2)) ),
inference(superposition,[],[f87,f121]) ).
fof(f242,plain,
! [X2,X0,X1] : eq2(X1,X2) = eq2(y(X0,X1),y(X0,X2)),
inference(trivial_inequality_removal,[],[f237]) ).
fof(f246,plain,
( ! [X0] : eq2(X0,sF2) = eq2(y(x2,X0),sF3)
| ~ spl9_4 ),
inference(superposition,[],[f242,f198]) ).
fof(f301,plain,
! [X2,X0,X1] :
( btrue != btrue
| eq2(X1,X2) = eq2(x(X0,X1),x(X0,X2)) ),
inference(superposition,[],[f83,f121]) ).
fof(f310,plain,
! [X2,X0,X1] : eq2(X1,X2) = eq2(x(X0,X1),x(X0,X2)),
inference(trivial_inequality_removal,[],[f301]) ).
fof(f320,plain,
( ! [X0] : eq2(X0,x2) = eq2(x(x2,X0),sF2)
| ~ spl9_3 ),
inference(superposition,[],[f310,f191]) ).
fof(f321,plain,
( ! [X0] : eq2(X0,sF3) = eq2(x(sF1,X0),sF4)
| ~ spl9_5 ),
inference(superposition,[],[f310,f205]) ).
fof(f378,plain,
! [X2,X3,X0,X1] : fail1(y(X0,X1),y(X2,X3)) = opt(x(y(X0,X1),y(X2,X3))),
inference(superposition,[],[f17,f62]) ).
fof(f381,plain,
! [X2,X3,X0,X1] : opt(x(y(X0,X1),y(X2,X3))) = aux(y(X0,X1),y(X2,X3),eq2(y(X0,X1),y(X2,X3))),
inference(forward_demodulation,[],[f378,f130]) ).
fof(f486,plain,
! [X0] : btrue != eq3(impl(eq2(opt(d(X0)),sF4),bfalse),bfalse),
inference(superposition,[],[f160,f175]) ).
fof(f558,definition,
( spl9_16
<=> n(s(z)) = d(x2) ),
introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition]) ).
fof(f560,plain,
( n(s(z)) = d(x2)
| ~ spl9_16 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f561,plain,
spl9_16,
inference(avatar_split_clause,[],[f53,f558]) ).
fof(f580,plain,
! [X2,X0,X1] :
( bfalse != bfalse
| bfalse = eq2(y(n(X0),X1),y(x2,X2)) ),
inference(superposition,[],[f85,f93]) ).
fof(f582,plain,
! [X2,X0,X1] : bfalse = eq2(y(n(X0),X1),y(x2,X2)),
inference(trivial_inequality_removal,[],[f580]) ).
fof(f649,plain,
! [X0,X1] : fail12(x2,x(X0,X1)) = opt(y(x2,x(X0,X1))),
inference(superposition,[],[f42,f69]) ).
fof(f652,plain,
! [X0,X1] : opt(y(x2,x(X0,X1))) = fail22(x2,x(X0,X1)),
inference(forward_demodulation,[],[f649,f38]) ).
fof(f658,plain,
! [X0,X1] : opt(y(x2,x(X0,X1))) = fail32(x2,x(X0,X1)),
inference(forward_demodulation,[],[f652,f30]) ).
fof(f664,plain,
! [X0,X1] : opt(y(x2,x(X0,X1))) = y(x2,opt(x(X0,X1))),
inference(forward_demodulation,[],[f658,f161]) ).
fof(f776,plain,
! [X0] : fail12(n(s(X0)),x2) = opt(y(n(s(X0)),x2)),
inference(superposition,[],[f44,f64]) ).
fof(f778,plain,
! [X2,X0,X1] : fail12(n(s(X0)),y(X1,X2)) = opt(y(n(s(X0)),y(X1,X2))),
inference(superposition,[],[f43,f64]) ).
fof(f1558,plain,
! [X0,X1] : btrue != eq3(impl(eq2(opt(x(y(d(X0),X1),y(X0,d(X1)))),sF4),bfalse),bfalse),
inference(superposition,[],[f486,f51]) ).
fof(f1920,definition,
( spl9_76
<=> ! [X0] : eq2(X0,sF3) = eq2(x(sF1,X0),sF4) ),
introduced(definition,[new_symbols(definition,[spl9_76])],[avatar_definition]) ).
fof(f1921,plain,
( ! [X0] : eq2(X0,sF3) = eq2(x(sF1,X0),sF4)
| ~ spl9_76 ),
inference(avatar_component_clause,[],[f1920]) ).
fof(f1922,plain,
( spl9_76
| ~ spl9_5 ),
inference(avatar_split_clause,[],[f321,f203,f1920]) ).
fof(f2334,plain,
! [X0] : opt(y(x2,n(s(X0)))) = fail12(x2,n(s(X0))),
inference(superposition,[],[f69,f39]) ).
fof(f2343,plain,
! [X0] : opt(y(x2,n(s(X0)))) = fail22(x2,n(s(X0))),
inference(forward_demodulation,[],[f2334,f38]) ).
fof(f2383,definition,
( spl9_105
<=> ! [X0] : eq2(X0,sF2) = eq2(y(x2,X0),sF3) ),
introduced(definition,[new_symbols(definition,[spl9_105])],[avatar_definition]) ).
fof(f2384,plain,
( ! [X0] : eq2(X0,sF2) = eq2(y(x2,X0),sF3)
| ~ spl9_105 ),
inference(avatar_component_clause,[],[f2383]) ).
fof(f2385,plain,
( spl9_105
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f246,f196,f2383]) ).
fof(f2777,definition,
( spl9_141
<=> ! [X0] : eq2(X0,x2) = eq2(x(x2,X0),sF2) ),
introduced(definition,[new_symbols(definition,[spl9_141])],[avatar_definition]) ).
fof(f2778,plain,
( ! [X0] : eq2(X0,x2) = eq2(x(x2,X0),sF2)
| ~ spl9_141 ),
inference(avatar_component_clause,[],[f2777]) ).
fof(f2779,plain,
( spl9_141
| ~ spl9_3 ),
inference(avatar_split_clause,[],[f320,f189,f2777]) ).
fof(f3054,plain,
! [X0,X1] : y(X0,X1) = opt(y(n(s(z)),y(X0,X1))),
inference(superposition,[],[f34,f778]) ).
fof(f3734,plain,
x2 = opt(y(n(s(z)),x2)),
inference(superposition,[],[f34,f776]) ).
fof(f4611,plain,
! [X2,X0,X1] : opt(x(y(n(X0),X1),y(x2,X2))) = aux(y(n(X0),X1),y(x2,X2),bfalse),
inference(superposition,[],[f381,f582]) ).
fof(f4732,plain,
! [X2,X0,X1] : opt(x(y(n(X0),X1),y(x2,X2))) = x(opt(y(n(X0),X1)),opt(y(x2,X2))),
inference(forward_demodulation,[],[f4611,f4]) ).
fof(f11569,plain,
x2 = opt(y(x2,n(s(z)))),
inference(superposition,[],[f28,f2343]) ).
fof(f11881,plain,
( ! [X0] : btrue != eq3(impl(eq2(opt(x(y(n(s(z)),X0),y(x2,d(X0)))),sF4),bfalse),bfalse)
| ~ spl9_16 ),
inference(superposition,[],[f1558,f560]) ).
fof(f11897,plain,
( ! [X0] : btrue != eq3(impl(eq2(x(opt(y(n(s(z)),X0)),opt(y(x2,d(X0)))),sF4),bfalse),bfalse)
| ~ spl9_16 ),
inference(forward_demodulation,[],[f11881,f4732]) ).
fof(f11900,definition,
( spl9_528
<=> ! [X0] : btrue != eq3(impl(eq2(x(opt(y(n(s(z)),X0)),opt(y(x2,d(X0)))),sF4),bfalse),bfalse) ),
introduced(definition,[new_symbols(definition,[spl9_528])],[avatar_definition]) ).
fof(f11901,plain,
( ! [X0] : btrue != eq3(impl(eq2(x(opt(y(n(s(z)),X0)),opt(y(x2,d(X0)))),sF4),bfalse),bfalse)
| ~ spl9_528 ),
inference(avatar_component_clause,[],[f11900]) ).
fof(f11902,plain,
( spl9_528
| ~ spl9_16 ),
inference(avatar_split_clause,[],[f11897,f558,f11900]) ).
fof(f11905,plain,
( ! [X0,X1] : btrue != eq3(impl(eq2(x(opt(y(n(s(z)),y(X0,X1))),opt(y(x2,x(y(d(X0),X1),y(X0,d(X1)))))),sF4),bfalse),bfalse)
| ~ spl9_528 ),
inference(superposition,[],[f11901,f51]) ).
fof(f11920,plain,
( ! [X0,X1] : btrue != eq3(impl(eq2(x(opt(y(n(s(z)),y(X0,X1))),y(x2,opt(x(y(d(X0),X1),y(X0,d(X1)))))),sF4),bfalse),bfalse)
| ~ spl9_528 ),
inference(forward_demodulation,[],[f11905,f664]) ).
fof(f11926,plain,
( ! [X0,X1] : btrue != eq3(impl(eq2(x(y(X0,X1),y(x2,opt(x(y(d(X0),X1),y(X0,d(X1)))))),sF4),bfalse),bfalse)
| ~ spl9_528 ),
inference(forward_demodulation,[],[f11920,f3054]) ).
fof(f14471,definition,
( spl9_656
<=> ! [X0,X1] : btrue != eq3(impl(eq2(x(y(X0,X1),y(x2,opt(x(y(d(X0),X1),y(X0,d(X1)))))),sF4),bfalse),bfalse) ),
introduced(definition,[new_symbols(definition,[spl9_656])],[avatar_definition]) ).
fof(f14472,plain,
( ! [X0,X1] : btrue != eq3(impl(eq2(x(y(X0,X1),y(x2,opt(x(y(d(X0),X1),y(X0,d(X1)))))),sF4),bfalse),bfalse)
| ~ spl9_656 ),
inference(avatar_component_clause,[],[f14471]) ).
fof(f14473,plain,
( spl9_656
| ~ spl9_528 ),
inference(avatar_split_clause,[],[f11926,f11900,f14471]) ).
fof(f14474,plain,
( btrue != eq3(impl(eq2(x(sF1,y(x2,opt(x(y(d(x2),x2),y(x2,d(x2)))))),sF4),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_656 ),
inference(superposition,[],[f14472,f184]) ).
fof(f14514,plain,
( btrue != eq3(impl(eq2(y(x2,opt(x(y(d(x2),x2),y(x2,d(x2))))),sF3),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_76
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14474,f1921]) ).
fof(f14527,plain,
( btrue != eq3(impl(eq2(opt(x(y(d(x2),x2),y(x2,d(x2)))),sF2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_76
| ~ spl9_105
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14514,f2384]) ).
fof(f14537,plain,
( btrue != eq3(impl(eq2(opt(x(y(n(s(z)),x2),y(x2,n(s(z))))),sF2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14527,f560]) ).
fof(f14538,plain,
( btrue != eq3(impl(eq2(x(opt(y(n(s(z)),x2)),opt(y(x2,n(s(z))))),sF2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14537,f4732]) ).
fof(f14539,plain,
( btrue != eq3(impl(eq2(x(opt(y(n(s(z)),x2)),x2),sF2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14538,f11569]) ).
fof(f14540,plain,
( btrue != eq3(impl(eq2(x(x2,x2),sF2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14539,f3734]) ).
fof(f14541,plain,
( btrue != eq3(impl(eq2(x2,x2),bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14540,f2778]) ).
fof(f14542,plain,
( btrue != eq3(impl(btrue,bfalse),bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14541,f121]) ).
fof(f14543,plain,
( btrue != eq3(bfalse,bfalse)
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(forward_demodulation,[],[f14542,f45]) ).
fof(f14544,plain,
( $false
| ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(forward_subsumption_resolution,[],[f14543,f123]) ).
fof(f14545,plain,
( ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(avatar_contradiction_clause,[],[f14544]) ).
cnf(s99,plain,
spl9_2,
inference(sat_conversion,[],[f185]) ).
cnf(s103,plain,
spl9_3,
inference(sat_conversion,[],[f192]) ).
cnf(s107,plain,
spl9_4,
inference(sat_conversion,[],[f199]) ).
cnf(s111,plain,
spl9_5,
inference(sat_conversion,[],[f206]) ).
cnf(s269,plain,
spl9_16,
inference(sat_conversion,[],[f561]) ).
cnf(s748,plain,
( ~ spl9_5
| spl9_76 ),
inference(sat_conversion,[],[f1922]) ).
cnf(s909,plain,
( ~ spl9_4
| spl9_105 ),
inference(sat_conversion,[],[f2385]) ).
cnf(s1080,plain,
( ~ spl9_3
| spl9_141 ),
inference(sat_conversion,[],[f2779]) ).
cnf(s5028,plain,
( ~ spl9_16
| spl9_528 ),
inference(sat_conversion,[],[f11902]) ).
cnf(s6168,plain,
( ~ spl9_528
| spl9_656 ),
inference(sat_conversion,[],[f14473]) ).
cnf(s6183,plain,
( ~ spl9_2
| ~ spl9_16
| ~ spl9_76
| ~ spl9_105
| ~ spl9_141
| ~ spl9_656 ),
inference(sat_conversion,[],[f14545]) ).
cnf(s6186,plain,
spl9_528,
inference(rat,[],[s5028,s269]) ).
cnf(s6187,plain,
spl9_656,
inference(rat,[],[s6168,s6186]) ).
cnf(s6208,plain,
spl9_76,
inference(rat,[],[s748,s111]) ).
cnf(s6281,plain,
spl9_105,
inference(rat,[],[s909,s107]) ).
cnf(s6386,plain,
spl9_141,
inference(rat,[],[s1080,s103]) ).
cnf(s6427,plain,
~ spl9_2,
inference(rat,[],[s6183,s6187,s6281,s6208,s269,s6386]) ).
cnf(s6542,plain,
$false,
inference(rat,[],[s99,s6427]) ).
fof(f14546,plain,
$false,
inference(avatar_sat_refutation,[],[s6542]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX189-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 15:09:27 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 16.75/3.11 % (3923416)Input is clausal, will run a generic CNF schedule.
% 16.75/3.11 % (3923445)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=589632129:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.75/3.11 % (3923443)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1720384275:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.75/3.11 % (3923442)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3147773999:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.75/3.11 % (3923441)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=1262344497:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.75/3.11 % (3923446)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3386757802:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.75/3.11 % (3923445)Instruction limit reached!
% 16.75/3.11 % (3923445)------------------------------
% 16.75/3.11 % (3923445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.11 % (3923445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.11 % (3923445)CaDiCaL version: 2.1.3
% 16.75/3.11 % (3923445)Termination reason: Instruction limit
% 16.75/3.11 % (3923445)Termination phase: Saturation
% 16.75/3.11 % (3923445)Time elapsed: 0.076 s
% 16.75/3.11 % (3923445)Peak memory usage: 89 MB
% 16.75/3.11 % (3923445)Instructions burned: 115 (million)
% 16.75/3.11 % (3923444)lrs+10_1_sil=8000:sp=occurrence:random_seed=3802388304:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.75/3.11 % (3923447)dis-21_1_sil=8000:lcm=predicate:random_seed=1888659115:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 16.75/3.11 % (3923447)Refutation not found, incomplete strategy
% 16.75/3.11 % (3923447)------------------------------
% 16.75/3.11 % (3923447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.11 % (3923447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.11 % (3923447)CaDiCaL version: 2.1.3
% 16.75/3.11 % (3923447)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.11 % (3923447)Time elapsed: 0.006 s
% 16.75/3.11 % (3923447)Peak memory usage: 88 MB
% 16.75/3.11 % (3923447)Instructions burned: 4 (million)
% 16.75/3.11 % (3923444)Instruction limit reached!
% 16.75/3.11 % (3923444)------------------------------
% 16.75/3.11 % (3923444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.11 % (3923444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.11 % (3923444)CaDiCaL version: 2.1.3
% 16.75/3.11 % (3923444)Termination reason: Instruction limit
% 16.75/3.11 % (3923444)Termination phase: Saturation
% 16.75/3.11 % (3923444)Time elapsed: 0.108 s
% 16.75/3.11 % (3923444)Peak memory usage: 89 MB
% 16.75/3.11 % (3923444)Instructions burned: 108 (million)
% 16.75/3.11 % (3923458)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1821284018:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 16.75/3.11 % (3923458)Refutation not found, incomplete strategy
% 16.75/3.11 % (3923458)------------------------------
% 16.75/3.11 % (3923458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.11 % (3923458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.11 % (3923458)CaDiCaL version: 2.1.3
% 16.75/3.11 % (3923458)Termination reason: Refutation not found, incomplete strategy
% 16.75/3.11 % (3923458)Time elapsed: 0.003 s
% 16.75/3.11 % (3923458)Peak memory usage: 88 MB
% 16.75/3.11 % (3923458)Instructions burned: 2 (million)
% 16.75/3.11 % (3923446)Instruction limit reached!
% 16.75/3.11 % (3923446)------------------------------
% 16.75/3.11 % (3923446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.75/3.11 % (3923446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.75/3.11 % (3923446)CaDiCaL version: 2.1.3
% 16.75/3.11 % (3923446)Termination reason: Instruction limit
% 16.75/3.11 % (3923446)Termination phase: Saturation
% 16.75/3.11 % (3923446)Time elapsed: 0.189 s
% 16.75/3.11 % (3923446)Peak memory usage: 90 MB
% 16.75/3.11 % (3923446)Instructions burned: 180 (million)
% 16.75/3.11 % (3923462)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=328027057:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 35.87/5.89 % (3923447)------------------------------
% 35.87/5.89 % (3923447)------------------------------
% 35.87/5.89 % (3923465)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1912950416:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 35.87/5.89 % (3923462)Instruction limit reached!
% 35.87/5.89 % (3923462)------------------------------
% 35.87/5.89 % (3923462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/5.89 % (3923462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/5.89 % (3923462)CaDiCaL version: 2.1.3
% 35.87/5.89 % (3923462)Termination reason: Instruction limit
% 35.87/5.89 % (3923462)Termination phase: Saturation
% 35.87/5.89 % (3923462)Time elapsed: 0.137 s
% 35.87/5.89 % (3923462)Peak memory usage: 91 MB
% 35.87/5.89 % (3923462)Instructions burned: 189 (million)
% 35.87/5.89 % (3923458)------------------------------
% 35.87/5.89 % (3923458)------------------------------
% 35.87/5.89 % (3923465)Instruction limit reached!
% 35.87/5.89 % (3923465)------------------------------
% 35.87/5.89 % (3923465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/5.89 % (3923465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/5.89 % (3923465)CaDiCaL version: 2.1.3
% 35.87/5.89 % (3923465)Termination reason: Instruction limit
% 35.87/5.89 % (3923465)Termination phase: Saturation
% 35.87/5.89 % (3923465)Time elapsed: 0.211 s
% 35.87/5.89 % (3923465)Peak memory usage: 91 MB
% 35.87/5.89 % (3923465)Instructions burned: 220 (million)
% 35.87/5.89 % (3923474)lrs+10_64_to=lpo:sil=8000:random_seed=552841974:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 35.87/5.89 % (3923475)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=897259155:avsq=on:i=194:fgj=on:bd=preordered_2993 on theBenchmark for (2993ds/194Mi)
% 35.87/5.89 % (3923476)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3762117143:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 35.87/5.89 % (3923474)Instruction limit reached!
% 35.87/5.89 % (3923474)------------------------------
% 35.87/5.89 % (3923474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/5.89 % (3923474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/5.89 % (3923474)CaDiCaL version: 2.1.3
% 35.87/5.89 % (3923474)Termination reason: Instruction limit
% 35.87/5.89 % (3923474)Termination phase: Saturation
% 35.87/5.89 % (3923474)Time elapsed: 0.125 s
% 35.87/5.89 % (3923474)Peak memory usage: 89 MB
% 35.87/5.89 % (3923474)Instructions burned: 126 (million)
% 35.87/5.89 % (3923480)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=576065518:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 35.87/5.89 % (3923475)Instruction limit reached!
% 35.87/5.89 % (3923475)------------------------------
% 35.87/5.89 % (3923475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/5.89 % (3923475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/5.89 % (3923475)CaDiCaL version: 2.1.3
% 35.87/5.89 % (3923475)Termination reason: Instruction limit
% 35.87/5.89 % (3923475)Termination phase: Saturation
% 35.87/5.89 % (3923475)Time elapsed: 0.171 s
% 35.87/5.89 % (3923475)Peak memory usage: 90 MB
% 35.87/5.89 % (3923475)Instructions burned: 194 (million)
% 35.87/5.89 % (3923476)Instruction limit reached!
% 35.87/5.89 % (3923476)------------------------------
% 35.87/5.89 % (3923476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.87/5.89 % (3923476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.87/5.89 % (3923476)CaDiCaL version: 2.1.3
% 35.87/5.89 % (3923476)Termination reason: Instruction limit
% 35.87/5.89 % (3923476)Termination phase: Saturation
% 35.87/5.89 % (3923476)Time elapsed: 0.165 s
% 35.87/5.89 % (3923476)Peak memory usage: 92 MB
% 35.87/5.89 % (3923476)Instructions burned: 158 (million)
% 35.87/5.89 % (3923486)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=27965794:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2990 on theBenchmark for (2990ds/106Mi)
% 35.87/5.89 % (3923491)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1925520650:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2988 on theBenchmark for (2988ds/242Mi)
% 56.56/8.70 % (3923488)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=514297722:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 56.56/8.70 % (3923488)Refutation not found, incomplete strategy
% 56.56/8.70 % (3923488)------------------------------
% 56.56/8.70 % (3923488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923488)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923488)Termination reason: Refutation not found, incomplete strategy
% 56.56/8.70 % (3923488)Time elapsed: 0.005 s
% 56.56/8.70 % (3923488)Peak memory usage: 88 MB
% 56.56/8.70 % (3923488)Instructions burned: 4 (million)
% 56.56/8.70 % (3923486)Instruction limit reached!
% 56.56/8.70 % (3923486)------------------------------
% 56.56/8.70 % (3923486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923486)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923486)Termination reason: Instruction limit
% 56.56/8.70 % (3923486)Termination phase: Saturation
% 56.56/8.70 % (3923486)Time elapsed: 0.129 s
% 56.56/8.70 % (3923486)Peak memory usage: 90 MB
% 56.56/8.70 % (3923486)Instructions burned: 107 (million)
% 56.56/8.70 % (3923491)Instruction limit reached!
% 56.56/8.70 % (3923491)------------------------------
% 56.56/8.70 % (3923491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923491)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923491)Termination reason: Instruction limit
% 56.56/8.70 % (3923491)Termination phase: Saturation
% 56.56/8.70 % (3923491)Time elapsed: 0.245 s
% 56.56/8.70 % (3923491)Peak memory usage: 91 MB
% 56.56/8.70 % (3923491)Instructions burned: 242 (million)
% 56.56/8.70 % (3923497)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=407383125:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 56.56/8.70 % (3923488)------------------------------
% 56.56/8.70 % (3923488)------------------------------
% 56.56/8.70 % (3923499)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3095117368:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 56.56/8.70 % (3923499)Instruction limit reached!
% 56.56/8.70 % (3923499)------------------------------
% 56.56/8.70 % (3923499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923499)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923499)Termination reason: Instruction limit
% 56.56/8.70 % (3923499)Termination phase: Saturation
% 56.56/8.70 % (3923499)Time elapsed: 0.078 s
% 56.56/8.70 % (3923499)Peak memory usage: 89 MB
% 56.56/8.70 % (3923499)Instructions burned: 134 (million)
% 56.56/8.70 % (3923503)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3494587606:i=499:bd=all_2983 on theBenchmark for (2983ds/499Mi)
% 56.56/8.70 % (3923505)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3891364586:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 56.56/8.70 % (3923505)Instruction limit reached!
% 56.56/8.70 % (3923505)------------------------------
% 56.56/8.70 % (3923505)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923505)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923505)Termination reason: Instruction limit
% 56.56/8.70 % (3923505)Termination phase: Saturation
% 56.56/8.70 % (3923505)Time elapsed: 0.196 s
% 56.56/8.70 % (3923505)Peak memory usage: 92 MB
% 56.56/8.70 % (3923505)Instructions burned: 191 (million)
% 56.56/8.70 % (3923503)Instruction limit reached!
% 56.56/8.70 % (3923503)------------------------------
% 56.56/8.70 % (3923503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.56/8.70 % (3923503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.56/8.70 % (3923503)CaDiCaL version: 2.1.3
% 56.56/8.70 % (3923503)Termination reason: Instruction limit
% 56.56/8.70 % (3923503)Termination phase: Saturation
% 56.56/8.70 % (3923503)Time elapsed: 0.488 s
% 56.56/8.70 % (3923503)Peak memory usage: 95 MB
% 56.56/8.70 % (3923503)Instructions burned: 499 (million)
% 101.97/15.08 % (3923512)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1835108119:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 101.97/15.08 % (3923515)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=8387283:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 101.97/15.08 % (3923512)Instruction limit reached!
% 101.97/15.08 % (3923512)------------------------------
% 101.97/15.08 % (3923512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/15.08 % (3923512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/15.08 % (3923512)CaDiCaL version: 2.1.3
% 101.97/15.08 % (3923512)Termination reason: Instruction limit
% 101.97/15.08 % (3923512)Termination phase: Saturation
% 101.97/15.08 % (3923512)Time elapsed: 0.242 s
% 101.97/15.08 % (3923512)Peak memory usage: 91 MB
% 101.97/15.08 % (3923512)Instructions burned: 264 (million)
% 101.97/15.08 % (3923515)Instruction limit reached!
% 101.97/15.08 % (3923515)------------------------------
% 101.97/15.08 % (3923515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/15.08 % (3923515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/15.08 % (3923515)CaDiCaL version: 2.1.3
% 101.97/15.08 % (3923515)Termination reason: Instruction limit
% 101.97/15.08 % (3923515)Termination phase: Saturation
% 101.97/15.08 % (3923515)Time elapsed: 0.157 s
% 101.97/15.08 % (3923515)Peak memory usage: 90 MB
% 101.97/15.08 % (3923515)Instructions burned: 156 (million)
% 101.97/15.08 % (3923518)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3766584240:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 101.97/15.08 % (3923520)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=803885687:i=537:av=off:ss=included_2972 on theBenchmark for (2972ds/537Mi)
% 101.97/15.08 % (3923520)Instruction limit reached!
% 101.97/15.08 % (3923520)------------------------------
% 101.97/15.08 % (3923520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/15.08 % (3923520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/15.08 % (3923520)CaDiCaL version: 2.1.3
% 101.97/15.08 % (3923520)Termination reason: Instruction limit
% 101.97/15.08 % (3923520)Termination phase: Saturation
% 101.97/15.08 % (3923520)Time elapsed: 0.513 s
% 101.97/15.08 % (3923520)Peak memory usage: 93 MB
% 101.97/15.08 % (3923520)Instructions burned: 538 (million)
% 101.97/15.08 % (3923526)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1809342407:i=180:bd=preordered:av=off_2965 on theBenchmark for (2965ds/180Mi)
% 101.97/15.08 % (3923526)Instruction limit reached!
% 101.97/15.08 % (3923526)------------------------------
% 101.97/15.08 % (3923526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/15.08 % (3923526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/15.08 % (3923526)CaDiCaL version: 2.1.3
% 101.97/15.08 % (3923526)Termination reason: Instruction limit
% 101.97/15.08 % (3923526)Termination phase: Saturation
% 101.97/15.08 % (3923526)Time elapsed: 0.173 s
% 101.97/15.08 % (3923526)Peak memory usage: 90 MB
% 101.97/15.08 % (3923526)Instructions burned: 180 (million)
% 101.97/15.08 % (3923528)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=29674554:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2961 on theBenchmark for (2961ds/10307Mi)
% 101.97/15.08 % (3923480)Instruction limit reached!
% 101.97/15.08 % (3923480)------------------------------
% 101.97/15.08 % (3923480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 101.97/15.08 % (3923480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.97/15.08 % (3923480)CaDiCaL version: 2.1.3
% 101.97/15.08 % (3923480)Termination reason: Instruction limit
% 101.97/15.08 % (3923480)Termination phase: Saturation
% 101.97/15.08 % (3923480)Time elapsed: 3.480 s
% 101.97/15.08 % (3923480)Peak memory usage: 155 MB
% 101.97/15.08 % (3923480)Instructions burned: 3394 (million)
% 101.97/15.08 % (3923532)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3848649768:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 101.97/15.08 % (3923532)Instruction limit reached!
% 101.97/15.08 % (3923532)------------------------------
% 101.97/15.08 % (3923532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923532)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923532)Termination reason: Instruction limit
% 139.22/20.32 % (3923532)Termination phase: Saturation
% 139.22/20.32 % (3923532)Time elapsed: 0.379 s
% 139.22/20.32 % (3923532)Peak memory usage: 96 MB
% 139.22/20.32 % (3923532)Instructions burned: 412 (million)
% 139.22/20.32 % (3923536)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2594233478:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 139.22/20.32 % (3923518)Instruction limit reached!
% 139.22/20.32 % (3923518)------------------------------
% 139.22/20.32 % (3923518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923518)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923518)Termination reason: Instruction limit
% 139.22/20.32 % (3923518)Termination phase: Saturation
% 139.22/20.32 % (3923518)Time elapsed: 3.352 s
% 139.22/20.32 % (3923518)Peak memory usage: 153 MB
% 139.22/20.32 % (3923518)Instructions burned: 3256 (million)
% 139.22/20.32 % (3923541)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2923765040:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2937 on theBenchmark for (2937ds/303Mi)
% 139.22/20.32 % (3923541)Refutation not found, incomplete strategy
% 139.22/20.32 % (3923541)------------------------------
% 139.22/20.32 % (3923541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923541)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923541)Termination reason: Refutation not found, incomplete strategy
% 139.22/20.32 % (3923541)Time elapsed: 0.074 s
% 139.22/20.32 % (3923541)Peak memory usage: 90 MB
% 139.22/20.32 % (3923541)Instructions burned: 72 (million)
% 139.22/20.32 % (3923497)Instruction limit reached!
% 139.22/20.32 % (3923497)------------------------------
% 139.22/20.32 % (3923497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923497)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923497)Termination reason: Instruction limit
% 139.22/20.32 % (3923497)Termination phase: Saturation
% 139.22/20.32 % (3923497)Time elapsed: 5.330 s
% 139.22/20.32 % (3923497)Peak memory usage: 173 MB
% 139.22/20.32 % (3923497)Instructions burned: 5209 (million)
% 139.22/20.32 % (3923541)------------------------------
% 139.22/20.32 % (3923541)------------------------------
% 139.22/20.32 % (3923547)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1918573712:st=4:i=720:sd=3:fsr=off:ss=axioms_2930 on theBenchmark for (2930ds/720Mi)
% 139.22/20.32 % (3923548)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1744139572:i=598:bs=on:bd=preordered:av=off:ss=axioms_2930 on theBenchmark for (2930ds/598Mi)
% 139.22/20.32 % (3923548)Instruction limit reached!
% 139.22/20.32 % (3923548)------------------------------
% 139.22/20.32 % (3923548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923548)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923548)Termination reason: Instruction limit
% 139.22/20.32 % (3923548)Termination phase: Saturation
% 139.22/20.32 % (3923548)Time elapsed: 0.599 s
% 139.22/20.32 % (3923548)Peak memory usage: 94 MB
% 139.22/20.32 % (3923548)Instructions burned: 598 (million)
% 139.22/20.32 % (3923547)Instruction limit reached!
% 139.22/20.32 % (3923547)------------------------------
% 139.22/20.32 % (3923547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.22/20.32 % (3923547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.22/20.32 % (3923547)CaDiCaL version: 2.1.3
% 139.22/20.32 % (3923547)Termination reason: Instruction limit
% 139.22/20.32 % (3923547)Termination phase: Saturation
% 139.22/20.32 % (3923547)Time elapsed: 0.672 s
% 139.22/20.32 % (3923547)Peak memory usage: 100 MB
% 139.22/20.32 % (3923547)Instructions burned: 720 (million)
% 139.22/20.32 % (3923554)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3221325784:i=2989:sd=3:ss=axioms:sgt=60_2922 on theBenchmark for (2922ds/2989Mi)
% 139.22/20.32 % (3923555)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=3187233349:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2922 on theBenchmark for (2922ds/1997Mi)
% 87.44/26.22 % (3923555)Instruction limit reached!
% 87.44/26.22 % (3923555)------------------------------
% 87.44/26.22 % (3923555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923555)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923555)Termination reason: Instruction limit
% 87.44/26.22 % (3923555)Termination phase: Saturation
% 87.44/26.22 % (3923555)Time elapsed: 2.104 s
% 87.44/26.22 % (3923555)Peak memory usage: 139 MB
% 87.44/26.22 % (3923555)Instructions burned: 1997 (million)
% 87.44/26.22 % (3923561)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2831224411:i=2088:bd=preordered:av=off_2899 on theBenchmark for (2899ds/2088Mi)
% 87.44/26.22 % (3923554)Instruction limit reached!
% 87.44/26.22 % (3923554)------------------------------
% 87.44/26.22 % (3923554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923554)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923554)Termination reason: Instruction limit
% 87.44/26.22 % (3923554)Termination phase: Saturation
% 87.44/26.22 % (3923554)Time elapsed: 3.035 s
% 87.44/26.22 % (3923554)Peak memory usage: 148 MB
% 87.44/26.22 % (3923554)Instructions burned: 2989 (million)
% 87.44/26.22 % (3923564)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4156209:i=1098:nicw=on_2890 on theBenchmark for (2890ds/1098Mi)
% 87.44/26.22 % (3923564)Instruction limit reached!
% 87.44/26.22 % (3923564)------------------------------
% 87.44/26.22 % (3923564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923564)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923564)Termination reason: Instruction limit
% 87.44/26.22 % (3923564)Termination phase: Saturation
% 87.44/26.22 % (3923564)Time elapsed: 1.039 s
% 87.44/26.22 % (3923564)Peak memory usage: 107 MB
% 87.44/26.22 % (3923564)Instructions burned: 1098 (million)
% 87.44/26.22 % (3923572)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1077242915:i=433:bd=preordered_2877 on theBenchmark for (2877ds/433Mi)
% 87.44/26.22 % (3923561)Instruction limit reached!
% 87.44/26.22 % (3923561)------------------------------
% 87.44/26.22 % (3923561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923561)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923561)Termination reason: Instruction limit
% 87.44/26.22 % (3923561)Termination phase: Saturation
% 87.44/26.22 % (3923561)Time elapsed: 2.181 s
% 87.44/26.22 % (3923561)Peak memory usage: 140 MB
% 87.44/26.22 % (3923561)Instructions burned: 2088 (million)
% 87.44/26.22 % (3923574)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=887381186:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2875 on theBenchmark for (2875ds/2942Mi)
% 87.44/26.22 % (3923572)Instruction limit reached!
% 87.44/26.22 % (3923572)------------------------------
% 87.44/26.22 % (3923572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923572)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923572)Termination reason: Instruction limit
% 87.44/26.22 % (3923572)Termination phase: Saturation
% 87.44/26.22 % (3923572)Time elapsed: 0.406 s
% 87.44/26.22 % (3923572)Peak memory usage: 95 MB
% 87.44/26.22 % (3923572)Instructions burned: 434 (million)
% 87.44/26.22 % (3923576)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2542691249:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2871 on theBenchmark for (2871ds/6922Mi)
% 87.44/26.22 % (3923536)Instruction limit reached!
% 87.44/26.22 % (3923536)------------------------------
% 87.44/26.22 % (3923536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923536)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923536)Termination reason: Instruction limit
% 87.44/26.22 % (3923536)Termination phase: Saturation
% 87.44/26.22 % (3923536)Time elapsed: 8.962 s
% 87.44/26.22 % (3923536)Peak memory usage: 201 MB
% 87.44/26.22 % (3923536)Instructions burned: 8478 (million)
% 87.44/26.22 % (3923584)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2513507313:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2856 on theBenchmark for (2856ds/596Mi)
% 87.44/26.22 % (3923528)Instruction limit reached!
% 87.44/26.22 % (3923528)------------------------------
% 87.44/26.22 % (3923528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923528)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923528)Termination reason: Instruction limit
% 87.44/26.22 % (3923528)Termination phase: Saturation
% 87.44/26.22 % (3923528)Time elapsed: 10.791 s
% 87.44/26.22 % (3923528)Peak memory usage: 227 MB
% 87.44/26.22 % (3923528)Instructions burned: 10307 (million)
% 87.44/26.22 % (3923584)Instruction limit reached!
% 87.44/26.22 % (3923584)------------------------------
% 87.44/26.22 % (3923584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923584)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923584)Termination reason: Instruction limit
% 87.44/26.22 % (3923584)Termination phase: Saturation
% 87.44/26.22 % (3923584)Time elapsed: 0.549 s
% 87.44/26.22 % (3923584)Peak memory usage: 95 MB
% 87.44/26.22 % (3923584)Instructions burned: 597 (million)
% 87.44/26.22 % (3923587)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1760315718:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2850 on theBenchmark for (2850ds/4123Mi)
% 87.44/26.22 % (3923590)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3648360138:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2848 on theBenchmark for (2848ds/16411Mi)
% 87.44/26.22 % (3923574)Instruction limit reached!
% 87.44/26.22 % (3923574)------------------------------
% 87.44/26.22 % (3923574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.22 % (3923574)CaDiCaL version: 2.1.3
% 87.44/26.22 % (3923574)Termination reason: Instruction limit
% 87.44/26.22 % (3923574)Termination phase: Saturation
% 87.44/26.22 % (3923574)Time elapsed: 3.239 s
% 87.44/26.22 % (3923574)Peak memory usage: 154 MB
% 87.44/26.22 % (3923574)Instructions burned: 2942 (million)
% 87.44/26.22 % (3923593)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2697642411:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2840 on theBenchmark for (2840ds/1670Mi)
% 87.44/26.22 % (3923593)Instruction limit reached!
% 87.44/26.22 % (3923593)------------------------------
% 87.44/26.22 % (3923593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.22 % (3923593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.23 % (3923593)CaDiCaL version: 2.1.3
% 87.44/26.23 % (3923593)Termination reason: Instruction limit
% 87.44/26.23 % (3923593)Termination phase: Saturation
% 87.44/26.23 % (3923593)Time elapsed: 1.746 s
% 87.44/26.23 % (3923593)Peak memory usage: 136 MB
% 87.44/26.23 % (3923593)Instructions burned: 1670 (million)
% 87.44/26.23 % (3923597)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=11367174:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2820 on theBenchmark for (2820ds/1722Mi)
% 87.44/26.23 % (3923587)Instruction limit reached!
% 87.44/26.23 % (3923587)------------------------------
% 87.44/26.23 % (3923587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.23 % (3923587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.23 % (3923587)CaDiCaL version: 2.1.3
% 87.44/26.23 % (3923587)Termination reason: Instruction limit
% 87.44/26.23 % (3923587)Termination phase: Saturation
% 87.44/26.23 % (3923587)Time elapsed: 4.207 s
% 87.44/26.23 % (3923587)Peak memory usage: 164 MB
% 87.44/26.23 % (3923587)Instructions burned: 4123 (million)
% 87.44/26.23 % (3923603)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1486532529:cts=off:cond=on:i=9530:bs=on:fsd=on_2806 on theBenchmark for (2806ds/9530Mi)
% 87.44/26.23 % (3923597)Instruction limit reached!
% 87.44/26.23 % (3923597)------------------------------
% 87.44/26.23 % (3923597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.23 % (3923597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.23 % (3923597)CaDiCaL version: 2.1.3
% 87.44/26.23 % (3923597)Termination reason: Instruction limit
% 87.44/26.23 % (3923597)Termination phase: Saturation
% 87.44/26.23 % (3923597)Time elapsed: 1.776 s
% 87.44/26.23 % (3923597)Peak memory usage: 135 MB
% 87.44/26.23 % (3923597)Instructions burned: 1722 (million)
% 87.44/26.23 % (3923607)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=436161452:st=2:i=4495:sd=10:ss=included_2800 on theBenchmark for (2800ds/4495Mi)
% 87.44/26.23 % (3923576)Instruction limit reached!
% 87.44/26.23 % (3923576)------------------------------
% 87.44/26.23 % (3923576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.23 % (3923576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.23 % (3923576)CaDiCaL version: 2.1.3
% 87.44/26.23 % (3923576)Termination reason: Instruction limit
% 87.44/26.23 % (3923576)Termination phase: Saturation
% 87.44/26.23 % (3923576)Time elapsed: 7.204 s
% 87.44/26.23 % (3923576)Peak memory usage: 194 MB
% 87.44/26.23 % (3923576)Instructions burned: 6922 (million)
% 87.44/26.23 % (3923609)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3142648310:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2797 on theBenchmark for (2797ds/4920Mi)
% 87.44/26.23 % (3923607)Instruction limit reached!
% 87.44/26.23 % (3923607)------------------------------
% 87.44/26.23 % (3923607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.44/26.23 % (3923607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.44/26.23 % (3923607)CaDiCaL version: 2.1.3
% 87.44/26.23 % (3923607)Termination reason: Instruction limit
% 87.44/26.23 % (3923607)Termination phase: Saturation
% 87.44/26.23 % (3923607)Time elapsed: 4.649 s
% 87.44/26.23 % (3923607)Peak memory usage: 167 MB
% 87.44/26.23 % (3923607)Instructions burned: 4495 (million)
% 87.44/26.23 % (3923603)First to succeed.
% 87.44/26.23 % (3923603)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3923416"
% 87.44/26.23 % (3923618)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2162086096:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2751 on theBenchmark for (2751ds/2083Mi)
% 87.44/26.23 % (3923603)Refutation found. Thanks to Tanya!
% 87.44/26.23 % SZS status Unsatisfiable for theBenchmark
% 87.44/26.23 % SZS output start Proof for theBenchmark
% See solution above
% 181.30/26.47 % (3923603)------------------------------
% 181.30/26.47 % (3923603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 181.30/26.47 % (3923603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 181.30/26.47 % (3923603)CaDiCaL version: 2.1.3
% 181.30/26.47 % (3923603)Termination reason: Refutation
% 181.30/26.47 % (3923603)Time elapsed: 5.411 s
% 181.30/26.47 % (3923603)Peak memory usage: 165 MB
% 181.30/26.47 % (3923603)Instructions burned: 4863 (million)
% 181.30/26.47 % (3923603)------------------------------
% 181.30/26.47 % (3923603)------------------------------
% 181.30/26.47 % (3923416)Success in time 25.485 s
% 181.30/26.47 % Vampire exiting
%------------------------------------------------------------------------------