%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL001-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 11:50:53 AM UTC 2026
% Result : Unsatisfiable 157.28s 32.22s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 25
% Syntax : Number of formulae : 170 ( 75 unt; 19 def)
% Number of atoms : 290 ( 28 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 239 ( 119 ~; 115 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 6 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 19 con; 0-2 aty)
% Number of variables : 178 ( 0 sgn 178 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_1) ).
fof(f3,axiom,
! [X0,X1] : is_a_theorem(or(not(or(X0,X1)),or(X1,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_2) ).
fof(f4,axiom,
! [X0,X1] : is_a_theorem(or(not(X0),or(X1,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_3) ).
fof(f5,axiom,
! [X0] : is_a_theorem(or(not(or(X0,X0)),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_4) ).
fof(f6,negated_conjecture,
~ is_a_theorem(or(not(or(not(or(not(a),b)),or(c,or(e,falsehood)))),or(not(or(not(e),a)),or(c,or(falsehood,a))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_an_CAMeredith) ).
fof(f7,definition,
sF0 = not(a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f8,plain,
not(a) = sF0,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF1 = or(sF0,b),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f10,plain,
or(sF0,b) = sF1,
inference(reorient_equations,[],[f9]) ).
fof(f11,definition,
sF2 = not(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f12,plain,
not(sF1) = sF2,
inference(reorient_equations,[],[f11]) ).
fof(f13,definition,
sF3 = or(e,falsehood),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f14,plain,
or(e,falsehood) = sF3,
inference(reorient_equations,[],[f13]) ).
fof(f15,definition,
sF4 = or(c,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f16,plain,
or(c,sF3) = sF4,
inference(reorient_equations,[],[f15]) ).
fof(f17,definition,
sF5 = or(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f18,plain,
or(sF2,sF4) = sF5,
inference(reorient_equations,[],[f17]) ).
fof(f19,definition,
sF6 = not(sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f20,plain,
not(sF5) = sF6,
inference(reorient_equations,[],[f19]) ).
fof(f21,definition,
sF7 = not(e),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f22,plain,
not(e) = sF7,
inference(reorient_equations,[],[f21]) ).
fof(f23,definition,
sF8 = or(sF7,a),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f24,plain,
or(sF7,a) = sF8,
inference(reorient_equations,[],[f23]) ).
fof(f25,definition,
sF9 = not(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f26,plain,
not(sF8) = sF9,
inference(reorient_equations,[],[f25]) ).
fof(f27,definition,
sF10 = or(falsehood,a),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f28,plain,
or(falsehood,a) = sF10,
inference(reorient_equations,[],[f27]) ).
fof(f29,definition,
sF11 = or(c,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f30,plain,
or(c,sF10) = sF11,
inference(reorient_equations,[],[f29]) ).
fof(f31,definition,
sF12 = or(sF9,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f32,plain,
or(sF9,sF11) = sF12,
inference(reorient_equations,[],[f31]) ).
fof(f33,definition,
sF13 = or(sF6,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f34,plain,
or(sF6,sF12) = sF13,
inference(reorient_equations,[],[f33]) ).
fof(f35,plain,
~ is_a_theorem(sF13),
inference(definition_folding,[],[f6,f34,f32,f30,f28,f26,f24,f22,f20,f18,f16,f14,f12,f10,f8]) ).
fof(f48,plain,
! [X0] : is_a_theorem(or(not(or(not(a),X0)),or(not(sF8),or(sF7,X0)))),
inference(superposition,[],[f2,f24]) ).
fof(f59,plain,
! [X0] : is_a_theorem(or(not(or(not(a),X0)),or(sF9,or(sF7,X0)))),
inference(forward_demodulation,[],[f48,f26]) ).
fof(f63,plain,
! [X0] : is_a_theorem(or(not(or(sF0,X0)),or(sF9,or(sF7,X0)))),
inference(forward_demodulation,[],[f59,f8]) ).
fof(f79,plain,
is_a_theorem(or(not(or(a,falsehood)),sF10)),
inference(superposition,[],[f3,f28]) ).
fof(f94,plain,
is_a_theorem(or(not(sF10),sF11)),
inference(superposition,[],[f4,f30]) ).
fof(f96,plain,
is_a_theorem(or(not(a),sF10)),
inference(superposition,[],[f4,f28]) ).
fof(f99,plain,
is_a_theorem(or(not(sF12),sF13)),
inference(superposition,[],[f4,f34]) ).
fof(f101,plain,
is_a_theorem(or(not(sF11),sF12)),
inference(superposition,[],[f4,f32]) ).
fof(f103,plain,
is_a_theorem(or(sF0,sF10)),
inference(forward_demodulation,[],[f96,f8]) ).
fof(f104,plain,
! [X0] :
( ~ is_a_theorem(or(X0,X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f1,f5]) ).
fof(f105,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,X1))
| is_a_theorem(or(X1,X0)) ),
inference(resolution,[],[f1,f3]) ).
fof(f106,plain,
! [X2,X0,X1] :
( is_a_theorem(or(not(or(X2,X0)),or(X2,X1)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(resolution,[],[f1,f2]) ).
fof(f107,plain,
! [X0] :
( is_a_theorem(or(sF9,or(sF7,X0)))
| ~ is_a_theorem(or(sF0,X0)) ),
inference(resolution,[],[f1,f63]) ).
fof(f154,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(X2,X0))
| is_a_theorem(or(X2,X1)) ),
inference(resolution,[],[f106,f1]) ).
fof(f160,plain,
! [X0] :
( is_a_theorem(or(not(sF5),or(sF2,X0)))
| ~ is_a_theorem(or(not(sF4),X0)) ),
inference(superposition,[],[f106,f18]) ).
fof(f174,plain,
! [X0] :
( is_a_theorem(or(sF6,or(sF2,X0)))
| ~ is_a_theorem(or(not(sF4),X0)) ),
inference(forward_demodulation,[],[f160,f20]) ).
fof(f183,plain,
! [X0,X1] : is_a_theorem(or(or(X0,X1),not(X1))),
inference(resolution,[],[f105,f4]) ).
fof(f238,plain,
! [X0,X1] :
( ~ is_a_theorem(or(X0,or(X1,X1)))
| is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f154,f5]) ).
fof(f239,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(X0,or(X1,X2)))
| is_a_theorem(or(X0,or(X2,X1))) ),
inference(resolution,[],[f154,f3]) ).
fof(f240,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(X0,or(X1,X2)))
| is_a_theorem(or(X0,or(X1,X3)))
| ~ is_a_theorem(or(not(X2),X3)) ),
inference(resolution,[],[f154,f106]) ).
fof(f243,plain,
! [X2,X0,X1] :
( is_a_theorem(or(X0,or(X2,X1)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f154,f4]) ).
fof(f250,plain,
! [X0,X1] : is_a_theorem(or(not(or(X0,X1)),or(X0,X1))),
inference(resolution,[],[f239,f3]) ).
fof(f251,plain,
! [X2,X0,X1] :
( is_a_theorem(or(not(or(X0,X1)),or(X2,X0)))
| ~ is_a_theorem(or(not(X1),X2)) ),
inference(resolution,[],[f239,f106]) ).
fof(f254,plain,
! [X0,X1] : is_a_theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f239,f4]) ).
fof(f265,plain,
! [X2,X0,X1] :
( is_a_theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ is_a_theorem(or(not(X0),X2)) ),
inference(resolution,[],[f240,f3]) ).
fof(f266,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(not(X3),X2))
| is_a_theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ is_a_theorem(or(not(X1),X3)) ),
inference(resolution,[],[f240,f106]) ).
fof(f283,plain,
! [X2,X0,X1] :
( is_a_theorem(or(X0,or(X1,X2)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f254,f154]) ).
fof(f292,plain,
is_a_theorem(or(not(c),sF11)),
inference(superposition,[],[f254,f30]) ).
fof(f299,plain,
is_a_theorem(or(not(sF9),sF12)),
inference(superposition,[],[f254,f32]) ).
fof(f386,plain,
! [X0,X1] :
( ~ is_a_theorem(or(or(X0,X1),X1))
| is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f243,f104]) ).
fof(f393,plain,
! [X0] :
( ~ is_a_theorem(or(X0,sF12))
| is_a_theorem(or(X0,sF13)) ),
inference(superposition,[],[f243,f34]) ).
fof(f558,plain,
is_a_theorem(or(sF10,sF0)),
inference(resolution,[],[f103,f105]) ).
fof(f583,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(not(X1),X3))
| is_a_theorem(or(not(or(X0,X2)),or(X2,X3)))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(resolution,[],[f265,f240]) ).
fof(f585,plain,
! [X0,X1] :
( is_a_theorem(or(not(or(X0,X1)),X1))
| ~ is_a_theorem(or(not(X0),X1)) ),
inference(resolution,[],[f265,f238]) ).
fof(f587,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(X0,X2))
| is_a_theorem(or(X2,X1)) ),
inference(resolution,[],[f265,f1]) ).
fof(f611,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(X2,or(X0,X1)))
| ~ is_a_theorem(or(not(X0),X1))
| is_a_theorem(or(X2,X1)) ),
inference(resolution,[],[f585,f154]) ).
fof(f747,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X1),or(X2,X2)))
| is_a_theorem(or(not(or(X0,X1)),or(X0,X2))) ),
inference(resolution,[],[f266,f5]) ).
fof(f799,plain,
! [X2,X0,X1] :
( is_a_theorem(or(not(or(X0,X2)),X1))
| ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(not(X2),X1)) ),
inference(resolution,[],[f611,f106]) ).
fof(f1086,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(X2,X0))
| is_a_theorem(or(X2,or(X1,X3))) ),
inference(resolution,[],[f283,f154]) ).
fof(f1088,plain,
! [X2,X0,X1] :
( is_a_theorem(or(or(X1,X2),X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f283,f105]) ).
fof(f1107,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(or(X0,X0),X1))
| is_a_theorem(or(or(X1,X2),X0)) ),
inference(resolution,[],[f1088,f238]) ).
fof(f1475,plain,
is_a_theorem(or(not(sF11),sF13)),
inference(resolution,[],[f393,f101]) ).
fof(f1509,plain,
! [X2,X0,X1] :
( is_a_theorem(or(X1,or(X2,X0)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f587,f4]) ).
fof(f1510,plain,
! [X2,X0,X1] :
( is_a_theorem(or(X1,or(X0,X2)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f587,f254]) ).
fof(f1536,plain,
! [X0] :
( ~ is_a_theorem(or(sF11,X0))
| is_a_theorem(or(X0,sF12)) ),
inference(resolution,[],[f587,f101]) ).
fof(f1549,plain,
! [X0,X1] :
( ~ is_a_theorem(or(sF0,X0))
| ~ is_a_theorem(or(a,X1))
| is_a_theorem(or(X1,X0)) ),
inference(superposition,[],[f587,f8]) ).
fof(f1663,definition,
( spl14_111
<=> is_a_theorem(or(sF0,sF12)) ),
introduced(definition,[new_symbols(definition,[spl14_111])],[avatar_definition]) ).
fof(f1664,plain,
( is_a_theorem(or(sF0,sF12))
| ~ spl14_111 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1665,plain,
( ~ is_a_theorem(or(sF0,sF12))
| spl14_111 ),
inference(avatar_component_clause,[],[f1663]) ).
fof(f1771,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(X2,X0))
| is_a_theorem(or(X1,X2)) ),
inference(resolution,[],[f251,f1]) ).
fof(f1800,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(X0,or(X1,X2)))
| is_a_theorem(or(or(X2,X1),X0)) ),
inference(resolution,[],[f1771,f3]) ).
fof(f2128,plain,
! [X2,X0,X1] :
( is_a_theorem(or(or(X0,X2),X1))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f1509,f1800]) ).
fof(f2154,plain,
! [X2,X0,X1] :
( is_a_theorem(or(or(X2,X0),X1))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[],[f1509,f105]) ).
fof(f2184,plain,
! [X0] :
( ~ is_a_theorem(or(sF10,X0))
| is_a_theorem(or(sF11,X0)) ),
inference(superposition,[],[f2154,f30]) ).
fof(f2213,plain,
! [X0] :
( ~ is_a_theorem(or(sF0,X0))
| is_a_theorem(or(sF1,X0)) ),
inference(superposition,[],[f2128,f10]) ).
fof(f2304,plain,
! [X0] :
( ~ is_a_theorem(or(sF6,X0))
| is_a_theorem(or(X0,sF13)) ),
inference(superposition,[],[f1510,f34]) ).
fof(f2310,plain,
! [X0] :
( is_a_theorem(or(or(sF2,X0),sF13))
| ~ is_a_theorem(or(not(sF4),X0)) ),
inference(resolution,[],[f2304,f174]) ).
fof(f2781,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X2),X1))
| ~ is_a_theorem(or(not(X0),X1))
| ~ is_a_theorem(or(X0,X2))
| is_a_theorem(X1) ),
inference(resolution,[],[f799,f1]) ).
fof(f2782,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(X3,or(X0,X2)))
| ~ is_a_theorem(or(not(X2),X1))
| ~ is_a_theorem(or(not(X0),X1))
| is_a_theorem(or(X3,X1)) ),
inference(resolution,[],[f799,f154]) ).
fof(f2873,plain,
( ~ is_a_theorem(or(not(sF4),sF13))
| is_a_theorem(or(sF2,sF13)) ),
inference(resolution,[],[f2310,f386]) ).
fof(f2878,definition,
( spl14_178
<=> is_a_theorem(or(sF2,sF13)) ),
introduced(definition,[new_symbols(definition,[spl14_178])],[avatar_definition]) ).
fof(f2882,definition,
( spl14_179
<=> is_a_theorem(or(not(sF4),sF13)) ),
introduced(definition,[new_symbols(definition,[spl14_179])],[avatar_definition]) ).
fof(f2884,plain,
( ~ is_a_theorem(or(not(sF4),sF13))
| spl14_179 ),
inference(avatar_component_clause,[],[f2882]) ).
fof(f2885,plain,
( spl14_178
| ~ spl14_179 ),
inference(avatar_split_clause,[],[f2873,f2882,f2878]) ).
fof(f3199,plain,
is_a_theorem(or(sF11,sF0)),
inference(resolution,[],[f2184,f558]) ).
fof(f3535,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X0),or(X1,X2)))
| ~ is_a_theorem(or(X0,X1))
| is_a_theorem(or(X1,X2)) ),
inference(resolution,[],[f2781,f254]) ).
fof(f3578,plain,
! [X0] :
( ~ is_a_theorem(or(not(X0),sF13))
| ~ is_a_theorem(or(X0,sF12))
| is_a_theorem(sF13) ),
inference(resolution,[],[f2781,f99]) ).
fof(f3603,plain,
! [X0] :
( ~ is_a_theorem(or(not(X0),sF13))
| ~ is_a_theorem(or(X0,sF12)) ),
inference(forward_subsumption_resolution,[],[f3578,f35]) ).
fof(f3747,plain,
( ~ is_a_theorem(or(sF2,sF13))
| ~ is_a_theorem(or(sF1,sF12)) ),
inference(superposition,[],[f3603,f12]) ).
fof(f3752,definition,
( spl14_182
<=> is_a_theorem(or(sF1,sF12)) ),
introduced(definition,[new_symbols(definition,[spl14_182])],[avatar_definition]) ).
fof(f3755,plain,
( ~ spl14_182
| ~ spl14_178 ),
inference(avatar_split_clause,[],[f3747,f2878,f3752]) ).
fof(f3770,definition,
( spl14_186
<=> is_a_theorem(or(sF0,sF13)) ),
introduced(definition,[new_symbols(definition,[spl14_186])],[avatar_definition]) ).
fof(f3771,plain,
( is_a_theorem(or(sF0,sF13))
| ~ spl14_186 ),
inference(avatar_component_clause,[],[f3770]) ).
fof(f3772,plain,
( ~ is_a_theorem(or(sF0,sF13))
| spl14_186 ),
inference(avatar_component_clause,[],[f3770]) ).
fof(f3964,plain,
! [X0,X1] : is_a_theorem(or(or(not(X0),X1),X0)),
inference(resolution,[],[f1107,f183]) ).
fof(f3987,plain,
! [X0,X1] : is_a_theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f3964,f105]) ).
fof(f4168,plain,
! [X0,X1] :
( ~ is_a_theorem(or(or(X0,X1),X1))
| is_a_theorem(or(X1,X0)) ),
inference(resolution,[],[f3535,f3]) ).
fof(f4170,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(or(X0,X1),X0))
| is_a_theorem(or(X0,X2))
| ~ is_a_theorem(or(not(X1),X2)) ),
inference(resolution,[],[f3535,f106]) ).
fof(f4238,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(or(X2,or(X0,X1)),X1))
| is_a_theorem(or(or(X0,X1),X2)) ),
inference(resolution,[],[f4168,f243]) ).
fof(f4501,plain,
is_a_theorem(or(not(sF9),sF13)),
inference(resolution,[],[f299,f393]) ).
fof(f5430,plain,
is_a_theorem(or(sF0,sF12)),
inference(resolution,[],[f1536,f3199]) ).
fof(f5452,plain,
( $false
| spl14_111 ),
inference(forward_subsumption_resolution,[],[f5430,f1665]) ).
fof(f5453,plain,
spl14_111,
inference(avatar_contradiction_clause,[],[f5452]) ).
fof(f8553,plain,
! [X0] :
( ~ is_a_theorem(or(X0,sF11))
| is_a_theorem(or(X0,sF13)) ),
inference(resolution,[],[f1475,f154]) ).
fof(f8558,plain,
! [X0] :
( ~ is_a_theorem(or(sF11,X0))
| is_a_theorem(or(X0,sF13)) ),
inference(resolution,[],[f1475,f587]) ).
fof(f8586,plain,
is_a_theorem(or(not(c),sF13)),
inference(resolution,[],[f8553,f292]) ).
fof(f8587,plain,
is_a_theorem(or(not(sF10),sF13)),
inference(resolution,[],[f8553,f94]) ).
fof(f8604,plain,
is_a_theorem(or(sF0,sF13)),
inference(resolution,[],[f8558,f3199]) ).
fof(f8634,plain,
( $false
| spl14_186 ),
inference(forward_subsumption_resolution,[],[f8604,f3772]) ).
fof(f8635,plain,
spl14_186,
inference(avatar_contradiction_clause,[],[f8634]) ).
fof(f8636,plain,
( ! [X0] :
( ~ is_a_theorem(or(a,X0))
| is_a_theorem(or(X0,sF13)) )
| ~ spl14_186 ),
inference(resolution,[],[f3771,f1549]) ).
fof(f8666,plain,
( ! [X0] : is_a_theorem(or(or(not(a),X0),sF13))
| ~ spl14_186 ),
inference(resolution,[],[f8636,f3987]) ).
fof(f8681,plain,
( ! [X0] : is_a_theorem(or(or(sF0,X0),sF13))
| ~ spl14_186 ),
inference(forward_demodulation,[],[f8666,f8]) ).
fof(f8692,plain,
( ! [X0] : is_a_theorem(or(or(X0,sF13),sF0))
| ~ spl14_186 ),
inference(resolution,[],[f8681,f4238]) ).
fof(f8722,plain,
! [X0] :
( ~ is_a_theorem(or(X0,sF10))
| is_a_theorem(or(X0,sF13)) ),
inference(resolution,[],[f8587,f154]) ).
fof(f8753,plain,
is_a_theorem(or(not(or(a,falsehood)),sF13)),
inference(resolution,[],[f8722,f79]) ).
fof(f9265,plain,
( ! [X0] : is_a_theorem(or(sF0,or(X0,sF13)))
| ~ spl14_186 ),
inference(resolution,[],[f8692,f105]) ).
fof(f9763,plain,
! [X0] :
( ~ is_a_theorem(or(sF9,X0))
| is_a_theorem(or(X0,sF13)) ),
inference(resolution,[],[f4501,f587]) ).
fof(f9780,plain,
! [X0] :
( is_a_theorem(or(or(sF7,X0),sF13))
| ~ is_a_theorem(or(sF0,X0)) ),
inference(resolution,[],[f9763,f107]) ).
fof(f10646,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(or(not(X0),or(X2,X2)))
| is_a_theorem(or(not(or(X0,X1)),or(X1,X2))) ),
inference(resolution,[],[f583,f5]) ).
fof(f10766,plain,
! [X0,X1] : is_a_theorem(or(not(or(or(X0,X0),X1)),or(X1,X0))),
inference(resolution,[],[f10646,f250]) ).
fof(f11069,plain,
! [X0] :
( ~ is_a_theorem(or(sF0,or(X0,sF13)))
| is_a_theorem(or(or(X0,sF13),sF7)) ),
inference(resolution,[],[f9780,f4238]) ).
fof(f11071,plain,
( ! [X0] : is_a_theorem(or(or(X0,sF13),sF7))
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f11069,f9265]) ).
fof(f11078,plain,
( ! [X0] :
( is_a_theorem(or(sF7,X0))
| ~ is_a_theorem(or(not(sF13),X0)) )
| ~ spl14_186 ),
inference(resolution,[],[f11071,f4170]) ).
fof(f12268,plain,
( is_a_theorem(or(sF1,sF12))
| ~ spl14_111 ),
inference(resolution,[],[f1664,f2213]) ).
fof(f12272,plain,
( spl14_182
| ~ spl14_111 ),
inference(avatar_split_clause,[],[f12268,f1663,f3752]) ).
fof(f25060,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(X0,or(or(X1,X1),X2)))
| is_a_theorem(or(X0,or(or(X2,X1),X3))) ),
inference(resolution,[],[f1086,f10766]) ).
fof(f25410,plain,
! [X2,X0,X1] : is_a_theorem(or(not(X0),or(or(X0,X1),X2))),
inference(resolution,[],[f25060,f4]) ).
fof(f25497,plain,
! [X2,X0,X1] : is_a_theorem(or(not(X0),or(or(X1,X0),X2))),
inference(resolution,[],[f25410,f25060]) ).
fof(f25588,plain,
! [X2,X0,X1] : is_a_theorem(or(not(X0),or(X1,or(X2,X0)))),
inference(resolution,[],[f25497,f239]) ).
fof(f26576,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(or(not(or(X3,X0)),X2))
| is_a_theorem(or(not(X0),or(X1,X2))) ),
inference(resolution,[],[f25588,f240]) ).
fof(f42983,plain,
! [X0] : is_a_theorem(or(not(falsehood),or(X0,sF13))),
inference(resolution,[],[f26576,f8753]) ).
fof(f44730,plain,
! [X0] : is_a_theorem(or(not(or(X0,falsehood)),or(X0,sF13))),
inference(resolution,[],[f42983,f747]) ).
fof(f48846,plain,
is_a_theorem(or(not(sF3),or(e,sF13))),
inference(superposition,[],[f44730,f14]) ).
fof(f48864,plain,
! [X0] :
( ~ is_a_theorem(or(not(sF13),X0))
| ~ is_a_theorem(or(not(e),X0))
| is_a_theorem(or(not(sF3),X0)) ),
inference(resolution,[],[f48846,f2782]) ).
fof(f48907,plain,
! [X0] :
( ~ is_a_theorem(or(sF7,X0))
| ~ is_a_theorem(or(not(sF13),X0))
| is_a_theorem(or(not(sF3),X0)) ),
inference(forward_demodulation,[],[f48864,f22]) ).
fof(f48920,plain,
( ! [X0] :
( ~ is_a_theorem(or(not(sF13),X0))
| is_a_theorem(or(not(sF3),X0)) )
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f48907,f11078]) ).
fof(f49244,plain,
( ! [X0] : is_a_theorem(or(not(sF3),or(X0,sF13)))
| ~ spl14_186 ),
inference(resolution,[],[f48920,f4]) ).
fof(f49330,plain,
( ! [X0] : is_a_theorem(or(not(or(X0,sF3)),or(X0,sF13)))
| ~ spl14_186 ),
inference(resolution,[],[f49244,f747]) ).
fof(f49974,plain,
( is_a_theorem(or(not(sF4),or(c,sF13)))
| ~ spl14_186 ),
inference(superposition,[],[f49330,f16]) ).
fof(f51705,plain,
( ~ is_a_theorem(or(not(c),sF13))
| is_a_theorem(or(not(sF4),sF13))
| ~ spl14_186 ),
inference(resolution,[],[f49974,f611]) ).
fof(f51759,plain,
( is_a_theorem(or(not(sF4),sF13))
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f51705,f8586]) ).
fof(f51766,plain,
( $false
| spl14_179
| ~ spl14_186 ),
inference(forward_subsumption_resolution,[],[f51759,f2884]) ).
fof(f51767,plain,
( spl14_179
| ~ spl14_186 ),
inference(avatar_contradiction_clause,[],[f51766]) ).
cnf(s118,plain,
( spl14_178
| ~ spl14_179 ),
inference(sat_conversion,[],[f2885]) ).
cnf(s129,plain,
( ~ spl14_178
| ~ spl14_182 ),
inference(sat_conversion,[],[f3755]) ).
cnf(s155,plain,
spl14_111,
inference(sat_conversion,[],[f5453]) ).
cnf(s223,plain,
spl14_186,
inference(sat_conversion,[],[f8635]) ).
cnf(s372,plain,
( ~ spl14_111
| spl14_182 ),
inference(sat_conversion,[],[f12272]) ).
cnf(s1068,plain,
( spl14_179
| ~ spl14_186 ),
inference(sat_conversion,[],[f51767]) ).
cnf(s1129,plain,
spl14_179,
inference(rat,[],[s1068,s223]) ).
cnf(s1251,plain,
spl14_182,
inference(rat,[],[s372,s155]) ).
cnf(s1276,plain,
~ spl14_178,
inference(rat,[],[s129,s1251]) ).
cnf(s1295,plain,
$false,
inference(rat,[],[s118,s1129,s1276]) ).
fof(f51770,plain,
$false,
inference(avatar_sat_refutation,[],[s1295]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL001-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 % Computer : n017.cluster.edu
% 0.13/0.42 % Model : x86_64 x86_64
% 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.42 % Memory : 8046.5625MB
% 0.13/0.42 % OS : Linux 6.8.0-71-generic
% 0.13/0.42 % CPULimit : 300
% 0.13/0.42 % WCLimit : 300
% 0.13/0.42 % DateTime : Sun Sep 27 15:11:35 UTC 2026
% 0.13/0.42 % CPUTime :
% 0.13/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.48 Running first-order theorem proving
% 0.13/0.48 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.57/3.64 % (2709680)Input is clausal, will run a generic CNF schedule.
% 18.57/3.64 % (2709694)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2060760821:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.57/3.64 % (2709691)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=64580262:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.57/3.64 % (2709690)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1137824370:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.57/3.64 % (2709689)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=2923193913:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.57/3.64 % (2709692)lrs+10_1_sil=8000:sp=occurrence:random_seed=631302851:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.57/3.64 % (2709693)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=985148242:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.57/3.64 % (2709695)dis-21_1_sil=8000:lcm=predicate:random_seed=762858897: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)
% 18.57/3.64 % (2709694)Instruction limit reached!
% 18.57/3.64 % (2709694)------------------------------
% 18.57/3.64 % (2709694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.57/3.64 % (2709694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.57/3.64 % (2709694)CaDiCaL version: 2.1.3
% 18.57/3.64 % (2709694)Termination reason: Instruction limit
% 18.57/3.64 % (2709694)Termination phase: Saturation
% 18.57/3.64 % (2709694)Time elapsed: 0.101 s
% 18.57/3.64 % (2709694)Peak memory usage: 89 MB
% 18.57/3.64 % (2709694)Instructions burned: 181 (million)
% 18.57/3.64 % (2709693)Instruction limit reached!
% 18.57/3.64 % (2709693)------------------------------
% 18.57/3.64 % (2709693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.57/3.64 % (2709693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.57/3.64 % (2709693)CaDiCaL version: 2.1.3
% 18.57/3.64 % (2709693)Termination reason: Instruction limit
% 18.57/3.64 % (2709693)Termination phase: Saturation
% 18.57/3.64 % (2709693)Time elapsed: 0.104 s
% 18.57/3.64 % (2709693)Peak memory usage: 88 MB
% 18.57/3.64 % (2709693)Instructions burned: 114 (million)
% 18.57/3.64 % (2709692)Instruction limit reached!
% 18.57/3.64 % (2709692)------------------------------
% 18.57/3.64 % (2709692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.57/3.64 % (2709692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.57/3.64 % (2709692)CaDiCaL version: 2.1.3
% 18.57/3.64 % (2709692)Termination reason: Instruction limit
% 18.57/3.64 % (2709692)Termination phase: Saturation
% 18.57/3.64 % (2709692)Time elapsed: 0.107 s
% 18.57/3.64 % (2709692)Peak memory usage: 88 MB
% 18.57/3.64 % (2709692)Instructions burned: 107 (million)
% 18.57/3.64 % (2709695)Instruction limit reached!
% 18.57/3.64 % (2709695)------------------------------
% 18.57/3.64 % (2709695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.57/3.64 % (2709695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.57/3.64 % (2709695)CaDiCaL version: 2.1.3
% 18.57/3.64 % (2709695)Termination reason: Instruction limit
% 18.57/3.64 % (2709695)Termination phase: Saturation
% 18.57/3.64 % (2709695)Time elapsed: 0.116 s
% 18.57/3.64 % (2709695)Peak memory usage: 88 MB
% 18.57/3.64 % (2709695)Instructions burned: 117 (million)
% 18.57/3.64 % (2709703)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=1822623696:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.57/3.64 % (2709703)Refutation not found, incomplete strategy
% 18.57/3.64 % (2709703)------------------------------
% 18.57/3.64 % (2709703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.57/3.64 % (2709703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.57/3.64 % (2709703)CaDiCaL version: 2.1.3
% 18.57/3.64 % (2709703)Termination reason: Refutation not found, incomplete strategy
% 18.57/3.64 % (2709703)Time elapsed: 0.001 s
% 18.57/3.64 % (2709703)Peak memory usage: 87 MB
% 18.57/3.64 % (2709704)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=579549135: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)
% 36.80/6.18 % (2709705)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2514317875:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 36.80/6.18 % (2709705)Refutation not found, incomplete strategy
% 36.80/6.18 % (2709705)------------------------------
% 36.80/6.18 % (2709705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.18 % (2709705)CaDiCaL version: 2.1.3
% 36.80/6.18 % (2709705)Termination reason: Refutation not found, incomplete strategy
% 36.80/6.18 % (2709705)Time elapsed: 0.002 s
% 36.80/6.18 % (2709705)Peak memory usage: 87 MB
% 36.80/6.18 % (2709706)lrs+10_64_to=lpo:sil=8000:random_seed=2771932196:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 36.80/6.18 % (2709703)------------------------------
% 36.80/6.18 % (2709703)------------------------------
% 36.80/6.18 % (2709706)Instruction limit reached!
% 36.80/6.18 % (2709706)------------------------------
% 36.80/6.18 % (2709706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.18 % (2709706)CaDiCaL version: 2.1.3
% 36.80/6.18 % (2709706)Termination reason: Instruction limit
% 36.80/6.18 % (2709706)Termination phase: Saturation
% 36.80/6.18 % (2709706)Time elapsed: 0.129 s
% 36.80/6.18 % (2709706)Peak memory usage: 88 MB
% 36.80/6.18 % (2709706)Instructions burned: 126 (million)
% 36.80/6.18 % (2709704)Instruction limit reached!
% 36.80/6.18 % (2709704)------------------------------
% 36.80/6.18 % (2709704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.18 % (2709704)CaDiCaL version: 2.1.3
% 36.80/6.18 % (2709704)Termination reason: Instruction limit
% 36.80/6.18 % (2709704)Termination phase: Saturation
% 36.80/6.18 % (2709704)Time elapsed: 0.186 s
% 36.80/6.18 % (2709704)Peak memory usage: 89 MB
% 36.80/6.18 % (2709704)Instructions burned: 189 (million)
% 36.80/6.18 % (2709711)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2033700359:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 36.80/6.18 % (2709713)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1526940896:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 36.80/6.18 % (2709705)------------------------------
% 36.80/6.18 % (2709705)------------------------------
% 36.80/6.18 % (2709711)Instruction limit reached!
% 36.80/6.18 % (2709711)------------------------------
% 36.80/6.18 % (2709711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.18 % (2709711)CaDiCaL version: 2.1.3
% 36.80/6.18 % (2709711)Termination reason: Instruction limit
% 36.80/6.18 % (2709711)Termination phase: Saturation
% 36.80/6.18 % (2709711)Time elapsed: 0.110 s
% 36.80/6.18 % (2709711)Peak memory usage: 90 MB
% 36.80/6.18 % (2709711)Instructions burned: 194 (million)
% 36.80/6.18 % (2709712)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1230211157:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 36.80/6.18 % (2709716)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=1167013341:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 36.80/6.18 % (2709712)Instruction limit reached!
% 36.80/6.18 % (2709712)------------------------------
% 36.80/6.18 % (2709712)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.80/6.18 % (2709712)CaDiCaL version: 2.1.3
% 36.80/6.18 % (2709712)Termination reason: Instruction limit
% 36.80/6.18 % (2709712)Termination phase: Saturation
% 36.80/6.18 % (2709712)Time elapsed: 0.169 s
% 36.80/6.18 % (2709712)Peak memory usage: 91 MB
% 36.80/6.18 % (2709712)Instructions burned: 158 (million)
% 36.80/6.18 % (2709716)Instruction limit reached!
% 36.80/6.18 % (2709716)------------------------------
% 36.80/6.18 % (2709716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.80/6.18 % (2709716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709716)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709716)Termination reason: Instruction limit
% 58.49/9.27 % (2709716)Termination phase: Saturation
% 58.49/9.27 % (2709716)Time elapsed: 0.099 s
% 58.49/9.27 % (2709716)Peak memory usage: 89 MB
% 58.49/9.27 % (2709716)Instructions burned: 107 (million)
% 58.49/9.27 % (2709718)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2404845991:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 58.49/9.27 % (2709718)Refutation not found, incomplete strategy
% 58.49/9.27 % (2709718)------------------------------
% 58.49/9.27 % (2709718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.49/9.27 % (2709718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709718)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709718)Termination reason: Refutation not found, incomplete strategy
% 58.49/9.27 % (2709718)Time elapsed: 0.001 s
% 58.49/9.27 % (2709718)Peak memory usage: 87 MB
% 58.49/9.27 % (2709722)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2577044971:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 58.49/9.27 % (2709723)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3445904154:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 58.49/9.27 % (2709722)Instruction limit reached!
% 58.49/9.27 % (2709722)------------------------------
% 58.49/9.27 % (2709722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.49/9.27 % (2709722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709722)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709722)Termination reason: Instruction limit
% 58.49/9.27 % (2709722)Termination phase: Saturation
% 58.49/9.27 % (2709722)Time elapsed: 0.234 s
% 58.49/9.27 % (2709722)Peak memory usage: 90 MB
% 58.49/9.27 % (2709722)Instructions burned: 242 (million)
% 58.49/9.27 % (2709718)------------------------------
% 58.49/9.27 % (2709718)------------------------------
% 58.49/9.27 % (2709727)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=200859149:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 58.49/9.27 % (2709727)Instruction limit reached!
% 58.49/9.27 % (2709727)------------------------------
% 58.49/9.27 % (2709727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.49/9.27 % (2709727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709727)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709727)Termination reason: Instruction limit
% 58.49/9.27 % (2709727)Termination phase: Saturation
% 58.49/9.27 % (2709727)Time elapsed: 0.080 s
% 58.49/9.27 % (2709727)Peak memory usage: 89 MB
% 58.49/9.27 % (2709727)Instructions burned: 136 (million)
% 58.49/9.27 % (2709728)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3231706374:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 58.49/9.27 % (2709731)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3857357602:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 58.49/9.27 % (2709731)Instruction limit reached!
% 58.49/9.27 % (2709731)------------------------------
% 58.49/9.27 % (2709731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.49/9.27 % (2709731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709731)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709731)Termination reason: Instruction limit
% 58.49/9.27 % (2709731)Termination phase: Saturation
% 58.49/9.27 % (2709731)Time elapsed: 0.202 s
% 58.49/9.27 % (2709731)Peak memory usage: 92 MB
% 58.49/9.27 % (2709731)Instructions burned: 191 (million)
% 58.49/9.27 % (2709728)Instruction limit reached!
% 58.49/9.27 % (2709728)------------------------------
% 58.49/9.27 % (2709728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.49/9.27 % (2709728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.49/9.27 % (2709728)CaDiCaL version: 2.1.3
% 58.49/9.27 % (2709728)Termination reason: Instruction limit
% 58.49/9.27 % (2709728)Termination phase: Saturation
% 58.49/9.27 % (2709728)Time elapsed: 0.454 s
% 58.49/9.27 % (2709728)Peak memory usage: 92 MB
% 58.49/9.27 % (2709728)Instructions burned: 499 (million)
% 58.49/9.27 % (2709735)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1751961579:i=264:kws=precedence:fsr=off_2976 on theBenchmark for (2976ds/264Mi)
% 98.52/15.02 % (2709736)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=347860736:cond=on:i=156:bs=on:gtg=exists_all:er=known_2974 on theBenchmark for (2974ds/156Mi)
% 98.52/15.02 % (2709735)Instruction limit reached!
% 98.52/15.02 % (2709735)------------------------------
% 98.52/15.02 % (2709735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.52/15.02 % (2709735)CaDiCaL version: 2.1.3
% 98.52/15.02 % (2709735)Termination reason: Instruction limit
% 98.52/15.02 % (2709735)Termination phase: Saturation
% 98.52/15.02 % (2709735)Time elapsed: 0.257 s
% 98.52/15.02 % (2709735)Peak memory usage: 92 MB
% 98.52/15.02 % (2709735)Instructions burned: 265 (million)
% 98.52/15.02 % (2709736)Instruction limit reached!
% 98.52/15.02 % (2709736)------------------------------
% 98.52/15.02 % (2709736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.52/15.02 % (2709736)CaDiCaL version: 2.1.3
% 98.52/15.02 % (2709736)Termination reason: Instruction limit
% 98.52/15.02 % (2709736)Termination phase: Saturation
% 98.52/15.02 % (2709736)Time elapsed: 0.126 s
% 98.52/15.02 % (2709736)Peak memory usage: 89 MB
% 98.52/15.02 % (2709736)Instructions burned: 156 (million)
% 98.52/15.02 % (2709740)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=1041485947:i=3256:kws=precedence:bd=preordered:av=off_2971 on theBenchmark for (2971ds/3256Mi)
% 98.52/15.02 % (2709742)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3818484435:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 98.52/15.02 % (2709742)Instruction limit reached!
% 98.52/15.02 % (2709742)------------------------------
% 98.52/15.02 % (2709742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.52/15.02 % (2709742)CaDiCaL version: 2.1.3
% 98.52/15.02 % (2709742)Termination reason: Instruction limit
% 98.52/15.02 % (2709742)Termination phase: Saturation
% 98.52/15.02 % (2709742)Time elapsed: 0.540 s
% 98.52/15.02 % (2709742)Peak memory usage: 91 MB
% 98.52/15.02 % (2709742)Instructions burned: 537 (million)
% 98.52/15.02 % (2709745)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2444652786:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 98.52/15.02 % (2709745)Instruction limit reached!
% 98.52/15.02 % (2709745)------------------------------
% 98.52/15.02 % (2709745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.52/15.02 % (2709745)CaDiCaL version: 2.1.3
% 98.52/15.02 % (2709745)Termination reason: Instruction limit
% 98.52/15.02 % (2709745)Termination phase: Saturation
% 98.52/15.02 % (2709745)Time elapsed: 0.175 s
% 98.52/15.02 % (2709745)Peak memory usage: 89 MB
% 98.52/15.02 % (2709745)Instructions burned: 180 (million)
% 98.52/15.02 % (2709747)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=2584216851:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/10307Mi)
% 98.52/15.02 % (2709713)Instruction limit reached!
% 98.52/15.02 % (2709713)------------------------------
% 98.52/15.02 % (2709713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.52/15.02 % (2709713)CaDiCaL version: 2.1.3
% 98.52/15.02 % (2709713)Termination reason: Instruction limit
% 98.52/15.02 % (2709713)Termination phase: Saturation
% 98.52/15.02 % (2709713)Time elapsed: 3.481 s
% 98.52/15.02 % (2709713)Peak memory usage: 148 MB
% 98.52/15.02 % (2709713)Instructions burned: 3394 (million)
% 98.52/15.02 % (2709749)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=4019871531:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 98.52/15.02 % (2709749)Instruction limit reached!
% 98.52/15.02 % (2709749)------------------------------
% 98.52/15.02 % (2709749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 98.52/15.02 % (2709749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709749)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709749)Termination reason: Instruction limit
% 138.62/20.55 % (2709749)Termination phase: Saturation
% 138.62/20.55 % (2709749)Time elapsed: 0.415 s
% 138.62/20.55 % (2709749)Peak memory usage: 93 MB
% 138.62/20.55 % (2709749)Instructions burned: 412 (million)
% 138.62/20.55 % (2709751)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=1222003523:s2pl=no:i=8478:s2at=4:nm=6_2948 on theBenchmark for (2948ds/8478Mi)
% 138.62/20.55 % (2709740)Instruction limit reached!
% 138.62/20.55 % (2709740)------------------------------
% 138.62/20.55 % (2709740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.62/20.55 % (2709740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709740)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709740)Termination reason: Instruction limit
% 138.62/20.55 % (2709740)Termination phase: Saturation
% 138.62/20.55 % (2709740)Time elapsed: 3.182 s
% 138.62/20.55 % (2709740)Peak memory usage: 150 MB
% 138.62/20.55 % (2709740)Instructions burned: 3256 (million)
% 138.62/20.55 % (2709756)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=3631077673:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2936 on theBenchmark for (2936ds/303Mi)
% 138.62/20.55 % (2709756)Instruction limit reached!
% 138.62/20.55 % (2709756)------------------------------
% 138.62/20.55 % (2709756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.62/20.55 % (2709756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709756)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709756)Termination reason: Instruction limit
% 138.62/20.55 % (2709756)Termination phase: Saturation
% 138.62/20.55 % (2709756)Time elapsed: 0.277 s
% 138.62/20.55 % (2709756)Peak memory usage: 90 MB
% 138.62/20.55 % (2709756)Instructions burned: 303 (million)
% 138.62/20.55 % (2709723)Instruction limit reached!
% 138.62/20.55 % (2709723)------------------------------
% 138.62/20.55 % (2709723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.62/20.55 % (2709723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709723)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709723)Termination reason: Instruction limit
% 138.62/20.55 % (2709723)Termination phase: Saturation
% 138.62/20.55 % (2709723)Time elapsed: 5.388 s
% 138.62/20.55 % (2709723)Peak memory usage: 161 MB
% 138.62/20.55 % (2709723)Instructions burned: 5209 (million)
% 138.62/20.55 % (2709759)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1998538039:st=4:i=720:sd=3:fsr=off:ss=axioms_2931 on theBenchmark for (2931ds/720Mi)
% 138.62/20.55 % (2709760)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1602790125:i=598:bs=on:bd=preordered:av=off:ss=axioms_2929 on theBenchmark for (2929ds/598Mi)
% 138.62/20.55 % (2709759)Instruction limit reached!
% 138.62/20.55 % (2709759)------------------------------
% 138.62/20.55 % (2709759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.62/20.55 % (2709759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709759)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709759)Termination reason: Instruction limit
% 138.62/20.55 % (2709759)Termination phase: Saturation
% 138.62/20.55 % (2709759)Time elapsed: 0.729 s
% 138.62/20.55 % (2709759)Peak memory usage: 98 MB
% 138.62/20.55 % (2709759)Instructions burned: 720 (million)
% 138.62/20.55 % (2709760)Instruction limit reached!
% 138.62/20.55 % (2709760)------------------------------
% 138.62/20.55 % (2709760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 138.62/20.55 % (2709760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.62/20.55 % (2709760)CaDiCaL version: 2.1.3
% 138.62/20.55 % (2709760)Termination reason: Instruction limit
% 138.62/20.55 % (2709760)Termination phase: Saturation
% 138.62/20.55 % (2709760)Time elapsed: 0.589 s
% 138.62/20.55 % (2709760)Peak memory usage: 95 MB
% 138.62/20.55 % (2709760)Instructions burned: 598 (million)
% 138.62/20.55 % (2709763)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2306865780:i=2989:sd=3:ss=axioms:sgt=60_2921 on theBenchmark for (2921ds/2989Mi)
% 138.62/20.55 % (2709764)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=3186434257:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2920 on theBenchmark for (2920ds/1997Mi)
% 187.91/27.41 % (2709764)Instruction limit reached!
% 187.91/27.41 % (2709764)------------------------------
% 187.91/27.41 % (2709764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709764)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709764)Termination reason: Instruction limit
% 187.91/27.41 % (2709764)Termination phase: Saturation
% 187.91/27.41 % (2709764)Time elapsed: 2.079 s
% 187.91/27.41 % (2709764)Peak memory usage: 135 MB
% 187.91/27.41 % (2709764)Instructions burned: 1997 (million)
% 187.91/27.41 % (2709769)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=2097089677:i=2088:bd=preordered:av=off_2896 on theBenchmark for (2896ds/2088Mi)
% 187.91/27.41 % (2709763)Instruction limit reached!
% 187.91/27.41 % (2709763)------------------------------
% 187.91/27.41 % (2709763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709763)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709763)Termination reason: Instruction limit
% 187.91/27.41 % (2709763)Termination phase: Saturation
% 187.91/27.41 % (2709763)Time elapsed: 3.260 s
% 187.91/27.41 % (2709763)Peak memory usage: 145 MB
% 187.91/27.41 % (2709763)Instructions burned: 2990 (million)
% 187.91/27.41 % (2709771)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1641769101:i=1098:nicw=on_2886 on theBenchmark for (2886ds/1098Mi)
% 187.91/27.41 % (2709771)Instruction limit reached!
% 187.91/27.41 % (2709771)------------------------------
% 187.91/27.41 % (2709771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709771)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709771)Termination reason: Instruction limit
% 187.91/27.41 % (2709771)Termination phase: Saturation
% 187.91/27.41 % (2709771)Time elapsed: 0.961 s
% 187.91/27.41 % (2709771)Peak memory usage: 99 MB
% 187.91/27.41 % (2709771)Instructions burned: 1098 (million)
% 187.91/27.41 % (2709769)Instruction limit reached!
% 187.91/27.41 % (2709769)------------------------------
% 187.91/27.41 % (2709769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709769)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709769)Termination reason: Instruction limit
% 187.91/27.41 % (2709769)Termination phase: Saturation
% 187.91/27.41 % (2709769)Time elapsed: 2.215 s
% 187.91/27.41 % (2709769)Peak memory usage: 136 MB
% 187.91/27.41 % (2709769)Instructions burned: 2088 (million)
% 187.91/27.41 % (2709773)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2507789821:i=433:bd=preordered_2873 on theBenchmark for (2873ds/433Mi)
% 187.91/27.41 % (2709774)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3560448616:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2871 on theBenchmark for (2871ds/2942Mi)
% 187.91/27.41 % (2709773)Instruction limit reached!
% 187.91/27.41 % (2709773)------------------------------
% 187.91/27.41 % (2709773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709773)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709773)Termination reason: Instruction limit
% 187.91/27.41 % (2709773)Termination phase: Saturation
% 187.91/27.41 % (2709773)Time elapsed: 0.435 s
% 187.91/27.41 % (2709773)Peak memory usage: 94 MB
% 187.91/27.41 % (2709773)Instructions burned: 433 (million)
% 187.91/27.41 % (2709777)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2731074403:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2866 on theBenchmark for (2866ds/6922Mi)
% 187.91/27.41 % (2709751)Instruction limit reached!
% 187.91/27.41 % (2709751)------------------------------
% 187.91/27.41 % (2709751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 187.91/27.41 % (2709751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 187.91/27.41 % (2709751)CaDiCaL version: 2.1.3
% 187.91/27.41 % (2709751)Termination reason: Instruction limit
% 187.91/27.41 % (2709751)Termination phase: Saturation
% 203.04/29.69 % (2709751)Time elapsed: 8.579 s
% 203.04/29.69 % (2709751)Peak memory usage: 201 MB
% 203.04/29.69 % (2709751)Instructions burned: 8478 (million)
% 203.04/29.69 % (2709779)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=379056855:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2859 on theBenchmark for (2859ds/596Mi)
% 203.04/29.69 % (2709779)Instruction limit reached!
% 203.04/29.69 % (2709779)------------------------------
% 203.04/29.69 % (2709779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.04/29.69 % (2709779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.04/29.69 % (2709779)CaDiCaL version: 2.1.3
% 203.04/29.69 % (2709779)Termination reason: Instruction limit
% 203.04/29.69 % (2709779)Termination phase: Saturation
% 203.04/29.69 % (2709779)Time elapsed: 0.538 s
% 203.04/29.69 % (2709779)Peak memory usage: 93 MB
% 203.04/29.69 % (2709779)Instructions burned: 596 (million)
% 203.04/29.69 % (2709747)Instruction limit reached!
% 203.04/29.69 % (2709747)------------------------------
% 203.04/29.69 % (2709747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.04/29.69 % (2709747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.04/29.69 % (2709747)CaDiCaL version: 2.1.3
% 203.04/29.69 % (2709747)Termination reason: Instruction limit
% 203.04/29.69 % (2709747)Termination phase: Saturation
% 203.04/29.69 % (2709747)Time elapsed: 10.401 s
% 203.04/29.69 % (2709747)Peak memory usage: 166 MB
% 203.04/29.69 % (2709747)Instructions burned: 10307 (million)
% 203.04/29.69 % (2709781)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=993809985:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2851 on theBenchmark for (2851ds/4123Mi)
% 203.04/29.69 % (2709782)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=398965224:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2851 on theBenchmark for (2851ds/16411Mi)
% 203.04/29.69 % (2709774)Instruction limit reached!
% 203.04/29.69 % (2709774)------------------------------
% 203.04/29.69 % (2709774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.04/29.69 % (2709774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.04/29.69 % (2709774)CaDiCaL version: 2.1.3
% 203.04/29.69 % (2709774)Termination reason: Instruction limit
% 203.04/29.69 % (2709774)Termination phase: Saturation
% 203.04/29.69 % (2709774)Time elapsed: 3.084 s
% 203.04/29.69 % (2709774)Peak memory usage: 139 MB
% 203.04/29.69 % (2709774)Instructions burned: 2942 (million)
% 203.04/29.69 % (2709785)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1297235344:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2838 on theBenchmark for (2838ds/1670Mi)
% 203.04/29.69 % (2709785)Instruction limit reached!
% 203.04/29.69 % (2709785)------------------------------
% 203.04/29.69 % (2709785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.04/29.69 % (2709785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.04/29.69 % (2709785)CaDiCaL version: 2.1.3
% 203.04/29.69 % (2709785)Termination reason: Instruction limit
% 203.04/29.69 % (2709785)Termination phase: Saturation
% 203.04/29.69 % (2709785)Time elapsed: 1.788 s
% 203.04/29.69 % (2709785)Peak memory usage: 136 MB
% 203.04/29.69 % (2709785)Instructions burned: 1671 (million)
% 203.04/29.69 % (2709789)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=1740110289:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2817 on theBenchmark for (2817ds/1722Mi)
% 203.04/29.69 % (2709781)Instruction limit reached!
% 203.04/29.69 % (2709781)------------------------------
% 203.04/29.69 % (2709781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 203.04/29.69 % (2709781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 203.04/29.69 % (2709781)CaDiCaL version: 2.1.3
% 203.04/29.69 % (2709781)Termination reason: Instruction limit
% 203.04/29.69 % (2709781)Termination phase: Saturation
% 203.04/29.69 % (2709781)Time elapsed: 4.128 s
% 203.04/29.69 % (2709781)Peak memory usage: 159 MB
% 203.04/29.69 % (2709781)Instructions burned: 4123 (million)
% 203.04/29.69 % (2709793)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=4124037500:cts=off:cond=on:i=9530:bs=on:fsd=on_2807 on theBenchmark for (2807ds/9530Mi)
% 157.28/32.21 % (2709777)Instruction limit reached!
% 157.28/32.21 % (2709777)------------------------------
% 157.28/32.21 % (2709777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709777)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709777)Termination reason: Instruction limit
% 157.28/32.21 % (2709777)Termination phase: Saturation
% 157.28/32.21 % (2709777)Time elapsed: 6.783 s
% 157.28/32.21 % (2709777)Peak memory usage: 182 MB
% 157.28/32.21 % (2709777)Instructions burned: 6922 (million)
% 157.28/32.21 % (2709789)Instruction limit reached!
% 157.28/32.21 % (2709789)------------------------------
% 157.28/32.21 % (2709789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709789)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709789)Termination reason: Instruction limit
% 157.28/32.21 % (2709789)Termination phase: Saturation
% 157.28/32.21 % (2709789)Time elapsed: 1.991 s
% 157.28/32.21 % (2709789)Peak memory usage: 135 MB
% 157.28/32.21 % (2709789)Instructions burned: 1722 (million)
% 157.28/32.21 % (2709795)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4021162058:st=2:i=4495:sd=10:ss=included_2795 on theBenchmark for (2795ds/4495Mi)
% 157.28/32.21 % (2709796)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=1821966173:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2794 on theBenchmark for (2794ds/4920Mi)
% 157.28/32.21 % (2709795)Instruction limit reached!
% 157.28/32.21 % (2709795)------------------------------
% 157.28/32.21 % (2709795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709795)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709795)Termination reason: Instruction limit
% 157.28/32.21 % (2709795)Termination phase: Saturation
% 157.28/32.21 % (2709795)Time elapsed: 4.429 s
% 157.28/32.21 % (2709795)Peak memory usage: 157 MB
% 157.28/32.21 % (2709795)Instructions burned: 4496 (million)
% 157.28/32.21 % (2709796)Instruction limit reached!
% 157.28/32.21 % (2709796)------------------------------
% 157.28/32.21 % (2709796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709796)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709796)Termination reason: Instruction limit
% 157.28/32.21 % (2709796)Termination phase: Saturation
% 157.28/32.21 % (2709796)Time elapsed: 4.494 s
% 157.28/32.21 % (2709796)Peak memory usage: 153 MB
% 157.28/32.21 % (2709796)Instructions burned: 4922 (million)
% 157.28/32.21 % (2709806)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=579498839:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2748 on theBenchmark for (2748ds/2083Mi)
% 157.28/32.21 % (2709807)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=1850362266:i=4629:av=off:gsp=on_2747 on theBenchmark for (2747ds/4629Mi)
% 157.28/32.21 % (2709807)Refutation not found, incomplete strategy
% 157.28/32.21 % (2709807)------------------------------
% 157.28/32.21 % (2709807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709807)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709807)Termination reason: Refutation not found, incomplete strategy
% 157.28/32.21 % (2709807)Time elapsed: 0.316 s
% 157.28/32.21 % (2709807)Peak memory usage: 127 MB
% 157.28/32.21 % (2709807)Instructions burned: 853 (million)
% 157.28/32.21 % (2709807)------------------------------
% 157.28/32.21 % (2709807)------------------------------
% 157.28/32.21 % (2709883)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3429690216:i=1258:av=off_2741 on theBenchmark for (2741ds/1258Mi)
% 157.28/32.21 % (2709883)Instruction limit reached!
% 157.28/32.21 % (2709883)------------------------------
% 157.28/32.21 % (2709883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709883)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709883)Termination reason: Instruction limit
% 157.28/32.21 % (2709883)Termination phase: Saturation
% 157.28/32.21 % (2709883)Time elapsed: 0.406 s
% 157.28/32.21 % (2709883)Peak memory usage: 99 MB
% 157.28/32.21 % (2709883)Instructions burned: 1260 (million)
% 157.28/32.21 % (2709963)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=768559703:i=7343:av=off:ss=included_2735 on theBenchmark for (2735ds/7343Mi)
% 157.28/32.21 % (2709806)Instruction limit reached!
% 157.28/32.21 % (2709806)------------------------------
% 157.28/32.21 % (2709806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709806)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709806)Termination reason: Instruction limit
% 157.28/32.21 % (2709806)Termination phase: Saturation
% 157.28/32.21 % (2709806)Time elapsed: 1.238 s
% 157.28/32.21 % (2709806)Peak memory usage: 133 MB
% 157.28/32.21 % (2709806)Instructions burned: 2084 (million)
% 157.28/32.21 % (2709966)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2244059457:i=1325:sd=2:ss=axioms:sgt=16_2734 on theBenchmark for (2734ds/1325Mi)
% 157.28/32.21 % (2709966)Refutation not found, incomplete strategy
% 157.28/32.21 % (2709966)------------------------------
% 157.28/32.21 % (2709966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709966)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709966)Termination reason: Refutation not found, incomplete strategy
% 157.28/32.21 % (2709966)Time elapsed: 0.001 s
% 157.28/32.21 % (2709966)Peak memory usage: 87 MB
% 157.28/32.21 % (2709966)------------------------------
% 157.28/32.21 % (2709966)------------------------------
% 157.28/32.21 % (2709968)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=4287772120:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2730 on theBenchmark for (2730ds/2646Mi)
% 157.28/32.21 % (2709793)Instruction limit reached!
% 157.28/32.21 % (2709793)------------------------------
% 157.28/32.21 % (2709793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709793)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709793)Termination reason: Instruction limit
% 157.28/32.21 % (2709793)Termination phase: Saturation
% 157.28/32.21 % (2709793)Time elapsed: 7.613 s
% 157.28/32.21 % (2709793)Peak memory usage: 164 MB
% 157.28/32.21 % (2709793)Instructions burned: 9531 (million)
% 157.28/32.21 % (2709970)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2252119044:i=1489:sd=2:ep=R:ss=axioms_2728 on theBenchmark for (2728ds/1489Mi)
% 157.28/32.21 % (2709970)Instruction limit reached!
% 157.28/32.21 % (2709970)------------------------------
% 157.28/32.21 % (2709970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.21 % (2709970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.21 % (2709970)CaDiCaL version: 2.1.3
% 157.28/32.21 % (2709970)Termination reason: Instruction limit
% 157.28/32.21 % (2709970)Termination phase: Saturation
% 157.28/32.21 % (2709970)Time elapsed: 0.958 s
% 157.28/32.21 % (2709970)Peak memory usage: 132 MB
% 157.28/32.22 % (2709970)Instructions burned: 1489 (million)
% 157.28/32.22 % (2709968)Instruction limit reached!
% 157.28/32.22 % (2709968)------------------------------
% 157.28/32.22 % (2709968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2709968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2709968)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2709968)Termination reason: Instruction limit
% 157.28/32.22 % (2709968)Termination phase: Saturation
% 157.28/32.22 % (2709968)Time elapsed: 1.267 s
% 157.28/32.22 % (2709968)Peak memory usage: 141 MB
% 157.28/32.22 % (2709968)Instructions burned: 2647 (million)
% 157.28/32.22 % (2709973)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=2387616654:i=1503_2717 on theBenchmark for (2717ds/1503Mi)
% 157.28/32.22 % (2709974)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=941511625:i=13942:kws=frequency_2715 on theBenchmark for (2715ds/13942Mi)
% 157.28/32.22 % (2709782)Instruction limit reached!
% 157.28/32.22 % (2709782)------------------------------
% 157.28/32.22 % (2709782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2709782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2709782)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2709782)Termination reason: Instruction limit
% 157.28/32.22 % (2709782)Termination phase: Saturation
% 157.28/32.22 % (2709782)Time elapsed: 13.476 s
% 157.28/32.22 % (2709782)Peak memory usage: 241 MB
% 157.28/32.22 % (2709782)Instructions burned: 16411 (million)
% 157.28/32.22 % (2709981)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3321508139:i=3604:fsr=off:er=filter_2713 on theBenchmark for (2713ds/3604Mi)
% 157.28/32.22 % (2709973)Instruction limit reached!
% 157.28/32.22 % (2709973)------------------------------
% 157.28/32.22 % (2709973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2709973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2709973)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2709973)Termination reason: Instruction limit
% 157.28/32.22 % (2709973)Termination phase: Saturation
% 157.28/32.22 % (2709973)Time elapsed: 0.975 s
% 157.28/32.22 % (2709973)Peak memory usage: 132 MB
% 157.28/32.22 % (2709973)Instructions burned: 1504 (million)
% 157.28/32.22 % (2710040)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2167266905:i=1876:sd=1:ss=included:sgt=32_2705 on theBenchmark for (2705ds/1876Mi)
% 157.28/32.22 % (2709963)Instruction limit reached!
% 157.28/32.22 % (2709963)------------------------------
% 157.28/32.22 % (2709963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2709963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2709963)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2709963)Termination reason: Instruction limit
% 157.28/32.22 % (2709963)Termination phase: Saturation
% 157.28/32.22 % (2709963)Time elapsed: 3.388 s
% 157.28/32.22 % (2709963)Peak memory usage: 190 MB
% 157.28/32.22 % (2709963)Instructions burned: 7343 (million)
% 157.28/32.22 % (2710042)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1994431695:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2700 on theBenchmark for (2700ds/1932Mi)
% 157.28/32.22 % (2710040)Instruction limit reached!
% 157.28/32.22 % (2710040)------------------------------
% 157.28/32.22 % (2710040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2710040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2710040)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2710040)Termination reason: Instruction limit
% 157.28/32.22 % (2710040)Termination phase: Saturation
% 157.28/32.22 % (2710040)Time elapsed: 1.175 s
% 157.28/32.22 % (2710040)Peak memory usage: 136 MB
% 157.28/32.22 % (2710040)Instructions burned: 1877 (million)
% 157.28/32.22 % (2709981)Instruction limit reached!
% 157.28/32.22 % (2709981)------------------------------
% 157.28/32.22 % (2709981)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 157.28/32.22 % (2709981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 157.28/32.22 % (2709981)CaDiCaL version: 2.1.3
% 157.28/32.22 % (2709981)Termination reason: Instruction limit
% 157.28/32.22 % (2709981)Termination phase: Saturation
% 157.28/32.22 % (2709981)Time elapsed: 1.995 s
% 157.28/32.22 % (2709981)Peak memory usage: 152 MB
% 157.28/32.22 % (2709981)Instructions burned: 3604 (million)
% 157.28/32.22 % (2710136)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2560014924:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2692 on theBenchmark for (2692ds/1980Mi)
% 157.28/32.22 % (2709974)First to succeed.
% 157.28/32.22 % (2709974)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2709680"
% 157.28/32.22 % (2710140)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3472663119:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2691 on theBenchmark for (2691ds/3902Mi)
% 157.28/32.22 % (2709974)Refutation found. Thanks to Tanya!
% 157.28/32.22 % SZS status Unsatisfiable for theBenchmark
% 157.28/32.22 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/32.42 % (2709974)------------------------------
% 0.21/32.42 % (2709974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/32.42 % (2709974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/32.42 % (2709974)CaDiCaL version: 2.1.3
% 0.21/32.42 % (2709974)Termination reason: Refutation
% 0.21/32.42 % (2709974)Time elapsed: 2.404 s
% 0.21/32.42 % (2709974)Peak memory usage: 180 MB
% 0.21/32.42 % (2709974)Instructions burned: 6971 (million)
% 0.21/32.42 % (2709974)------------------------------
% 0.21/32.42 % (2709974)------------------------------
% 0.21/32.42 % (2709680)Success in time 31.2 s
% 0.21/32.42 % Vampire exiting
%------------------------------------------------------------------------------